OAI/RingTheory/Multiplicity/LechCokernelComp.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.cokernel_comp_shortExact line 16
  2. def OAI.Lech.cokernelIsoOfShortExact line 27
  3. lemma OAI.Lech.cokernel_homology_property_of_shortExact line 31
  4. lemma OAI.Lech.homology_middle_property line 39
  5. lemma OAI.Lech.cokernel_comp_homology_property line 47
  6. lemma OAI.Lech.FilteredFraction.fraction_one_zero line 60
  7. def OAI.Lech.FilteredFraction.augmentationEquiv line 68
  8. lemma OAI.Lech.FilteredFraction.augmentationEquiv_val line 83
  9. lemma OAI.Lech.FilteredFraction.augmentationEquiv_mem line 86
  10. lemma OAI.Lech.linearMap_sum_smul line 103
  11. def OAI.Lech.cochainOfMap line 111
  12. def OAI.Lech.SourceGraded.filteredReductionCochains line 134
  13. lemma OAI.Lech.SourceGraded.filteredReductionCochains_d line 141
  14. def OAI.Lech.SourceGraded.filteredReductionCech line 159
  15. lemma OAI.Lech.SourceGraded.filteredReductionCochains_surjective line 170
  16. lemma OAI.Lech.SourceGraded.filteredReductionCochains_kernel line 177
  17. lemma OAI.Lech.SourceGraded.filteredReductionCech_comp_zero line 200
  18. def OAI.Lech.SourceGraded.filteredLayerSequence line 213
  19. lemma OAI.Lech.SourceGraded.filteredLayerSequence_shortExact line 217
  20. def OAI.Lech.SourceGraded.finiteThickening line 238
  21. lemma OAI.Lech.SourceGraded.finiteThickening_homology_zero line 243
  22. def OAI.Lech.SourceGraded.finiteThickeningTransition line 271
  23. lemma OAI.Lech.SourceGraded.finiteThickeningTransition_refl line 277
  24. lemma OAI.Lech.SourceGraded.finiteThickeningTransition_comp line 283
  25. lemma OAI.Lech.prop_additive_free line 298
  26. def OAI.Lech.TensorTotal.functor line 332
  27. def OAI.Lech.TensorTotal.degreeMap line 341
  28. lemma OAI.Lech.TensorTotal.ι_degreeMap line 347
  29. lemma OAI.Lech.TensorTotal.degreeMap_id line 354
  30. lemma OAI.Lech.TensorTotal.degreeMap_comp line 361
  31. lemma OAI.Lech.TensorTotal.degreeMap_add line 374
  32. lemma OAI.Lech.TensorTotal.map_f line 384
  33. instance OAI.Lech.TensorTotal.(instance at line 397) line 397
  34. def OAI.Lech.TensorTotal.splitting line 407
  35. def OAI.Lech.TensorTotal.singleRingHomologyIso line 430