MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget

Exact source: MathlibAnnex/Analysis/CStarAlgebra/AtomicConstruction/Concrete.lean, lines 21–25.

Raw UTF-8 source

Back to An irreducible operator algebra constructed from projection shells · 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