OAI/Topology/CoarseAssembly/MultiplierIsometryInvariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The Roe boundary is invariant under multiplier isometries

  1. theorem OAI.CoarseAssembly.Analytic.nonunitalIdentityExtension_square_defect line 15
  2. def OAI.CoarseAssembly.DiscreteRoe.isometricMultiplier line 33
  3. theorem OAI.CoarseAssembly.DiscreteRoe.isometricMultiplier_selfAdjoint line 38
  4. theorem OAI.CoarseAssembly.DiscreteRoe.isometricMultiplier_defect_mem line 43
  5. theorem OAI.CoarseAssembly.DiscreteRoe.rationalBoundaryUnitary_isometricMultiplier line 54
  6. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryClass_isometry line 65

    Source documentation

    Stabilizing a multiplier by an isometry does not change its actual Roe K₁ boundary.

    theorem multiplierBoundaryClass_isometry
    (V : multiplierAlgebra (X := X) (H := H)) (hV : star V * V = 1)
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.multiplierAlgebra

  7. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryClass_unitaryConjugation line 84

    Source documentation

    Arbitrary multiplier unitaries preserve the boundary; no path is assumed.

    theorem multiplierBoundaryClass_unitaryConjugation
    (u : unitary (multiplierAlgebra (X := X) (H := H)))
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.multiplierAlgebra