OAI/RingTheory/Multiplicity/TensorTotalHomologyProperty.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.TensorTotal.homology_property_of_bounded_free line 18
  2. lemma OAI.Lech.homology_property_extendUpNat line 44
  3. def OAI.Lech.TensorTotal.Right.functor line 66
  4. def OAI.Lech.TensorTotal.Right.degreeMap line 75
  5. lemma OAI.Lech.TensorTotal.Right.ι_degreeMap line 81
  6. lemma OAI.Lech.TensorTotal.Right.degreeMap_id line 88
  7. lemma OAI.Lech.TensorTotal.Right.degreeMap_comp line 95
  8. lemma OAI.Lech.TensorTotal.Right.degreeMap_add line 108
  9. lemma OAI.Lech.TensorTotal.Right.map_f line 118
  10. instance OAI.Lech.TensorTotal.Right.(instance at line 131) line 131
  11. def OAI.Lech.TensorTotal.Right.splitting line 141
  12. def OAI.Lech.TensorTotal.bottomSequence line 172
  13. lemma OAI.Lech.TensorTotal.bottomSequence_shortExact line 175
  14. def OAI.Lech.TensorTotal.bottomComparison line 180
  15. lemma OAI.Lech.TensorTotal.bottomComparison_isoModSerre line 185
  16. lemma OAI.Lech.TensorTotal.bottomComparison_naturality line 191
  17. abbrev OAI.Lech.TensorTotal.singleZero line 209
  18. abbrev OAI.Lech.TensorTotal.tensorSingle line 210
  19. abbrev OAI.Lech.TensorTotal.termTensor line 211
  20. def OAI.Lech.TensorTotal.intoTensorSingle line 213
  21. def OAI.Lech.TensorTotal.outOfTensorSingle line 217
  22. lemma OAI.Lech.TensorTotal.into_out line 223
  23. lemma OAI.Lech.TensorTotal.out_into line 230
  24. def OAI.Lech.TensorTotal.tensorSingleXIso line 246
  25. lemma OAI.Lech.TensorTotal.tensorSingle_d₂ line 252
  26. lemma OAI.Lech.TensorTotal.intoTensorSingle_comm line 259
  27. def OAI.Lech.TensorTotal.tensorSingleIso line 270
  28. def OAI.Lech.TensorTotal.termTensorMap line 273
  29. lemma OAI.Lech.TensorTotal.tensorSingleIso_naturality line 277
  30. def OAI.Lech.moduleQuotient line 297
  31. instance OAI.Lech.moduleQuotient_additive line 308
  32. def OAI.Lech.moduleQuotientπ line 315
  33. instance OAI.Lech.moduleQuotientπ_epi line 321
  34. lemma OAI.Lech.moduleQuotient_annihilated line 325
  35. def OAI.Lech.complexQuotient line 333
  36. instance OAI.Lech.complexQuotient_additive line 337
  37. def OAI.Lech.complexQuotientπ line 341
  38. lemma OAI.Lech.complexQuotient_annihilated line 346
  39. def OAI.Lech.TensorTotal.termTensorQuotientIso line 361
  40. def OAI.Lech.TensorTotal.tensorSingleQuotientIso line 378
  41. def OAI.Lech.LocalizationCech.augmentationIso line 392
  42. def OAI.Lech.FilteredCech.augmentationIso line 408
  43. lemma OAI.Lech.FilteredCech.augmentationIso_naturality line 417
  44. def OAI.Lech.idealCokernelIso line 438
  45. lemma OAI.Lech.idealCokernelIso_π line 445