OAI/RingTheory/Multiplicity/KoszulHomologyMap.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.Koszul.homologyMap_smul line 20
  2. lemma OAI.Lech.Koszul.scalar_annihilates_homology line 26
  3. def OAI.Lech.Koszul.entryIdeal line 34
  4. lemma OAI.Lech.Koszul.tensor_homology_annihilator line 36
  5. lemma OAI.Lech.Koszul.tensor_homology_torsion line 44
  6. lemma OAI.Lech.Koszul.tensor_bounded line 51
  7. def OAI.Lech.Koszul.unit line 62
  8. lemma OAI.Lech.Koszul.unit_bounded line 65
  9. lemma OAI.Lech.Koszul.unit_homology_zero line 71
  10. lemma OAI.Lech.Koszul.cone_homology_exact line 78
  11. lemma OAI.Lech.Koszul.cone_homology_inr_epi line 93
  12. def OAI.Lech.Koszul.unitHomologyGenerator line 117
  13. instance OAI.Lech.Koszul.unitHomologyGenerator_epi line 123
  14. def OAI.Lech.Koszul.unitHomologyQuotient line 135
  15. instance OAI.Lech.Koszul.unitHomologyQuotient_epi line 143
  16. def OAI.Lech.Koszul.inclusion line 159
  17. def OAI.Lech.Koszul.retraction line 164
  18. lemma OAI.Lech.Koszul.inclusion_retraction line 172
  19. lemma OAI.Lech.Koszul.inclusion_homology_injective line 185
  20. def OAI.Lech.Koszul.powerMap line 199
  21. lemma OAI.Lech.Koszul.powerMap_inclusion line 212
  22. lemma OAI.Lech.Koszul.powerMap_refl line 224
  23. lemma OAI.Lech.Koszul.powerMap_comp line 232
  24. def OAI.Lech.Koszul.coneFst line 259
  25. lemma OAI.Lech.Koszul.homology_middle_range_le line 267
  26. def OAI.Lech.Koszul.coneShortComplex line 280
  27. lemma OAI.Lech.Koszul.coneShortComplex_shortExact line 286
  28. def OAI.Lech.Koszul.coneShortComplexMap line 307
  29. def OAI.Lech.Koszul.scalarPowerHomotopy line 320
  30. lemma OAI.Lech.Koszul.powerMap_range_le_inr line 327
  31. lemma OAI.Lech.Koszul.powerMap_range_eq line 355
  32. lemma OAI.Lech.Koszul.scalar_comp_zero line 417
  33. def OAI.Lech.Koszul.augmentation line 423
  34. lemma OAI.Lech.Koszul.inclusion_augmentation line 431
  35. lemma OAI.Lech.Koszul.augmentation_naturality_target line 442
  36. lemma OAI.Lech.Koszul.powerMap_augmentation line 462
  37. def OAI.Lech.Koszul.quotientAugmentation line 480
  38. lemma OAI.Lech.Koszul.quotientAugmentation_inclusion line 487