import MathlibAnnex.Analysis.CStarAlgebra.Generated

/-!
The concrete target generated inside an already existing bounded-operator
algebra.  This introduces no universal completion.
-/

set_option autoImplicit false

namespace MathlibAnnex.CStarAlgebra.AtomicConstruction

universe u v w

variable {A : Type u} [Semiring A] [Algebra ℂ A] [StarRing A]
variable {H : Type v}
variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable {J : Type w}

open MathlibAnnex.Analysis.CStarAlgebra

/-- The norm-closed star algebra generated by a displayed source
representation and a family of additional bounded operators. -/
noncomputable def concreteTarget (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (U : J → H →L[ℂ] H) : StarSubalgebra ℂ (H →L[ℂ] H) :=
  generated (Set.range pi ∪ Set.range U)

/-- The generated concrete target carries its defining closedness as an
instance, hence inherits Mathlib's C*-algebra instance for closed star
subalgebras. -/
noncomputable instance concreteTarget.instIsClosed
    (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (U : J → H →L[ℂ] H) :
    IsClosed (concreteTarget pi U : Set (H →L[ℂ] H)) :=
  isClosed_generated (Set.range pi ∪ Set.range U)

/-- The represented source as a star homomorphism into the concrete target. -/
noncomputable def sourceHom (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (U : J → H →L[ℂ] H) : A →⋆ₐ[ℂ] concreteTarget pi U :=
  pi.codRestrict (concreteTarget pi U) fun a ↦
    subset_generated _ (Set.mem_union_left _ (Set.mem_range_self a))

@[simp]
theorem sourceHom_coe (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (U : J → H →L[ℂ] H) (a : A) :
    ((sourceHom pi U a : concreteTarget pi U) : H →L[ℂ] H) = pi a :=
  rfl

/-- Faithfulness of the concrete source inclusion is exactly faithfulness of
the displayed source representation; no target simplicity is used. -/
theorem sourceHom_injective (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (U : J → H →L[ℂ] H) (hpi : Function.Injective pi) :
    Function.Injective (sourceHom pi U) := by
  intro a b hab
  apply hpi
  exact congrArg Subtype.val hab

/-- Each additional nominated operator is an actual element of the target. -/
noncomputable def generator (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (U : J → H →L[ℂ] H) (j : J) : concreteTarget pi U :=
  ⟨U j, subset_generated _ (Set.mem_union_right _ (Set.mem_range_self j))⟩

@[simp]
theorem generator_coe (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (U : J → H →L[ℂ] H) (j : J) :
    ((generator pi U j : concreteTarget pi U) : H →L[ℂ] H) = U j :=
  rfl

/-- The concrete target's displayed representation is literal subtype
inclusion and is therefore faithful. -/
noncomputable def ambientInclusion (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (U : J → H →L[ℂ] H) :
    concreteTarget pi U →⋆ₐ[ℂ] (H →L[ℂ] H) :=
  (concreteTarget pi U).subtype

theorem ambientInclusion_injective (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (U : J → H →L[ℂ] H) :
    Function.Injective (ambientInclusion pi U) :=
  Subtype.val_injective

end MathlibAnnex.CStarAlgebra.AtomicConstruction