Exact source: MathlibAnnex/Analysis/CStarAlgebra/AtomicConstruction/Concrete.lean, lines 35–39.
Back to The CAR source map into the fixed shell-family target · Back to The closed operator algebra generated by a representation and extra operators
1import MathlibAnnex.Analysis.CStarAlgebra.Generated 2 3/-! 4The concrete target generated inside an already existing bounded-operator 5algebra. This introduces no universal completion. 6-/ 7 8set_option autoImplicit false 9 10namespace MathlibAnnex.CStarAlgebra.AtomicConstruction 11 12universe u v w 13 14variable {A : Type u} [Semiring A] [Algebra ℂ A] [StarRing A] 15variable {H : Type v} 16variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 17variable {J : Type w} 18 19open MathlibAnnex.Analysis.CStarAlgebra 20 21/-- The norm-closed star algebra generated by a displayed source 22representation and a family of additional bounded operators. -/ 23noncomputable def concreteTarget (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) 24 (U : J → H →L[ℂ] H) : StarSubalgebra ℂ (H →L[ℂ] H) := 25 generated (Set.range pi ∪ Set.range U) 26 27/-- The generated concrete target carries its defining closedness as an 28instance, hence inherits Mathlib's C*-algebra instance for closed star 29subalgebras. -/ 30noncomputable instance concreteTarget.instIsClosed 31 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (U : J → H →L[ℂ] H) : 32 IsClosed (concreteTarget pi U : Set (H →L[ℂ] H)) := 33 isClosed_generated (Set.range pi ∪ Set.range U) 34 35/-- The represented source as a star homomorphism into the concrete target. -/ 36noncomputable def sourceHom (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) 37 (U : J → H →L[ℂ] H) : A →⋆ₐ[ℂ] concreteTarget pi U := 38 pi.codRestrict (concreteTarget pi U) fun a ↦ 39 subset_generated _ (Set.mem_union_left _ (Set.mem_range_self a)) 40 41@[simp] 42theorem sourceHom_coe (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) 43 (U : J → H →L[ℂ] H) (a : A) : 44 ((sourceHom pi U a : concreteTarget pi U) : H →L[ℂ] H) = pi a := 45 rfl 46 47/-- Faithfulness of the concrete source inclusion is exactly faithfulness of 48the displayed source representation; no target simplicity is used. -/ 49theorem sourceHom_injective (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) 50 (U : J → H →L[ℂ] H) (hpi : Function.Injective pi) : 51 Function.Injective (sourceHom pi U) := by 52 intro a b hab 53 apply hpi 54 exact congrArg Subtype.val hab 55 56/-- Each additional nominated operator is an actual element of the target. -/ 57noncomputable def generator (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) 58 (U : J → H →L[ℂ] H) (j : J) : concreteTarget pi U := 59 ⟨U j, subset_generated _ (Set.mem_union_right _ (Set.mem_range_self j))⟩ 60 61@[simp] 62theorem generator_coe (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) 63 (U : J → H →L[ℂ] H) (j : J) : 64 ((generator pi U j : concreteTarget pi U) : H →L[ℂ] H) = U j := 65 rfl 66 67/-- The concrete target's displayed representation is literal subtype 68inclusion and is therefore faithful. -/ 69noncomputable def ambientInclusion (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) 70 (U : J → H →L[ℂ] H) : 71 concreteTarget pi U →⋆ₐ[ℂ] (H →L[ℂ] H) := 72 (concreteTarget pi U).subtype 73 74theorem ambientInclusion_injective (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) 75 (U : J → H →L[ℂ] H) : 76 Function.Injective (ambientInclusion pi U) := 77 Subtype.val_injective 78 79end MathlibAnnex.CStarAlgebra.AtomicConstruction