RelativeIsometry.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Isometric stabilization preserves the actual relative K₁ class

theorem OAI.CoarseAssembly.OperatorKTheory.isometryExtensionUnitary_relative line 18

theorem OAI.CoarseAssembly.OperatorKTheory.relativeClass_isometry line 28

Source documentation

The dilation homotopy proves equality in K₁, not just equality in a quotient of operators.

theorem relativeClass_isometry (φ : A →⋆ₐ[ℂ] R) (hφc : Continuous φ)
    (hφ : ∀ a b, b ∈ S → φ a * b ∈ S ∧ b * φ a ∈ S)
    (V : A) (hV : star V * V = 1) (u : unitary A)
    (hu : φ (u : A) - 1 ∈ S) :
    relativeClass S (Unitary.map (StarMonoidHom.ofClass φ) u) hu =
      relativeClass S (Unitary.map (StarMonoidHom.ofClass φ) (isometryExtensionUnitary V hV u))
        (isometryExtensionUnitary_relative S φ hφ V hV u hu) := by
…

Mentions: OAI.CoarseAssembly.OperatorKTheory.relativeClass, OAI.CoarseAssembly.OperatorKTheory.isometryExtensionUnitary_relative