OAI/RingTheory/Multiplicity/CechNormalization.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Lech.CechNormalization.fullCochains line 14
  2. abbrev OAI.Lech.CechNormalization.fullD line 15
  3. abbrev OAI.Lech.CechNormalization.fullSort line 16
  4. abbrev OAI.Lech.CechNormalization.fullExpand line 17
  5. abbrev OAI.Lech.CechNormalization.fullH line 18
  6. abbrev OAI.Lech.CechNormalization.fullN line 19
  7. lemma OAI.Lech.CechNormalization.fullD_square line 22
  8. lemma OAI.Lech.CechNormalization.sortedD_eq line 30
  9. lemma OAI.Lech.CechNormalization.fullSort_d line 43
  10. lemma OAI.Lech.CechNormalization.fullExpand_d line 50
  11. lemma OAI.Lech.CechNormalization.fullSort_expand line 56
  12. lemma OAI.Lech.CechNormalization.fullExpand_sort line 61
  13. lemma OAI.Lech.CechNormalization.fullH_zero line 65
  14. lemma OAI.Lech.CechNormalization.fullH_identity line 71
  15. def OAI.Lech.CechNormalization.fullPositive line 83
  16. lemma OAI.Lech.CechNormalization.fullPositive_d line 91
  17. def OAI.Lech.CechNormalization.sortMap line 96
  18. def OAI.Lech.CechNormalization.expandMap line 102
  19. lemma OAI.Lech.CechNormalization.expand_sortMap line 108
  20. lemma OAI.Lech.CechNormalization.sort_expandMap line 114
  21. def OAI.Lech.CechNormalization.homotopyComponent line 117
  22. lemma OAI.Lech.CechNormalization.homotopyComponent_succ line 120
  23. def OAI.Lech.CechNormalization.normalizationHomotopy line 124
  24. def OAI.Lech.CechNormalization.homotopyEquiv line 149