OAI/RingTheory/Tachikawa/Delta.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Tachikawa.Enveloping.(instance at line 13) line 13
  2. lemma OAI.Tachikawa.Enveloping.evalMap_smul line 27
  3. def OAI.Tachikawa.Construction.WZeroEquiv line 41
  4. def OAI.Tachikawa.Construction.wZero line 44
  5. lemma OAI.Tachikawa.Construction.wZero_ne_zero line 46
  6. def OAI.Tachikawa.Construction.evaluatedStableMap line 53
  7. lemma OAI.Tachikawa.Construction.exists_normalized_map line 67
  8. def OAI.Tachikawa.Construction.normalizedMap line 80
  9. lemma OAI.Tachikawa.Construction.normalizedMap_class line 83
  10. lemma OAI.Tachikawa.projective_kernel_of_surjective line 94
  11. def OAI.Tachikawa.Enveloping.leftProdEquiv line 112
  12. def OAI.Tachikawa.Enveloping.rightProdEquiv line 121
  13. def OAI.Tachikawa.Enveloping.fiberCover line 132
  14. def OAI.Tachikawa.Enveloping.fiberMiddle line 133
  15. def OAI.Tachikawa.Enveloping.fiberProjection line 136
  16. lemma OAI.Tachikawa.Enveloping.fiberProjection_surjective line 140
  17. def OAI.Tachikawa.Enveloping.fiber line 147
  18. def OAI.Tachikawa.Enveloping.fiberInclusion line 157
  19. lemma OAI.Tachikawa.Enveloping.fiberInclusion_injective line 160
  20. lemma OAI.Tachikawa.Enveloping.fiber_exact line 163
  21. lemma OAI.Tachikawa.Enveloping.fiber_left_projective line 167
  22. lemma OAI.Tachikawa.Enveloping.fiber_right_projective line 180
  23. def OAI.Tachikawa.Construction.concreteF line 205
  24. lemma OAI.Tachikawa.Construction.concreteF_side_projective line 209
  25. abbrev OAI.Tachikawa.Construction.concreteMiddle line 230
  26. abbrev OAI.Tachikawa.Construction.concreteProjection line 231
  27. abbrev OAI.Tachikawa.Construction.concreteInclusion line 233
  28. lemma OAI.Tachikawa.Construction.concrete_evaluated_injective line 236
  29. lemma OAI.Tachikawa.Construction.concrete_evaluated_exact line 245
  30. lemma OAI.Tachikawa.Construction.concrete_evaluated_surjective line 256
  31. def OAI.Tachikawa.Enveloping.fiberInl line 270
  32. def OAI.Tachikawa.Enveloping.fiberInm line 271
  33. def OAI.Tachikawa.Enveloping.fiberInr line 273
  34. def OAI.Tachikawa.Enveloping.fiberFst line 275
  35. def OAI.Tachikawa.Enveloping.fiberSnd line 276
  36. lemma OAI.Tachikawa.Enveloping.fiberInl_fst line 279
  37. lemma OAI.Tachikawa.Enveloping.fiberInl_snd line 280
  38. lemma OAI.Tachikawa.Enveloping.fiberInm_fst line 281
  39. lemma OAI.Tachikawa.Enveloping.fiberInm_snd line 282
  40. lemma OAI.Tachikawa.Enveloping.fiberInr_fst line 283
  41. lemma OAI.Tachikawa.Enveloping.fiberInr_snd line 284
  42. lemma OAI.Tachikawa.Enveloping.fiberInl_projection line 287
  43. lemma OAI.Tachikawa.Enveloping.fiberInm_projection line 291
  44. lemma OAI.Tachikawa.Enveloping.fiberInr_projection line 295
  45. lemma OAI.Tachikawa.exists_stable_kernel_lift line 310
  46. abbrev OAI.Tachikawa.Construction.concreteFst line 351
  47. abbrev OAI.Tachikawa.Construction.concreteSnd line 353
  48. lemma OAI.Tachikawa.Construction.exists_concrete_vZero line 356
  49. def OAI.Tachikawa.Construction.concreteVZero line 450
  50. lemma OAI.Tachikawa.Construction.concreteVZero_fst line 451
  51. lemma OAI.Tachikawa.Construction.concreteVZero_snd line 454
  52. lemma OAI.Tachikawa.completeHpair_bijective line 475
  53. def OAI.Tachikawa.Enveloping.fiberThird line 518
  54. lemma OAI.Tachikawa.Enveloping.fiber_sum_id line 522
  55. abbrev OAI.Tachikawa.Construction.XHom line 546
  56. abbrev OAI.Tachikawa.Construction.FHom line 547
  57. abbrev OAI.Tachikawa.Construction.middleHom line 549
  58. abbrev OAI.Tachikawa.Construction.FHomInclusion line 551
  59. abbrev OAI.Tachikawa.Construction.FHomProjection line 553
  60. lemma OAI.Tachikawa.Construction.FHom_shortExact line 556
  61. def OAI.Tachikawa.Construction.middleHpair line 567
  62. lemma OAI.Tachikawa.Construction.middleHpair_bijective line 574
  63. lemma OAI.Tachikawa.Construction.FHomInclusion_bijective line 611
  64. lemma OAI.Tachikawa.VectorSplit.Hmap_exact line 631
  65. abbrev OAI.Tachikawa.Construction.zeroHomEquiv line 677
  66. lemma OAI.Tachikawa.Construction.FHomProjection_zero_surjective line 682
  67. lemma OAI.Tachikawa.Construction.FHomInclusion_one_bijective line 716
  68. def OAI.Tachikawa.Construction.middleHpairX line 724
  69. lemma OAI.Tachikawa.Construction.middleHpairX_bijective line 730
  70. def OAI.Tachikawa.Construction.FHomPair line 734
  71. lemma OAI.Tachikawa.Construction.middleHom_zero line 738
  72. lemma OAI.Tachikawa.Construction.FHomInclusion_injective line 743
  73. lemma OAI.Tachikawa.Construction.FHom_minusThree_zero line 749
  74. lemma OAI.Tachikawa.Construction.FHomPair_bijective line 755
  75. lemma OAI.Tachikawa.Enveloping.evalMap_comp line 776
  76. lemma OAI.Tachikawa.Enveloping.completeHmap_eval_comp line 779
  77. lemma OAI.Tachikawa.Construction.uXIso_hom_twist line 796
  78. lemma OAI.Tachikawa.Construction.uXIso_inv_twist line 809
  79. abbrev OAI.Tachikawa.Construction.concreteLift line 828
  80. abbrev OAI.Tachikawa.Construction.FAction line 830
  81. abbrev OAI.Tachikawa.Construction.VAction line 833
  82. abbrev OAI.Tachikawa.Construction.FFirst line 835
  83. abbrev OAI.Tachikawa.Construction.FSecond line 838
  84. lemma OAI.Tachikawa.Construction.FHomPair_eq line 842
  85. lemma OAI.Tachikawa.Construction.FAction_first line 867
  86. lemma OAI.Tachikawa.Construction.FAction_second line 879
  87. lemma OAI.Tachikawa.Construction.VAction_first line 891
  88. lemma OAI.Tachikawa.Construction.VAction_second line 893
  89. def OAI.Tachikawa.scalarPair line 903
  90. lemma OAI.Tachikawa.scalarPair_bijective line 907
  91. def OAI.Tachikawa.Construction.delta line 946
  92. lemma OAI.Tachikawa.Construction.delta_pair line 951
  93. lemma OAI.Tachikawa.Construction.delta_bijective_weights line 966
  94. lemma OAI.Tachikawa.Construction.delta_bijective_of_zero line 981
  95. lemma OAI.Tachikawa.Construction.delta_minusTwo_injective line 989
  96. abbrev OAI.Tachikawa.SourceField.sourceDelta line 997
  97. lemma OAI.Tachikawa.SourceField.sourceDelta_positive line 1000
  98. lemma OAI.Tachikawa.SourceField.sourceDelta_negative line 1010
  99. lemma OAI.Tachikawa.SourceField.sourceDelta_bijective line 1017
  100. lemma OAI.Tachikawa.exact_line_surjective line 1035
  101. lemma OAI.Tachikawa.Construction.VAction_injective line 1064
  102. lemma OAI.Tachikawa.Construction.VAction_zero_surjective line 1075
  103. lemma OAI.Tachikawa.Construction.delta_zero_surjective line 1090
  104. theorem OAI.Tachikawa.SourceField.sourceDelta_vanishing_ranges line 1102