OAI/Analysis/PureInfiniteness/FiniteJointSubalgebra.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The commutative unital algebra generated by a finite commuting family in its unitization. The augmentation character records membership in the original nonunital algebra.

  1. def OAI.WeakPureInfiniteness.jointSpectralAlgebra line 16
  2. instance OAI.WeakPureInfiniteness.jointSpectralAlgebra_closed line 19
  3. def OAI.WeakPureInfiniteness.jointSpectralGenerator line 23
  4. lemma OAI.WeakPureInfiniteness.jointSpectralGenerator_selfAdjoint line 27
  5. lemma OAI.WeakPureInfiniteness.jointSpectralAlgebra_commutative line 32
  6. def OAI.WeakPureInfiniteness.unitizationAugmentation line 50
  7. def OAI.WeakPureInfiniteness.jointSpectralAugmentation line 53
  8. lemma OAI.WeakPureInfiniteness.jointSpectralAugmentation_generator line 56
  9. lemma OAI.WeakPureInfiniteness.jointSpectralAugmentation_zero_iff line 59
  10. def OAI.WeakPureInfiniteness.jointOriginalElement line 74

    Source documentation

    The original-algebra coordinate; the augmentation-zero hypothesis below is what makes its inclusion equal to the original element.

    def jointOriginalElement (a : I → A) (x : jointSpectralAlgebra a) : A :=
…

    Mentions: OAI.WeakPureInfiniteness.jointSpectralAlgebra

  11. lemma OAI.WeakPureInfiniteness.jointOriginalElement_inr line 77
  12. lemma OAI.WeakPureInfiniteness.jointOriginalElement_norm line 84
  13. lemma OAI.WeakPureInfiniteness.jointSpectralGenerator_nonneg line 94
  14. lemma OAI.WeakPureInfiniteness.jointOriginalElement_nonneg line 99