OAI/Geometry/HyperbolicGroups/HSpacePathObstruction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The cellular obstruction and its exact change under edge corrections.

  1. def OAI.HyperbolicObstruction.HSpacePathObstruction.pairToUnit line 17
  2. lemma OAI.HyperbolicObstruction.HSpacePathObstruction.pairToUnit_trans line 20
  3. def OAI.HyperbolicObstruction.HSpacePathObstruction.loopClass line 29
  4. lemma OAI.HyperbolicObstruction.HSpacePathObstruction.loopClass_combine line 31
  5. def OAI.HyperbolicObstruction.HSpacePathObstruction.difference line 37

    Source documentation

    Difference of two paths ending at the same basepoint.

    def difference {a : Y} (p q : Path a e) : FundamentalGroup Y e := Q (p.symm.trans q)
  6. lemma OAI.HyperbolicObstruction.HSpacePathObstruction.difference_eq_one_iff line 39
  7. lemma OAI.HyperbolicObstruction.HSpacePathObstruction.difference_trans line 53
  8. def OAI.HyperbolicObstruction.HSpacePathObstruction.obstruction line 64

    Source documentation

    Obstruction for a face joining the products of its opposite pairs.

    def obstruction (F : Path (m (a,b)) (m (c,d)))
    (pa : Path a e) (pb : Path b e) (pc : Path c e) (pd : Path d e) :
    FundamentalGroup Y e := difference (pairToUnit pa pb) (F.trans (pairToUnit pc pd))

    Mentions: OAI.HyperbolicObstruction.HSpacePathObstruction.difference, OAI.HyperbolicObstruction.HSpacePathObstruction.pairToUnit

  9. lemma OAI.HyperbolicObstruction.HSpacePathObstruction.correction line 68
  10. lemma OAI.HyperbolicObstruction.HSpacePathObstruction.obstruction_vanishes_iff line 87

    Source documentation

    The face extends once the corrected obstruction is killed, with the actual prescribed boundary paths retained.

    lemma obstruction_vanishes_iff (F : Path (m (a,b)) (m (c,d)))
    (pa : Path a e) (pb : Path b e) (pc : Path c e) (pd : Path d e) :
    obstruction F pa pb pc pd = 1 ↔
      ((pairToUnit pa pb).trans (Path.refl e)).Homotopic (F.trans (pairToUnit pc pd)) := by
…

    Mentions: OAI.HyperbolicObstruction.HSpacePathObstruction.obstruction, OAI.HyperbolicObstruction.HSpacePathObstruction.pairToUnit