OAI/Analysis/PureInfiniteness/AbsorptionFromQuotientNuclearity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Absorption from quotient nuclearity and a connected approximate half-flip. The represented left algebra is a quotient of the unitized nuclear source. Nuclearity of this quotient follows from Choi–Effros, Duke Math. J. 43 (1976), Corollary 3.3, and permanence under unitization.

  1. def OAI.WeakPureInfiniteness.UnitizedFactorImageNuclear line 22
  2. theorem OAI.WeakPureInfiniteness.elementary_generation_from_factor_images line 30
  3. theorem OAI.WeakPureInfiniteness.Campaign.nuclear_absorption_from_quotient_nuclearity_and_halfFlip line 48