OAI/RingTheory/Multiplicity/SourceGradedThickeningNat.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.SourceGraded.thickeningNatSequence line 20
  2. lemma OAI.Lech.SourceGraded.thickeningNatSequence_shortExact line 25
  3. def OAI.Lech.SourceGraded.thickeningAugSequence line 34
  4. lemma OAI.Lech.SourceGraded.thickeningAugSequence_shortExact line 37
  5. def OAI.Lech.SourceGraded.thickeningPositiveSequence line 42
  6. lemma OAI.Lech.SourceGraded.thickeningPositiveSequence_shortExact line 48
  7. lemma OAI.Lech.SourceGraded.thickeningPositiveSequence_f line 52
  8. lemma OAI.Lech.SourceGraded.thickeningPositiveSequence_X₂ line 56
  9. lemma OAI.Lech.SourceGraded.thickeningPositiveSequence_X₃ line 59
  10. def OAI.Lech.SourceGraded.thickeningNatSequenceMap line 62
  11. def OAI.Lech.SourceGraded.thickeningPositiveSequenceMap line 71
  12. instance OAI.Lech.SourceGraded.thickeningPositiveSequenceMap_middleIso line 83
  13. lemma OAI.Lech.SourceGraded.thickeningPositiveSequenceMap_τ₁ line 95
  14. lemma OAI.Lech.SourceGraded.thickeningPositiveSequenceMap_τ₃ line 99
  15. def OAI.Lech.SourceGraded.thickeningTensorSequence line 104
  16. lemma OAI.Lech.SourceGraded.thickeningTensorSequence_shortExact line 107
  17. def OAI.Lech.SourceGraded.thickeningTensorSequenceMap line 111
  18. lemma OAI.Lech.stableImage_isIso line 123
  19. lemma OAI.Lech.shortExactTransition_stableImage_isIso line 156
  20. instance OAI.Lech.SourceGraded.thickeningTensorSequenceMap_middleIso line 194
  21. lemma OAI.Lech.SourceGraded.thickeningTensorSequenceMap_τ₃ line 199
  22. def OAI.Lech.SourceGraded.geometricStructureMap line 205
  23. lemma OAI.Lech.SourceGraded.geometricStructureMap_transition line 210
  24. lemma OAI.Lech.SourceGraded.uniform_step_to_gap line 216
  25. lemma OAI.Lech.SourceGraded.exists_uniform_geometric_stableImage line 224
  26. lemma OAI.Lech.Koszul.ofHom_smul line 264
  27. def OAI.Lech.Koszul.coneRetraction line 270
  28. lemma OAI.Lech.Koszul.inr_coneRetraction line 274
  29. def OAI.Lech.Koszul.coneScalarHomotopy line 279
  30. def OAI.Lech.Koszul.coneEntryHomotopy line 318
  31. def OAI.Lech.Koszul.tensor line 331
  32. lemma OAI.Lech.Koszul.tensor_nil line 334
  33. lemma OAI.Lech.Koszul.tensor_cons line 335
  34. def OAI.Lech.Koszul.tensorScalarHomotopy line 339
  35. lemma OAI.Lech.Koszul.tensor_entry_nullhomotopic line 345
  36. def OAI.Lech.Koszul.coneFunctor line 356
  37. instance OAI.Lech.Koszul.(instance at line 362) line 362
  38. def OAI.Lech.Koszul.termIso line 373
  39. lemma OAI.Lech.Koszul.coneFunctor_map_f line 377
  40. def OAI.Lech.Koszul.biprodShortComplex line 403
  41. def OAI.Lech.Koszul.biprodSplitting line 407
  42. def OAI.Lech.Koszul.coneShortComplexIso line 426
  43. def OAI.Lech.Koszul.coneSplitting line 434
  44. def OAI.Lech.Koszul.tensorMap line 440
  45. lemma OAI.Lech.Koszul.tensorMap_id line 448
  46. lemma OAI.Lech.Koszul.tensorMap_comp line 459
  47. def OAI.Lech.Koszul.tensorFunctor line 474
  48. instance OAI.Lech.Koszul.(instance at line 480) line 480
  49. def OAI.Lech.Koszul.tensorSplitting line 489
  50. lemma OAI.Lech.Koszul.tensorFunctor_obj line 498
  51. def OAI.Lech.Koszul.tensorShiftIso line 502
  52. lemma OAI.Lech.Koszul.cone_triangleh_epi line 516
  53. def OAI.Lech.Koszul.coneHomologyProjection line 525
  54. lemma OAI.Lech.Koszul.coneHomologyProjection_epi line 536
  55. lemma OAI.Lech.Koszul.prop_homology_of_cone line 556
  56. lemma OAI.Lech.Koszul.prop_homology_of_tensor line 564