OAI/Analysis/OInfinity/Simple.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Simplicity of O∞ from finite vacuum corners

A nonzero Fock coefficient becomes a nonzero vacuum coefficient after a word sandwich. Compressing a polynomial by an unused generator gives exactly that vacuum coefficient times the unit. Polynomial approximation therefore puts an invertible element in every nonzero two-sided ideal.

  1. lemma OAI.WeakPureInfiniteness.norm_complex_smul_one line 27
  2. lemma OAI.WeakPureInfiniteness.norm_contraction_sandwich line 31
  3. def OAI.WeakPureInfiniteness.fockVacuumCoefficient line 43
  4. lemma OAI.WeakPureInfiniteness.fockVacuumCoefficient_sub line 46
  5. lemma OAI.WeakPureInfiniteness.fockVacuumCoefficient_norm_le line 50
  6. lemma OAI.WeakPureInfiniteness.finiteFockAlgebraWord_fock line 60
  7. lemma OAI.WeakPureInfiniteness.fockVacuumCoefficient_word_sandwich line 64
  8. lemma OAI.WeakPureInfiniteness.exists_fock_coefficient_ne_zero line 77
  9. lemma OAI.WeakPureInfiniteness.unusedGenerator_polynomial line 92
  10. lemma OAI.WeakPureInfiniteness.oInfinityIsometry_norm_le_one line 105
  11. lemma OAI.WeakPureInfiniteness.unusedGenerator_error line 110
  12. lemma OAI.WeakPureInfiniteness.twoSidedIdeal_eq_top_of_vacuumCoefficient_ne_zero line 135
  13. theorem OAI.WeakPureInfiniteness.oInfinity_twoSidedIdeal_trivial line 167

    Source documentation

    Every nonzero two-sided ideal of O∞ contains a unit.

    theorem oInfinity_twoSidedIdeal_trivial (I : TwoSidedIdeal OInfinity) : I = ⊥ ∨ I = ⊤ := by
…

    Mentions: OAI.WeakPureInfiniteness.OInfinity

  14. theorem OAI.WeakPureInfiniteness.oInfinity_topologicallySimple line 184