OAI/AlgebraicGeometry/SurfaceCones/ChartDominance.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

Injectivity of every completed source-chart ring map. These are needed to transport the positive generic rank of the arbitrary input M.

  1. instance OAI.SourceConeMorphism.p_dominant line 12
  2. instance OAI.SourcePullbackChart.completedSourceChart_nontrivial line 28
  3. instance OAI.SourcePullbackChart.completedSourceChart_integral line 30
  4. instance OAI.SourcePullbackChart.completedSourceChart_domain line 32
  5. instance OAI.SourcePullbackChart.completedIota_dominant line 34
  6. def OAI.SourcePullbackChart.completedConeMap line 38

    Source documentation

    The coordinate map induced by p on the completed chart Bᵢ ⊗[S] A.

    def completedConeMap (i : Fin 3) : CommRingCat.of ExplicitCone.completedRing ⟶
    CommRingCat.of (completedSourceChart i) :=
…

    Mentions: OAI.ExplicitCone.completedRing, OAI.SourcePullbackChart.completedSourceChart

  7. lemma OAI.SourcePullbackChart.completedConeMap_spec line 42
  8. lemma OAI.SourcePullbackChart.completedConeMap_injective line 45
  9. lemma OAI.PrincipalDivisorGeneric.surjection_rank line 67
  10. lemma OAI.CoherentModelActual.affineE_surjection_rank_eq line 99
  11. def OAI.SourceExceptionalRestriction.chartModelIso line 126

    Source documentation

    The affine double-dual restriction model for P on each surface chart.

    def chartModelIso (M : ModuleCat.{0} ExplicitCone.completedRing) (i : Fin 3) :
    (restrictFunctor (surfaceIota i)).obj (P M) ≅
      (Scheme.Modules.pullback (completedZeroChart i)).obj
        (CoherentModelActual.E (Spec.map (completedConeMap i)) M) :=
…

    Mentions: OAI.ExplicitCone.completedRing, OAI.SourceExceptionalRestriction.P, OAI.CoherentModelActual.E

  12. abbrev OAI.SourceExceptionalRestriction.chartSections line 136
  13. lemma OAI.SourceExceptionalRestriction.chart_rank_eq line 140
  14. lemma OAI.SourceExceptionalRestriction.chart_rank_pos line 155
  15. def OAI.SourceZeroSections.sourceIdealChartIso line 179
  16. def OAI.SourceZeroSections.sourceIdealLine line 190

    Source documentation

    Line trivialization of the kernel ideal sheaf on W.

    def sourceIdealLine : LineTrivialization W.sheaf (idealSheaf completedSourceZero) :=
…

    Mentions: OAI.SourceZeroSections.completedSourceZero

  17. lemma OAI.SourceZeroSections.sourceIdeal_coherent line 194
  18. lemma OAI.SheafTorsion.pushforward line 210

    Source documentation

    Dominant quasi-compact pushforward between integral schemes preserves sectionwise torsion freedom.

    lemma pushforward {X Y : Scheme.{0}} [IsIntegral X] [IsIntegral Y]
    (f : X ⟶ Y) [IsDominant f] [QuasiCompact f] (M : X.Modules)
    (hM : ∀ U, @Module.IsTorsionFree (X.sheaf.obj.obj U) (M.val.obj U) _ _
      (M.val.obj U).isModule)
    (U : Y.Opensᵒᵖ) : @Module.IsTorsionFree (Y.sheaf.obj.obj U)
      (((Scheme.Modules.pushforward f).obj M).val.obj U) _ _
      (((Scheme.Modules.pushforward f).obj M).val.obj U).isModule := by
…
  19. lemma OAI.SheafTorsion.coherent_pushforward line 253

    Source documentation

    The torsion-free property is compatible with the exact finite pushforward on the coherent categories.

    lemma coherent_pushforward {X Y : Scheme.{0}} [IsIntegral X] [IsIntegral Y]
    [IsLocallyNoetherian Y] (f : X ⟶ Y) [IsDominant f] [IsFinite f]
    (M : CoherentGlobal.Coh X)
    (hM : ∀ U, @Module.IsTorsionFree (X.sheaf.obj.obj U) (M.obj.val.obj U) _ _
      (M.obj.val.obj U).isModule)
    (U : Y.Opensᵒᵖ) : @Module.IsTorsionFree (Y.sheaf.obj.obj U)
      (((CoherentGlobal.cohPushforward f).obj M).obj.val.obj U) _ _
      (((CoherentGlobal.cohPushforward f).obj M).obj.val.obj U).isModule :=
…

    Mentions: OAI.CoherentGlobal.Coh, OAI.CoherentGlobal.cohPushforward

  20. instance OAI.SourcePullbackChart.planeChart_domain line 276
  21. instance OAI.SourcePullbackChart.plane_reduced line 278
  22. def OAI.SourcePullbackChart.blowupCover line 286
  23. instance OAI.SourcePullbackChart.directionMap_flat line 303
  24. instance OAI.SourcePullbackChart.direction_flat line 311
  25. instance OAI.SourcePullbackChart.completedDirection_flat line 321
  26. instance OAI.SourcePullbackChart.source_g_schematicallyDominant line 325
  27. instance OAI.SourcePullbackChart.source_g_finite line 334
  28. instance OAI.SourcePullbackChart.source_g_surjective line 335
  29. instance OAI.SourcePullbackChart.source_V_integral line 336
  30. instance OAI.SourcePullbackChart.source_V_noetherian line 337
  31. abbrev OAI.SourcePullbackChart.modelPushforward line 340
  32. lemma OAI.SourcePullbackChart.modelPushforward_coherent line 343
  33. lemma OAI.SourcePullbackChart.modelPushforward_torsionFree line 348
  34. instance OAI.SourcePullbackChart.blowupChart_domain line 371
  35. abbrev OAI.SourcePullbackChart.chartRatio line 374
  36. lemma OAI.SourcePullbackChart.ratio_generate line 377
  37. lemma OAI.SourcePullbackChart.baseMap_restrict_isIso line 402
  38. lemma OAI.SourcePullbackChart.blowdown_restrict_isIso line 414
  39. abbrev OAI.KummerSourceModel.polynomialPuncture line 423
  40. abbrev OAI.KummerSourceModel.seriesPuncture line 425
  41. instance OAI.KummerSourceModel.blowdown_puncture_isIso line 428
  42. lemma OAI.KummerSourceModel.completion_preimage_puncture line 432
  43. instance OAI.KummerSourceModel.completedBlowdown_puncture_isIso line 441
  44. lemma OAI.SourcePullbackChart.zeroEvaluation_kernel line 466
  45. lemma OAI.SourcePullbackChart.baseFiber_regular line 476
  46. def OAI.SourcePullbackChart.zeroAlg line 482
  47. abbrev OAI.SourcePullbackChart.completedBlowupChart line 485
  48. def OAI.SourcePullbackChart.completedBlowupFiber line 492
  49. abbrev OAI.SourcePullbackChart.completedBlowupZeroIdeal line 493
  50. lemma OAI.SourcePullbackChart.completedBlowupZeroIdeal_eq line 498
  51. def OAI.SourcePullbackChart.completedPlaneQuotient line 503
  52. def OAI.SourcePullbackChart.completedPlaneEvaluation line 508
  53. lemma OAI.SourcePullbackChart.completedPlaneEvaluation_tmul line 511
  54. lemma OAI.SourcePullbackChart.completedPlaneEvaluation_surjective line 520
  55. lemma OAI.SourcePullbackChart.completedPlaneEvaluation_kernel line 523
  56. lemma OAI.SourcePullbackChart.completedBlowupFiber_regular line 531
  57. def OAI.SourcePullbackChart.baseChartFirst line 549
  58. def OAI.SourcePullbackChart.baseChartSecond line 551
  59. lemma OAI.SourcePullbackChart.baseChartTensor_isPullback line 554
  60. def OAI.SourcePullbackChart.completedBlowupIota line 567
  61. lemma OAI.SourcePullbackChart.completedBlowupIota_first line 571
  62. lemma OAI.SourcePullbackChart.completedBlowupIota_second line 574
  63. lemma OAI.SourcePullbackChart.completedBlowupIota_isPullback line 578
  64. instance OAI.SourcePullbackChart.(instance at line 588) line 588
  65. lemma OAI.SourcePullbackChart.completedBlowupIota_opensRange line 592
  66. lemma OAI.SourcePullbackChart.completedBlowupCover line 600
  67. lemma OAI.SourcePullbackChart.completedPlaneEvaluation_left line 607
  68. lemma OAI.SourcePullbackChart.completedPlaneEvaluation_right line 615
  69. abbrev OAI.SourcePullbackChart.completedPlaneZeroChart line 625
  70. lemma OAI.SourcePullbackChart.completedPlaneZeroChart_first line 628
  71. lemma OAI.SourcePullbackChart.completedPlaneZeroChart_second line 633
  72. lemma OAI.SourcePullbackChart.planeIota_completedPlaneZero line 639
  73. lemma OAI.SourcePullbackChart.planeZero_chart_preimage line 649
  74. lemma OAI.SourcePullbackChart.completedPlaneZeroChart_isPullback line 658
  75. instance OAI.SourcePullbackChart.completedBlowupChart_noetherian line 665
  76. def OAI.SourcePullbackChart.blowupInAlg line 687
  77. def OAI.SourcePullbackChart.completedProjectionMap line 690
  78. lemma OAI.SourcePullbackChart.completedProjectionMap_tmul line 693
  79. lemma OAI.SourcePullbackChart.completedProjectionMap_fiber line 696
  80. abbrev OAI.SourcePullbackChart.completedProjection line 699
  81. lemma OAI.SourcePullbackChart.completedProjection_first line 703
  82. lemma OAI.SourcePullbackChart.completedProjection_second line 709
  83. lemma OAI.SourcePullbackChart.completedIota_projection line 714
  84. lemma OAI.SourcePullbackChart.completedProjection_chart_preimage line 724
  85. lemma OAI.SourcePullbackChart.completedProjection_isPullback line 730
  86. lemma OAI.SourcePullbackChart.completedProjection_zero line 737
  87. lemma OAI.SourcePullbackChart.completedClosedChart_commute line 772
  88. lemma OAI.SourcePullbackChart.completedClosedChart_isPullback line 778
  89. lemma OAI.SourcePullbackChart.completedClosedChart_isPushout line 785
  90. def OAI.AffineClosedBaseChange.moduleIso line 807

    Source documentation

    The coordinate-ring base-change isomorphism, with the restriction and extension of scalars in both corners.

    def moduleIso (M : ModuleCat C) :
    (ModuleCat.extendScalars z.hom).obj ((ModuleCat.restrictScalars f.hom).obj M) ≅
      (ModuleCat.restrictScalars q.hom).obj ((ModuleCat.extendScalars w.hom).obj M) := by
…
  91. def OAI.AffineClosedBaseChange.tildeIso line 825

    Source documentation

    The base-change isomorphism for quasicoherent sheaves on spectra.

    def tildeIso (M : ModuleCat C) :
    (Scheme.Modules.pullback (Spec.map z)).obj
      ((Scheme.Modules.pushforward (Spec.map f)).obj (tilde M)) ≅
    (Scheme.Modules.pushforward (Spec.map q)).obj
      ((Scheme.Modules.pullback (Spec.map w)).obj (tilde M)) :=
…
  92. def OAI.AffineClosedBaseChange.sheafIso line 836