Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CaptureZero.lean
Pinned GitHub source · Raw UTF-8 source
Back to An irreducible target representation has a surviving fixed space · Back to A common root vector realizes every selected state through the generators
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TargetReconstruction2import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.IrreduciblePure3import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.GeneratedReduction4import MathlibAnnex.Analysis.InnerProductSpace.Reduction56/-!7# The zero-defect branch for the completed-CAR target89If every represented initial limiting fixed space vanished, reduction for the10restricted completed-CAR representation would pass through the target-side11strong shell sums to every added generator. It would therefore pass to the12whole norm-closed generated target. Target irreducibility would make the13source restriction irreducible, while chosen pure-GNS coverage supplies a14nonzero common fixed vector. This contradiction closes the zero-defect15branch without moving any strong limit through the representation.16-/1718set_option autoImplicit false19set_option maxHeartbeats 12000002021noncomputable section2223open Filter Topology24open scoped ComplexOrder ENNReal lp InnerProduct2526namespace MathlibAnnex.CStarAlgebra.CAR2728open MathlibAnnex.Analysis.CStarAlgebra29open MathlibAnnex.Analysis.InnerProductSpace3031universe v3233/-- Under the all-zero limiting-defect hypothesis, the completed-CAR34restriction of an irreducible target representation is itself irreducible. -/35theorem isIrreducible_restrictedRepresentation_of_all_fixed_bot36 (family : RepresentativeShellFamily)37 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →38 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]39 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)40 (hLunit : ∀ i, L i ∈ unitary41 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]42 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))43 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation44 (transportedFlag family i n - transportedFlag family i (n + 1))) =45 representedShellLink family i n)46 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]47 [CompleteSpace K] (rho : Representation (AtomicTarget L) K)48 (hrho : rho.IsIrreducible)49 (hzero : ∀ i, (⨅ n,50 ((restrictedRepresentation L rho) (transportedFlag family i n)).range) = ⊥) :51 (restrictedRepresentation L rho).IsIrreducible := by52 letI : Nontrivial K := Representation.nontrivial_of_isNonzero rho hrho.153 refine ⟨Representation.isNonzero_of_nontrivial _, ?_⟩54 intro M hM55 have hgenerator (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :56 M.Reduces (rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i)) := by57 obtain ⟨S, T, P, Q, R, hS, hT, -, -, hAdj, -, hPrange, -, -, -, -,58 heq, hR, -, -, -, -⟩ :=59 exists_targetShellReconstruction family L hLunit hLsource rho i60 have hPzero : P = 0 := by61 apply ContinuousLinearMap.ext62 intro x63 have hx : P x ∈ P.range := ⟨x, rfl⟩64 rw [hPrange, hzero i, Submodule.mem_bot] at hx65 exact hx66 have hRzero : R = 0 := by67 rw [hR, hPzero]68 simp69 have hsum :70 ((Unitary.linearIsometryEquiv71 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) :72 K →L[ℂ] K) = S := by73 simpa [hRzero] using heq74 have hW (n : ℕ) : M.Reduces75 ((restrictedRepresentation L rho)76 ((representativeShellData family i).link n)) := by77 constructor78 · intro x hx79 exact (hM.2 ((representativeShellData family i).link n) x hx).180 · intro x hx81 exact (hM.2 ((representativeShellData family i).link n) x hx).282 have hSreduces : M.Reduces S :=83 Submodule.Reduces.of_stronglyConverges_partialSum hM.1 hW hS hT hAdj84 change M.Reduces85 (((representedGeneratorUnitary L hLunit rho i : unitary (K →L[ℂ] K)) :86 K →L[ℂ] K))87 rw [show ((representedGeneratorUnitary L hLunit rho i :88 unitary (K →L[ℂ] K)) : K →L[ℂ] K) = S by simpa using hsum]89 exact hSreduces90 have hsource (a : Limit) :91 M.Reduces (rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L a)) := by92 constructor93 · intro x hx94 exact (hM.2 a x hx).195 · intro x hx96 exact (hM.2 a x hx).297 have hall := MathlibAnnex.CStarAlgebra.AtomicConstruction.reduces_concreteTarget_of_generators98 selectedAtomicRepresentation L rho M hM.1 hsource hgenerator99 apply hrho.2 M100 refine ⟨hM.1, ?_⟩101 intro a x hx102 exact ⟨(hall a).1 hx, (hall a).2 hx⟩103104/-- Every irreducible representation of the actual completed-CAR atomic105target has a surviving represented initial limiting defect. This is the106formal conclusion of the all-zero/surviving-defect split's first branch. -/107theorem exists_nonzero_targetFixedSpace108 (family : RepresentativeShellFamily)109 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →110 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]111 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)112 (hLunit : ∀ i, L i ∈ unitary113 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]114 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))115 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation116 (transportedFlag family i n - transportedFlag family i (n + 1))) =117 representedShellLink family i n)118 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]119 [CompleteSpace K] (rho : Representation (AtomicTarget L) K)120 (hrho : rho.IsIrreducible) :121 ∃ i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit,122 (⨅ n, ((restrictedRepresentation L rho)123 (transportedFlag family i n)).range) ≠ ⊥ := by124 by_contra hnone125 have hzero : ∀ i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit,126 (⨅ n, ((restrictedRepresentation L rho)127 (transportedFlag family i n)).range) = ⊥ := by128 intro i129 by_contra hi130 exact hnone ⟨i, hi⟩131 have hsigma := isIrreducible_restrictedRepresentation_of_all_fixed_bot132 family L hLunit hLsource rho hrho hzero133 obtain ⟨j, e, he⟩ := MathlibAnnex.CStarAlgebra.irreducible_covered_by_pureState_representative134 completedRootPureState (restrictedRepresentation L rho) hsigma135 let xi := MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState j136 let eta : K := e.symm xi137 have heta_norm : ‖eta‖ = 1 := by138 simp [eta, xi, MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector]139 have hfix (n : ℕ) :140 (restrictedRepresentation L rho) (transportedFlag family j n) eta = eta := by141 apply e.injective142 calc143 e ((restrictedRepresentation L rho) (transportedFlag family j n) eta) =144 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j)145 (transportedFlag family j n) (e eta) := by146 simpa [MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation] using147 he (transportedFlag family j n) eta148 _ = (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j)149 (transportedFlag family j n) xi := by simp [eta]150 _ = xi := selectedVector_fixed_transportedFlag family j n151 _ = e eta := by simp [eta]152 have heta_mem : eta ∈ (⨅ n,153 ((restrictedRepresentation L rho) (transportedFlag family j n)).range) := by154 rw [Submodule.mem_iInf]155 intro n156 exact ⟨eta, hfix n⟩157 rw [hzero j, Submodule.mem_bot] at heta_mem158 have := congrArg norm heta_mem159 simpa [heta_norm] using this160161end MathlibAnnex.CStarAlgebra.CAR