OAI/AlgebraicGeometry/SurfaceCones/AffineLineEpiIso.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

Conormal lines and generators on completed surface cones

This development accompanies A Complete Local Domain without a Small Cohen–Macaulay Module (OpenAI, 2026).

  1. lemma OAI.ActualAffineLine.gamma_epi line 37
  2. lemma OAI.ActualAffineLine.unit_endo_isIso line 53
  3. lemma OAI.ActualAffineLine.epi_isIso line 77
  4. def OAI.SourcePullbackChart.closedStructureBaseChangeIso line 108

    Source documentation

    The composite of base change with the pullback unit isomorphism.

    def closedStructureBaseChangeIso :
    (Scheme.Modules.pullback g).obj ((pushforward completedPlaneZero).obj
      (SheafOfModules.unit ExplicitCone.plane.ringCatSheaf)) ≅
    (pushforward completedSourceZero).obj (SheafOfModules.unit ExplicitCone.projectiveSurface.ringCatSheaf) := by
…
  5. lemma OAI.SourcePullbackChart.closedStructureBaseChange_comm line 119
  6. def OAI.SourcePullbackChart.idealBaseChange line 127

    Source documentation

    The canonical morphism from the pulled-back ideal to the ideal.

    def idealBaseChange : (Scheme.Modules.pullback g).obj (idealSheaf completedPlaneZero) ⟶
    idealSheaf completedSourceZero :=
…
  7. instance OAI.SourcePullbackChart.idealBaseChange_epi line 133
  8. lemma OAI.SourcePullbackChart.idealBaseChange_ι line 139
  9. def OAI.SourcePullbackChart.pulledPlaneIdealChartIso line 144

    Source documentation

    Pulled-back plane ideal, on the completed source chart.

    def pulledPlaneIdealChartIso (i : Fin 3) :
    (restrictFunctor (completedIota i)).obj
      ((Scheme.Modules.pullback g).obj (idealSheaf completedPlaneZero)) ≅
    SheafOfModules.unit (Spec (.of (completedSourceChart i))).ringCatSheaf :=
…

    Mentions: OAI.SourcePullbackChart.completedIota, OAI.SourcePullbackChart.completedSourceChart

  10. lemma OAI.SourcePullbackChart.idealBaseChange_chart_isIso line 156
  11. instance OAI.SourcePullbackChart.idealBaseChange_isIso line 160
  12. def OAI.SourcePullbackChart.idealBaseChangeIso line 174
  13. def OAI.SourcePullbackChart.conormalBaseChangeIso line 178

    Source documentation

    The conormal identity i*J ≅ f*(z*I) for the two kernel ideals.

    def conormalBaseChangeIso :
    (Scheme.Modules.pullback completedSourceZero).obj (idealSheaf completedSourceZero) ≅
    (Scheme.Modules.pullback ExplicitCone.projectiveNormalization).obj
      ((Scheme.Modules.pullback completedPlaneZero).obj (idealSheaf completedPlaneZero)) :=
…

    Mentions: OAI.ExplicitCone.projectiveNormalization

  14. def OAI.ActualSections.restrictTop line 197
  15. def OAI.ActualSections.family line 200
  16. def OAI.ActualSections.fromUnit line 206
  17. lemma OAI.ActualSections.fromUnit_app line 209
  18. lemma OAI.ActualSections.fromUnit_top line 214
  19. lemma OAI.ActualSections.fromUnit_comp line 224
  20. abbrev OAI.ActualSections.scalar line 233
  21. def OAI.ActualCartier.idealGlobalSection line 241
  22. lemma OAI.ActualCartier.idealGlobalSection_ι line 245
  23. def OAI.ActualCartier.idealGenerator line 250
  24. lemma OAI.ActualCartier.idealGenerator_ι line 254
  25. lemma OAI.ActualAffineLine.isIso_of_top_bijective line 269
  26. lemma OAI.ActualSections.restrictScalar_top line 294
  27. def OAI.ActualCartier.chartGenerator line 316
  28. lemma OAI.ActualCartier.chartGenerator_section line 320
  29. lemma OAI.ActualCartier.chartGenerator_isIso line 334
  30. lemma OAI.SourcePullbackChart.completedBlowupFiber_eq_right line 369
  31. def OAI.SourcePullbackChart.planeParameter line 376
  32. lemma OAI.SourcePullbackChart.planeParameter_killed line 379
  33. lemma OAI.SourcePullbackChart.planeParameter_chart line 393
  34. def OAI.SourcePullbackChart.planeIdealGenerator line 406
  35. lemma OAI.SourcePullbackChart.planeIdealGenerator_chart_isIso line 410
  36. lemma OAI.CoherentGlobal.hom_ext_of_open_charts line 438
  37. lemma OAI.CoherentGlobal.epi_of_open_charts line 450
  38. def OAI.SourcePullbackChart.planeIdealPresentation line 473
  39. lemma OAI.SourcePullbackChart.planeIdealPresentation_generator line 476
  40. instance OAI.SourcePullbackChart.planeIdealPresentation_epi line 480
  41. def OAI.SourcePullbackChart.pullbackFreeIso line 494
  42. def OAI.SourcePullbackChart.planeConormalPresentation line 501
  43. instance OAI.SourcePullbackChart.planeConormalPresentation_epi line 507
  44. def OAI.SourcePullbackChart.sourceConormalPresentation line 517
  45. instance OAI.SourcePullbackChart.sourceConormalPresentation_epi line 524
  46. theorem OAI.SourcePullbackChart.sourceConormal_generated line 540

    Source documentation

    Global generation by three global sections on the source surface. The target is the conormal to its completed zero section.

    theorem sourceConormal_generated : ∃ (φ :
    SheafOfModules.free (R := ExplicitCone.projectiveSurface.ringCatSheaf) (Fin 3) ⟶
…
  47. def OAI.ActualChartPullback.squareIso line 557
  48. lemma OAI.ActualChartPullback.map_isIso line 564
  49. lemma OAI.CoherentChartRank.module_add line 579
  50. lemma OAI.CoherentChartRank.affineGamma_shortExact line 591
  51. abbrev OAI.CoherentChartRank.chartSections line 604
  52. lemma OAI.CoherentChartRank.chartSections_finite line 608
  53. lemma OAI.CoherentChartRank.chart_add line 615
  54. abbrev OAI.SourceConeMorphism.surfaceChartRank line 654
  55. def OAI.SourceConeMorphism.conormalChartUnitIso line 657
  56. def OAI.SourceConeMorphism.conormalChartIso line 665
  57. lemma OAI.SourceConeMorphism.conormal_rank line 673
  58. lemma OAI.SourceConeMorphism.elementaryTransform_rank line 679
  59. lemma OAI.SourceConeMorphism.initial_restriction_rank line 699
  60. def OAI.SourcePullbackChart.sourceIdealGenerator line 725
  61. lemma OAI.SourcePullbackChart.sourceIdealGenerator_chart_isIso line 730
  62. def OAI.SourcePullbackChart.sourceConormalGenerator line 743
  63. lemma OAI.SourcePullbackChart.sourceConormalGenerator_chart_isIso line 749
  64. def OAI.SourcePullbackChart.sourceConormalFrame line 761

    Source documentation

    Line trivializations induced by these global sections.

    def sourceConormalFrame (i : Fin 3) :
    (restrictFunctor (surfaceIota i)).obj
      ((Scheme.Modules.pullback completedSourceZero).obj (idealSheaf completedSourceZero)) ≅
        SheafOfModules.unit (Spec (.of (surfaceChart i))).ringCatSheaf := by
…

    Mentions: OAI.SourcePullbackChart.surfaceIota, OAI.SourcePullbackChart.surfaceChart

  65. def OAI.SourcePullbackChart.sourceConormalLine line 769
  66. lemma OAI.ActualSections.unitHom_ext_top line 784
  67. lemma OAI.ActualCartier.chartGenerator_ratio line 806
  68. def OAI.SourcePullbackChart.planeTransitionCoefficient line 833

    Source documentation

    The pullback of the projective coordinate x_j/x_i to V_i.

    def planeTransitionCoefficient (i j : Fin 3) : completedBlowupChart i :=
…

    Mentions: OAI.SourcePullbackChart.completedBlowupChart

  69. lemma OAI.SourcePullbackChart.planeTransitionCoefficient_mul_fiber line 836
  70. lemma OAI.SourcePullbackChart.planeParameter_on_chart line 847
  71. lemma OAI.SourcePullbackChart.planeParameter_chart_ratio line 858
  72. lemma OAI.SourcePullbackChart.planeIdealGenerator_chart_ratio line 865
  73. lemma OAI.SourcePullbackChart.planeTransitionCoefficient_residue line 876