Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/InvolutionLift.lean
Pinned GitHub source · Raw UTF-8 source
Back to Lifting a corner involution to an ambient CAR unitary
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CornerLift2import MathlibAnnex.Analysis.CStarAlgebra.CAR.StagePurification3import MathlibAnnex.Analysis.CStarAlgebra.SmallUnitary4import MathlibAnnex.Analysis.CStarAlgebra.Representation.Adapters5import MathlibAnnex.Analysis.InnerProductSpace.InvolutionExponential67set_option autoImplicit false89noncomputable section1011open NormedSpace12open scoped CStarAlgebra13open MathlibAnnex.Analysis.CStarAlgebra14open MathlibAnnex.Analysis.InnerProductSpace1516namespace MathlibAnnex.CStarAlgebra.CAR1718abbrev rootCornerSubspace19 {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)).toLinearMap2324theorem representation_liftedCornerExponential_apply_of_root25 {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 := by33 let z := cornerExponential n h34 have hz := isRootCornerUnitary_cornerExponential n h heh hhe35 change rho (cornerLift n z) x = rho z x36 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 _ hi43 have h0i : rho (limitMatrixUnit n 0 i) x = 0 := by44 rw [← hx, ← mul_apply_eq_comp, ← map_mul]45 simp [hi]46 simp [h0i]47 · simp4849set_option maxHeartbeats 800000 in50theorem exists_rootCornerSupported_exponential_apply_eq_involution51 {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) := by61 let e : Limit := limitMatrixUnit n 0 062 let K : Submodule ℂ H := rootCornerSubspace rho n63 have hroot : IsStarProjection (rho e) := by64 exact (isStarProjection_limitMatrixUnit_zero_zero n).map rho65 letI : CompleteSpace K := IsComplete.completeSpace_coe66 (ContinuousLinearMap.IsIdempotentElem.isClosed_range67 hroot.isIdempotentElem).isComplete68 have hKnot : ¬ FiniteDimensional ℂ K := by69 simpa [K, e, rootCornerSubspace] using70 not_finiteDimensional_range_rootCorner rho71 ((MathlibAnnex.Analysis.CStarAlgebra.Representation.isIrreducible_iff_starAlgHom rho).mpr72 hrho) n73 letI : Nontrivial K := by74 rw [← not_subsingleton_iff_nontrivial]75 intro hsub76 apply hKnot77 letI : Subsingleton K := hsub78 exact FiniteDimensional.of_rank_eq_zero (rank_subsingleton' ℂ K)79 letI : NormedRing (K →L[ℂ] K) := ContinuousLinearMap.toNormedRing80 letI : K.HasOrthogonalProjection := by81 simpa [K] using82 (ContinuousLinearMap.IsIdempotentElem.hasOrthogonalProjection_range83 hroot.isIdempotentElem)84 let P : K →L[ℂ] K := U.involutionProjection85 have hPstar : IsStarProjection P := U.isStarProjection_involutionProjection hU86 let PH : H →L[ℂ] H :=87 MathlibAnnex.Analysis.CStarAlgebra.zeroExtension K P88 let T : H →L[ℂ] H := (Real.pi : ℂ) • PH89 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 ℂ S92 letI : FiniteDimensional ℂ E :=93 FiniteDimensional.span_of_finite ℂ94 ((Set.finite_range fun i => (v i : H)).union95 (Set.finite_range fun i => (U (v i) : H)))96 letI : E.HasOrthogonalProjection := inferInstance97 have hKfix (x : K) : rho e (x : H) = (x : H) := by98 exact (LinearMap.IsIdempotentElem.mem_range_iff99 (ContinuousLinearMap.IsIdempotentElem.toLinearMap100 hroot.isIdempotentElem)).mp x.property101 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 := by106 intro x hx107 refine Submodule.span_induction108 (p := fun x _ => rho e x = x) ?_ (by simp) ?_ ?_ hx109 · intro x hx110 rcases hx with hx | hx111 · obtain ⟨i, rfl⟩ := hx112 exact hKfix (v i)113 · obtain ⟨i, rfl⟩ := hx114 exact hKfix (U (v i))115 · intro x y _ _ hx hy116 simpa using congrArg₂ (· + ·) hx hy117 · intro c x _ hx118 simpa using congrArg (fun y => c • y) hx119 have hPHself : IsSelfAdjoint PH :=120 MathlibAnnex.Analysis.CStarAlgebra.isSelfAdjoint_zeroExtension121 K P hPstar.isSelfAdjoint122 have hTself : IsSelfAdjoint T := by123 dsimp only [T]124 rw [isSelfAdjoint_iff, star_smul, hPHself.star_eq]125 simp126 have hTroot : rho e * T = T := by127 apply ContinuousLinearMap.ext128 intro x129 change rho e (T x) = T x130 exact hKfix ⟨T x, by131 dsimp only [T]132 rw [ContinuousLinearMap.smul_apply]133 apply K.smul_mem134 dsimp [PH, MathlibAnnex.Analysis.CStarAlgebra.zeroExtension]135 exact (P (K.orthogonalProjectionOnto x)).property⟩136 have hTmap : Set.MapsTo T E E := by137 intro x hx138 refine Submodule.span_induction139 (p := fun x _ => T x ∈ E) ?_ (by simp [T]) ?_ ?_ hx140 · intro x hx141 rcases hx with hx | hx142 · obtain ⟨i, rfl⟩ := hx143 rw [show T (v i : H) =144 (Real.pi : ℂ) • ((2 : ℂ)⁻¹ •145 ((v i : H) - (U (v i) : H))) by146 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⟩ := hx152 rw [show T (U (v i) : H) =153 (Real.pi : ℂ) • ((2 : ℂ)⁻¹ •154 ((U (v i) : H) - (v i : H))) by155 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 hy161 simpa using E.add_mem hx hy162 · intro c x _ hx163 simpa using E.smul_mem c hx164 obtain ⟨h, -, heh, hhe, hexp⟩ :=165 exists_rootCornerSupported_exponential_eq_on166 rho hrho n E hEroot T hTself hTroot hTmap167 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 := by171 dsimp only [T]172 module173 rw [hsmul]174 have hzero : ((Real.pi : ℂ) * Complex.I) • PH =175 MathlibAnnex.Analysis.CStarAlgebra.zeroExtension K176 (((Real.pi : ℂ) * Complex.I) • P) := by177 ext x178 simp [PH, MathlibAnnex.Analysis.CStarAlgebra.zeroExtension, smul_smul]179 rw [hzero, MathlibAnnex.Analysis.CStarAlgebra.exp_zeroExtension_apply180 K (((Real.pi : ℂ) * Complex.I) • P) (v i)]181 exact congrArg Subtype.val182 (MathlibAnnex.Analysis.InnerProductSpace.exp_pi_mul_involutionProjection_apply183 U hU (v i))184185/-- The ambient unitary obtained by amplifying the same corner exponential186acts as the prescribed involution on the selected root-corner family. -/187theorem exists_liftedCornerExponential_apply_eq_involution188 {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) := by199 obtain ⟨h, heh, hhe, hcorner⟩ :=200 exists_rootCornerSupported_exponential_apply_eq_involution201 rho hrho n d v U hU202 refine ⟨h, heh, hhe, fun i => ?_⟩203 rw [representation_liftedCornerExponential_apply_of_root204 rho n h heh hhe (v i) ?_]205 · exact hcorner i206 · exact (LinearMap.IsIdempotentElem.mem_range_iff207 (ContinuousLinearMap.IsIdempotentElem.toLinearMap208 ((isStarProjection_limitMatrixUnit_zero_zero n).map rho).isIdempotentElem)).mp209 (v i).property210211end MathlibAnnex.CStarAlgebra.CAR