OAI/Topology/CoarseAssembly/BoundaryEmbedding.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The exact spatial boundary factorization

Boundary fibers have depth zero and are singletons. The normalized fiber embedding therefore agrees exactly with the coordinate inclusion there, which proves the operator factorization needed by assembly naturality.

  1. def OAI.CoarseAssembly.BoundaryVertex line 19
  2. instance OAI.CoarseAssembly.boundaryVertexDecidableEq line 21
  3. def OAI.CoarseAssembly.boundaryToBase line 23
  4. def OAI.CoarseAssembly.boundaryToVertex line 25
  5. def OAI.CoarseAssembly.boundaryBaseIsometry line 34
  6. def OAI.CoarseAssembly.boundaryVertexIsometry line 37
  7. theorem OAI.CoarseAssembly.fiberEmbedding_boundary line 41
  8. theorem OAI.CoarseAssembly.boundary_operator_factorization line 63