OAI/RingTheory/Multiplicity/TotalGhostRowHom.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.TotalGhost.row_hom_transport line 17
  2. def OAI.Lech.TotalGhost.RowHomotopy.ofRows line 26
  3. def OAI.Lech.TotalGhost.Shifted line 50
  4. lemma OAI.Lech.TotalGhost.shifted_identity line 57
  5. lemma OAI.Lech.TotalGhost.shifted_comp line 62
  6. lemma OAI.Lech.TotalGhost.shifted_correction line 71
  7. lemma OAI.Lech.TotalGhost.shifted_eq_zero line 78
  8. def OAI.Lech.TotalGhost.towerPath line 95
  9. lemma OAI.Lech.TotalGhost.homologyMap_path line 99
  10. lemma OAI.Lech.TotalGhost.shifted_path line 108
  11. lemma OAI.Lech.TotalGhost.homologyMap_path_eq_zero line 118
  12. lemma OAI.Lech.TotalGhost.towerPath_map line 134
  13. def OAI.Lech.FilteredCech.tensorBic line 150
  14. lemma OAI.Lech.FilteredCech.tensorBic_total_map line 153
  15. lemma OAI.Lech.FilteredCech.tensorBic_isZero line 161
  16. def OAI.Lech.FilteredCech.bicRowHomotopy line 167
  17. def OAI.Lech.FilteredCech.bicRowHomotopyAt line 171
  18. def OAI.Lech.FilteredCech.twistStep line 177
  19. lemma OAI.Lech.FilteredCech.twistPath line 180
  20. lemma OAI.Lech.FilteredCech.positive_homologyMap_zero line 194
  21. def OAI.Lech.baseChangeFunctor line 222
  22. instance OAI.Lech.baseChangeFunctor_additive line 228
  23. def OAI.Lech.baseChangeHomEquiv line 232
  24. instance OAI.Lech.baseChangeFunctor_linear line 246
  25. lemma OAI.Lech.baseChangeHom_isBaseChange line 253
  26. instance OAI.Lech.baseChangeFunctor_map_localized line 265
  27. lemma OAI.Lech.baseChange_contractible line 284
  28. lemma OAI.Lech.localizedModule_retract line 322
  29. lemma OAI.Lech.projective_baseChange line 362
  30. def OAI.Lech.precompLinear line 376
  31. lemma OAI.Lech.baseChangeHom_localized_projective line 383
  32. lemma OAI.Lech.baseChangeFunctor_map_localized_projective line 416
  33. lemma OAI.Lech.baseChange_projective_contractible line 427