OAI/GroupTheory/FiniteType/ChainShortExact.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ChainShortExact.quasiIso_g line 14
  2. lemma OAI.ChainShortExact.zero_homology₃_zero line 25
  3. lemma OAI.RelativeChains.univ_homology_isZero line 38
  4. lemma OAI.RelativeChains.contractible_singleton_homology_isZero line 41
  5. lemma OAI.RelativeChains.singleton_quotient_quasiIso line 57
  6. lemma OAI.RelativeChains.preimage_singleton_inclusion line 74
  7. def OAI.RelativeChains.suspensionIso line 80
  8. lemma OAI.RelativeChains.suspension_zero line 98
  9. lemma OAI.SingularSubspace.constant_mem line 119
  10. lemma OAI.SingularSubspace.constant_fixed line 128
  11. def OAI.RelativeChains.pointChange line 147
  12. lemma OAI.RelativeChains.pointChange_projection line 154
  13. lemma OAI.RelativeChains.pointChange_comp line 158
  14. lemma OAI.RelativeChains.pointChange_self line 173
  15. def OAI.RelativeChains.pointChangeIso line 181
  16. def OAI.RelativeChains.pointHomologyIso line 187
  17. lemma OAI.RelativeChains.pointMap_quasiIso line 191
  18. def OAI.RelativeChains.pointHomotopyEquivIso line 203
  19. lemma OAI.SingularChains.isEmpty_homology_isZero line 214
  20. def OAI.SingularChains.unique_homologyZeroIso line 221