OAI/NumberTheory/PiExponent/Cohomology/FiniteCoverCohomology.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponentSeshadri.schemeUnit line 9
  2. def OAI.PiExponentSeshadri.AdicInjective.adicTorsion line 17
  3. lemma OAI.PiExponentSeshadri.AdicInjective.torsion_mono line 20
  4. lemma OAI.PiExponentSeshadri.AdicInjective.mem_adicTorsion line 23
  5. lemma OAI.PiExponentSeshadri.AdicInjective.fg_uniform_exponent line 28
  6. lemma OAI.PiExponentSeshadri.AdicInjective.exists_power_inf_le line 38
  7. theorem OAI.PiExponentSeshadri.AdicInjective.adicTorsion_injective line 47
  8. lemma OAI.PiExponentSeshadri.InjectiveRange.injective_of_retract line 106
  9. lemma OAI.PiExponentSeshadri.InjectiveRange.range_injective line 118
  10. lemma OAI.PiExponentSeshadri.InjectiveRange.surjective_of_torsion_cokernel line 138
  11. abbrev OAI.PiExponentSeshadri.AffineDenominators.schemeBasicOpen line 167
  12. lemma OAI.PiExponentSeshadri.AffineDenominators.schemeBasicOpen_mul line 169
  13. lemma OAI.PiExponentSeshadri.AffineDenominators.schemeBasicOpen_mul_le_left line 173
  14. lemma OAI.PiExponentSeshadri.AffineDenominators.schemeBasicOpen_mul_le_right line 177
  15. lemma OAI.PiExponentSeshadri.AffineDenominators.schemeIsSMulRegular line 181
  16. structure OAI.PiExponentSeshadri.AffineDenominators.Aux line 185
  17. lemma OAI.PiExponentSeshadri.AffineDenominators.Aux.of_le line 192
  18. lemma OAI.PiExponentSeshadri.AffineDenominators.Aux.of_eq_iSup_basicOpen line 207
  19. lemma OAI.PiExponentSeshadri.AffineDenominators.isLocalizing_iff_aux line 323
  20. theorem OAI.PiExponentSeshadri.AffineDenominators.aux_of_isCompact line 341
  21. def OAI.PiExponentSeshadri.AffineDenominators.res line 350
  22. lemma OAI.PiExponentSeshadri.AffineDenominators.res_comp line 353
  23. lemma OAI.PiExponentSeshadri.AffineDenominators.eq_zero_of_cover line 357
  24. lemma OAI.PiExponentSeshadri.AffineDenominators.power_in_ideal_of_generator_powers line 367
  25. lemma OAI.PiExponentSeshadri.AffineDenominators.kernel_is_torsion line 376
  26. lemma OAI.PiExponentSeshadri.AffineDenominators.torsion_free line 390
  27. lemma OAI.PiExponentSeshadri.AffineDenominators.torsion_in_kernel line 402
  28. lemma OAI.PiExponentSeshadri.AffineDenominators.cokernel_is_torsion line 411
  29. theorem OAI.PiExponentSeshadri.TildeFlasque.top_surjective line 446
  30. theorem OAI.PiExponentSeshadri.TildeFlasque.flasque_of_injective_global line 466
  31. instance OAI.PiExponentSeshadri.TildeFlasque.tilde_injective_isFlasque line 478
  32. instance OAI.PiExponentSeshadri.TildeExact.map_mono line 493
  33. instance OAI.PiExponentSeshadri.TildeExact.preservesMonomorphisms line 503
  34. instance OAI.PiExponentSeshadri.TildeExact.preservesHomology line 506
  35. instance OAI.PiExponentSeshadri.TildeExact.preservesFiniteLimits line 509
  36. instance OAI.PiExponentSeshadri.ModuleGrothendieck.presheafAB5 line 519
  37. instance OAI.PiExponentSeshadri.ModuleGrothendieck.presheafHasSeparator line 523
  38. instance OAI.PiExponentSeshadri.ModuleGrothendieck.presheafGrothendieck line 527
  39. instance OAI.PiExponentSeshadri.ModuleGrothendieck.sheafAB5 line 532
  40. lemma OAI.PiExponentSeshadri.ModuleGrothendieck.freeSheafSeparating line 536
  41. instance OAI.PiExponentSeshadri.ModuleGrothendieck.sheafHasSeparator line 550
  42. instance OAI.PiExponentSeshadri.ModuleGrothendieck.sheafGrothendieck line 555
  43. theorem OAI.PiExponentSeshadri.ModuleGrothendieck.enoughInjectives line 557
  44. abbrev OAI.PiExponentSeshadri.ModuleFlasque.freeOpen line 567
  45. abbrev OAI.PiExponentSeshadri.ModuleFlasque.freeOpenMap line 571
  46. lemma OAI.PiExponentSeshadri.ModuleFlasque.freeMap_mono line 575
  47. instance OAI.PiExponentSeshadri.ModuleFlasque.freeOpenMap_mono line 583
  48. def OAI.PiExponentSeshadri.ModuleFlasque.freeOpenEquiv line 588
  49. lemma OAI.PiExponentSeshadri.ModuleFlasque.freeYoneda_naturality line 593
  50. lemma OAI.PiExponentSeshadri.ModuleFlasque.freeOpenEquiv_naturality line 604
  51. theorem OAI.PiExponentSeshadri.ModuleFlasque.restriction_surjective line 616
  52. instance OAI.PiExponentSeshadri.ModuleFlasque.injective_isFlasque line 625
  53. abbrev OAI.PiExponentSeshadri.schemeFreeOpen line 633
  54. instance OAI.PiExponentSeshadri.ModuleSheafExact.toSheafPreservesColimit line 642
  55. instance OAI.PiExponentSeshadri.ModuleSheafExact.toSheafPreservesColimits line 658
  56. theorem OAI.PiExponentSeshadri.ModuleSheafExact.shortExact_map line 662
  57. def OAI.PiExponentSeshadri.FlasqueCohomology.sectionsTopEquiv line 674
  58. def OAI.PiExponentSeshadri.FlasqueCohomology.globalHomEquiv line 691
  59. lemma OAI.PiExponentSeshadri.FlasqueCohomology.globalHomEquiv_comp line 695
  60. theorem OAI.PiExponentSeshadri.FlasqueCohomology.globalHom_surjective line 699
  61. instance OAI.PiExponentSeshadri.FlasqueCohomology.moduleSheafHasExt line 718
  62. theorem OAI.PiExponentSeshadri.FlasqueCohomology.flasque_ext_zero line 721
  63. lemma OAI.PiExponentSeshadri.AffineCohomology.globalHom_tilde_surjective line 760
  64. theorem OAI.PiExponentSeshadri.AffineCohomology.tilde_ext_zero line 776
  65. theorem OAI.PiExponentSeshadri.AffineCohomology.quasicoherent_ext_zero line 808
  66. instance OAI.PiExponentSeshadri.RestrictionExact.restriction_mono line 824
  67. instance OAI.PiExponentSeshadri.RestrictionExact.restriction_preservesMonomorphisms line 832
  68. instance OAI.PiExponentSeshadri.RestrictionExact.restriction_additive line 836
  69. instance OAI.PiExponentSeshadri.RestrictionExact.restriction_preservesHomology line 839
  70. instance OAI.PiExponentSeshadri.RestrictionExact.restriction_preservesFiniteLimits line 843
  71. instance OAI.PiExponentSeshadri.RestrictionExact.restriction_flasque line 847
  72. def OAI.PiExponentSeshadri.AffineSchemeCohomology.restrictionEquivalence line 863
  73. theorem OAI.PiExponentSeshadri.AffineSchemeCohomology.affine_ext_zero line 872
  74. def OAI.PiExponentSeshadri.ExtSectionComparison.mapFrom line 907
  75. lemma OAI.PiExponentSeshadri.ExtSectionComparison.mapFrom_apply line 910
  76. lemma OAI.PiExponentSeshadri.ExtSectionComparison.mapFrom_mk₀ line 913
  77. lemma OAI.PiExponentSeshadri.ExtSectionComparison.mapFrom_comp line 917
  78. theorem OAI.PiExponentSeshadri.ExtSectionComparison.mapFrom_bijective line 924
  79. lemma OAI.PiExponentSeshadri.RestrictionCohomology.freeOpenEquiv_comp line 977
  80. def OAI.PiExponentSeshadri.RestrictionCohomology.restrictionSectionsIso line 982
  81. def OAI.PiExponentSeshadri.RestrictionCohomology.restrictionHomEquiv line 985
  82. lemma OAI.PiExponentSeshadri.RestrictionCohomology.restrictionHomEquiv_comp line 992
  83. def OAI.PiExponentSeshadri.RestrictionCohomology.restrictionGenerator line 1010
  84. lemma OAI.PiExponentSeshadri.RestrictionCohomology.restrictionGenerator_comp line 1014
  85. theorem OAI.PiExponentSeshadri.RestrictionCohomology.restriction_ext_bijective line 1021
  86. def OAI.PiExponentSeshadri.ModuleMayerVietoris.freeOpenFunctor line 1052
  87. lemma OAI.PiExponentSeshadri.ModuleMayerVietoris.freeOpen_isPushout line 1055
  88. def OAI.PiExponentSeshadri.ModuleMayerVietoris.shortComplex line 1070
  89. instance OAI.PiExponentSeshadri.ModuleMayerVietoris.shortComplex_mono line 1081
  90. lemma OAI.PiExponentSeshadri.ModuleMayerVietoris.shortComplex_shortExact line 1088
  91. lemma OAI.PiExponentSeshadri.ModuleMayerVietoris.union_ext_zero line 1097
  92. theorem OAI.PiExponentSeshadri.FiniteCoverCohomology.affine_open_ext_zero line 1125
  93. theorem OAI.PiExponentSeshadri.FiniteCoverCohomology.affine_union_ext_zero line 1139
  94. def OAI.PiExponentSeshadri.FreeOpenUnit.isoFromHomEquiv line 1182
  95. def OAI.PiExponentSeshadri.FreeOpenUnit.freeTopIso line 1196
  96. theorem OAI.PiExponentSeshadri.FiniteCoverCohomology.cover_ext_zero line 1216