OAI/RingTheory/Tachikawa/StableDuality.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Tachikawa.projectiveFactors line 14
  2. lemma OAI.Tachikawa.mem_projectiveFactors_iff line 34
  3. lemma OAI.Tachikawa.projectiveFactors_precomp line 40
  4. lemma OAI.Tachikawa.projectiveFactors_postcomp line 47
  5. lemma OAI.Tachikawa.id_mem_projectiveFactors_iff line 53
  6. def OAI.Tachikawa.StableHom line 62
  7. instance OAI.Tachikawa.(instance at line 64) line 64
  8. instance OAI.Tachikawa.(instance at line 66) line 66
  9. def OAI.Tachikawa.stableClass line 69
  10. lemma OAI.Tachikawa.stableClass_eq_zero_iff line 73
  11. lemma OAI.Tachikawa.stable_id_ne_zero_iff line 77
  12. def OAI.Tachikawa.stablePostcompose line 81
  13. lemma OAI.Tachikawa.stablePostcompose_class line 91
  14. lemma OAI.Tachikawa.stableClass_surjective line 96
  15. def OAI.Tachikawa.stablePostcomposeLinear line 100
  16. def OAI.Tachikawa.stableComp line 118
  17. lemma OAI.Tachikawa.stableComp_class line 130
  18. instance OAI.Tachikawa.(instance at line 134) line 134
  19. lemma OAI.Tachikawa.injective_of_retract line 149
  20. lemma OAI.Tachikawa.injective_of_finite_projective line 162
  21. def OAI.Tachikawa.finiteCoinducedEmbedding line 170
  22. lemma OAI.Tachikawa.finiteCoinducedEmbedding_injective line 174
  23. lemma OAI.Tachikawa.projective_of_finite_injective line 183
  24. def OAI.Tachikawa.homPrecompose line 204
  25. def OAI.Tachikawa.homPostcompose line 209
  26. lemma OAI.Tachikawa.factors_iff_extends line 216
  27. lemma OAI.Tachikawa.factors_iff_lifts line 233
  28. lemma OAI.Tachikawa.projectiveFactors_eq_range_precompose line 245
  29. lemma OAI.Tachikawa.projectiveFactors_eq_range_postcompose line 253
  30. def OAI.Tachikawa.SymmetrizingForm.homDual line 270
  31. lemma OAI.Tachikawa.SymmetrizingForm.homDual_apply line 276
  32. lemma OAI.Tachikawa.SymmetrizingForm.homDual_bijective line 279
  33. def OAI.Tachikawa.SymmetrizingForm.homDualEquiv line 297
  34. lemma OAI.Tachikawa.SymmetrizingForm.homDualEquiv_apply line 300
  35. def OAI.Tachikawa.homPiEquiv line 305
  36. def OAI.Tachikawa.SymmetrizingForm.freeHomDual line 317
  37. lemma OAI.Tachikawa.SymmetrizingForm.freeHomDual_apply line 323
  38. lemma OAI.Tachikawa.SymmetrizingForm.freeHomDual_natural line 328
  39. lemma OAI.Tachikawa.SymmetrizingForm.freeHomDual_cyclic line 334
  40. lemma OAI.Tachikawa.SymmetrizingForm.freeHomDual_cyclic_rect line 358
  41. def OAI.Tachikawa.SymmetrizingForm.syzygyPair line 396
  42. lemma OAI.Tachikawa.SymmetrizingForm.syzygyPair_apply line 400
  43. lemma OAI.Tachikawa.SymmetrizingForm.syzygyPair_vanish_left line 404
  44. lemma OAI.Tachikawa.SymmetrizingForm.syzygyPair_vanish_right line 418
  45. def OAI.Tachikawa.SymmetrizingForm.syzygyPairOnStable line 433
  46. lemma OAI.Tachikawa.SymmetrizingForm.syzygyPairOnStable_apply line 450
  47. def OAI.Tachikawa.SymmetrizingForm.stableDualMap line 454
  48. lemma OAI.Tachikawa.SymmetrizingForm.stableDualMap_apply line 467
  49. lemma OAI.Tachikawa.SymmetrizingForm.precompose_range_eq_ker line 475
  50. lemma OAI.Tachikawa.SymmetrizingForm.syzygyPair_eq_zero_iff line 502
  51. lemma OAI.Tachikawa.SymmetrizingForm.stableDualMap_injective line 533
  52. lemma OAI.Tachikawa.SymmetrizingForm.stableDualMap_surjective line 546
  53. def OAI.Tachikawa.SymmetrizingForm.stableDualEquiv line 585
  54. structure OAI.Tachikawa.FiniteFreeCover line 603
  55. def OAI.Tachikawa.finiteFreeCover line 608
  56. def OAI.Tachikawa.SymmetrizingForm.freeEmbedding line 616
  57. lemma OAI.Tachikawa.SymmetrizingForm.freeEmbedding_injective line 620
  58. theorem OAI.Tachikawa.SymmetrizingForm.exists_stableDualEquiv line 626
  59. def OAI.Tachikawa.resolutionOfExact line 653
  60. theorem OAI.Tachikawa.ext_subsingleton_of_boundaries line 696