def MatProd_algEquiv_PiMat (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'

Equations

• MatProd_algEquiv_PiMat n' = matrixPiFinTwo_algEquiv_prod.symm

@[reducible, inline]

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

Equations

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

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)

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 MatProd_algEquiv_PiMat_swap (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')

Equations

• MatProd_algEquiv_PiMat_swap n' = MatProd_algEquiv_PiMat (PiFinTwo.swap n')

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

Equations

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

@[simp]

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

@[simp]

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

def PiMat_finTwo_swapAlgEquiv {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')

Equations

• PiMat_finTwo_swapAlgEquiv = (MatProd_algEquiv_PiMat n').symm.trans ((Prod.swap_algEquiv (Matrix (n' 0) (n' 0) ℂ) (Matrix (n' 1) (n' 1) ℂ)).trans (MatProd_algEquiv_PiMat_swap n'))

@[reducible, inline]

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

Equations

• PiFinTwo_same n x✝ = n

instance instFintypePiFinTwo_same {n : Type u_1} [Fintype n] (i : Fin 2) : Fintype (PiFinTwo_same n i)

Equations

• instFintypePiFinTwo_same i = inferInstance

instance instDecidableEqPiFinTwo_same {n : Type u_1} [DecidableEq n] (i : Fin 2) : DecidableEq (PiFinTwo_same n i)

Equations

• instDecidableEqPiFinTwo_same i = inferInstance

theorem PiMat_finTwo_swapAlgEquiv_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) ℂ) : PiMat_finTwo_swapAlgEquiv ((MatProd_algEquiv_PiMat n') (x, y)) = (MatProd_algEquiv_PiMat (PiFinTwo.swap n')) (y, x)

theorem PiFinTwo_same_swap {n : Type u_1} : PiFinTwo.swap (PiFinTwo_same n) = PiFinTwo_same n

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

Equations

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

theorem PiMat_finTwo_same_swapAlgEquiv_apply {n : Type u_1} [Fintype n] [DecidableEq n] (x y : Matrix n n ℂ) : PiMat_finTwo_same_swapAlgEquiv ((MatProd_algEquiv_PiMat (PiFinTwo_same n)) (x, y)) = (MatProd_algEquiv_PiMat (PiFinTwo_same n)) (y, x)

theorem AlgEquiv.prod_map_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.prod_map g).IsInner

instance MatProd_algEquiv_PiMat_same_invertible_of {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ × Matrix n n ℂ} (hU : Invertible U) : Invertible ((MatProd_algEquiv_PiMat (PiFinTwo_same n)) U)

Equations

• MatProd_algEquiv_PiMat_same_invertible_of hU = { invOf := (MatProd_algEquiv_PiMat (PiFinTwo_same 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) : ((MatProd_algEquiv_PiMat (PiFinTwo_same n)).symm.trans (f.trans (MatProd_algEquiv_PiMat (PiFinTwo_same n)))).IsInner

theorem AlgEquiv.PiMat_finTwo_same {n : Type u_1} [Fintype n] [DecidableEq n] (f : PiMat ℂ (Fin 2) (PiFinTwo_same n) ≃ₐ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo_same n)) : f.IsInner ∨ ∃ (g : PiMat ℂ (Fin 2) (PiFinTwo_same n) ≃ₐ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo_same n)) (_ : g.IsInner), f = PiMat_finTwo_same_swapAlgEquiv.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))) (PiMat_toEuclideanLM y x)

theorem QuantumGraph.Real.dim_of_piMat_submodule_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) : ⋯.dim_of_piMat_submodule = ∑ i : ι × ι, Module.finrank ℂ ↥(hA.PiMat_submodule i)

theorem Module.Dual.pi.IsFaithfulPosMap.includeBlock_right_inner {ι : Type u_2} {p : ι → Type u_3} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {i : ι} (x : PiMat ℂ ι p) (y : Matrix (p i) (p i) ℂ) : inner x (Matrix.includeBlock y) = inner (x i) y

theorem LinearMap.proj_adjoint_apply {ι : 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 : ι) (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 : ι) → DecidableEq (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 : ι) → DecidableEq (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 ι] [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) : A = ∑ i : ι × ι, adjoint (proj i.1) ∘ₗ (proj i.1 ∘ₗ A ∘ₗ adjoint (proj i.2)) ∘ₗ proj i.2

theorem Pi.nat_eq_zero_of_sum_eq_one_and_unique_one {ι : Type u_4} [Fintype ι] [DecidableEq ι] {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 ι] [DecidableEq ι] {f : ι → ℕ} (h : ∑ i : ι, f i = 1) : ∃! i : ι, f i = 1

theorem QuantumGraph.Real.dim_of_piMat_submodule_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) : ⋯.dim_of_piMat_submodule = 0 ↔ A = 0

theorem QuantumGraph.Real.exists_unique_includeMap_of_adjoint_and_dim_ofPiMat_submodule_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 : ⋯.dim_of_piMat_submodule = 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 (PiFinTwo_same n i) (PiFinTwo_same n i) ℂ)} [hψ : ∀ (i : Fin 2), (ψ i).IsFaithfulPosMap] {A : PiMat ℂ (Fin 2) (PiFinTwo_same n) →ₗ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo_same n)} (hA : Real (PiMat ℂ (Fin 2) (PiFinTwo_same n)) A) (hA₂ : LinearMap.adjoint A = A) (hd : ⋯.dim_of_piMat_submodule = 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

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 : ι) → Semiring (φ i)] [(i : ι) → Algebra R (φ i)] (i : ι) : φ i →ₙₐ[R] (i : ι) → φ i

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 : ι) → Semiring (φ i)] [(i : ι) → Algebra 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 : ι) → Semiring (φ i)] [(i : ι) → Algebra R (φ i)] (i : ι) : (single R φ i).toLinearMap = 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} [DecidableEq ι] [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)] [DecidableEq ι] (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)] [DecidableEq ι] (f g : B →ₗ[R] (r : ι) → φ r) : (∀ (i : ι), proj i ∘ₗ f = proj i ∘ₗ g) ↔ f = g

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.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 ι] [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 : 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} [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 : 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.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 ι] [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 : ι} (hij : 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 : ι} (hij : 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 = (MatProd_algEquiv_PiMat (PiFinTwo_same 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 = (MatProd_algEquiv_PiMat (PiFinTwo_same n)) (0, x)

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

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

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

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

theorem PiMat_finTwo_same_swapAlgEquiv_comp_linearMapSingle_one {n : Type u_1} [Fintype n] [DecidableEq n] : PiMat_finTwo_same_swapAlgEquiv.toLinearMap ∘ₗ LinearMap.single ℂ (fun (j : Fin 2) => Mat ℂ (PiFinTwo_same n j)) 1 = LinearMap.single ℂ (fun (j : Fin 2) => Mat ℂ (PiFinTwo_same 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))