Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CaptureZero.lean, lines 33–102.
Back to An irreducible target representation has a surviving fixed space
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TargetReconstruction 2import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.IrreduciblePure 3import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.GeneratedReduction 4import MathlibAnnex.Analysis.InnerProductSpace.Reduction 5 6/-! 7# The zero-defect branch for the completed-CAR target 8 9If every represented initial limiting fixed space vanished, reduction for the 10restricted completed-CAR representation would pass through the target-side 11strong shell sums to every added generator. It would therefore pass to the 12whole norm-closed generated target. Target irreducibility would make the 13source restriction irreducible, while chosen pure-GNS coverage supplies a 14nonzero common fixed vector. This contradiction closes the zero-defect 15branch without moving any strong limit through the representation. 16-/ 17 18set_option autoImplicit false 19set_option maxHeartbeats 1200000 20 21noncomputable section 22 23open Filter Topology 24open scoped ComplexOrder ENNReal lp InnerProduct 25 26namespace MathlibAnnex.CStarAlgebra.CAR 27 28open MathlibAnnex.Analysis.CStarAlgebra 29open MathlibAnnex.Analysis.InnerProductSpace 30 31universe v 32 33/-- Under the all-zero limiting-defect hypothesis, the completed-CAR 34restriction of an irreducible target representation is itself irreducible. -/ 35theorem isIrreducible_restrictedRepresentation_of_all_fixed_bot 36 (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 ∈ unitary 41 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 42 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 43 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation 44 (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 := by 52 letI : Nontrivial K := Representation.nontrivial_of_isNonzero rho hrho.1 53 refine ⟨Representation.isNonzero_of_nontrivial _, ?_⟩ 54 intro M hM 55 have hgenerator (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 56 M.Reduces (rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i)) := by 57 obtain ⟨S, T, P, Q, R, hS, hT, -, -, hAdj, -, hPrange, -, -, -, -, 58 heq, hR, -, -, -, -⟩ := 59 exists_targetShellReconstruction family L hLunit hLsource rho i 60 have hPzero : P = 0 := by 61 apply ContinuousLinearMap.ext 62 intro x 63 have hx : P x ∈ P.range := ⟨x, rfl⟩ 64 rw [hPrange, hzero i, Submodule.mem_bot] at hx 65 exact hx 66 have hRzero : R = 0 := by 67 rw [hR, hPzero] 68 simp 69 have hsum : 70 ((Unitary.linearIsometryEquiv 71 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) : 72 K →L[ℂ] K) = S := by 73 simpa [hRzero] using heq 74 have hW (n : ℕ) : M.Reduces 75 ((restrictedRepresentation L rho) 76 ((representativeShellData family i).link n)) := by 77 constructor 78 · intro x hx 79 exact (hM.2 ((representativeShellData family i).link n) x hx).1 80 · intro x hx 81 exact (hM.2 ((representativeShellData family i).link n) x hx).2 82 have hSreduces : M.Reduces S := 83 Submodule.Reduces.of_stronglyConverges_partialSum hM.1 hW hS hT hAdj 84 change M.Reduces 85 (((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 hSreduces 90 have hsource (a : Limit) : 91 M.Reduces (rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L a)) := by 92 constructor 93 · intro x hx 94 exact (hM.2 a x hx).1 95 · intro x hx 96 exact (hM.2 a x hx).2 97 have hall := MathlibAnnex.CStarAlgebra.AtomicConstruction.reduces_concreteTarget_of_generators 98 selectedAtomicRepresentation L rho M hM.1 hsource hgenerator 99 apply hrho.2 M 100 refine ⟨hM.1, ?_⟩ 101 intro a x hx 102 exact ⟨(hall a).1 hx, (hall a).2 hx⟩ 103 104/-- Every irreducible representation of the actual completed-CAR atomic 105target has a surviving represented initial limiting defect. This is the 106formal conclusion of the all-zero/surviving-defect split's first branch. -/ 107theorem exists_nonzero_targetFixedSpace 108 (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 ∈ unitary 113 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 114 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 115 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation 116 (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) ≠ ⊥ := by 124 by_contra hnone 125 have hzero : ∀ i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit, 126 (⨅ n, ((restrictedRepresentation L rho) 127 (transportedFlag family i n)).range) = ⊥ := by 128 intro i 129 by_contra hi 130 exact hnone ⟨i, hi⟩ 131 have hsigma := isIrreducible_restrictedRepresentation_of_all_fixed_bot 132 family L hLunit hLsource rho hrho hzero 133 obtain ⟨j, e, he⟩ := MathlibAnnex.CStarAlgebra.irreducible_covered_by_pureState_representative 134 completedRootPureState (restrictedRepresentation L rho) hsigma 135 let xi := MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState j 136 let eta : K := e.symm xi 137 have heta_norm : ‖eta‖ = 1 := by 138 simp [eta, xi, MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector] 139 have hfix (n : ℕ) : 140 (restrictedRepresentation L rho) (transportedFlag family j n) eta = eta := by 141 apply e.injective 142 calc 143 e ((restrictedRepresentation L rho) (transportedFlag family j n) eta) = 144 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j) 145 (transportedFlag family j n) (e eta) := by 146 simpa [MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation] using 147 he (transportedFlag family j n) eta 148 _ = (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j) 149 (transportedFlag family j n) xi := by simp [eta] 150 _ = xi := selectedVector_fixed_transportedFlag family j n 151 _ = e eta := by simp [eta] 152 have heta_mem : eta ∈ (⨅ n, 153 ((restrictedRepresentation L rho) (transportedFlag family j n)).range) := by 154 rw [Submodule.mem_iInf] 155 intro n 156 exact ⟨eta, hfix n⟩ 157 rw [hzero j, Submodule.mem_bot] at heta_mem 158 have := congrArg norm heta_mem 159 simpa [heta_norm] using this 160 161end MathlibAnnex.CStarAlgebra.CAR