OAI/Topology/CoarseAssembly/RipsBoundaryRepresentative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual boundary representative on a finite Rips component

This constructs the component operator and Roe K₁ class. No inference from componentwise classes to the whole coarse disjoint union is made here.

  1. def OAI.CoarseAssembly.Rips.ripsMultiplier line 22
  2. theorem OAI.CoarseAssembly.Rips.ripsMultiplier_selfAdjoint line 28
  3. theorem OAI.CoarseAssembly.Rips.ripsSpatialOperator_square_mem_roe line 34
  4. def OAI.CoarseAssembly.Rips.ripsBoundaryRepresentative line 46

    Source documentation

    The constructed boundary element, before passage to the fixed ample module and before descent of the entire assembly homomorphism.

    def ripsBoundaryRepresentative (c : OddCycle C(Point X r, ℂ))
    (hπ : c.representation 1 = 1) (hF : IsSelfAdjoint c.operator) :
    OperatorKTheory.K1 (algebra (X := X) (H := c.space)) :=
…

    Mentions: OAI.CoarseAssembly.Rips.Point, OAI.CoarseAssembly.OperatorKTheory.K1