OAI/Analysis/PureInfiniteness/ConnectedUnitaryLift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Connected lifts of connected unitaries, retaining the component of the identity needed when a central buffer is realized in a norm ultrapower.

  1. theorem OAI.CStarConnectedLift.connected_unitary_lift line 14

    Source documentation

    The exponential-product lift stays in the identity path component.

    theorem connected_unitary_lift (q : C →⋆ₐ[ℂ] D) (hq : Function.Surjective q)
    (u : unitary D) (hu : Joined 1 u) :
    ∃ v : unitary C, Joined 1 v ∧ Unitary.map (starMonoidHom q) v = u := by
…

    Mentions: OAI.CStarConnectedLift.starMonoidHom