BoundaryAssemblyMaps.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The actual boundary assembly diagram

All three Roe maps below are constructed spatial homomorphisms on the ordinary reduced locally compact Roe algebras. The transfer factorization is proved before the two published assembly naturality equations are used.

def OAI.CoarseAssembly.BoundaryRoe line 27
def OAI.CoarseAssembly.BaseRoe line 28
instance OAI.CoarseAssembly.(instance at line 29) line 29
instance OAI.CoarseAssembly.(instance at line 31) line 31
def OAI.CoarseAssembly.boundaryBaseCoarsening line 33
def OAI.CoarseAssembly.boundaryTotalCoarsening line 38
def OAI.CoarseAssembly.boundaryBaseRoeHom line 43
def OAI.CoarseAssembly.boundaryTotalRoeHom line 47
def OAI.CoarseAssembly.transferRoeHom line 51
theorem OAI.CoarseAssembly.transferRoeHom_boundary line 55
theorem OAI.CoarseAssembly.transferK1_boundary line 65
structure OAI.CoarseAssembly.PublishedBoundaryAssemblyInput line 75
Source documentation
The exact published index/naturality specializations used here: Willett--Yu, Higher Index Theory (2020), §§5.1, 6.7, 7.1--7.2, with errata 30--31. The objects and both geometric/Roe maps are fixed above. There is no transfer-naturality premise.
```
structure PublishedBoundaryAssemblyInput where
…
```
theorem OAI.CoarseAssembly.boundary_assembly_zero line 86
Source documentation
Vanishing in the base annihilates the included boundary index by the proved spatial transfer. Filling is a geometric premise, not a published input.
```
theorem boundary_assembly_zero (input : PublishedBoundaryAssemblyInput)
    (hgap : PublishedKazhdanInput) (β : Rips.KX1 BoundaryVertex)
    (hfilled : boundaryBaseCoarsening.homologyMap β = 0) :
    input.total.assembly (boundaryTotalCoarsening.homologyMap β) = 0 := by
…
```
Mentions: OAI.CoarseAssembly.PublishedBoundaryAssemblyInput, OAI.CoarseAssembly.PublishedKazhdanInput, OAI.CoarseAssembly.Rips.KX1, OAI.CoarseAssembly.BoundaryVertex