OAI/RingTheory/Tachikawa/Socle.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Tachikawa.Construction.T line 12
  2. abbrev OAI.Tachikawa.Construction.E line 13
  3. def OAI.Tachikawa.Construction.characterT line 15
  4. def OAI.Tachikawa.Construction.characterE line 17
  5. def OAI.Tachikawa.Construction.formE line 20
  6. def OAI.Tachikawa.Construction.X line 23
  7. instance OAI.Tachikawa.Construction.(instance at line 24) line 24
  8. instance OAI.Tachikawa.Construction.(instance at line 25) line 25
  9. instance OAI.Tachikawa.Construction.(instance at line 26) line 26
  10. instance OAI.Tachikawa.Construction.(instance at line 27) line 27
  11. instance OAI.Tachikawa.Construction.(instance at line 32) line 32
  12. instance OAI.Tachikawa.Construction.(instance at line 33) line 33
  13. lemma OAI.Tachikawa.Construction.X_smul line 35
  14. def OAI.Tachikawa.Construction.sigma line 37
  15. lemma OAI.Tachikawa.Construction.characterT_scaleDual line 41
  16. lemma OAI.Tachikawa.Construction.characterE_sigma line 44
  17. lemma OAI.Tachikawa.Construction.formE_sigma line 50
  18. abbrev OAI.Tachikawa.Construction.sFinite line 68
  19. abbrev OAI.Tachikawa.Construction.sResolution line 70
  20. abbrev OAI.Tachikawa.Construction.XTensorObj line 71
  21. def OAI.Tachikawa.Construction.XExtKunneth line 74
  22. lemma OAI.Tachikawa.Construction.XExt_zero_off_multiples line 81
  23. lemma OAI.Tachikawa.Construction.XExtThree_nontrivial line 98
  24. lemma OAI.Tachikawa.Construction.XTensor_nonprojective line 113
  25. instance OAI.Tachikawa.Construction.simpleTwist_preserves_projective line 131
  26. def OAI.Tachikawa.Construction.simpleResolutionTwistLift line 137
  27. abbrev OAI.Tachikawa.Construction.simpleResolutionTwist line 142
  28. lemma OAI.Tachikawa.Construction.simpleResolutionTwist_scalar line 146
  29. abbrev OAI.Tachikawa.Construction.eTwist line 170
  30. abbrev OAI.Tachikawa.Construction.XTensorTwistIso line 171
  31. abbrev OAI.Tachikawa.Construction.xTensorTwistLift line 174
  32. abbrev OAI.Tachikawa.Construction.xTensorResolution line 178
  33. abbrev OAI.Tachikawa.Construction.xTensorTwist line 179
  34. lemma OAI.Tachikawa.Construction.tensorHom_twist_scalar line 183
  35. lemma OAI.Tachikawa.Construction.xTensorTwist_homology_scalar line 216
  36. lemma OAI.Tachikawa.Construction.XTensorTwist_weight line 229
  37. def OAI.Tachikawa.Construction.sCanon line 245
  38. def OAI.Tachikawa.Construction.simpleUnderlying line 248
  39. lemma OAI.Tachikawa.Construction.simpleUnderlying_smul line 260
  40. def OAI.Tachikawa.Construction.XTensorUnderlying line 264
  41. lemma OAI.Tachikawa.Construction.XTensorUnderlying_smul line 268
  42. def OAI.Tachikawa.Construction.XTensorEquiv line 285
  43. def OAI.Tachikawa.Construction.XTensorIso line 294
  44. def OAI.Tachikawa.Construction.XExt line 296
  45. lemma OAI.Tachikawa.Construction.X_nonprojective line 302
  46. lemma OAI.Tachikawa.Construction.XExt_zero line 309
  47. lemma OAI.Tachikawa.extIso_trans line 324
  48. lemma OAI.Tachikawa.extIso_map line 333
  49. lemma OAI.Tachikawa.extTwist_weight_transport line 341
  50. def OAI.Tachikawa.Construction.zT line 363
  51. def OAI.Tachikawa.Construction.pT line 364
  52. def OAI.Tachikawa.Construction.zeta line 365
  53. def OAI.Tachikawa.Construction.pE line 366
  54. lemma OAI.Tachikawa.Construction.zT_left line 368
  55. lemma OAI.Tachikawa.Construction.zT_right line 378
  56. lemma OAI.Tachikawa.Construction.zeta_left line 388
  57. lemma OAI.Tachikawa.Construction.zeta_right line 396
  58. lemma OAI.Tachikawa.Construction.formE_zeta line 404
  59. lemma OAI.Tachikawa.Construction.zeta_ne_zero line 408
  60. lemma OAI.Tachikawa.Construction.characterE_zeta line 414
  61. lemma OAI.Tachikawa.Construction.characterE_pE line 418
  62. lemma OAI.Tachikawa.Construction.pE_idempotent line 422
  63. def OAI.Tachikawa.Construction.socleEmbedding line 430
  64. lemma OAI.Tachikawa.Construction.socleEmbedding_injective line 438
  65. def OAI.Tachikawa.Construction.presentation line 448
  66. def OAI.Tachikawa.Construction.OmegaX line 455
  67. instance OAI.Tachikawa.Construction.(instance at line 456) line 456
  68. instance OAI.Tachikawa.Construction.(instance at line 457) line 457
  69. instance OAI.Tachikawa.Construction.(instance at line 458) line 458
  70. instance OAI.Tachikawa.Construction.(instance at line 459) line 459
  71. lemma OAI.Tachikawa.Construction.socleEmbedding_corner line 461
  72. def OAI.Tachikawa.Construction.socleInOmega line 466
  73. lemma OAI.Tachikawa.Construction.socleInOmega_ne_zero line 472
  74. lemma OAI.Tachikawa.Construction.socleInOmega_not_factors line 480
  75. lemma OAI.Tachikawa.Construction.socleInOmega_stable_ne_zero line 500
  76. lemma OAI.Tachikawa.Construction.scaleDual_zT line 513
  77. lemma OAI.Tachikawa.Construction.sigma_zeta line 519
  78. lemma OAI.Tachikawa.Construction.sigma_pE line 524
  79. abbrev OAI.Tachikawa.Construction.twistE line 530
  80. def OAI.Tachikawa.Construction.presentationTwistComparison line 533
  81. def OAI.Tachikawa.Construction.XTwistComparison line 551
  82. lemma OAI.Tachikawa.Construction.presentationTwist_commutes line 564
  83. def OAI.Tachikawa.Construction.OmegaTwistComparison line 572
  84. lemma OAI.Tachikawa.Construction.socle_twist_weight line 585
  85. def OAI.Tachikawa.Construction.XTwistIso line 606
  86. lemma OAI.Tachikawa.Construction.XTwistIso_hom line 610
  87. lemma OAI.Tachikawa.Construction.XTwist_weight line 630
  88. lemma OAI.Tachikawa.Construction.sigma_symm line 646
  89. def OAI.Tachikawa.Construction.XInverseTwistIso line 655
  90. lemma OAI.Tachikawa.Construction.XInverseTwistIso_hom_apply line 675
  91. lemma OAI.Tachikawa.Construction.XTwist_weight_of_eq line 677
  92. lemma OAI.Tachikawa.Construction.XInverseTwist_weight line 694