Exact source: MathlibAnnex/Analysis/CStarAlgebra/AtomicConstruction/GeneratedExt.lean, lines 83–107.
Back to Pointed unitary transport between trace-cyclic target representations
1import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.GeneratedReduction 2import Mathlib.Analysis.InnerProductSpace.Adjoint 3 4/-! 5# Extensionality for an actual norm-closed generated algebra 6 7These lemmas use the defining norm closure only. They introduce no universal 8completion and no claim that finite relations determine an operator norm. 9-/ 10 11set_option autoImplicit false 12 13open Topology 14open scoped CStarAlgebra 15 16namespace MathlibAnnex.CStarAlgebra.AtomicConstruction 17 18open MathlibAnnex.Analysis.CStarAlgebra 19 20universe u v w z 21variable {A : Type u} [CStarAlgebra A] 22variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 23variable {J : Type w} 24 25/-- A closed star subalgebra containing the actual source and added generators 26is the whole concrete target. -/ 27theorem eq_top_of_source_mem_of_generator_mem 28 (π : Representation A H) (U : J → H →L[ℂ] H) 29 (C : StarSubalgebra ℂ (concreteTarget π U)) 30 (hC : IsClosed (C : Set (concreteTarget π U))) 31 (hsource : ∀ a, sourceHom π U a ∈ C) 32 (hgenerator : ∀ i, generator π U i ∈ C) : C = ⊤ := by 33 let B : StarSubalgebra ℂ (H →L[ℂ] H) := 34 StarAlgebra.adjoin ℂ (Set.range π ∪ Set.range U) 35 have hlift (x : H →L[ℂ] H) (hx : x ∈ B) : 36 (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : concreteTarget π U) ∈ C := by 37 induction hx using StarAlgebra.adjoin_induction with 38 | mem x hx => 39 rcases hx with ⟨a, rfl⟩ | ⟨i, rfl⟩ 40 · exact hsource a 41 · exact hgenerator i 42 | algebraMap c => exact C.algebraMap_mem c 43 | add x y hx hy hxc hyc => exact C.add_mem hxc hyc 44 | mul x y hx hy hxc hyc => exact C.mul_mem hxc hyc 45 | star x hx hxc => 46 change star (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 47 concreteTarget π U) ∈ C 48 exact star_mem hxc 49 let inclusion : B →⋆ₐ[ℂ] concreteTarget π U := 50 StarSubalgebra.inclusion (StarSubalgebra.le_topologicalClosure B) 51 have hdense : DenseRange inclusion := by 52 change DenseRange (Set.inclusion (StarSubalgebra.le_topologicalClosure B)) 53 apply (denseRange_inclusion_iff _).2 54 change closure (B : Set (H →L[ℂ] H)) ⊆ closure (B : Set (H →L[ℂ] H)) 55 exact le_rfl 56 apply top_unique 57 intro x _ 58 have hrange : Set.range inclusion ⊆ (C : Set (concreteTarget π U)) := by 59 rintro _ ⟨b, rfl⟩ 60 exact hlift b b.property 61 apply closure_minimal hrange hC 62 rw [hdense.closure_range] 63 exact Set.mem_univ x 64 65/-- Two continuous star homomorphisms out of the same concrete target agree 66if they agree on its displayed generators. -/ 67theorem starAlgHom_ext {D : Type z} [CStarAlgebra D] 68 (π : Representation A H) (U : J → H →L[ℂ] H) 69 (f g : concreteTarget π U →⋆ₐ[ℂ] D) 70 (hsource : ∀ a, f (sourceHom π U a) = g (sourceHom π U a)) 71 (hgenerator : ∀ i, f (generator π U i) = g (generator π U i)) : f = g := by 72 let C : StarSubalgebra ℂ (concreteTarget π U) := StarAlgHom.equalizer f g 73 have hclosed : IsClosed (C : Set (concreteTarget π U)) := 74 isClosed_eq (map_continuous f) (map_continuous g) 75 have htop : C = ⊤ := 76 eq_top_of_source_mem_of_generator_mem π U C hclosed hsource hgenerator 77 ext a 78 have ha : a ∈ C := by rw [htop]; trivial 79 exact ha 80 81/-- Intertwining two arbitrary representations, rather than requiring one of 82them to be the concrete ambient inclusion. -/ 83theorem intertwines_of_source_of_generators 84 {K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 85 {L : Type*} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L] 86 (π : Representation A H) (U : J → H →L[ℂ] H) 87 (ρ : Representation (concreteTarget π U) K) 88 (σ : Representation (concreteTarget π U) L) (e : K ≃ₗᵢ[ℂ] L) 89 (hsource : ∀ a, (e : K →L[ℂ] L).comp (ρ (sourceHom π U a)) = 90 (σ (sourceHom π U a)).comp (e : K →L[ℂ] L)) 91 (hgenerator : ∀ i, (e : K →L[ℂ] L).comp (ρ (generator π U i)) = 92 (σ (generator π U i)).comp (e : K →L[ℂ] L)) : 93 ∀ a, (e : K →L[ℂ] L).comp (ρ a) = (σ a).comp (e : K →L[ℂ] L) := by 94 let f := e.conjStarAlgEquiv.toStarAlgHom.comp ρ 95 have hconj (a : concreteTarget π U) 96 (ha : (e : K →L[ℂ] L).comp (ρ a) = (σ a).comp (e : K →L[ℂ] L)) : 97 f a = σ a := by 98 ext y 99 have h := congrArg (fun T : K →L[ℂ] L ↦ T (e.symm y)) ha 100 simpa [f, ContinuousLinearMap.comp_apply] using h 101 have hfg : f = σ := starAlgHom_ext π U f σ 102 (fun b ↦ hconj _ (hsource b)) (fun i ↦ hconj _ (hgenerator i)) 103 intro a 104 ext x 105 have h := congrArg (fun p : concreteTarget π U →⋆ₐ[ℂ] (L →L[ℂ] L) ↦ 106 p a (e x)) hfg 107 simpa [f, ContinuousLinearMap.comp_apply] using h 108 109end MathlibAnnex.CStarAlgebra.AtomicConstruction