Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/InvolutionLift.lean, lines 24–47.
Back to Lifting a corner involution to an ambient CAR unitary
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CornerLift 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.StagePurification 3import MathlibAnnex.Analysis.CStarAlgebra.SmallUnitary 4import MathlibAnnex.Analysis.CStarAlgebra.Representation.Adapters 5import MathlibAnnex.Analysis.InnerProductSpace.InvolutionExponential 6 7set_option autoImplicit false 8 9noncomputable section 10 11open NormedSpace 12open scoped CStarAlgebra 13open MathlibAnnex.Analysis.CStarAlgebra 14open MathlibAnnex.Analysis.InnerProductSpace 15 16namespace MathlibAnnex.CStarAlgebra.CAR 17 18abbrev rootCornerSubspace 19 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 20 [CompleteSpace H] 21 (rho : Representation Limit H) (n : ℕ) : Submodule ℂ H := 22 LinearMap.range (rho (limitMatrixUnit n 0 0)).toLinearMap 23 24theorem representation_liftedCornerExponential_apply_of_root 25 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 26 [CompleteSpace H] (rho : Representation Limit H) (n : ℕ) 27 (h : selfAdjoint Limit) 28 (heh : limitMatrixUnit n 0 0 * (h : Limit) = h) 29 (hhe : (h : Limit) * limitMatrixUnit n 0 0 = h) 30 (x : H) (hx : rho (limitMatrixUnit n 0 0) x = x) : 31 rho (liftedCornerExponential n h heh hhe : Limit) x = 32 rho (cornerExponential n h) x := by 33 let z := cornerExponential n h 34 have hz := isRootCornerUnitary_cornerExponential n h heh hhe 35 change rho (cornerLift n z) x = rho z x 36 rw [representation_cornerLift_apply] 37 rw [Finset.sum_eq_single (0 : Fin (2 ^ n))] 38 · simp only [z] 39 rw [show rho (limitMatrixUnit n 0 0) x = x by exact hx] 40 change rho (limitMatrixUnit n 0 0) (rho (cornerExponential n h) x) = _ 41 rw [← mul_apply_eq_comp, ← map_mul, hz.2.2.1] 42 · intro i _ hi 43 have h0i : rho (limitMatrixUnit n 0 i) x = 0 := by 44 rw [← hx, ← mul_apply_eq_comp, ← map_mul] 45 simp [hi] 46 simp [h0i] 47 · simp 48 49set_option maxHeartbeats 800000 in 50theorem exists_rootCornerSupported_exponential_apply_eq_involution 51 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 52 [CompleteSpace H] [Nontrivial H] 53 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 54 (n d : ℕ) (v : Fin d → rootCornerSubspace rho n) 55 (U : rootCornerSubspace rho n ≃ₗᵢ[ℂ] rootCornerSubspace rho n) 56 (hU : ∀ x, U (U x) = x) : 57 ∃ h : selfAdjoint Limit, 58 limitMatrixUnit n 0 0 * (h : Limit) = h ∧ 59 (h : Limit) * limitMatrixUnit n 0 0 = h ∧ 60 ∀ i, rho (cornerExponential n h) (v i : H) = (U (v i) : H) := by 61 let e : Limit := limitMatrixUnit n 0 0 62 let K : Submodule ℂ H := rootCornerSubspace rho n 63 have hroot : IsStarProjection (rho e) := by 64 exact (isStarProjection_limitMatrixUnit_zero_zero n).map rho 65 letI : CompleteSpace K := IsComplete.completeSpace_coe 66 (ContinuousLinearMap.IsIdempotentElem.isClosed_range 67 hroot.isIdempotentElem).isComplete 68 have hKnot : ¬ FiniteDimensional ℂ K := by 69 simpa [K, e, rootCornerSubspace] using 70 not_finiteDimensional_range_rootCorner rho 71 ((MathlibAnnex.Analysis.CStarAlgebra.Representation.isIrreducible_iff_starAlgHom rho).mpr 72 hrho) n 73 letI : Nontrivial K := by 74 rw [← not_subsingleton_iff_nontrivial] 75 intro hsub 76 apply hKnot 77 letI : Subsingleton K := hsub 78 exact FiniteDimensional.of_rank_eq_zero (rank_subsingleton' ℂ K) 79 letI : NormedRing (K →L[ℂ] K) := ContinuousLinearMap.toNormedRing 80 letI : K.HasOrthogonalProjection := by 81 simpa [K] using 82 (ContinuousLinearMap.IsIdempotentElem.hasOrthogonalProjection_range 83 hroot.isIdempotentElem) 84 let P : K →L[ℂ] K := U.involutionProjection 85 have hPstar : IsStarProjection P := U.isStarProjection_involutionProjection hU 86 let PH : H →L[ℂ] H := 87 MathlibAnnex.Analysis.CStarAlgebra.zeroExtension K P 88 let T : H →L[ℂ] H := (Real.pi : ℂ) • PH 89 let S : Set H := 90 Set.range (fun i => (v i : H)) ∪ Set.range (fun i => (U (v i) : H)) 91 let E : Submodule ℂ H := Submodule.span ℂ S 92 letI : FiniteDimensional ℂ E := 93 FiniteDimensional.span_of_finite ℂ 94 ((Set.finite_range fun i => (v i : H)).union 95 (Set.finite_range fun i => (U (v i) : H))) 96 letI : E.HasOrthogonalProjection := inferInstance 97 have hKfix (x : K) : rho e (x : H) = (x : H) := by 98 exact (LinearMap.IsIdempotentElem.mem_range_iff 99 (ContinuousLinearMap.IsIdempotentElem.toLinearMap 100 hroot.isIdempotentElem)).mp x.property 101 have hvE (i : Fin d) : (v i : H) ∈ E := 102 Submodule.subset_span (Or.inl (Set.mem_range_self i)) 103 have hUvE (i : Fin d) : (U (v i) : H) ∈ E := 104 Submodule.subset_span (Or.inr (Set.mem_range_self i)) 105 have hEroot : ∀ x : H, x ∈ E → rho e x = x := by 106 intro x hx 107 refine Submodule.span_induction 108 (p := fun x _ => rho e x = x) ?_ (by simp) ?_ ?_ hx 109 · intro x hx 110 rcases hx with hx | hx 111 · obtain ⟨i, rfl⟩ := hx 112 exact hKfix (v i) 113 · obtain ⟨i, rfl⟩ := hx 114 exact hKfix (U (v i)) 115 · intro x y _ _ hx hy 116 simpa using congrArg₂ (· + ·) hx hy 117 · intro c x _ hx 118 simpa using congrArg (fun y => c • y) hx 119 have hPHself : IsSelfAdjoint PH := 120 MathlibAnnex.Analysis.CStarAlgebra.isSelfAdjoint_zeroExtension 121 K P hPstar.isSelfAdjoint 122 have hTself : IsSelfAdjoint T := by 123 dsimp only [T] 124 rw [isSelfAdjoint_iff, star_smul, hPHself.star_eq] 125 simp 126 have hTroot : rho e * T = T := by 127 apply ContinuousLinearMap.ext 128 intro x 129 change rho e (T x) = T x 130 exact hKfix ⟨T x, by 131 dsimp only [T] 132 rw [ContinuousLinearMap.smul_apply] 133 apply K.smul_mem 134 dsimp [PH, MathlibAnnex.Analysis.CStarAlgebra.zeroExtension] 135 exact (P (K.orthogonalProjectionOnto x)).property⟩ 136 have hTmap : Set.MapsTo T E E := by 137 intro x hx 138 refine Submodule.span_induction 139 (p := fun x _ => T x ∈ E) ?_ (by simp [T]) ?_ ?_ hx 140 · intro x hx 141 rcases hx with hx | hx 142 · obtain ⟨i, rfl⟩ := hx 143 rw [show T (v i : H) = 144 (Real.pi : ℂ) • ((2 : ℂ)⁻¹ • 145 ((v i : H) - (U (v i) : H))) by 146 simp [T, PH, P, 147 MathlibAnnex.Analysis.CStarAlgebra.zeroExtension_apply_of_mem, 148 LinearIsometryEquiv.involutionProjection_apply, smul_smul] 149 module] 150 exact E.smul_mem _ (E.smul_mem _ (E.sub_mem (hvE i) (hUvE i))) 151 · obtain ⟨i, rfl⟩ := hx 152 rw [show T (U (v i) : H) = 153 (Real.pi : ℂ) • ((2 : ℂ)⁻¹ • 154 ((U (v i) : H) - (v i : H))) by 155 simp [T, PH, P, 156 MathlibAnnex.Analysis.CStarAlgebra.zeroExtension_apply_of_mem, 157 LinearIsometryEquiv.involutionProjection_apply, hU, smul_smul] 158 module] 159 exact E.smul_mem _ (E.smul_mem _ (E.sub_mem (hUvE i) (hvE i))) 160 · intro x y _ _ hx hy 161 simpa using E.add_mem hx hy 162 · intro c x _ hx 163 simpa using E.smul_mem c hx 164 obtain ⟨h, -, heh, hhe, hexp⟩ := 165 exists_rootCornerSupported_exponential_eq_on 166 rho hrho n E hEroot T hTself hTroot hTmap 167 refine ⟨h, heh, hhe, fun i => ?_⟩ 168 rw [hexp (v i : H) (hvE i)] 169 have hsmul : Complex.I • T = 170 ((Real.pi : ℂ) * Complex.I) • PH := by 171 dsimp only [T] 172 module 173 rw [hsmul] 174 have hzero : ((Real.pi : ℂ) * Complex.I) • PH = 175 MathlibAnnex.Analysis.CStarAlgebra.zeroExtension K 176 (((Real.pi : ℂ) * Complex.I) • P) := by 177 ext x 178 simp [PH, MathlibAnnex.Analysis.CStarAlgebra.zeroExtension, smul_smul] 179 rw [hzero, MathlibAnnex.Analysis.CStarAlgebra.exp_zeroExtension_apply 180 K (((Real.pi : ℂ) * Complex.I) • P) (v i)] 181 exact congrArg Subtype.val 182 (MathlibAnnex.Analysis.InnerProductSpace.exp_pi_mul_involutionProjection_apply 183 U hU (v i)) 184 185/-- The ambient unitary obtained by amplifying the same corner exponential 186acts as the prescribed involution on the selected root-corner family. -/ 187theorem exists_liftedCornerExponential_apply_eq_involution 188 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 189 [CompleteSpace H] [Nontrivial H] 190 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 191 (n d : ℕ) (v : Fin d → rootCornerSubspace rho n) 192 (U : rootCornerSubspace rho n ≃ₗᵢ[ℂ] rootCornerSubspace rho n) 193 (hU : ∀ x, U (U x) = x) : 194 ∃ (h : selfAdjoint Limit) 195 (heh : limitMatrixUnit n 0 0 * (h : Limit) = h) 196 (hhe : (h : Limit) * limitMatrixUnit n 0 0 = h), 197 ∀ i, rho (liftedCornerExponential n h heh hhe : Limit) (v i : H) = 198 (U (v i) : H) := by 199 obtain ⟨h, heh, hhe, hcorner⟩ := 200 exists_rootCornerSupported_exponential_apply_eq_involution 201 rho hrho n d v U hU 202 refine ⟨h, heh, hhe, fun i => ?_⟩ 203 rw [representation_liftedCornerExponential_apply_of_root 204 rho n h heh hhe (v i) ?_] 205 · exact hcorner i 206 · exact (LinearMap.IsIdempotentElem.mem_range_iff 207 (ContinuousLinearMap.IsIdempotentElem.toLinearMap 208 ((isStarProjection_limitMatrixUnit_zero_zero n).map rho).isIdempotentElem)).mp 209 (v i).property 210 211end MathlibAnnex.CStarAlgebra.CAR