OAI/Geometry/HyperbolicGroups/VoltageCellGluing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Genuine homotopy gluing on the locally finite family of closed lifted simplices, with no alteration of the voltage-cover topology.

  1. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.faceLiftHomeomorph line 18
  2. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.homotopyOnRange line 27
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.homotopyOnRange_agree line 32
  4. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.glueFaceHomotopies line 41

    Source documentation

    The actual global continuous prism.

    def glueFaceHomotopies : C(I × v.TotalSpace,X) :=
…
  5. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.glueFaceHomotopies_apply line 46
  6. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.glueFaceHomotopies_endpoint line 54