Skip to content

Commit 058c7f7

Browse files
themathqueenthemathqueen
committed
last fix for the day
1 parent 8742352 commit 058c7f7

File tree

1 file changed

+132
-51
lines changed

1 file changed

+132
-51
lines changed

‎Monlib/QuantumGraph/Matrix.lean‎

Lines changed: 132 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -658,58 +658,139 @@ theorem PiMat_finTwo_same_proj_one_comp_swapStarAlgEquiv
658658
= LinearMap.proj 0 :=
659659
rfl
660660

661-
theorem QuantumGraph.Real.piMatFinTwo_same_isSelfAdjoint_reflexive_and_numOfEdges_eq_one_equiv
661+
set_option maxHeartbeats 500000 in
662+
theorem
663+
QuantumGraph.Real.piMatFinTwo_same_eq_zero_of_isSelfAdjoint_and_reflexive_and_numOfEdges_eq_one
662664
[Nontrivial n]
663665
(hc : Coalgebra.counit (R := ℂ) (A := PiMat ℂ (Fin 2) (PiFinTwo_same n)) = PiMat.traceLinearMap)
664-
{A B : PiMat ℂ (Fin 2) (PiFinTwo_same n) →ₗ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo_same n)}
666+
{A : PiMat ℂ (Fin 2) (PiFinTwo_same n) →ₗ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo_same n)}
665667
(hA : QuantumGraph.Real _ A) (hA₂ : LinearMap.adjoint A = A) (hA₃ : A •ₛ 1 = 1)
666-
(hA₄ : QuantumGraph.NumOfEdges A = 1)
667-
(hB : QuantumGraph.Real _ B) (hB₂ : LinearMap.adjoint B = B) (hB₃ : B •ₛ 1 = 1)
668-
(hB₄ : QuantumGraph.NumOfEdges B = 1) :
669-
∃ f : PiMat ℂ (Fin 2) (PiFinTwo_same n) ≃⋆ₐ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo_same n),
670-
QuantumGraph.equiv A B f :=
668+
(hA₄ : QuantumGraph.NumOfEdges A = 1) :
669+
A = 0 :=
671670
by
672-
have hA₅ := hA.PiMatFinTwo_same_isSelfAdjoint_reflexive_and_numOfEdges_eq_one hc hA₂ hA₃ hA₄
673-
have hB₅ := hB.PiMatFinTwo_same_isSelfAdjoint_reflexive_and_numOfEdges_eq_one hc hB₂ hB₃ hB₄
674-
have H1 : ∀ i : Fin 2, (A = LinearMap.adjoint (LinearMap.proj i)
675-
∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n i)) ∘ₗ LinearMap.proj i
676-
∧ B = LinearMap.adjoint (LinearMap.proj i)
677-
∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n i)) ∘ₗ LinearMap.proj i)
678-
→
679-
QuantumGraph.equiv A B (StarAlgEquiv.refl) :=
680-
by
681-
intro i h
682-
refine ⟨fun x1 ↦ congrFun rfl, ?_⟩
683-
apply LinearMap.ext
684-
simp only [h, Fin.isValue, LinearMap.coe_comp, LinearMap.coe_proj, Function.comp_apply,
685-
Function.eval, StarAlgEquiv.toLinearMap_apply, StarAlgEquiv.coe_refl, id_eq, implies_true]
686-
have H2 :
687-
((A = LinearMap.adjoint (LinearMap.proj 0)
688-
∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n 0)) ∘ₗ LinearMap.proj 0
689-
∧ B = LinearMap.adjoint (LinearMap.proj 1)
690-
∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n 1)) ∘ₗ LinearMap.proj 1)
691-
∨
692-
(A = LinearMap.adjoint (LinearMap.proj 1)
693-
∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n 1)) ∘ₗ LinearMap.proj 1
694-
∧ B = LinearMap.adjoint (LinearMap.proj 0)
695-
∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n 0)) ∘ₗ LinearMap.proj 0))
696-
→ QuantumGraph.equiv A B (PiMat_finTwo_same_swapStarAlgEquiv) :=
697-
by
698-
rintro (h | h)
699-
all_goals
700-
constructor
701-
. rw [QuantumSet.starAlgEquiv_isometry_iff_adjoint_eq_symm]
702-
exact PiMat_finTwo_same_swapStarAlgEquiv_isometry
703-
. simp_rw [h.1, h.2, LinearMap.comp_assoc]
704-
simp only [PiMat_finTwo_same_proj_one_comp_swapStarAlgEquiv,
705-
PiMat_finTwo_same_proj_zero_comp_swapStarAlgEquiv,
706-
← LinearMap.comp_assoc, LinearMap.proj_adjoint,
707-
PiMat_finTwo_same_swapStarAlgEquiv_comp_linearMapSingle_zero,
708-
PiMat_finTwo_same_swapStarAlgEquiv_comp_linearMapSingle_one]
709-
obtain (hf | hf) := hA₅
710-
. obtain (hg | hg) := hB₅
711-
. exact ⟨_, H1 _ ⟨hf, hg⟩⟩
712-
. exact ⟨_, H2 (Or.inl ⟨hf, hg⟩)⟩
713-
. obtain (hg | hg) := hB₅
714-
. exact ⟨_, H2 (Or.inr ⟨hf, hg⟩)⟩
715-
. exact ⟨_, H1 _ ⟨hf, hg⟩⟩
671+
rw [← QuantumGraph.dim_of_piMat_submodule_eq_numOfEdges_of_trace_counit hc hA.toQuantumGraph,
672+
Nat.cast_eq_one] at hA₄
673+
obtain ⟨i, hi, hf⟩ := hA.exists_unique_includeMap_of_adjoint_and_dim_ofPiMat_submodule_eq_one hA₂ hA₄
674+
let p : _ → PiMat ℂ _ (PiFinTwo_same n) →ₗ[ℂ] Mat ℂ _ := λ j => LinearMap.proj j
675+
have hp : ∀ j, p j = LinearMap.proj j := λ j => rfl
676+
have : ∀ j, p j ∘ₗ LinearMap.adjoint (p j) = 1 :=
677+
λ j => by
678+
simp only [LinearMap.proj_adjoint, p, LinearMap.one_eq_id, LinearMap.proj_comp_single_same]
679+
have this' : ∀ j, (p j ∘ₗ A ∘ₗ LinearMap.adjoint (p j)) •ₛ 1 = 1 :=
680+
λ j => by
681+
calc (p j ∘ₗ A ∘ₗ LinearMap.adjoint (p j)) •ₛ 1
682+
= (p j ∘ₗ A ∘ₗ LinearMap.adjoint (p j) ∘ₗ 1) •ₛ (p j ∘ₗ 1 ∘ₗ LinearMap.adjoint (p j)) :=
683+
by simp only [LinearMap.one_comp, LinearMap.comp_one, this]
684+
_ = p j ∘ₗ ((A ∘ₗ LinearMap.adjoint (p j)) •ₛ (1 ∘ₗ LinearMap.adjoint (p j))) :=
685+
schurMul_proj_comp (hφ := λ _ => hφ) _ _ _
686+
_ = p j ∘ₗ (A •ₛ 1) ∘ₗ LinearMap.adjoint (p j) :=
687+
by rw [schurMul_comp_proj_adjoint (hφ := λ _ => hφ)]
688+
_ = 1 := by simp only [hA₃, LinearMap.one_comp, this]
689+
have :=
690+
calc
691+
LinearMap.adjoint (p i) ∘ₗ p i + ∑ j ∈ Finset.univ \ {i}, LinearMap.adjoint (p j) ∘ₗ p j
692+
= ∑ j, LinearMap.adjoint (p j) ∘ₗ p j :=
693+
by
694+
simp only [Finset.subset_univ, Finset.sum_sdiff_eq_sub, Fin.sum_univ_two, Fin.isValue,
695+
Finset.sum_singleton, add_sub_cancel, p]
696+
_ = 1 :=
697+
by
698+
rw [LinearMap.one_eq_id, ← LinearMap.sum_single_comp_proj]
699+
simp only [p, LinearMap.proj_adjoint]
700+
_ = A •ₛ 1 := hA₃.symm
701+
_ = ∑ j, (LinearMap.adjoint (p i) ∘ₗ (p i) ∘ₗ A ∘ₗ LinearMap.adjoint (p i) ∘ₗ (p i))
702+
•ₛ (LinearMap.adjoint (p j) ∘ₗ 1 ∘ₗ p j) :=
703+
by
704+
simp only [p, hi]
705+
simp_rw [← map_sum,
706+
LinearMap.one_comp]
707+
congr
708+
rw [LinearMap.one_eq_id, ← LinearMap.sum_single_comp_proj]
709+
simp only [p, LinearMap.proj_adjoint, map_sum]
710+
_ = (LinearMap.adjoint (p i) ∘ₗ (p i) ∘ₗ A ∘ₗ LinearMap.adjoint (p i) ∘ₗ (p i))
711+
•ₛ (LinearMap.adjoint (p i) ∘ₗ 1 ∘ₗ p i)
712+
+ ∑ j ∈ Finset.univ \ {i},
713+
(LinearMap.adjoint (p i) ∘ₗ (p i) ∘ₗ A ∘ₗ LinearMap.adjoint (p i) ∘ₗ (p i))
714+
•ₛ (LinearMap.adjoint (p j) ∘ₗ 1 ∘ₗ p j) :=
715+
by
716+
simp only [schurMul_apply_apply, Fin.sum_univ_two, Fin.isValue, Finset.subset_univ,
717+
Finset.sum_sdiff_eq_sub, Finset.sum_singleton, add_sub_cancel,]
718+
_ = LinearMap.adjoint (p i) ∘ₗ p i :=
719+
by
720+
simp only [map_add, LinearMap.add_apply, p, schurMul_proj_adjoint_comp]
721+
simp only [← LinearMap.comp_assoc, schurMul_comp_proj]
722+
simp only [LinearMap.comp_assoc, ← hp, this']
723+
simp only [LinearMap.one_comp, add_right_eq_self]
724+
apply Finset.sum_eq_zero
725+
simp only [Finset.mem_sdiff, Finset.mem_univ, Finset.mem_singleton, true_and]
726+
push_neg
727+
intro j hj
728+
rw [schurMul_proj_adjoint_comp_of_ne_eq_zero (hφ := λ _ => hφ) hj.symm]
729+
simp only [Finset.subset_univ, Finset.sum_sdiff_eq_sub, Fin.sum_univ_two, Fin.isValue,
730+
Finset.sum_singleton, add_sub_cancel, LinearMap.ext_iff, LinearMap.add_apply,
731+
LinearMap.comp_apply, LinearMap.proj_apply, LinearMap.proj_adjoint_apply, funext_iff,
732+
Pi.add_apply, p] at this
733+
have hii : i = 0 ∨ i = 1 := Fin.exists_fin_two.mp ⟨i, rfl⟩
734+
specialize this 1 (if i = 0 then 1 else 0)
735+
rcases hii with (hii | hii)
736+
<;> rw [hii] at this
737+
<;> simp only [add_right_eq_self, add_left_eq_self, includeBlock_apply,
738+
LinearMap.single_apply, dite_eq_right_iff] at this
739+
<;> simp only [Fin.isValue, ↓reduceIte, ↓dreduceIte, Pi.one_apply, eq_mp_eq_cast, cast_eq,
740+
one_ne_zero, imp_false, not_true_eq_false, p] at this
741+
742+
-- theorem QuantumGraph.Real.piMatFinTwo_same_isSelfAdjoint_reflexive_and_numOfEdges_eq_one_equiv
743+
-- [Nontrivial n]
744+
-- (hc : Coalgebra.counit (R := ℂ) (A := PiMat ℂ (Fin 2) (PiFinTwo_same n)) = PiMat.traceLinearMap)
745+
-- {A B : PiMat ℂ (Fin 2) (PiFinTwo_same n) →ₗ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo_same n)}
746+
-- (hA : QuantumGraph.Real _ A) (hA₂ : LinearMap.adjoint A = A) (hA₃ : A •ₛ 1 = 1)
747+
-- (hA₄ : QuantumGraph.NumOfEdges A = 1)
748+
-- (hB : QuantumGraph.Real _ B) (hB₂ : LinearMap.adjoint B = B) (hB₃ : B •ₛ 1 = 1)
749+
-- (hB₄ : QuantumGraph.NumOfEdges B = 1) :
750+
-- ∃ f : PiMat ℂ (Fin 2) (PiFinTwo_same n) ≃⋆ₐ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo_same n),
751+
-- QuantumGraph.equiv A B f :=
752+
-- by
753+
-- have hA₅ := hA.PiMatFinTwo_same_isSelfAdjoint_reflexive_and_numOfEdges_eq_one hc hA₂ hA₃ hA₄
754+
-- have hB₅ := hB.PiMatFinTwo_same_isSelfAdjoint_reflexive_and_numOfEdges_eq_one hc hB₂ hB₃ hB₄
755+
-- have H1 : ∀ i : Fin 2, (A = LinearMap.adjoint (LinearMap.proj i)
756+
-- ∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n i)) ∘ₗ LinearMap.proj i
757+
-- ∧ B = LinearMap.adjoint (LinearMap.proj i)
758+
-- ∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n i)) ∘ₗ LinearMap.proj i)
759+
-- →
760+
-- QuantumGraph.equiv A B (StarAlgEquiv.refl) :=
761+
-- by
762+
-- intro i h
763+
-- refine ⟨fun x1 ↦ congrFun rfl, ?_⟩
764+
-- apply LinearMap.ext
765+
-- simp only [h, Fin.isValue, LinearMap.coe_comp, LinearMap.coe_proj, Function.comp_apply,
766+
-- Function.eval, StarAlgEquiv.toLinearMap_apply, StarAlgEquiv.coe_refl, id_eq, implies_true]
767+
-- have H2 :
768+
-- ((A = LinearMap.adjoint (LinearMap.proj 0)
769+
-- ∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n 0)) ∘ₗ LinearMap.proj 0
770+
-- ∧ B = LinearMap.adjoint (LinearMap.proj 1)
771+
-- ∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n 1)) ∘ₗ LinearMap.proj 1)
772+
-- ∨
773+
-- (A = LinearMap.adjoint (LinearMap.proj 1)
774+
-- ∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n 1)) ∘ₗ LinearMap.proj 1
775+
-- ∧ B = LinearMap.adjoint (LinearMap.proj 0)
776+
-- ∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n 0)) ∘ₗ LinearMap.proj 0))
777+
-- → QuantumGraph.equiv A B (PiMat_finTwo_same_swapStarAlgEquiv) :=
778+
-- by
779+
-- rintro (h | h)
780+
-- all_goals
781+
-- constructor
782+
-- . rw [QuantumSet.starAlgEquiv_isometry_iff_adjoint_eq_symm]
783+
-- exact PiMat_finTwo_same_swapStarAlgEquiv_isometry
784+
-- . simp_rw [h.1, h.2, LinearMap.comp_assoc]
785+
-- simp only [PiMat_finTwo_same_proj_one_comp_swapStarAlgEquiv,
786+
-- PiMat_finTwo_same_proj_zero_comp_swapStarAlgEquiv,
787+
-- ← LinearMap.comp_assoc, LinearMap.proj_adjoint,
788+
-- PiMat_finTwo_same_swapStarAlgEquiv_comp_linearMapSingle_zero,
789+
-- PiMat_finTwo_same_swapStarAlgEquiv_comp_linearMapSingle_one]
790+
-- obtain (hf | hf) := hA₅
791+
-- . obtain (hg | hg) := hB₅
792+
-- . exact ⟨_, H1 _ ⟨hf, hg⟩⟩
793+
-- . exact ⟨_, H2 (Or.inl ⟨hf, hg⟩)⟩
794+
-- . obtain (hg | hg) := hB₅
795+
-- . exact ⟨_, H2 (Or.inr ⟨hf, hg⟩)⟩
796+
-- . exact ⟨_, H1 _ ⟨hf, hg⟩⟩

0 commit comments

Comments
 (0)