LeanPool.Monlib4.QuantumGraph.PiMatFinTwo

Imported Lean Pool material for LeanPool.Monlib4.QuantumGraph.PiMatFinTwo.

def «termWithPiBlockQuantum[_]_» : Lean.ParserDescr

Elaborate a product-of-blocks statement with matrix quantum-set instances on each block.

Equations

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

def «tacticWithPiBlockQuantumCtx[_]» : Lean.ParserDescr

Introduce product and blockwise matrix quantum-set instances in a proof.

Equations

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

def «termWithPiBlockCoalgebraQuantum[_]_» : Lean.ParserDescr

Elaborate a product-of-blocks statement with blockwise quantum and coalgebra instances.

Equations

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

def «tacticWithPiBlockCoalgebraQuantumCtx[_]» : Lean.ParserDescr

Introduce product, blockwise quantum, and coalgebra instances in a proof.

Equations

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

def MatProdAlgEquivPiMat (n' : Fin 2 → Type u_1) [(i : Fin 2) → Fintype (n' i)] [(i : Fin 2) → DecidableEq (n' i)] : (Matrix (n' 0) (n' 0) ℂ × Matrix (n' 1) (n' 1) ℂ) ≃ₐ[ℂ] PiMat ℂ (Fin 2) n'

The algebra equivalence between a two-block product of matrix algebras and the matching PiMat.

Equations

• MatProdAlgEquivPiMat n' = matrixPiFinTwoAlgEquivProd.symm

@[reducible, inline]

abbrev PiFinTwo.swap (n' : Fin 2 → Type u_1) : Fin 2 → Type u_1

Swap the two types in a Fin 2-indexed family.

Equations

• PiFinTwo.swap n' i = if i = 0 then n' 1 else n' 0

@[implicit_reducible]

instance instFintypeSwap {n' : Fin 2 → Type u_1} [(i : Fin 2) → Fintype (n' i)] (i : Fin 2) : Fintype (PiFinTwo.swap n' i)

Equations

• instFintypeSwap i = id (if h : i = 0 then ⋯.mpr inferInstance else ⋯.mpr inferInstance)

@[implicit_reducible]

instance instDecidableEqSwap {n' : Fin 2 → Type u_1} [(i : Fin 2) → DecidableEq (n' i)] (i : Fin 2) : DecidableEq (PiFinTwo.swap n' i)

Equations

• instDecidableEqSwap i = id (if h : i = 0 then ⋯.mpr inferInstance else ⋯.mpr inferInstance)

def MatProdAlgEquivPiMatSwap (n' : Fin 2 → Type u_1) [(i : Fin 2) → Fintype (n' i)] [(i : Fin 2) → DecidableEq (n' i)] : (Matrix (n' 1) (n' 1) ℂ × Matrix (n' 0) (n' 0) ℂ) ≃ₐ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo.swap n')

The swapped product-to-PiMat equivalence for two matrix blocks.

Equations

• MatProdAlgEquivPiMatSwap n' = MatProdAlgEquivPiMat (PiFinTwo.swap n')

def Prod.swapAlgEquiv (α : Type u_1) (β : Type u_2) [Semiring α] [Semiring β] [Algebra ℂ α] [Algebra ℂ β] : (α × β) ≃ₐ[ℂ] β × α

Swap the two factors of a product as an algebra equivalence.

Equations

• Prod.swapAlgEquiv α β = { toFun := fun (x : α × β) => x.swap, invFun := fun (x : β × α) => x.swap, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Prod.swapAlgEquiv_apply (α : Type u_1) (β : Type u_2) [Semiring α] [Semiring β] [Algebra ℂ α] [Algebra ℂ β] (x : α × β) : (swapAlgEquiv α β) x = x.swap

@[simp]

theorem Prod.swapAlgEquiv_symm_apply (α : Type u_1) (β : Type u_2) [Semiring α] [Semiring β] [Algebra ℂ α] [Algebra ℂ β] (x : β × α) : (swapAlgEquiv α β).symm x = x.swap

def PiMatFinTwoSwapAlgEquiv {n' : Fin 2 → Type u_1} [(i : Fin 2) → Fintype (n' i)] [(i : Fin 2) → DecidableEq (n' i)] : PiMat ℂ (Fin 2) n' ≃ₐ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo.swap n')

Swap the two blocks of a PiMat indexed by Fin 2.

Equations

• PiMatFinTwoSwapAlgEquiv = (MatProdAlgEquivPiMat n').symm.trans ((Prod.swapAlgEquiv (Matrix (n' 0) (n' 0) ℂ) (Matrix (n' 1) (n' 1) ℂ)).trans (MatProdAlgEquivPiMatSwap n'))

@[reducible, inline]

abbrev PiFinTwoSame (n : Type u_1) : Fin 2 → Type u_1

The constant Fin 2-indexed family with value n.

Equations

• PiFinTwoSame n i = n

@[implicit_reducible]

instance instFintypePiFinTwoSame {n : Type u_1} [Fintype n] (i : Fin 2) : Fintype (PiFinTwoSame n i)

Equations

• instFintypePiFinTwoSame i = inferInstance

@[implicit_reducible]

instance instDecidableEqPiFinTwoSame {n : Type u_1} [DecidableEq n] (i : Fin 2) : DecidableEq (PiFinTwoSame n i)

Equations

• instDecidableEqPiFinTwoSame i = inferInstance

theorem PiMatFinTwoSwapAlgEquiv_apply {n' : Fin 2 → Type u_1} [(i : Fin 2) → Fintype (n' i)] [(i : Fin 2) → DecidableEq (n' i)] (x : Matrix (n' 0) (n' 0) ℂ) (y : Matrix (n' 1) (n' 1) ℂ) : PiMatFinTwoSwapAlgEquiv ((MatProdAlgEquivPiMat n') (x, y)) = (MatProdAlgEquivPiMat (PiFinTwo.swap n')) (y, x)

theorem PiFinTwoSame_swap {n : Type u_1} : PiFinTwo.swap (PiFinTwoSame n) = PiFinTwoSame n

def PiMatFinTwoSameSwapAlgEquiv {n : Type u_1} [Fintype n] [DecidableEq n] : PiMat ℂ (Fin 2) (PiFinTwoSame n) ≃ₐ[ℂ] PiMat ℂ (Fin 2) (PiFinTwoSame n)

Swap the two identical matrix blocks of a PiMat indexed by Fin 2.

Equations

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

theorem PiMatFinTwoSameSwapAlgEquiv_apply {n : Type u_1} [Fintype n] [DecidableEq n] (x y : Matrix n n ℂ) : PiMatFinTwoSameSwapAlgEquiv ((MatProdAlgEquivPiMat (PiFinTwoSame n)) (x, y)) = (MatProdAlgEquivPiMat (PiFinTwoSame n)) (y, x)

theorem AlgEquiv.prodMap_inner_of {K : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [CommSemiring K] [Semiring R₁] [Semiring R₂] [Algebra K R₁] [Algebra K R₂] {f : R₁ ≃ₐ[K] R₁} (hf : f.IsInner) {g : R₂ ≃ₐ[K] R₂} (hg : g.IsInner) : (f.prodMap g).IsInner

@[reducible]

def MatProdAlgEquivPiMatSameInvertibleOf {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ × Matrix n n ℂ} (hU : Invertible U) : Invertible ((MatProdAlgEquivPiMat (PiFinTwoSame n)) U)

Invertibility is preserved by the product-to-PiMat equivalence in the same-block case.

Equations

• MatProdAlgEquivPiMatSameInvertibleOf hU = { invOf := (MatProdAlgEquivPiMat (PiFinTwoSame n)) ⅟U, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem AlgEquiv.toPiMat_finTwo_same_inner_of_matrix_prod_inner {n : Type u_1} [Fintype n] [DecidableEq n] {f : (Matrix n n ℂ × Matrix n n ℂ) ≃ₐ[ℂ] Matrix n n ℂ × Matrix n n ℂ} (hf : f.IsInner) : ((MatProdAlgEquivPiMat (PiFinTwoSame n)).symm.trans (f.trans (MatProdAlgEquivPiMat (PiFinTwoSame n)))).IsInner

theorem AlgEquiv.PiMat_finTwo_same {n : Type u_1} [Fintype n] [DecidableEq n] (f : PiMat ℂ (Fin 2) (PiFinTwoSame n) ≃ₐ[ℂ] PiMat ℂ (Fin 2) (PiFinTwoSame n)) : f.IsInner ∨ ∃ (g : PiMat ℂ (Fin 2) (PiFinTwoSame n) ≃ₐ[ℂ] PiMat ℂ (Fin 2) (PiFinTwoSame n)) (_ : g.IsInner), f = PiMatFinTwoSameSwapAlgEquiv.trans g

theorem PiMat.trace_eq_linearMap_trace_toEuclideanLM {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] (y : PiMat ℂ (ι × ι) fun (i : ι × ι) => p i.1 × p i.2) : traceLinearMap y = ∑ x : ι × ι, (LinearMap.trace ℂ (EuclideanSpace ℂ (p x.1 × p x.2))) (PiMatToEuclideanLM y x)

theorem QuantumGraph.Real.dimOfPiMatSubmodule_eq {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) : ⋯.dimOfPiMatSubmodule = ∑ i : ι × ι, Module.finrank ℂ ↥(hA.PiMatSubmodule i)

theorem LinearMap.proj_adjoint_apply {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (i : ι) (x : Matrix (p i) (p i) ℂ) : (adjoint (proj i)) x = Matrix.includeBlock x

theorem LinearMap.proj_adjoint {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (i : ι) : adjoint (proj i) = single ℂ (fun (r : ι) => Mat ℂ (p r)) i

theorem LinearMap.single_adjoint {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (i : ι) : adjoint (single ℂ (fun (r : ι) => Mat ℂ (p r)) i) = proj i

theorem LinearMap.eq_sum_conj_adjoint_proj_comp_proj {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [(i : ι) → Fintype (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p) : A = ∑ i : ι × ι, adjoint (proj i.1) ∘ₗ (proj i.1 ∘ₗ A ∘ₗ adjoint (proj i.2)) ∘ₗ proj i.2

theorem QuantumGraph.Real.piFinTwo_same_piMat_submodule_eq_bot_of_adjoint_and_dim_eq_one {n : Type u_1} [Fintype n] [DecidableEq n] {ψ : (i : Fin 2) → Module.Dual ℂ (Matrix (PiFinTwoSame n i) (PiFinTwoSame n i) ℂ)} [hψ : ∀ (i : Fin 2), (ψ i).IsFaithfulPosMap] {A : PiMat ℂ (Fin 2) (PiFinTwoSame n) →ₗ[ℂ] PiMat ℂ (Fin 2) (PiFinTwoSame n)} (hA : Real (PiMat ℂ (Fin 2) (PiFinTwoSame n)) A) : LinearMap.adjoint A = A → ⋯.dimOfPiMatSubmodule = 1 → hA.PiMatSubmodule (1, 0) = ⊥ ∧ (Module.finrank ℂ ↥(hA.PiMatSubmodule 0) = 1 ∧ hA.PiMatSubmodule 1 = ⊥ ∨ hA.PiMatSubmodule 0 = ⊥ ∧ Module.finrank ℂ ↥(hA.PiMatSubmodule 1) = 1)

theorem Pi.nat_eq_zero_of_sum_eq_one_and_unique_one {ι : Type u_4} [Fintype ι] {f : ι → ℕ} (h : ∑ i : ι, f i = 1) {i : ι} (hd : f i = 1) {j : ι} (hj : j ≠ i) : f j = 0

theorem Finset.sum_nat_eq_one_iff_exists_unique_eq_one {ι : Type u_4} [Fintype ι] {f : ι → ℕ} (h : ∑ i : ι, f i = 1) : ∃! i : ι, f i = 1

theorem QuantumGraph.Real.dimOfPiMatSubmodule_eq_zero_iff_eq_zero {ι : Type u_4} {p : ι → Type u_5} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) : ⋯.dimOfPiMatSubmodule = 0 ↔ A = 0

theorem QuantumGraph.Real.exists_unique_includeMap_of_adjoint_and_dim_ofPiMatSubmodule_eq_one {ι : Type u_4} {p : ι → Type u_5} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) (hA₂ : LinearMap.adjoint A = A) (hd : ⋯.dimOfPiMatSubmodule = 1) : ∃! i : ι, LinearMap.adjoint (LinearMap.proj i) ∘ₗ LinearMap.proj i ∘ₗ A ∘ₗ LinearMap.adjoint (LinearMap.proj i) ∘ₗ LinearMap.proj i = A

theorem QuantumGraph.Real.piFinTwo_same_exists_matrix_map_eq_map_of_adjoint_and_dim_eq_one {n : Type u_1} [Fintype n] [DecidableEq n] {ψ : (i : Fin 2) → Module.Dual ℂ (Matrix (PiFinTwoSame n i) (PiFinTwoSame n i) ℂ)} [hψ : ∀ (i : Fin 2), (ψ i).IsFaithfulPosMap] {A : PiMat ℂ (Fin 2) (PiFinTwoSame n) →ₗ[ℂ] PiMat ℂ (Fin 2) (PiFinTwoSame n)} (hA : Real (PiMat ℂ (Fin 2) (PiFinTwoSame n)) A) : LinearMap.adjoint A = A → ⋯.dimOfPiMatSubmodule = 1 → LinearMap.adjoint (LinearMap.proj 0) ∘ₗ LinearMap.proj 0 ∘ₗ A ∘ₗ LinearMap.adjoint (LinearMap.proj 0) ∘ₗ LinearMap.proj 0 = A ∨ LinearMap.adjoint (LinearMap.proj 1) ∘ₗ LinearMap.proj 1 ∘ₗ A ∘ₗ LinearMap.adjoint (LinearMap.proj 1) ∘ₗ LinearMap.proj 1 = A

def AlgHom.proj (R : Type u_4) {ι : Type u_5} [CommSemiring R] {φ : ι → Type u_6} [(i : ι) → Semiring (φ i)] [(i : ι) → Algebra R (φ i)] (i : ι) : ((i : ι) → φ i) →ₐ[R] φ i

Projection from a dependent product as an algebra homomorphism.

Equations

• AlgHom.proj R i = { toFun := fun (x : (i : ι) → φ i) => x i, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem AlgHom.proj_apply {R : Type u_4} {ι : Type u_5} [CommSemiring R] {φ : ι → Type u_6} [(i : ι) → Semiring (φ i)] [(i : ι) → Algebra R (φ i)] (x : (i : ι) → φ i) (i : ι) : (proj R i) x = x i

theorem AlgHom.proj_toLinearMap {R : Type u_4} {ι : Type u_5} [CommSemiring R] {φ : ι → Type u_6} [(i : ι) → Semiring (φ i)] [(i : ι) → Algebra R (φ i)] (i : ι) : (proj R i).toLinearMap = LinearMap.proj i

def NonUnitalAlgHom.single (R : Type u_4) {ι : Type u_5} [CommSemiring R] [DecidableEq ι] (φ : ι → Type u_6) [(i : ι) → Ring (φ i)] [(i : ι) → Module R (φ i)] (i : ι) : φ i →ₙₐ[R] (i : ι) → φ i

Insert one component into a dependent product as a non-unital algebra homomorphism.

Equations

• NonUnitalAlgHom.single R φ i = { toFun := fun (x : φ i) => (LinearMap.single R φ i) x, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

theorem NonUnitalAlgHom.single_apply {R : Type u_4} {ι : Type u_5} [CommSemiring R] [DecidableEq ι] {φ : ι → Type u_6} [(i : ι) → Ring (φ i)] [(i : ι) → Module R (φ i)] (i : ι) (x : φ i) : (single R φ i) x = Pi.single i x

theorem NonUnitalAlgHom.single_toLinearMap {R : Type u_4} {ι : Type u_5} [CommSemiring R] [DecidableEq ι] {φ : ι → Type u_6} [(i : ι) → Ring (φ i)] [(i : ι) → Module R (φ i)] (i : ι) : LinearMapClass.linearMap (single R φ i) = LinearMap.single R φ i

theorem LinearMap.single_isReal {R : Type u_4} {ι : Type u_5} [DecidableEq ι] [Semiring R] {φ : ι → Type u_6} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [(i : ι) → StarAddMonoid (φ i)] (i : ι) : IsReal (single R φ i)

theorem LinearMap.proj_isReal {R : Type u_4} {ι : Type u_5} [Semiring R] {φ : ι → Type u_6} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [(i : ι) → StarAddMonoid (φ i)] (i : ι) : IsReal (proj i)

theorem LinearMap.single_comp_inj {R : Type u_4} {ι : Type u_5} {B : Type u_6} [Semiring R] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [AddCommMonoid B] [Module R B] [(i : ι) → Module R (φ i)] [DecidableEq ι] (i : ι) (f g : B →ₗ[R] φ i) : single R φ i ∘ₗ f = single R φ i ∘ₗ g ↔ f = g

theorem LinearMap.comp_proj_inj {R : Type u_4} {ι : Type u_5} {B : Type u_6} [Semiring R] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [AddCommMonoid B] [Module R B] [(i : ι) → Module R (φ i)] (i : ι) (f g : φ i →ₗ[R] B) : f ∘ₗ proj i = g ∘ₗ proj i ↔ f = g

theorem LinearMap.proj_comp_inj {R : Type u_4} {ι : Type u_5} {B : Type u_6} [Semiring R] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [AddCommMonoid B] [Module R B] [(i : ι) → Module R (φ i)] (f g : B →ₗ[R] (r : ι) → φ r) : (∀ (i : ι), proj i ∘ₗ f = proj i ∘ₗ g) ↔ f = g

theorem NonUnitalAlgHom.id_toLinearMap {R : Type u_4} {A : Type u_5} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] : LinearMapClass.linearMap (NonUnitalAlgHom.id R A) = 1

theorem QuantumGraph.Real.conj_proj_isReal {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : Real (PiMat ℂ ι p) f) (i : ι) : Real (Mat ℂ (p i)) (LinearMap.proj i ∘ₗ f ∘ₗ LinearMap.adjoint (LinearMap.proj i))

theorem schurMul_proj_adjoint_comp {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [(i : ι) → Fintype (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {B : Type u_4} [starAlgebra B] [QuantumSet B] (i : ι) (f g : B →ₗ[ℂ] Mat ℂ (p i)) : (LinearMap.adjoint (LinearMap.proj i) ∘ₗ f) •ₛ LinearMap.adjoint (LinearMap.proj i) ∘ₗ g = LinearMap.adjoint (LinearMap.proj i) ∘ₗ f •ₛ g

theorem schurMul_proj_comp {ι : Type u_2} {p : ι → Type u_3} [(i : ι) → Fintype (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {B : Type u_4} [starAlgebra B] [QuantumSet B] [Finite ι] (f g : B →ₗ[ℂ] PiMat ℂ ι p) (i : ι) : (LinearMap.proj i ∘ₗ f) •ₛ LinearMap.proj i ∘ₗ g = LinearMap.proj i ∘ₗ f •ₛ g

theorem schurMul_comp_proj {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {B : Type u_4} [starAlgebra B] [QuantumSet B] (i : ι) (f g : Mat ℂ (p i) →ₗ[ℂ] B) : (f ∘ₗ LinearMap.proj i) •ₛ g ∘ₗ LinearMap.proj i = (f •ₛ g) ∘ₗ LinearMap.proj i

theorem schurMul_comp_proj_adjoint {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {B : Type u_4} [starAlgebra B] [QuantumSet B] (f g : PiMat ℂ ι p →ₗ[ℂ] B) (i : ι) : (f ∘ₗ LinearMap.adjoint (LinearMap.proj i)) •ₛ g ∘ₗ LinearMap.adjoint (LinearMap.proj i) = (f •ₛ g) ∘ₗ LinearMap.adjoint (LinearMap.proj i)

theorem QuantumGraph.isReal_iff_conj_proj_adjoint_isReal {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (i : ι) (f : Mat ℂ (p i) →ₗ[ℂ] Mat ℂ (p i)) : Real (Mat ℂ (p i)) f ↔ Real (PiMat ℂ ι p) (LinearMap.adjoint (LinearMap.proj i) ∘ₗ f ∘ₗ LinearMap.proj i)

theorem QuantumGraph.Real.proj_adjoint_comp_proj_conj_isRealQuantumGraph {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : Real (PiMat ℂ ι p) f) (i : ι × ι) : Real (PiMat ℂ ι p) (LinearMap.adjoint (LinearMap.proj i.1) ∘ₗ LinearMap.proj i.1 ∘ₗ f ∘ₗ LinearMap.adjoint (LinearMap.proj i.2) ∘ₗ LinearMap.proj i.2)

theorem schurMul_proj_adjoint_comp_of_ne_eq_zero {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [(i : ι) → Fintype (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {B : Type u_4} [starAlgebra B] [QuantumSet B] {i j : ι} : i ≠ j → ∀ (f : B →ₗ[ℂ] Mat ℂ (p i)) (g : B →ₗ[ℂ] Mat ℂ (p j)), (LinearMap.adjoint (LinearMap.proj i) ∘ₗ f) •ₛ LinearMap.adjoint (LinearMap.proj j) ∘ₗ g = 0

theorem schurMul_comp_proj_of_ne_eq_zero {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {B : Type u_4} [starAlgebra B] [QuantumSet B] {i j : ι} : i ≠ j → ∀ (f : Mat ℂ (p i) →ₗ[ℂ] B) (g : Mat ℂ (p j) →ₗ[ℂ] B), (f ∘ₗ LinearMap.proj i) •ₛ g ∘ₗ LinearMap.proj j = 0

theorem piMat_isRealQuantumGraph_iff_forall_conj_adjoint_proj_comp_proj {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} : QuantumGraph.Real (PiMat ℂ ι p) f ↔ ∀ (i : ι × ι), QuantumGraph.Real (PiMat ℂ ι p) (LinearMap.adjoint (LinearMap.proj i.1) ∘ₗ LinearMap.proj i.1 ∘ₗ f ∘ₗ LinearMap.adjoint (LinearMap.proj i.2) ∘ₗ LinearMap.proj i.2)

theorem Pi.single_zero_piFinTwo_same_apply {n : Type u_1} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) : single 0 x = (MatProdAlgEquivPiMat (PiFinTwoSame n)) (x, 0)

theorem Pi.single_one_piFinTwo_same_apply {n : Type u_1} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) : single 1 x = (MatProdAlgEquivPiMat (PiFinTwoSame n)) (0, x)

theorem PiMat_finTwo_same_swap_swap {n : Type u_1} [Fintype n] [DecidableEq n] (x : PiMat ℂ (Fin 2) (PiFinTwoSame n)) : PiMatFinTwoSameSwapAlgEquiv (PiMatFinTwoSameSwapAlgEquiv x) = x

theorem PiMatFinTwoSameSwapAlgEquiv_apply_piSingle_zero {n : Type u_1} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) : PiMatFinTwoSameSwapAlgEquiv (Pi.single 0 x) = Pi.single 1 x

theorem PiMatFinTwoSameSwapAlgEquiv_comp_linearMapSingle_zero {n : Type u_1} [Fintype n] [DecidableEq n] : PiMatFinTwoSameSwapAlgEquiv.toLinearMap ∘ₗ LinearMap.single ℂ (fun (j : Fin 2) => Mat ℂ (PiFinTwoSame n j)) 0 = LinearMap.single ℂ (fun (j : Fin 2) => Mat ℂ (PiFinTwoSame n j)) 1

theorem PiMatFinTwoSameSwapAlgEquiv_apply_piSingle_one {n : Type u_1} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) : PiMatFinTwoSameSwapAlgEquiv (Pi.single 1 x) = Pi.single 0 x

theorem PiMatFinTwoSameSwapAlgEquiv_comp_linearMapSingle_one {n : Type u_1} [Fintype n] [DecidableEq n] : PiMatFinTwoSameSwapAlgEquiv.toLinearMap ∘ₗ LinearMap.single ℂ (fun (j : Fin 2) => Mat ℂ (PiFinTwoSame n j)) 1 = LinearMap.single ℂ (fun (j : Fin 2) => Mat ℂ (PiFinTwoSame n j)) 0

theorem QuantumGraph.Real.schurProjection_proj_conj {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : Real (PiMat ℂ ι p) f) (i : ι × ι) : schurProjection (LinearMap.proj i.1 ∘ₗ f ∘ₗ LinearMap.adjoint (LinearMap.proj i.2))