MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.Representation.isSimpleCStarAlgebra_of_singleton_of_injective

Raw UTF-8 source

theorem isSimpleCStarAlgebra_of_singleton_of_injective [Nontrivial A]
    (pi : Representation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
    (hinj : Function.Injective pi) : IsSimpleCStarAlgebra A

1 import MathlibAnnex.Analysis.CStarAlgebra.State.Ideal
2 
3 /-!
4 # A single unitary-equivalence class of irreducible representations
5 -/
6 
7 set_option autoImplicit false
8 
9 open scoped ComplexOrder
10 
11 namespace MathlibAnnex.Analysis.CStarAlgebra
12 
13 universe u v w
14 
15 variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
16 variable {H : Type v}
17 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
18 
19 namespace Representation
20 
21 /-- The represented irreducible is a model for every irreducible
22 representation.  Faithfulness is deliberately not part of this predicate. -/
23 def IsSingletonIrreducibleModel (pi : Representation A H) : Prop :=
24   pi.IsIrreducible ∧
25     ∀ (K : Type w) [NormedAddCommGroup K] [InnerProductSpace ℂ K]
26       [CompleteSpace K] (rho : Representation A K),
27       rho.IsIrreducible → pi.UnitaryEquivalent rho
28 
29 /-- Once faithfulness has been proved separately, a singleton irreducible
30 model forces closed-two-sided-ideal simplicity. -/
31 theorem isSimpleCStarAlgebra_of_singleton_of_injective [Nontrivial A]
32     (pi : Representation A H)
33     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
34     (hinj : Function.Injective pi) : IsSimpleCStarAlgebra A := by
35   refine ⟨inferInstance, ?_⟩
36   intro I hclosed
37   by_cases hI : I = ⊤
38   · exact Or.inr hI
39   · left
40     apply le_antisymm
41     · intro x hx
42       obtain ⟨phi, hphi, _hpure, hirr, hann⟩ :=
43         exists_irreducibleGNS_annihilating I hI hclosed
44       let f : A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace phi hphi
45       obtain ⟨U, hU⟩ := hsingle.2 f.GNS f.gnsStarAlgHom hirr
46       have hpi : pi x = 0 := by
47         apply ContinuousLinearMap.ext
48         intro y
49         apply U.injective
50         calc
51           U (pi x y) = f.gnsStarAlgHom x (U y) := hU x y
52           _ = 0 := by rw [hann x hx]; rfl
53           _ = U 0 := (map_zero U).symm
54       exact hinj (by simpa using hpi)
55     · exact bot_le
56 
57 end Representation
58 
59 end MathlibAnnex.Analysis.CStarAlgebra