ConnectedUltrapowerLift.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A connected unitary in the norm ultrapower has representatives joined to the identity in every coordinate. The lift uses the actual quotient map.

theorem OAI.WeakPureInfiniteness.connected_ultrapower_unitary_representative line 17

Source documentation

The coordinate representatives preserve the identity path component.

theorem connected_ultrapower_unitary_representative (U : Ultrafilter ℕ)
    (u : unitary (QuotientAlgebra (fun _ : ℕ => A) U)) (hu : Joined 1 u) :
    ∃ v : ℕ → unitary A, (∀ n, Joined 1 (v n)) ∧
      mk U (boundedUnitary v) = (u : QuotientAlgebra (fun _ : ℕ => A) U) := by
…

theorem OAI.WeakPureInfiniteness.connected_finite_conjugacy_of_ultrapower line 53

Source documentation

A finite family of strict conjugacy estimates descends to one connected coordinate unitary.

theorem connected_finite_conjugacy_of_ultrapower (U : Ultrafilter ℕ)
    (F : Finset (A × A)) {ε : ℝ}
    (u : unitary (QuotientAlgebra (fun _ : ℕ => A) U)) (hu : Joined 1 u)
    (he : ∀ p ∈ F,
      ‖(u : QuotientAlgebra (fun _ : ℕ => A) U) * diagonalHom U p.1 *
        star (u : QuotientAlgebra (fun _ : ℕ => A) U) - diagonalHom U p.2‖ < ε) :
    ∃ v : unitary A, Joined 1 v ∧
      ∀ p ∈ F, ‖(v : A) * p.1 * star (v : A) - p.2‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.diagonalHom