import Mathlib.Analysis.CStarAlgebra.GelfandDuality
import MathlibAnnex.Analysis.CStarAlgebra.Representation.Singleton
import MathlibAnnex.Analysis.CStarAlgebra.State.Extension

/-!
# Faithfulness from a singleton irreducible model

Pure states obtained by extending characters of singly generated commutative
C-star subalgebras separate the points of a unital C-star algebra.  Comparing
their irreducible GNS representations with a singleton irreducible model then
forces that model to be faithful.
-/

set_option autoImplicit false

open Set
open scoped ComplexOrder InnerProduct

namespace MathlibAnnex.Analysis.CStarAlgebra

universe u v

variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
variable {H : Type v}
variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

/-- Every nonzero element is detected, after forming `a⋆a`, by a pure state.
The construction uses only the commutative C-star algebra generated by
`a⋆a`, so no separability hypothesis on the ambient algebra is involved. -/
theorem exists_pureState_nonzero_on_star_mul_self [Nontrivial A]
    {a : A} (ha : a ≠ 0) :
    ∃ phi : A →L[ℂ] ℂ,
      phi ∈ stateSpace A ∧ IsPureState A phi ∧ phi (star a * a) ≠ 0 := by
  let b : A := star a * a
  have hb : b ≠ 0 := by
    simpa only [b, CStarRing.star_mul_self_ne_zero_iff] using ha
  letI : IsStarNormal b := (IsSelfAdjoint.star_mul_self a).isStarNormal
  have hbself : IsSelfAdjoint b := by
    simpa only [b] using IsSelfAdjoint.star_mul_self a
  let D : StarSubalgebra ℂ A := StarAlgebra.elemental ℂ b
  let bd : D := ⟨b, StarAlgebra.elemental.self_mem ℂ b⟩
  obtain ⟨z, hzmem, hzrad⟩ := spectrum.exists_nnnorm_eq_spectralRadius b
  have hz : z ≠ 0 := by
    intro hzero
    subst z
    have hnorm : ‖b‖₊ = 0 := by
      apply ENNReal.coe_injective
      change (↑‖b‖₊ : ENNReal) = (0 : ENNReal)
      rw [← hbself.spectralRadius_eq_nnnorm]
      simpa using hzrad.symm
    exact hb (nnnorm_eq_zero.mp hnorm)
  obtain ⟨chi, hchi⟩ :=
    (StarAlgebra.elemental.bijective_characterSpaceToSpectrum b).2
      (⟨z, hzmem⟩ : spectrum ℂ b)
  have hchi_ne : chi bd ≠ 0 := by
    have hvalue := congrArg Subtype.val hchi
    change chi bd = z at hvalue
    exact hvalue.symm ▸ hz
  letI : IsClosed (D : Set A) := StarAlgebra.elemental.isClosed ℂ b
  obtain ⟨phi, hphi, hpure, hext⟩ := exists_pureState_extension D chi
  refine ⟨phi, hphi, hpure, ?_⟩
  have hvalue := hext bd
  change phi b = chi bd at hvalue
  exact fun hzero => hchi_ne (hvalue ▸ hzero)

namespace Representation

/-- A unital representation representing the sole unitary-equivalence class
of nonzero irreducible representations is faithful. -/
theorem injective_of_singleton [Nontrivial A]
    (pi : Representation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    Function.Injective pi := by
  intro x y hxy
  let a : A := x - y
  have ha : pi a = 0 := by
    simp only [a, map_sub, hxy, sub_self]
  have hazero : a = 0 := by
    by_contra hane
    obtain ⟨phi, hphi, hpure, hdetect⟩ :=
      exists_pureState_nonzero_on_star_mul_self hane
    let f : A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace phi hphi
    let xi : f.GNS := f.gnsCyclicVector
    have hxi : ‖xi‖ = 1 :=
      PositiveLinearMap.norm_gnsCyclicVector f
        (positiveLinearMapOfMemStateSpace_one phi hphi)
    have hxi_ne : xi ≠ 0 := by
      intro hzero
      simp [hzero] at hxi
    letI : Nontrivial f.GNS := nontrivial_of_ne xi 0 hxi_ne
    have hirr : Representation.IsIrreducible f.gnsStarAlgHom :=
      (Representation.isIrreducible_iff_starAlgHom f.gnsStarAlgHom).2
        (isIrreducible_pureState_gnsStarAlgHom phi hphi hpure)
    obtain ⟨U, hU⟩ := hsingle.2 f.GNS f.gnsStarAlgHom hirr
    have hfa : f.gnsStarAlgHom a = 0 := by
      apply ContinuousLinearMap.ext
      intro z
      obtain ⟨q, rfl⟩ := U.surjective z
      calc
        f.gnsStarAlgHom a (U q) = U (pi a q) := (hU a q).symm
        _ = 0 := by rw [ha]; simp
    apply hdetect
    calc
      phi (star a * a) =
          inner ℂ xi (f.gnsStarAlgHom (star a * a) xi) :=
        (PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f _).symm
      _ = 0 := by rw [map_mul, map_star, hfa]; simp
  exact sub_eq_zero.mp hazero

end Representation

end MathlibAnnex.Analysis.CStarAlgebra