OAI/Analysis/KadisonKastler/MaximalClosedStarIdeal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A maximal proper closed star ideal in a unital C-star algebra

This supplies the quotient step in the unital specialization of Sakai's ideal-extension argument. The closure of a proper ideal remains proper: otherwise the original ideal meets the open set of invertible elements.

  1. theorem OAI.KadisonKastler.twoSidedIdeal_eq_top_of_isUnit_mem line 22
  2. theorem OAI.KadisonKastler.closedTwoSidedIdeal_ne_top line 28
  3. def OAI.KadisonKastler.idealChainUnion line 40
  4. theorem OAI.KadisonKastler.mem_idealChainUnion line 52
  5. theorem OAI.KadisonKastler.closedTwoSidedIdeal_star line 57
  6. theorem OAI.KadisonKastler.exists_maximal_proper_closedStarIdeal line 66
  7. theorem OAI.KadisonKastler.maximal_closedStarIdeal_quotient_injective line 108

    Source documentation

    Every unital representation of the maximal quotient is faithful. The preimage of its kernel is a closed star ideal, so maximality applies directly.

    theorem maximal_closedStarIdeal_quotient_injective
    (J : ClosedStarIdeal B)
    (hmax : ∀ K : ClosedStarIdeal B, K.ideal ≠ ⊤ →
      J.ideal ≤ K.ideal → K.ideal = J.ideal)
    {C : Type*} [CStarAlgebra C] [Nontrivial C]
    (ψ : J.Quotient →⋆ₐ[ℂ] C) : Function.Injective ψ := by
…