Include block

This file defines matrix.includeBlock, which imitates direct_sum.component_of for pi instead of direct_sum :TODO:

The direct sum in these files are sort of misleading.

theorem Finset.sum_sigma_univ {β : Type u_1} {α : Type u_2} [AddCommMonoid β] [Fintype α] {σ : α → Type u_3} [(i : α) → Fintype (σ i)] (f : (i : α) × σ i → β) : ∑ x : (i : α) × σ i, f x = ∑ a : α, ∑ s : σ a, f ⟨a, s⟩

def Matrix.blockDiagonal'AlgHom {o : Type u_1} {m' : o → Type u_2} {α : Type u_3} [Fintype o] [DecidableEq o] [(i : o) → Fintype (m' i)] [(i : o) → DecidableEq (m' i)] [CommSemiring α] : PiMat α o m' →ₐ[α] Matrix ((i : o) × m' i) ((i : o) × m' i) α

The algebra homomorphism from block-indexed matrices to their block diagonal matrix.

Equations

• Matrix.blockDiagonal'AlgHom = { toFun := fun (a : PiMat α o m') => Matrix.blockDiagonal' a, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem Matrix.blockDiagonal'AlgHom_apply {o : Type u_1} {m' : o → Type u_2} {α : Type u_3} [Fintype o] [DecidableEq o] [(i : o) → Fintype (m' i)] [(i : o) → DecidableEq (m' i)] [CommSemiring α] (x : PiMat α o m') : blockDiagonal'AlgHom x = blockDiagonal' x

def Matrix.blockDiag'LinearMap {o : Type u_1} {m' : o → Type u_2} {n' : o → Type u_3} {α : Type u_4} [Semiring α] : Matrix ((i : o) × m' i) ((i : o) × n' i) α →ₗ[α] (i : o) → Matrix (m' i) (n' i) α

The linear map sending a matrix to the family of its diagonal blocks.

Equations

• Matrix.blockDiag'LinearMap = { toFun := fun (x : Matrix ((i : o) × m' i) ((i : o) × n' i) α) => x.blockDiag', map_add' := ⋯, map_smul' := ⋯ }

theorem Matrix.blockDiag'LinearMap_apply {o : Type u_1} {m' : o → Type u_2} {n' : o → Type u_3} {α : Type u_4} [Semiring α] (x : Matrix ((i : o) × m' i) ((i : o) × n' i) α) : blockDiag'LinearMap x = x.blockDiag'

theorem Matrix.blockDiag'LinearMap_blockDiagonal'AlgHom {o : Type u_1} {m' : o → Type u_2} {α : Type u_3} [Fintype o] [DecidableEq o] [(i : o) → Fintype (m' i)] [(i : o) → DecidableEq (m' i)] [CommSemiring α] (x : PiMat α o m') : blockDiag'LinearMap (blockDiagonal'AlgHom x) = x

theorem Matrix.blockDiagonal'_ext {R : Type u_1} {k : Type u_2} {s : k → Type u_3} (x y : Matrix ((i : k) × s i) ((i : k) × s i) R) : x = y ↔ ∀ (i : k) (j : s i) (k_1 : k) (l : s k_1), x ⟨i, j⟩ ⟨k_1, l⟩ = y ⟨i, j⟩ ⟨k_1, l⟩

def Matrix.IsBlockDiagonal {o : Type u_1} {m' : o → Type u_2} {n' : o → Type u_3} {α : Type u_4} [DecidableEq o] [Zero α] (x : Matrix ((i : o) × m' i) ((i : o) × n' i) α) : Prop

A matrix indexed by a sigma type is block diagonal when its off-diagonal blocks vanish.

Equations

• x.IsBlockDiagonal = (Matrix.blockDiagonal' x.blockDiag' = x)

def Matrix.includeBlock {o : Type u_1} [DecidableEq o] {m' : o → Type u_2} {α : Type u_3} [Semiring α] {i : o} : Matrix (m' i) (m' i) α →ₗ[α] PiMat α o m'

Include a single matrix block in the corresponding component of a block-indexed family.

Equations

• Matrix.includeBlock = LinearMap.single α (fun (j : o) => Matrix (m' j) (m' j) α) i

theorem Matrix.includeBlock_apply {o : Type u_1} [DecidableEq o] {m' : o → Type u_2} {α : Type u_3} [CommSemiring α] {i : o} (x : Matrix (m' i) (m' i) α) : includeBlock x = fun (j : o) => if h : i = j then ⋯.mp x else 0

theorem Matrix.includeBlock_hMul_same {o : Type u_1} [DecidableEq o] {m' : o → Type u_2} {α : Type u_3} [(i : o) → Fintype (m' i)] [CommSemiring α] {i : o} (x y : Matrix (m' i) (m' i) α) : includeBlock x * includeBlock y = includeBlock (x * y)

theorem Matrix.includeBlock_hMul_ne_same {o : Type u_1} [DecidableEq o] {m' : o → Type u_2} {α : Type u_3} [(i : o) → Fintype (m' i)] [CommSemiring α] {i j : o} (h : i ≠ j) (x : Matrix (m' i) (m' i) α) (y : Matrix (m' j) (m' j) α) : includeBlock x * includeBlock y = 0

theorem Matrix.includeBlock_hMul {o : Type u_1} [DecidableEq o] {m' : o → Type u_2} {α : Type u_3} [(i : o) → Fintype (m' i)] [CommSemiring α] {i : o} (x : Matrix (m' i) (m' i) α) (y : PiMat α o m') : includeBlock x * y = includeBlock (x * y i)

theorem Matrix.hMul_includeBlock {o : Type u_1} [DecidableEq o] {m' : o → Type u_2} {α : Type u_3} [(i : o) → Fintype (m' i)] [CommSemiring α] {i : o} (x : PiMat α o m') (y : Matrix (m' i) (m' i) α) : x * includeBlock y = includeBlock (x i * y)

theorem Matrix.sum_includeBlock {R : Type u_1} {k : Type u_2} [CommSemiring R] [Fintype k] [DecidableEq k] {s : k → Type u_3} (x : PiMat R k s) : ∑ i : k, includeBlock (x i) = x

theorem Matrix.blockDiagonal'_includeBlock_trace {R : Type u_1} {k : Type u_2} [CommSemiring R] [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] (x : PiMat R k s) (j : k) : (blockDiagonal' (includeBlock (x j))).trace = trace (x j)

theorem Matrix.single_hMul_trace {R : Type u_1} {n : Type u_2} {p : Type u_3} [Semiring R] [Fintype p] [DecidableEq p] [Fintype n] [DecidableEq n] (i : n) (j : p) (x : Matrix p n R) : (single i j 1 * x).trace = x j i

theorem Matrix.ext_iff_trace {R : Type u_1} {n : Type u_2} {p : Type u_3} [Fintype n] [Fintype p] [CommSemiring R] (x y : Matrix n p R) : x = y ↔ ∀ (a : Matrix p n R), (x * a).trace = (y * a).trace

theorem Matrix.IsBlockDiagonal.eq {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} {x : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) : Matrix.blockDiagonal' x.blockDiag' = x

theorem Matrix.IsBlockDiagonal.add {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} {x y : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) (hy : y.IsBlockDiagonal) : (x + y).IsBlockDiagonal

@[reducible]

def Matrix.BlockDiagonals (R : Type u_1) (k : Type u_2) [Zero R] [DecidableEq k] (s : k → Type u_3) : Type (max 0 (max u_1 u_2) u_3)

The subtype of block-diagonal square matrices indexed by a sigma type.

Equations

• Matrix.BlockDiagonals R k s = { x : Matrix ((i : k) × s i) ((i : k) × s i) R // x.IsBlockDiagonal }

theorem Matrix.IsBlockDiagonal.zero {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} : IsBlockDiagonal 0

@[implicit_reducible]

instance Matrix.IsBlockDiagonal.HAdd {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} : Add (BlockDiagonals R k s)

Equations

• Matrix.IsBlockDiagonal.HAdd = { add := fun (x y : Matrix.BlockDiagonals R k s) => ⟨↑x + ↑y, ⋯⟩ }

theorem Matrix.IsBlockDiagonal.coe_add {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} {x y : BlockDiagonals R k s} : ↑(x + y) = ↑x + ↑y

@[implicit_reducible]

instance Matrix.IsBlockDiagonal.Zero {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} : _root_.Zero (BlockDiagonals R k s)

Equations

• Matrix.IsBlockDiagonal.Zero = { zero := ⟨0, ⋯⟩ }

theorem Matrix.IsBlockDiagonal.coe_zero {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} : ↑0 = 0

theorem Matrix.IsBlockDiagonal.smul {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} {x : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) (α : R) : (α • x).IsBlockDiagonal

@[implicit_reducible]

instance Matrix.IsBlockDiagonal.Smul {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} : SMul R (BlockDiagonals R k s)

Equations

• Matrix.IsBlockDiagonal.Smul = { smul := fun (a : R) (x : Matrix.BlockDiagonals R k s) => ⟨a • ↑x, ⋯⟩ }

theorem Matrix.IsBlockDiagonal.coe_smul {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} (a : R) (x : BlockDiagonals R k s) : ↑(a • x) = a • ↑x

@[implicit_reducible]

instance Matrix.addCommMonoidBlockDiagonal {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} : AddCommMonoid (BlockDiagonals R k s)

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.IsBlockDiagonal.coe_sum {R : Type u_4} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} {n : Type u_3} [Fintype n] {x : n → BlockDiagonals R k s} : ↑(∑ i : n, x i) = ∑ i : n, ↑(x i)

@[implicit_reducible]

instance Matrix.mulActionBlockDiagonal {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} : MulAction R (BlockDiagonals R k s)

Equations

• Matrix.mulActionBlockDiagonal = { toSMul := Matrix.IsBlockDiagonal.Smul, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

instance Matrix.distribMulActionBlockDiagonal {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} : DistribMulAction R (BlockDiagonals R k s)

Equations

• Matrix.distribMulActionBlockDiagonal = { toMulAction := Matrix.mulActionBlockDiagonal, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

instance Matrix.moduleBlockDiagonal {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} : Module R (BlockDiagonals R k s)

Equations

• Matrix.moduleBlockDiagonal = { toDistribMulAction := Matrix.distribMulActionBlockDiagonal, add_smul := ⋯, zero_smul := ⋯ }

theorem Matrix.IsBlockDiagonal.blockDiagonal' {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} (x : PiMat R k s) : (Matrix.blockDiagonal' x).IsBlockDiagonal

theorem Matrix.isBlockDiagonal_iff {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} (x : Matrix ((i : k) × s i) ((i : k) × s i) R) : x.IsBlockDiagonal ↔ ∃ (y : PiMat R k s), x = blockDiagonal' y

def Matrix.singleBlockDiagonal {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} [(i : k) → DecidableEq (s i)] (i : k) (j l : s i) (α : R) : BlockDiagonals R k s

A block-diagonal matrix with one nonzero matrix-entry inside a specified block.

Equations

• Matrix.singleBlockDiagonal i j l α = ⟨Matrix.single ⟨i, j⟩ ⟨i, l⟩ α, ⋯⟩

theorem Matrix.includeBlock_conjTranspose {R : Type u_1} {k : Type u_2} [CommSemiring R] [StarRing R] [DecidableEq k] {s : k → Type u_3} {i : k} {x : Matrix (s i) (s i) R} : star (includeBlock x) = includeBlock x.conjTranspose

theorem Matrix.includeBlock_inj {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} {i : k} {x y : Matrix (s i) (s i) R} : includeBlock x = includeBlock y ↔ x = y

theorem Matrix.blockDiagonal'_includeBlock_isHermitian_iff {R : Type u_1} {k : Type u_2} [CommSemiring R] [StarRing R] [DecidableEq k] {s : k → Type u_3} {i : k} (x : Matrix (s i) (s i) R) : (blockDiagonal' (includeBlock x)).IsHermitian ↔ x.IsHermitian

theorem Matrix.matrix_eq_sum_includeBlock {R : Type u_1} {k : Type u_2} [CommSemiring R] [Fintype k] [DecidableEq k] {s : k → Type u_3} (x : PiMat R k s) : x = ∑ i : k, includeBlock (x i)

theorem Matrix.includeBlock_apply_same {R : Type u_1} {k : Type u_2} [CommSemiring R] [DecidableEq k] {s : k → Type u_3} {i : k} (x : Matrix (s i) (s i) R) : includeBlock x i = x

theorem Matrix.includeBlock_apply_ne_same {R : Type u_1} {k : Type u_2} [CommSemiring R] [DecidableEq k] {s : k → Type u_3} {i j : k} (x : Matrix (s i) (s i) R) (h : i ≠ j) : includeBlock x j = 0

theorem Matrix.includeBlock_apply_single {R : Type u_1} {k : Type u_2} [CommSemiring R] [DecidableEq k] {s : k → Type u_3} [(i : k) → DecidableEq (s i)] {i : k} (a b : s i) : includeBlock (single a b 1) = (single ⟨i, a⟩ ⟨i, b⟩ 1).blockDiag'

theorem Matrix.includeBlock_hMul_includeBlock {R : Type u_1} {k : Type u_2} [CommSemiring R] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] {i j : k} (x : Matrix (s i) (s i) R) (y : Matrix (s j) (s j) R) : includeBlock x * includeBlock y = if h : j = i then includeBlock (x * ⋯.mpr y) else 0

theorem Matrix.IsBlockDiagonal.mul {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] {x y : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) (hy : y.IsBlockDiagonal) : (x * y).IsBlockDiagonal

@[reducible]

instance Matrix.IsBlockDiagonal.hasMul {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] : Mul (BlockDiagonals R k s)

Equations

• Matrix.IsBlockDiagonal.hasMul = { mul := fun (x y : Matrix.BlockDiagonals R k s) => ⟨↑x * ↑y, ⋯⟩ }

theorem Matrix.IsBlockDiagonal.coe_mul {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] {x y : BlockDiagonals R k s} : ↑(x * y) = ↑x * ↑y

theorem Matrix.IsBlockDiagonal.one {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} [(i : k) → DecidableEq (s i)] : IsBlockDiagonal 1

@[reducible]

instance Matrix.IsBlockDiagonal.hasOne {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} [(i : k) → DecidableEq (s i)] : One (BlockDiagonals R k s)

Equations

• Matrix.IsBlockDiagonal.hasOne = { one := ⟨1, ⋯⟩ }

theorem Matrix.IsBlockDiagonal.coe_one {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} [(i : k) → DecidableEq (s i)] : ↑1 = 1

theorem Matrix.IsBlockDiagonal.coe_nsmul {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} (n : ℕ) (x : BlockDiagonals R k s) : ↑(n • x) = n • ↑x

theorem Matrix.IsBlockDiagonal.npow {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (n : ℕ) {x : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) : (x ^ n).IsBlockDiagonal

@[reducible]

instance Matrix.IsBlockDiagonal.hasNpow {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] : Pow (BlockDiagonals R k s) ℕ

Equations

• Matrix.IsBlockDiagonal.hasNpow = { pow := fun (x : Matrix.BlockDiagonals R k s) (n : ℕ) => ⟨↑x ^ n, ⋯⟩ }

theorem Matrix.IsBlockDiagonal.coe_npow {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (n : ℕ) (x : BlockDiagonals R k s) : ↑(x ^ n) = ↑x ^ n

@[reducible]

instance Matrix.IsBlockDiagonal.semiring {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] : Semiring (BlockDiagonals R k s)

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

instance Matrix.IsBlockDiagonal.algebra {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] : Algebra R (BlockDiagonals R k s)

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.IsBlockDiagonal.coe_blockDiagonal'_blockDiag' {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} (x : BlockDiagonals R k s) : Matrix.blockDiagonal' (↑x).blockDiag' = ↑x

def Matrix.isBlockDiagonalPiAlgEquiv {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] : BlockDiagonals R k s ≃ₐ[R] PiMat R k s

Block-diagonal matrices are algebra-equivalent to block-indexed matrix families.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.isBlockDiagonalPiAlgEquiv_symm_apply_coe {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : PiMat R k s) : ↑(isBlockDiagonalPiAlgEquiv.symm x) = blockDiagonal' x

@[simp]

theorem Matrix.isBlockDiagonalPiAlgEquiv_apply {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : BlockDiagonals R k s) (k✝ : k) : isBlockDiagonalPiAlgEquiv x k✝ = (↑x).blockDiag' k✝

theorem Matrix.IsBlockDiagonal.star {R : Type u_1} [CommSemiring R] [StarAddMonoid R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} {x : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) : x.conjTranspose.IsBlockDiagonal

@[reducible]

instance Matrix.IsBlockDiagonal.hasStar {R : Type u_1} [CommSemiring R] [StarAddMonoid R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} : Star (BlockDiagonals R k s)

Equations

• Matrix.IsBlockDiagonal.hasStar = { star := fun (x : Matrix.BlockDiagonals R k s) => ⟨(↑x).conjTranspose, ⋯⟩ }

theorem Matrix.IsBlockDiagonal.coe_star {R : Type u_1} [CommSemiring R] [StarAddMonoid R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} (y : BlockDiagonals R k s) : ↑(Star.star y) = (↑y).conjTranspose

theorem Matrix.isBlockDiagonalPiAlgEquiv.map_star {R : Type u_1} [CommSemiring R] [StarAddMonoid R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : BlockDiagonals R k s) : isBlockDiagonalPiAlgEquiv (star x) = star (isBlockDiagonalPiAlgEquiv x)

theorem Matrix.isBlockDiagonalPiAlgEquiv.symm_map_star {R : Type u_1} [CommSemiring R] [StarAddMonoid R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : PiMat R k s) : isBlockDiagonalPiAlgEquiv.symm (star x) = star (isBlockDiagonalPiAlgEquiv.symm x)

def Matrix.Equiv.sigmaProdDistrib' {ι : Type u_1} (β : Type u_2) (α : ι → Type u_3) : β × (i : ι) × α i ≃ (i : ι) × β × α i

A variant of Equiv.sigmaProdDistrib with the product coordinate first.

Equations

• Matrix.Equiv.sigmaProdDistrib' β α = ((Equiv.prodComm β ((i : ι) × α i)).trans (Equiv.sigmaProdDistrib α β)).trans (Equiv.sigmaCongrRight fun (i : ι) => Equiv.prodComm β (α i)).symm

@[simp]

theorem Matrix.Equiv.sigmaProdDistrib'_apply_snd {ι : Type u_1} (β : Type u_2) (α : ι → Type u_3) (a✝ : β × (i : ι) × α i) : ((sigmaProdDistrib' β α) a✝).snd = (Equiv.prodComm (α a✝.2.fst) β) (a✝.2.snd, a✝.1)

@[simp]

theorem Matrix.Equiv.sigmaProdDistrib'_symm_apply {ι : Type u_1} (β : Type u_2) (α : ι → Type u_3) (a✝ : (i : ι) × β × α i) : (sigmaProdDistrib' β α).symm a✝ = (a✝.snd.1, ⟨a✝.fst, a✝.snd.2⟩)

@[simp]

theorem Matrix.Equiv.sigmaProdDistrib'_apply_fst {ι : Type u_1} (β : Type u_2) (α : ι → Type u_3) (a✝ : β × (i : ι) × α i) : ((sigmaProdDistrib' β α) a✝).fst = a✝.2.fst

def Matrix.sigmaProdSigma {α : Type u_1} {β : Type u_2} {ζ : α → Type u_3} {℘ : β → Type u_4} : ((i : α) × ζ i) × (i : β) × ℘ i ≃ (i : α) × (j : β) × ζ i × ℘ j

Distribute a product of sigma types into a nested sigma type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.sigmaProdSigma_apply_fst {α : Type u_1} {β : Type u_2} {ζ : α → Type u_3} {℘ : β → Type u_4} (x : ((i : α) × ζ i) × (i : β) × ℘ i) : (sigmaProdSigma x).fst = ((Equiv.sigmaProdDistrib ζ ((i : β) × ℘ i)) x).fst

@[simp]

theorem Matrix.sigmaProdSigma_apply_snd_fst {α : Type u_1} {β : Type u_2} {ζ : α → Type u_3} {℘ : β → Type u_4} (x : ((i : α) × ζ i) × (i : β) × ℘ i) : (sigmaProdSigma x).snd.fst = ((Equiv.sigmaProdDistrib' ((i : α) × ζ i) ℘) x).fst

@[simp]

theorem Matrix.sigmaProdSigma_symm_apply {α : Type u_1} {β : Type u_2} {ζ : α → Type u_3} {℘ : β → Type u_4} (x : (i : α) × (j : β) × ζ i × ℘ j) : sigmaProdSigma.symm x = (⟨x.fst, x.snd.snd.1⟩, ⟨x.snd.fst, x.snd.snd.2⟩)

@[simp]

theorem Matrix.sigmaProdSigma_apply_snd_snd {α : Type u_1} {β : Type u_2} {ζ : α → Type u_3} {℘ : β → Type u_4} (x : ((i : α) × ζ i) × (i : β) × ℘ i) : (sigmaProdSigma x).snd.snd = (x.1.snd, x.2.snd)

theorem Matrix.IsBlockDiagonal.apply_of_ne {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} {x : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) (i j : (i : k) × s i) (h : i.fst ≠ j.fst) : x i j = 0

theorem Matrix.IsBlockDiagonal.apply_of_ne_coe {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} (x : BlockDiagonals R k s) (i j : (i : k) × s i) (h : i.fst ≠ j.fst) : ↑x i j = 0

theorem Matrix.IsBlockDiagonal.kronecker_hMul {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : k → Type u_3} {x y : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) : IsBlockDiagonal fun (i j : (i : k) × (j : k) × s i × s j) => kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y (sigmaProdSigma.symm i) (sigmaProdSigma.symm j)

def Matrix.directSumLinearMapAlgEquivIsBlockDiagonalLinearMap {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] : (PiMat R k s →ₗ[R] PiMat R k s) ≃ₐ[R] BlockDiagonals R k s →ₗ[R] BlockDiagonals R k s

Conjugation by the block-diagonal/pi-matrix algebra equivalence on endomorphisms.

Equations

• Matrix.directSumLinearMapAlgEquivIsBlockDiagonalLinearMap = (↑Matrix.isBlockDiagonalPiAlgEquiv.symm).innerConj

@[simp]

theorem Matrix.directSumLinearMapAlgEquivIsBlockDiagonalLinearMap_apply_apply_coe {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (f : PiMat R k s →ₗ[R] PiMat R k s) (x : BlockDiagonals R k s) : ↑((directSumLinearMapAlgEquivIsBlockDiagonalLinearMap f) x) = blockDiagonal' (f (isBlockDiagonalPiAlgEquiv x))

@[simp]

theorem Matrix.directSumLinearMapAlgEquivIsBlockDiagonalLinearMap_symm_apply_apply {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (f : BlockDiagonals R k s →ₗ[R] BlockDiagonals R k s) (x : PiMat R k s) (i : k) : (directSumLinearMapAlgEquivIsBlockDiagonalLinearMap.symm f) x i = (↑(f (isBlockDiagonalPiAlgEquiv.symm x))).blockDiag' i

theorem TensorProduct.assoc_includeBlock {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : k → Type u_2} {i j : k} : ↑(TensorProduct.assoc R (PiMat R k s) (PiMat R k s) (PiMat R k s)).symm ∘ₗ map Matrix.includeBlock (map Matrix.includeBlock Matrix.includeBlock) = map (map Matrix.includeBlock Matrix.includeBlock) Matrix.includeBlock ∘ₗ ↑(TensorProduct.assoc R (Matrix (s i) (s i) R) (Matrix (s j) (s j) R) (Matrix (s j) (s j) R)).symm