Include block #
This file defines matrix.includeBlock
which immitates direct_sum.component_of
but 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 → β)
:
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 α]
:
Equations
- Matrix.blockDiagonal'AlgHom = { toFun := fun (a : PiMat α o m') => Matrix.blockDiagonal' a, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
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')
:
def
Matrix.blockDiag'LinearMap
{o : Type u_1}
{m' : o → Type u_2}
{n' : o → Type u_3}
{α : Type u_4}
[Semiring α]
:
Equations
- Matrix.blockDiag'LinearMap = { toFun := fun (x : Matrix ((i : o) × m' i) ((i : o) × n' i) α) => x.blockDiag', map_add' := ⋯, map_smul' := ⋯ }
Instances For
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')
:
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) α)
:
Equations
- x.IsBlockDiagonal = (Matrix.blockDiagonal' x.blockDiag' = x)
Instances For
def
Matrix.includeBlock
{o : Type u_1}
[DecidableEq o]
{m' : o → Type u_2}
{α : Type u_3}
[Semiring α]
{i : o}
:
Equations
- Matrix.includeBlock = LinearMap.single α (fun (j : o) => Matrix (m' j) (m' j) α) i
Instances For
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) α)
:
theorem
Matrix.includeBlock_hMul_same
{o : Type u_1}
[Fintype o]
[DecidableEq o]
{m' : o → Type u_2}
{α : Type u_3}
[(i : o) → Fintype (m' i)]
[(i : o) → DecidableEq (m' i)]
[CommSemiring α]
{i : o}
(x y : Matrix (m' i) (m' i) α)
:
theorem
Matrix.includeBlock_hMul_ne_same
{o : Type u_1}
[Fintype o]
[DecidableEq o]
{m' : o → Type u_2}
{α : Type u_3}
[(i : o) → Fintype (m' i)]
[(i : o) → DecidableEq (m' i)]
[CommSemiring α]
{i j : o}
(h : i ≠ j)
(x : Matrix (m' i) (m' i) α)
(y : Matrix (m' j) (m' j) α)
:
theorem
Matrix.includeBlock_hMul
{o : Type u_1}
[Fintype o]
[DecidableEq o]
{m' : o → Type u_2}
{α : Type u_3}
[(i : o) → Fintype (m' i)]
[(i : o) → DecidableEq (m' i)]
[CommSemiring α]
{i : o}
(x : Matrix (m' i) (m' i) α)
(y : PiMat α o m')
:
theorem
Matrix.hMul_includeBlock
{o : Type u_1}
[Fintype o]
[DecidableEq o]
{m' : o → Type u_2}
{α : Type u_3}
[(i : o) → Fintype (m' i)]
[(i : o) → DecidableEq (m' i)]
[CommSemiring α]
{i : o}
(x : PiMat α o m')
(y : Matrix (m' i) (m' i) α)
:
theorem
Matrix.sum_includeBlock
{R : Type u_1}
{k : Type u_2}
[CommSemiring R]
[Fintype k]
[DecidableEq k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
(x : PiMat R k s)
:
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)]
[(i : k) → DecidableEq (s i)]
(x : PiMat R k s)
(j : k)
:
theorem
Matrix.stdBasisMatrix_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)
:
theorem
Matrix.ext_iff_trace
{R : Type u_1}
{n : Type u_2}
{p : Type u_3}
[Fintype n]
[Fintype p]
[DecidableEq n]
[DecidableEq p]
[CommSemiring R]
(x y : Matrix n p R)
:
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)
:
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)
Equations
- Matrix.BlockDiagonals R k s = { x : Matrix ((i : k) × s i) ((i : k) × s i) R // x.IsBlockDiagonal }
Instances For
theorem
Matrix.IsBlockDiagonal.zero
{R : Type u_3}
[CommSemiring R]
{k : Type u_1}
[DecidableEq k]
{s : k → Type u_2}
:
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}
[Fintype k]
[DecidableEq k]
{s : k → Type u_2}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
{x y : BlockDiagonals R k s}
:
instance
Matrix.IsBlockDiagonal.Zero
{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)]
:
_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}
[Fintype k]
[DecidableEq k]
{s : k → Type u_2}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
:
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
instance
Matrix.IsBlockDiagonal.Smul
{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)]
:
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}
[Fintype k]
[DecidableEq k]
{s : k → Type u_2}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
(a : R)
(x : BlockDiagonals R k s)
:
instance
Matrix.addCommMonoidBlockDiagonal
{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)]
:
AddCommMonoid (BlockDiagonals R k s)
Equations
theorem
Matrix.IsBlockDiagonal.coe_sum
{R : Type u_4}
[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 : Type u_3}
[Fintype n]
{x : n → BlockDiagonals R k s}
:
instance
Matrix.mulActionBlockDiagonal
{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)]
:
MulAction R (BlockDiagonals R k s)
Equations
instance
Matrix.distribMulActionBlockDiagonal
{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)]
:
DistribMulAction R (BlockDiagonals R k s)
Equations
instance
Matrix.moduleBlockDiagonal
{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)]
:
Module R (BlockDiagonals R k s)
Equations
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)
:
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)
:
def
Matrix.stdBasisMatrixBlockDiagonal
{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
Equations
- Matrix.stdBasisMatrixBlockDiagonal i j l α = ⟨Matrix.stdBasisMatrix ⟨i, j⟩ ⟨i, l⟩ α, ⋯⟩
Instances For
theorem
Matrix.includeBlock_conjTranspose
{R : Type u_1}
{k : Type u_2}
[CommSemiring R]
[StarRing R]
[Fintype k]
[DecidableEq k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
{i : k}
{x : Matrix (s i) (s i) R}
:
theorem
Matrix.includeBlock_inj
{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)]
{i : k}
{x y : Matrix (s i) (s i) R}
:
theorem
Matrix.blockDiagonal'_includeBlock_isHermitian_iff
{R : Type u_1}
{k : Type u_2}
[CommSemiring R]
[StarRing R]
[Fintype k]
[DecidableEq k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
{i : k}
(x : Matrix (s i) (s i) R)
:
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}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
(x : PiMat R k s)
:
theorem
Matrix.includeBlock_apply_same
{R : Type u_1}
{k : Type u_2}
[CommSemiring R]
[Fintype k]
[DecidableEq k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
{i : k}
(x : Matrix (s i) (s i) R)
:
theorem
Matrix.includeBlock_apply_ne_same
{R : Type u_1}
{k : Type u_2}
[CommSemiring R]
[Fintype k]
[DecidableEq k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
{i j : k}
(x : Matrix (s i) (s i) R)
(h : i ≠ j)
:
theorem
Matrix.includeBlock_apply_stdBasisMatrix
{R : Type u_1}
{k : Type u_2}
[CommSemiring R]
[Fintype k]
[DecidableEq k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
{i : k}
(a b : s i)
:
theorem
Matrix.includeBlock_hMul_includeBlock
{R : Type u_1}
{k : Type u_2}
[CommSemiring R]
[Fintype k]
[DecidableEq k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
{i j : k}
(x : Matrix (s i) (s i) R)
(y : Matrix (s j) (s j) R)
:
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
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)]
[(i : k) → DecidableEq (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)]
[(i : k) → DecidableEq (s i)]
{x y : BlockDiagonals R k s}
:
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)]
:
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}
[Fintype k]
[DecidableEq k]
{s : k → Type u_2}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
:
theorem
Matrix.IsBlockDiagonal.coe_nsmul
{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)
:
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
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)
:
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
- Matrix.IsBlockDiagonal.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ (fun (n : ℕ) (x : Matrix.BlockDiagonals R k s) => x ^ n) ⋯ ⋯
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
- Matrix.IsBlockDiagonal.algebra = Algebra.mk { toFun := fun (r : R) => r • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯
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)
:
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)]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
@[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)
:
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)
:
instance
Matrix.IsBlockDiagonal.hasStar
{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)]
:
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}
[Fintype k]
[DecidableEq k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
(y : BlockDiagonals R k s)
:
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)
:
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)
:
Equations
- Matrix.Equiv.sigmaProdDistrib' β α = ((Equiv.prodComm β ((i : ι) × α i)).trans (Equiv.sigmaProdDistrib α β)).trans (Equiv.sigmaCongrRight fun (i : ι) => Equiv.prodComm β (α i)).symm
Instances For
@[simp]
theorem
Matrix.Equiv.sigmaProdDistrib'_apply_fst
{ι : Type u_1}
(β : Type u_2)
(α : ι → Type u_3)
(a✝ : β × (i : ι) × α i)
:
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)
:
theorem
Matrix.IsBlockDiagonal.apply_of_ne_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 : BlockDiagonals R k s)
(i j : (i : k) × s i)
(h : i.fst ≠ j.fst)
:
theorem
Matrix.IsBlockDiagonal.kronecker_hMul
{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 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)]
:
Equations
Instances For
@[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)]
(a : Module.End R (PiMat R k s))
(a✝ : BlockDiagonals R k s)
:
@[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)]
(a : Module.End R (BlockDiagonals R k s))
(a✝ : PiMat R k s)
(i : k)
:
(directSumLinearMapAlgEquivIsBlockDiagonalLinearMap.symm a) a✝ i = (↑(a (isBlockDiagonalPiAlgEquiv.symm a✝))).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