Exact source: MathlibAnnex/Analysis/CStarAlgebra/AtomicConstruction/GeneratedExt.lean
Pinned GitHub source · Raw UTF-8 source
Back to The unique trace extension is tracial on the whole target
1import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.GeneratedReduction2import Mathlib.Analysis.InnerProductSpace.Adjoint34/-!5# Extensionality for an actual norm-closed generated algebra67These lemmas use the defining norm closure only. They introduce no universal8completion and no claim that finite relations determine an operator norm.9-/1011set_option autoImplicit false1213open Topology14open scoped CStarAlgebra1516namespace MathlibAnnex.CStarAlgebra.AtomicConstruction1718open MathlibAnnex.Analysis.CStarAlgebra1920universe u v w z21variable {A : Type u} [CStarAlgebra A]22variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]23variable {J : Type w}2425/-- A closed star subalgebra containing the actual source and added generators26is the whole concrete target. -/27theorem eq_top_of_source_mem_of_generator_mem28 (π : 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 = ⊤ := by33 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 := by37 induction hx using StarAlgebra.adjoin_induction with38 | mem x hx =>39 rcases hx with ⟨a, rfl⟩ | ⟨i, rfl⟩40 · exact hsource a41 · exact hgenerator i42 | algebraMap c => exact C.algebraMap_mem c43 | add x y hx hy hxc hyc => exact C.add_mem hxc hyc44 | mul x y hx hy hxc hyc => exact C.mul_mem hxc hyc45 | star x hx hxc =>46 change star (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ :47 concreteTarget π U) ∈ C48 exact star_mem hxc49 let inclusion : B →⋆ₐ[ℂ] concreteTarget π U :=50 StarSubalgebra.inclusion (StarSubalgebra.le_topologicalClosure B)51 have hdense : DenseRange inclusion := by52 change DenseRange (Set.inclusion (StarSubalgebra.le_topologicalClosure B))53 apply (denseRange_inclusion_iff _).254 change closure (B : Set (H →L[ℂ] H)) ⊆ closure (B : Set (H →L[ℂ] H))55 exact le_rfl56 apply top_unique57 intro x _58 have hrange : Set.range inclusion ⊆ (C : Set (concreteTarget π U)) := by59 rintro _ ⟨b, rfl⟩60 exact hlift b b.property61 apply closure_minimal hrange hC62 rw [hdense.closure_range]63 exact Set.mem_univ x6465/-- Two continuous star homomorphisms out of the same concrete target agree66if 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 := by72 let C : StarSubalgebra ℂ (concreteTarget π U) := StarAlgHom.equalizer f g73 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 hgenerator77 ext a78 have ha : a ∈ C := by rw [htop]; trivial79 exact ha8081/-- Intertwining two arbitrary representations, rather than requiring one of82them to be the concrete ambient inclusion. -/83theorem intertwines_of_source_of_generators84 {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) := by94 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 := by98 ext y99 have h := congrArg (fun T : K →L[ℂ] L ↦ T (e.symm y)) ha100 simpa [f, ContinuousLinearMap.comp_apply] using h101 have hfg : f = σ := starAlgHom_ext π U f σ102 (fun b ↦ hconj _ (hsource b)) (fun i ↦ hconj _ (hgenerator i))103 intro a104 ext x105 have h := congrArg (fun p : concreteTarget π U →⋆ₐ[ℂ] (L →L[ℂ] L) ↦106 p a (e x)) hfg107 simpa [f, ContinuousLinearMap.comp_apply] using h108109end MathlibAnnex.CStarAlgebra.AtomicConstruction