OAI/RingTheory/Multiplicity/LechMapCochain.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.map_cochain_smul line 21
  2. lemma OAI.Lech.cochain_surj_away line 26
  3. lemma OAI.Lech.cochain_eq_zero_away line 51
  4. lemma OAI.Lech.ofHom_smul line 75
  5. lemma OAI.Lech.nullhomotopy_away line 80
  6. lemma OAI.Lech.nullhomotopy_of_projective_acyclic_away line 103
  7. lemma OAI.Lech.uniform_nullhomotopy_of_projective_acyclic_away line 129
  8. lemma OAI.Lech.FilteredCech.positive_homologyMap_zero_of_le line 155
  9. lemma OAI.Lech.FilteredCech.exists_uniform_positive_nilpotence line 167
  10. lemma OAI.Lech.FiniteComplex.dropBottomMap_comp line 189
  11. lemma OAI.Lech.FiniteComplex.dropBottomMap_zero line 201
  12. def OAI.Lech.FiniteComplex.dropShortComplex line 213
  13. lemma OAI.Lech.FiniteComplex.dropShortComplex_shortExact line 217
  14. lemma OAI.Lech.extend_shortExact line 239
  15. lemma OAI.Lech.FiniteComplex.dropBottomMap_id line 268
  16. def OAI.Lech.FiniteComplex.dropShortComplexMap line 275
  17. lemma OAI.Lech.FiniteComplex.dropBottomMap_extend_id line 299
  18. lemma OAI.Lech.FiniteComplex.isIso_dropBottomMap line 309
  19. lemma OAI.Lech.FiniteComplex.isIso_dropShortComplexMap_τ₂ line 315
  20. lemma OAI.Lech.functorCategory_shortExact line 333
  21. def OAI.Lech.discreteShortComplex line 348
  22. lemma OAI.Lech.discreteShortComplex_shortExact line 356
  23. lemma OAI.Lech.coproduct_shortExact line 363
  24. def OAI.Lech.TensorTotal.Right.degreeSequenceFamily line 376
  25. def OAI.Lech.TensorTotal.Right.degreeSequenceIso line 381
  26. lemma OAI.Lech.TensorTotal.Right.shortExact line 417