OAI/RingTheory/Tachikawa/OuterExt.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Tachikawa.vectorTensor_quasiIso line 12
  2. instance OAI.Tachikawa.OuterTensor.restrictionPreservesHomology line 30
  3. lemma OAI.Tachikawa.OuterTensor.quasiIso line 35
  4. def OAI.Tachikawa.bifunctorZeroIso line 55
  5. abbrev OAI.Tachikawa.singleBifunctor line 75
  6. lemma OAI.Tachikawa.singleBifunctor_isZero line 79
  7. def OAI.Tachikawa.bifunctorSingleIso line 92
  8. lemma OAI.Tachikawa.OuterTensor.total_projective line 119
  9. def OAI.Tachikawa.OuterTensor.resolution line 133
  10. def OAI.Tachikawa.coproductHomEquiv line 152
  11. def OAI.Tachikawa.coproductPiEquiv line 162
  12. lemma OAI.Tachikawa.coproductPiEquiv_ι line 165
  13. lemma OAI.Tachikawa.coproductPiEquiv_ι_self line 176
  14. lemma OAI.Tachikawa.coproductPiEquiv_ι_ne line 181
  15. instance OAI.Tachikawa.TotalDualPairing.(instance at line 195) line 195
  16. abbrev OAI.Tachikawa.TotalDualPairing.Diag line 207
  17. abbrev OAI.Tachikawa.TotalDualPairing.chainFamily line 212
  18. abbrev OAI.Tachikawa.TotalDualPairing.cochainFamily line 213
  19. instance OAI.Tachikawa.TotalDualPairing.(instance at line 215) line 215
  20. def OAI.Tachikawa.TotalDualPairing.equiv line 224
  21. lemma OAI.Tachikawa.TotalDualPairing.evaluate line 229
  22. lemma OAI.Tachikawa.TotalDualPairing.evaluate_ι_self line 235
  23. lemma OAI.Tachikawa.TotalDualPairing.evaluate_ι_ne line 243
  24. lemma OAI.Tachikawa.TotalDualPairing.units_smul_eq line 262
  25. lemma OAI.Tachikawa.TotalDualPairing.up_d₁ line 274
  26. lemma OAI.Tachikawa.TotalDualPairing.up_d₂ line 281
  27. lemma OAI.Tachikawa.TotalDualPairing.down_d₁ line 287
  28. lemma OAI.Tachikawa.TotalDualPairing.down_d₂ line 295
  29. lemma OAI.Tachikawa.TotalDualPairing.down_d₁_zero line 301
  30. lemma OAI.Tachikawa.TotalDualPairing.down_d₂_zero line 304
  31. lemma OAI.Tachikawa.TotalDualPairing.horizontal line 314
  32. lemma OAI.Tachikawa.TotalDualPairing.vertical line 348
  33. lemma OAI.Tachikawa.TotalDualPairing.comm line 398
  34. def OAI.Tachikawa.TotalDualPairing.comparison line 419
  35. instance OAI.Tachikawa.TotalDualPairing.(instance at line 426) line 426
  36. def OAI.Tachikawa.TotalDualPairing.iso line 431
  37. abbrev OAI.Tachikawa.OuterTensor.homBicomplex line 445
  38. def OAI.Tachikawa.OuterTensor.homBicomplexEquiv line 452
  39. lemma OAI.Tachikawa.OuterTensor.precompose_id line 456
  40. lemma OAI.Tachikawa.OuterTensor.homBicomplexEquiv_horizontal line 462
  41. lemma OAI.Tachikawa.OuterTensor.homBicomplexEquiv_vertical line 472
  42. def OAI.Tachikawa.OuterTensor.homTotalIso line 484
  43. def OAI.Tachikawa.VectorSplit.homologyIsoH line 500
  44. abbrev OAI.Tachikawa.OuterTensor.tensorResolution line 518
  45. abbrev OAI.Tachikawa.OuterTensor.homologyTensor line 519
  46. def OAI.Tachikawa.OuterTensor.extKunneth line 523
  47. lemma OAI.Tachikawa.OuterTensor.bifunctor_maps line 553
  48. instance OAI.Tachikawa.OuterTensor.algebraTwist_preserves_projective line 559
  49. def OAI.Tachikawa.OuterTensor.tensorTwistObjIso line 571
  50. abbrev OAI.Tachikawa.OuterTensor.tensorTwistLiftHom line 580
  51. lemma OAI.Tachikawa.OuterTensor.ι_tensorTwistLiftHom line 585
  52. lemma OAI.Tachikawa.OuterTensor.ι_resolution_π_zero line 606
  53. def OAI.Tachikawa.OuterTensor.tensorTwistLift line 617
  54. lemma OAI.Tachikawa.OuterTensor.tensorF_maps line 656
  55. lemma OAI.Tachikawa.OuterTensor.homTotal_evaluate line 674
  56. lemma OAI.Tachikawa.OuterTensor.homTotal_evaluate_ne line 682
  57. abbrev OAI.Tachikawa.OuterTensor.tensorResolutionTwist line 695
  58. lemma OAI.Tachikawa.OuterTensor.homMap_twist line 703
  59. lemma OAI.Tachikawa.OuterTensor.homTotal_twist line 735