OAI/Topology/CoarseAssembly/RelativePartialIsometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CoarseAssembly.OperatorKTheory.partialIsometryDilation_conjugates_unitary line 16
2. theorem OAI.CoarseAssembly.OperatorKTheory.relativeClass_partialIsometry line 34

   Source documentation

   A partial isometry between supported defects gives equality in the original K₁.

   theorem relativeClass_partialIsometry (φ : A →⋆ₐ[ℂ] R) (hφc : Continuous φ)
       (hφ : ∀ a b, b ∈ S → φ a * b ∈ S ∧ b * φ a ∈ S)
       (T : A) (hT : T * star T * T = T) (u v : unitary A)
       (hleft : (star T * T) * ((u : A) - 1) = (u : A) - 1)
       (hright : ((u : A) - 1) * (star T * T) = (u : A) - 1)
       (hv : (v : A) = 1 + T * ((u : A) - 1) * star T)
       (huS : φ (u : A) - 1 ∈ S) (hvS : φ (v : A) - 1 ∈ S) :
       relativeClass S (Unitary.map (StarMonoidHom.ofClass φ) u) huS =
         relativeClass S (Unitary.map (StarMonoidHom.ofClass φ) v) hvS := by
   …

   Mentions: OAI.CoarseAssembly.OperatorKTheory.relativeClass