OAI/RingTheory/Tachikawa/DerivedInduction.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Tachikawa.Construction.restrictedLeftResolution line 12
  2. lemma OAI.Tachikawa.Construction.restrictedLeftResolution_above line 16
  3. def OAI.Tachikawa.Construction.restrictedRightResolution line 19
  4. lemma OAI.Tachikawa.Construction.restrictedRightResolution_above line 26
  5. lemma OAI.Tachikawa.Construction.c5_left_projective line 31
  6. lemma OAI.Tachikawa.Construction.c5_right_projective line 37
  7. abbrev OAI.Tachikawa.Construction.Y line 42
  8. lemma OAI.Tachikawa.Construction.Y_side_projective line 46
  9. def OAI.Tachikawa.Construction.cSimpleCanon line 62
  10. def OAI.Tachikawa.Construction.cSimpleUnderlying line 65
  11. def OAI.Tachikawa.Construction.bSimpleTensorUnderlying line 77
  12. lemma OAI.Tachikawa.Construction.bSimpleTensorUnderlying_smul line 82
  13. def OAI.Tachikawa.Construction.bSimpleTensorRestrictionEquiv line 99
  14. def OAI.Tachikawa.Construction.bSimpleTensorRestrictionIso line 113
  15. def OAI.Tachikawa.Construction.restrictedXResolution line 117
  16. def OAI.Tachikawa.Construction.evaluatedKComparison line 130
  17. abbrev OAI.Tachikawa.TrivialInduction.inclusion line 148
  18. def OAI.Tachikawa.TrivialInduction.tensorGenerators line 151
  19. def OAI.Tachikawa.TrivialInduction.tensorComparison line 173
  20. lemma OAI.Tachikawa.TrivialInduction.tensorComparison_mk line 178
  21. def OAI.Tachikawa.TrivialInduction.tensorPure line 183
  22. lemma OAI.Tachikawa.TrivialInduction.tensorPure_inr_smul line 189
  23. def OAI.Tachikawa.TrivialInduction.lowerBilinear line 208
  24. lemma OAI.Tachikawa.TrivialInduction.lowerBilinear_balanced line 231
  25. def OAI.Tachikawa.TrivialInduction.lowerTensor line 244
  26. def OAI.Tachikawa.TrivialInduction.tensorInverse line 251
  27. lemma OAI.Tachikawa.TrivialInduction.tensorComparison_lower line 257
  28. lemma OAI.Tachikawa.TrivialInduction.tensorComparison_inverse line 275
  29. lemma OAI.Tachikawa.TrivialInduction.tensorInverse_zero line 289
  30. lemma OAI.Tachikawa.TrivialInduction.tensorInverse_add line 294
  31. lemma OAI.Tachikawa.TrivialInduction.tensorInverse_comparison line 305
  32. def OAI.Tachikawa.TrivialInduction.tensorComparisonEquiv line 350
  33. def OAI.Tachikawa.TrivialInduction.tensorComparisonIso line 357
  34. lemma OAI.Tachikawa.TrivialInduction.tensorComparison_natural line 371
  35. def OAI.Tachikawa.TrivialInduction.tensorComplexIso line 384
  36. lemma OAI.Tachikawa.C.resObj_finite_k line 402
  37. lemma OAI.Tachikawa.C.projectiveResolution_d line 416
  38. def OAI.Tachikawa.C.inducedJComparison line 421
  39. abbrev OAI.Tachikawa.C.balancedInducedResolution line 446
  40. def OAI.Tachikawa.C.inducedJTensorComparison line 450
  41. abbrev OAI.Tachikawa.OuterTensor.outerDouble line 472
  42. abbrev OAI.Tachikawa.OuterTensor.inducedOuterDouble line 475
  43. def OAI.Tachikawa.OuterTensor.inductionDoubleComparison line 480
  44. instance OAI.Tachikawa.OuterTensor.inductionDoubleComparison_isIso line 497
  45. def OAI.Tachikawa.OuterTensor.inductionTotalIso line 506
  46. def OAI.Tachikawa.Construction.inducedBToJComparison line 528
  47. def OAI.Tachikawa.Construction.evaluatedKJComparison line 537
  48. def OAI.Tachikawa.Enveloping.homOfLinear line 554
  49. def OAI.Tachikawa.AlgebraInduction.resUnderlyingEquiv line 573
  50. instance OAI.Tachikawa.AlgebraInduction.resFinite line 585
  51. def OAI.Tachikawa.Enveloping.restrictedRegularMap line 598
  52. lemma OAI.Tachikawa.Enveloping.restrictedRegularMap_apply line 610
  53. abbrev OAI.Tachikawa.AlgebraInduction.complexInduction line 625
  54. abbrev OAI.Tachikawa.AlgebraInduction.complexRestriction line 626
  55. def OAI.Tachikawa.AlgebraInduction.complexUnit line 628
  56. def OAI.Tachikawa.AlgebraInduction.complexExtend line 633
  57. lemma OAI.Tachikawa.AlgebraInduction.complexUnit_extend line 646
  58. abbrev OAI.Tachikawa.Enveloping.inducedRegularCochain line 664
  59. def OAI.Tachikawa.Enveloping.regularPreAugmentation line 668
  60. def OAI.Tachikawa.Enveloping.inducedRegularAugmentation line 675
  61. lemma OAI.Tachikawa.Enveloping.induced_regular_square line 679
  62. lemma OAI.Tachikawa.kProjective_chain_representative line 715
  63. lemma OAI.Tachikawa.finite_resolution_cochain line 738
  64. instance OAI.Tachikawa.Enveloping.inducedRegularCochain_finite line 754
  65. instance OAI.Tachikawa.Enveloping.inducedRegularCochain_projective line 766
  66. instance OAI.Tachikawa.Enveloping.inducedRegularCochain_bounded line 774
  67. instance OAI.Tachikawa.Enveloping.inducedRegularCochain_isKProjective line 780
  68. def OAI.Tachikawa.negUpDown line 791
  69. instance OAI.Tachikawa.(instance at line 796) line 796
  70. def OAI.Tachikawa.negDownUp line 799
  71. instance OAI.Tachikawa.(instance at line 804) line 804
  72. abbrev OAI.Tachikawa.reflectChain line 809
  73. abbrev OAI.Tachikawa.reflectCochain line 810
  74. abbrev OAI.Tachikawa.reflectChainMap line 811
  75. abbrev OAI.Tachikawa.reflectCochainMap line 813
  76. lemma OAI.Tachikawa.complex_d_transport line 816
  77. def OAI.Tachikawa.reflectCochainIso line 821
  78. lemma OAI.Tachikawa.reflectCochainIso_natural line 825
  79. def OAI.Tachikawa.reflectChainHomotopy line 833
  80. lemma OAI.Tachikawa.chainInt_exactAt_iff line 857
  81. lemma OAI.Tachikawa.chainNat_exactAt_iff line 863
  82. lemma OAI.Tachikawa.Construction.inducedRegularComplex_exact line 875
  83. lemma OAI.Tachikawa.resolution_reflect_exact line 898
  84. lemma OAI.Tachikawa.Enveloping.inducedReflect_exact line 930
  85. lemma OAI.Tachikawa.Construction.inducedRegularCochain_reflect_exact line 941