OAI/Topology/CoarseAssembly/ControlledBoundaryClass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The K₁ boundary representative of a controlled Fredholm operator

The operator, its self-adjointness, and its Roe square defect are concrete data. Localization of arbitrary Fredholm cycles and descent through their relations are separate obligations of the assembly construction.

  1. def OAI.CoarseAssembly.DiscreteRoe.unitalRoeIdeal line 29
  2. theorem OAI.CoarseAssembly.DiscreteRoe.mem_unitalRoeIdeal line 37
  3. def OAI.CoarseAssembly.DiscreteRoe.controlledBoundaryUnitary line 41
  4. theorem OAI.CoarseAssembly.DiscreteRoe.controlledBoundaryUnitary_sub_one_mem line 47
  5. def OAI.CoarseAssembly.DiscreteRoe.controlledBoundaryClass line 60

    Source documentation

    An actual class of the reduced locally compact Roe algebra.

    def controlledBoundaryClass
    (F : unitalStructureAlgebra (X := X) (H := H)) (hF : IsSelfAdjoint F)
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.unitalStructureAlgebra

  6. theorem OAI.CoarseAssembly.DiscreteRoe.controlledBoundaryClass_of_involution line 68