OAI/GroupTheory/FiniteType/SingularExcision.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingularExcision.eventually_split line 13
  2. lemma OAI.SingularExcision.split_chain line 34
  3. lemma OAI.RelativeChains.inclusion_d line 51
  4. abbrev OAI.SingularExcision.scInclusion line 64
  5. lemma OAI.SingularExcision.scInclusion_surjective line 69
  6. lemma OAI.SingularExcision.scInclusion_injective line 92
  7. theorem OAI.SingularExcision.inclusion_quasiIsoAt line 127
  8. theorem OAI.SingularExcision.inclusion_quasiIso line 138
  9. theorem OAI.SingularExcision.excise_closed line 143
  10. def OAI.RelativeChains.sequence line 159
  11. theorem OAI.RelativeChains.shortExact line 165
  12. def OAI.RelativeChains.connecting line 178
  13. lemma OAI.RelativeChains.connecting_isIso line 181
  14. def OAI.RelativeChains.restrictMap line 185
  15. def OAI.RelativeChains.sequenceMap line 188
  16. lemma OAI.RelativeChains.map_quasiIso line 201
  17. def OAI.SingularChains.homotopyChainEquiv line 213
  18. lemma OAI.SingularChains.homotopyEquiv_quasiIso line 226
  19. lemma OAI.SingularChains.contractible_homology_isZero line 229
  20. lemma OAI.SingularChains.map_iso line 239