OAI/Geometry/HyperbolicGroups/HSpaceFundamental.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual fundamental group of an H-space is abelian. The proof uses the relative unit homotopies, not an assumed pi-2 comparison theorem.

  1. def OAI.HyperbolicObstruction.HSpaceFundamental.combine line 16
  2. def OAI.HyperbolicObstruction.HSpaceFundamental.combinePath line 19
  3. lemma OAI.HyperbolicObstruction.HSpaceFundamental.combine_mk line 21
  4. lemma OAI.HyperbolicObstruction.HSpaceFundamental.combine_refl_right line 24
  5. lemma OAI.HyperbolicObstruction.HSpaceFundamental.combine_refl_left line 47
  6. lemma OAI.HyperbolicObstruction.HSpaceFundamental.combine_one_right line 70
  7. lemma OAI.HyperbolicObstruction.HSpaceFundamental.combine_one_left line 73
  8. lemma OAI.HyperbolicObstruction.HSpaceFundamental.combine_interchange line 77
  9. def OAI.HyperbolicObstruction.HSpaceFundamental.commGroup line 90

    Source documentation

    The group multiplication is the original fundamental-group multiplication.

    @[instance_reducible] def commGroup : CommGroup (FundamentalGroup X e) :=
…
  10. lemma OAI.HyperbolicObstruction.HSpaceFundamental.combine_eq_mul line 95