Exact source: MathlibAnnex/Analysis/CStarAlgebra/AtomicConstruction/Concrete.lean
Pinned GitHub source · Raw UTF-8 source
Back to The closed operator algebra generated by a representation and extra operators · Back to An irreducible operator algebra constructed from projection shells · Back to The ambient inclusion of the fixed shell-family target
1import MathlibAnnex.Analysis.CStarAlgebra.Generated23/-!4The concrete target generated inside an already existing bounded-operator5algebra. This introduces no universal completion.6-/78set_option autoImplicit false910namespace MathlibAnnex.CStarAlgebra.AtomicConstruction1112universe u v w1314variable {A : Type u} [Semiring A] [Algebra ℂ A] [StarRing A]15variable {H : Type v}16variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]17variable {J : Type w}1819open MathlibAnnex.Analysis.CStarAlgebra2021/-- The norm-closed star algebra generated by a displayed source22representation 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)2627/-- The generated concrete target carries its defining closedness as an28instance, hence inherits Mathlib's C*-algebra instance for closed star29subalgebras. -/30noncomputable instance concreteTarget.instIsClosed31 (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)3435/-- 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))4041@[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 rfl4647/-- Faithfulness of the concrete source inclusion is exactly faithfulness of48the 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) := by52 intro a b hab53 apply hpi54 exact congrArg Subtype.val hab5556/-- 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))⟩6061@[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 rfl6667/-- The concrete target's displayed representation is literal subtype68inclusion 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).subtype7374theorem ambientInclusion_injective (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))75 (U : J → H →L[ℂ] H) :76 Function.Injective (ambientInclusion pi U) :=77 Subtype.val_injective7879end MathlibAnnex.CStarAlgebra.AtomicConstruction