OAI/Topology/CoarseAssembly/FamilyFilling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The entire family of base loops vanishes through its actual filling

Both arrows through the disjoint union of compact polygons are constructed proper maps. The vanishing follows only from the specified published compact homotopy and countable-additivity inputs.

  1. def OAI.CoarseAssembly.baseBoundaryLoops line 22
  2. def OAI.CoarseAssembly.filledBoundaryLoops line 25
  3. theorem OAI.CoarseAssembly.boundaryFamily_factors line 28
  4. theorem OAI.CoarseAssembly.baseBoundaryFamily_zero line 41

    Source documentation

    Every class pushed along this family of closed base walks vanishes already at scale one, before passage to the coarse direct limit.

    theorem baseBoundaryFamily_zero (input : PublishedCompactHomotopyInput)
    (hadd : CountableAdditivityInput FilledDisc)
    (a : LocallyFiniteK1 (Sigma (fun _ : ℕ => WindingCircle))) :
    letI := separatedMetric o
…

    Mentions: OAI.CoarseAssembly.FilledDisc, OAI.CoarseAssembly.WindingCircle, OAI.CoarseAssembly.separatedMetric