OAI/RingTheory/Tachikawa/Coresolution.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Tachikawa.coresolutionOfExact line 11
  2. theorem OAI.Tachikawa.ext_subsingleton_of_coboundaries line 44
  3. lemma OAI.Tachikawa.FiniteModule.embed_exact line 64
  4. def OAI.Tachikawa.FiniteModule.coresolution line 78
  5. lemma OAI.Tachikawa.FiniteModule.coresolution_d line 86
  6. lemma OAI.Tachikawa.FiniteModule.coresolution_ι line 91
  7. def OAI.Tachikawa.SymmetrizingForm.inverseTwistHom line 102
  8. lemma OAI.Tachikawa.SymmetrizingForm.inverseTwistHom_apply line 113
  9. def OAI.Tachikawa.SymmetrizingForm.inverseTwistComplex line 118
  10. def OAI.Tachikawa.mappedCoresolution line 138
  11. def OAI.Tachikawa.mappedCoresolutionCochainXIso line 145
  12. lemma OAI.Tachikawa.mappedCoresolutionCochainXIso_nonneg line 155
  13. lemma OAI.Tachikawa.mappedCoresolutionCochainXIso_comm line 165
  14. def OAI.Tachikawa.mappedCoresolutionCochainIso line 184
  15. lemma OAI.Tachikawa.mappedCoresolutionCochainIso_ι line 189
  16. lemma OAI.Tachikawa.map_fromSingle_shifted line 211
  17. instance OAI.Tachikawa.SymmetrizingForm.twist_isEquivalence line 238
  18. instance OAI.Tachikawa.SymmetrizingForm.twist_preserves_injective line 241
  19. instance OAI.Tachikawa.SymmetrizingForm.twist_preserves_projective line 242
  20. lemma OAI.Tachikawa.mappedCoresolution_ι_zero line 251
  21. lemma OAI.Tachikawa.SymmetrizingForm.twistIso_inv_apply line 265
  22. def OAI.Tachikawa.SymmetrizingForm.inverseCoresolutionHom line 271
  23. lemma OAI.Tachikawa.injective_extMk_hom_roof line 300
  24. lemma OAI.Tachikawa.mappedCoresolutionCochain_cocycle line 315
  25. lemma OAI.Tachikawa.shifted_map_precomp line 355
  26. lemma OAI.Tachikawa.shifted_map_postcomp line 358
  27. lemma OAI.Tachikawa.derived_roof_map line 369
  28. lemma OAI.Tachikawa.derived_roof_map_dual line 432
  29. lemma OAI.Tachikawa.mapExactFunctor_injective_extMk line 496
  30. abbrev OAI.Tachikawa.VectorSplit.homologyComplex line 537
  31. def OAI.Tachikawa.VectorSplit.inclusion line 543
  32. def OAI.Tachikawa.VectorSplit.projection line 554
  33. lemma OAI.Tachikawa.VectorSplit.inclusion_projection line 566
  34. def OAI.Tachikawa.VectorSplit.hom line 576
  35. lemma OAI.Tachikawa.VectorSplit.hom_eq line 582
  36. lemma OAI.Tachikawa.VectorSplit.hom_eq_zero line 586
  37. lemma OAI.Tachikawa.VectorSplit.d_hom_of_rel line 588
  38. lemma OAI.Tachikawa.VectorSplit.d_hom line 597
  39. lemma OAI.Tachikawa.VectorSplit.hom_d line 611
  40. def OAI.Tachikawa.VectorSplit.idHomotopy line 622
  41. def OAI.Tachikawa.VectorSplit.homologyHomotopyEquiv line 640
  42. lemma OAI.Tachikawa.bifunctorMap_comp line 660
  43. lemma OAI.Tachikawa.bifunctorMap_id line 668
  44. def OAI.Tachikawa.bifunctorHomotopyEquiv line 676
  45. abbrev OAI.Tachikawa.VectorSplit.tensorFunctor line 700
  46. def OAI.Tachikawa.VectorSplit.tensorHomologyHomotopyEquiv line 704
  47. lemma OAI.Tachikawa.VectorSplit.tensorHomology_d line 710
  48. def OAI.Tachikawa.VectorSplit.zeroDifferentialHomologyIso line 731
  49. def OAI.Tachikawa.VectorSplit.tensorHomologyIso line 737
  50. def OAI.Tachikawa.resolutionHom line 753
  51. lemma OAI.Tachikawa.resolutionHom_X line 756
  52. lemma OAI.Tachikawa.resolutionHom_d line 759
  53. lemma OAI.Tachikawa.resolutionHom_memZ line 762
  54. lemma OAI.Tachikawa.extMk_smul line 771
  55. def OAI.Tachikawa.resolutionCyclesToExt line 779
  56. lemma OAI.Tachikawa.resolutionCyclesToExt_surjective line 785
  57. lemma OAI.Tachikawa.resolutionCyclesToExt_ker line 791
  58. def OAI.Tachikawa.resolutionHomologyExt line 809
  59. lemma OAI.Tachikawa.extMk_zeroDegree_eq_zero line 827
  60. lemma OAI.Tachikawa.resolutionBoundary_zero line 845
  61. lemma OAI.Tachikawa.resolutionCyclesToExt_ker_all line 854
  62. def OAI.Tachikawa.resolutionHomologyExtAll line 871
  63. def OAI.Tachikawa.coresolutionHom line 889
  64. lemma OAI.Tachikawa.coresolutionHom_X line 892
  65. lemma OAI.Tachikawa.coresolutionHom_d line 894
  66. lemma OAI.Tachikawa.coresolutionHom_memZ line 896
  67. lemma OAI.Tachikawa.injective_extMk_smul line 903
  68. def OAI.Tachikawa.coresolutionCyclesToExt line 911
  69. lemma OAI.Tachikawa.coresolutionCyclesToExt_surjective line 917
  70. lemma OAI.Tachikawa.coresolutionCyclesToExt_ker line 922
  71. lemma OAI.Tachikawa.injective_extMk_zeroDegree_eq_zero line 938
  72. lemma OAI.Tachikawa.coresolutionBoundary_zero line 955
  73. lemma OAI.Tachikawa.coresolutionCyclesToExt_ker_all line 963
  74. def OAI.Tachikawa.coresolutionHomologyExtAll line 974
  75. def OAI.Tachikawa.extIso line 992
  76. def OAI.Tachikawa.coresolutionTwistHom line 1012
  77. lemma OAI.Tachikawa.coresolutionTwistHom_extMk line 1034
  78. lemma OAI.Tachikawa.coresolutionTwist_diff_boundary line 1057
  79. lemma OAI.Tachikawa.SymmetrizingForm.freeHomDual_semilinear_adjoint line 1096
  80. lemma OAI.Tachikawa.SymmetrizingForm.free_boundary_iff_pair_cycles line 1132
  81. lemma OAI.Tachikawa.SymmetrizingForm.free_boundary_of_adjoint_scalar line 1149
  82. lemma OAI.Tachikawa.FiniteModule.negativeTwist_diff_boundary line 1182