OAI/Analysis/PureInfiniteness/NonunitalContractionLift.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact contraction lifting for a surjective nonunital star homomorphism. Unitization reduces this to the unital contraction lift; the scalar coordinate of the lifted element is zero.

  1. def OAI.WeakPureInfiniteness.unitizedHom line 17
  2. lemma OAI.WeakPureInfiniteness.unitizedHom_coordinates line 20
  3. lemma OAI.WeakPureInfiniteness.unitizedHom_surjective line 28
  4. theorem OAI.WeakPureInfiniteness.nonunital_exists_contraction line 36