OAI/RingTheory/Tachikawa/Induction.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Tachikawa.Enveloping.rightRegularEndUnderlying line 12
  2. def OAI.Tachikawa.Enveloping.ordinaryEndEquiv line 15
  3. lemma OAI.Tachikawa.Enveloping.ordinaryEndEquiv_tmul line 19
  4. lemma OAI.Tachikawa.Enveloping.ordinaryEndEquiv_left line 27
  5. lemma OAI.Tachikawa.Enveloping.ordinaryEndEquiv_right line 39
  6. def OAI.Tachikawa.Enveloping.dualRegularUnderlying line 53
  7. lemma OAI.Tachikawa.Enveloping.dualRegularUnderlying_left line 66
  8. lemma OAI.Tachikawa.Enveloping.dualRegularUnderlying_right line 75
  9. def OAI.Tachikawa.Enveloping.ordinaryAlpha line 86
  10. lemma OAI.Tachikawa.Enveloping.ordinaryAlpha_left line 90
  11. lemma OAI.Tachikawa.Enveloping.ordinaryAlpha_right line 98
  12. def OAI.Tachikawa.Enveloping.ordinaryBeta line 106
  13. lemma OAI.Tachikawa.Enveloping.ordinaryBeta_end line 110
  14. lemma OAI.Tachikawa.Enveloping.ordinaryBeta_left line 116
  15. lemma OAI.Tachikawa.Enveloping.ordinaryBeta_right line 124
  16. lemma OAI.Tachikawa.Enveloping.ordinaryBeta_alpha line 132
  17. def OAI.Tachikawa.characterBimoduleMap line 148
  18. lemma OAI.Tachikawa.characterBimoduleMap_apply line 156
  19. lemma OAI.Tachikawa.ordinary_morphism_factorization_pf_zero line 162
  20. def OAI.Tachikawa.Construction.rho line 180
  21. lemma OAI.Tachikawa.Construction.rho_tmul line 185
  22. lemma OAI.Tachikawa.Construction.rho_left line 188
  23. lemma OAI.Tachikawa.Construction.rho_right line 207
  24. lemma OAI.Tachikawa.Construction.sigma_inclusionB line 226
  25. lemma OAI.Tachikawa.Construction.rho_zeta line 240
  26. lemma OAI.Tachikawa.Construction.character_inclusion line 245
  27. lemma OAI.Tachikawa.Construction.rho_representation_socle line 250
  28. def OAI.Tachikawa.AlgebraInduction.regularHom line 267
  29. def OAI.Tachikawa.AlgebraInduction.regularInv line 273
  30. lemma OAI.Tachikawa.AlgebraInduction.regularHom_unit line 277
  31. lemma OAI.Tachikawa.AlgebraInduction.regularInv_apply line 282
  32. def OAI.Tachikawa.AlgebraInduction.regularIso line 286
  33. def OAI.Tachikawa.Enveloping.LeftRestrictedRegular line 320
  34. instance OAI.Tachikawa.Enveloping.(instance at line 321) line 321
  35. instance OAI.Tachikawa.Enveloping.(instance at line 322) line 322
  36. instance OAI.Tachikawa.Enveloping.(instance at line 323) line 323
  37. instance OAI.Tachikawa.Enveloping.(instance at line 324) line 324
  38. instance OAI.Tachikawa.Enveloping.(instance at line 325) line 325
  39. instance OAI.Tachikawa.Enveloping.(instance at line 329) line 329
  40. instance OAI.Tachikawa.Enveloping.(instance at line 331) line 331
  41. abbrev OAI.Tachikawa.Enveloping.leftRestrictedRegular line 334
  42. def OAI.Tachikawa.Enveloping.regularRightUnitTarget line 337
  43. def OAI.Tachikawa.Enveloping.rightIndRegularHom line 356
  44. lemma OAI.Tachikawa.Enveloping.rightIndRegularHom_mk line 360
  45. def OAI.Tachikawa.Enveloping.rightIndRegularInvLinear line 366
  46. lemma OAI.Tachikawa.Enveloping.rightIndRegularInvLinear_apply line 373
  47. lemma OAI.Tachikawa.Enveloping.rightIndRegularInvLinear_left line 380
  48. def OAI.Tachikawa.Enveloping.rightIndRegularInv line 403
  49. def OAI.Tachikawa.Enveloping.rightIndRegularIso line 412
  50. def OAI.Tachikawa.Enveloping.leftRestrictedRegularIso line 450
  51. abbrev OAI.Tachikawa.Enveloping.leftEnvelopingMap line 478
  52. def OAI.Tachikawa.Enveloping.leftIndUnit line 481
  53. lemma OAI.Tachikawa.Enveloping.leftIndUnit_apply line 515
  54. def OAI.Tachikawa.Enveloping.leftIndResMap line 522
  55. lemma OAI.Tachikawa.Enveloping.leftIndResMap_right line 535
  56. def OAI.Tachikawa.Enveloping.leftIndExtendLinear line 545
  57. lemma OAI.Tachikawa.Enveloping.leftIndExtendLinear_right line 550
  58. def OAI.Tachikawa.Enveloping.leftIndExtend line 561
  59. lemma OAI.Tachikawa.Enveloping.leftIndExtend_mk line 566
  60. lemma OAI.Tachikawa.Enveloping.leftInd_hom_ext line 574
  61. def OAI.Tachikawa.Enveloping.leftIndComparisonHom line 589
  62. def OAI.Tachikawa.Enveloping.leftIndComparisonInv line 594
  63. lemma OAI.Tachikawa.Enveloping.leftIndComparison_inv_unit line 601
  64. lemma OAI.Tachikawa.Enveloping.leftIndComparison_hom_unit line 608
  65. lemma OAI.Tachikawa.Enveloping.leftIndComparison_hom_inv line 614
  66. lemma OAI.Tachikawa.Enveloping.leftIndComparison_inv_hom line 624
  67. def OAI.Tachikawa.Enveloping.leftIndComparisonIso line 643
  68. def OAI.Tachikawa.Enveloping.leftIndComparison line 650
  69. def OAI.Tachikawa.Enveloping.leftIndUnderlyingComparison line 662
  70. abbrev OAI.Tachikawa.Enveloping.leftComplex line 675
  71. abbrev OAI.Tachikawa.Enveloping.rightComplex line 677
  72. def OAI.Tachikawa.Enveloping.leftCokerEquiv line 680
  73. def OAI.Tachikawa.Enveloping.rightCokerEquiv line 689
  74. lemma OAI.Tachikawa.Enveloping.coker_left_projective_of_homotopy line 698
  75. lemma OAI.Tachikawa.Enveloping.coker_right_projective_of_homotopy line 707
  76. def OAI.Tachikawa.transportResolution line 724
  77. lemma OAI.Tachikawa.Enveloping.rightInducedResolution_finite line 741
  78. def OAI.Tachikawa.Enveloping.rightInducedLeftResolution line 750
  79. def OAI.Tachikawa.Enveloping.inducedFactorIso line 758
  80. def OAI.Tachikawa.Enveloping.inducedLeftComplexIso line 766
  81. def OAI.Tachikawa.Enveloping.inducedLeftHomotopy line 783
  82. lemma OAI.Tachikawa.Enveloping.inducedCoker_left_projective line 791
  83. lemma OAI.Tachikawa.Enveloping.left_induction_regular_quasiIso line 805
  84. def OAI.Tachikawa.Enveloping.leftInducedResolution line 836
  85. abbrev OAI.Tachikawa.Enveloping.rightRestrictedRegular line 861
  86. def OAI.Tachikawa.Enveloping.regularLeftUnitTarget line 864
  87. def OAI.Tachikawa.Enveloping.leftIndRegularHom line 884
  88. lemma OAI.Tachikawa.Enveloping.leftIndRegularHom_mk line 888
  89. def OAI.Tachikawa.Enveloping.leftIndRegularInvLinear line 894
  90. lemma OAI.Tachikawa.Enveloping.leftIndRegularInvLinear_apply line 900
  91. lemma OAI.Tachikawa.Enveloping.leftIndRegularInvLinear_right line 907
  92. def OAI.Tachikawa.Enveloping.leftIndRegularInv line 928
  93. def OAI.Tachikawa.Enveloping.leftIndRegularIso line 934
  94. def OAI.Tachikawa.Enveloping.rightRestrictedRegularIso line 971
  95. lemma OAI.Tachikawa.Enveloping.leftInducedResolution_finite line 1000
  96. def OAI.Tachikawa.Enveloping.leftInducedRightResolution line 1009
  97. def OAI.Tachikawa.Enveloping.inducedRightFactorIso line 1017
  98. def OAI.Tachikawa.Enveloping.inducedRightComplexIso line 1025
  99. def OAI.Tachikawa.Enveloping.inducedRightHomotopy line 1042
  100. lemma OAI.Tachikawa.Enveloping.inducedCoker_right_projective line 1050
  101. abbrev OAI.Tachikawa.Construction.opTensorB line 1069
  102. abbrev OAI.Tachikawa.Construction.opTensorE line 1071
  103. def OAI.Tachikawa.Construction.tRightUnderlying line 1074
  104. lemma OAI.Tachikawa.Construction.tRightUnderlying_smul line 1086
  105. def OAI.Tachikawa.Construction.eRightTensorEquiv line 1096
  106. abbrev OAI.Tachikawa.Construction.inclusionOppTensor line 1100
  107. lemma OAI.Tachikawa.Construction.eRightTensorEquiv_action line 1103
  108. lemma OAI.Tachikawa.Construction.inclusionOppTensor_natural line 1127
  109. abbrev OAI.Tachikawa.Construction.opTensorRestriction line 1131
  110. def OAI.Tachikawa.Construction.eRightUnderlying line 1133
  111. lemma OAI.Tachikawa.Construction.eRightUnderlying_smul line 1136
  112. def OAI.Tachikawa.Construction.eRightRestrictionIso line 1148