OAI/Topology/CoarseAssembly/ExplicitBoundaryRepresentative.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual Roe representative of the counterexample's boundary cycle

This constructs the index representative from the explicit circle Fredholm operator and the paper's hexagonal loops. Identification with the descended canonical coarse assembly map remains a separate theorem.

  1. def OAI.CoarseAssembly.circleRipsCycle line 21
  2. theorem OAI.CoarseAssembly.circleRipsCycle_unital line 24
  3. theorem OAI.CoarseAssembly.circleRipsCycle_selfAdjoint line 29
  4. theorem OAI.CoarseAssembly.circleRipsCycle_norm line 32
  5. def OAI.CoarseAssembly.explicitBoundaryCycle line 49
  6. def OAI.CoarseAssembly.explicitBoundaryFamilyRepresentative line 52
  7. def OAI.CoarseAssembly.boundaryReindexRoeHom line 59
  8. def OAI.CoarseAssembly.explicitBoundaryRoeRepresentative line 66

    Source documentation

    A concrete class in the same reduced Roe algebra used by the conditional assembly diagram. Canonical assembly identification is not presumed here.

    def explicitBoundaryRoeRepresentative : OperatorKTheory.K1 BoundaryRoe :=
…

    Mentions: OAI.CoarseAssembly.OperatorKTheory.K1, OAI.CoarseAssembly.BoundaryRoe

  9. def OAI.CoarseAssembly.explicitBaseRoeRepresentative line 69
  10. def OAI.CoarseAssembly.explicitTotalRoeRepresentative line 72
  11. theorem OAI.CoarseAssembly.explicitRoeRepresentative_transfer line 77

    Source documentation

    The constructed representative satisfies the previously proved spatial transfer identity. Its base vanishing still requires the assembly descent.

    theorem explicitRoeRepresentative_transfer (hgap : PublishedKazhdanInput) :
    OperatorKTheory.map (transferRoeHom hgap) explicitBaseRoeRepresentative =
      explicitTotalRoeRepresentative :=
…

    Mentions: OAI.CoarseAssembly.PublishedKazhdanInput, OAI.CoarseAssembly.OperatorKTheory.map, OAI.CoarseAssembly.transferRoeHom, OAI.CoarseAssembly.explicitBaseRoeRepresentative, OAI.CoarseAssembly.explicitTotalRoeRepresentative