OAI/AlgebraicGeometry/SurfaceCones/ScalarPullback.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Conormal coordinates, regularity and ranks

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

  1. lemma OAI.ActualSections.scalar_structure line 23
  2. lemma OAI.ActualSections.pullback_scalar line 37
  3. lemma OAI.ActualSections.pullback_scalar_inv line 75
  4. def OAI.SourcePullbackChart.planeConormalChartTransport line 90

    Source documentation

    The exact inverse image of the global conormal on this chart.

    def planeConormalChartTransport (i : Fin 3) :
    (restrictFunctor (planeIota i)).obj
      ((Scheme.Modules.pullback completedPlaneZero).obj (idealSheaf completedPlaneZero)) ≅
    (Scheme.Modules.pullback (completedPlaneZeroChart i)).obj
      ((restrictFunctor (completedBlowupIota i)).obj (idealSheaf completedPlaneZero)) :=
…

    Mentions: OAI.SourcePullbackChart.planeIota, OAI.SourcePullbackChart.completedPlaneZeroChart, OAI.SourcePullbackChart.completedBlowupIota

  5. def OAI.SourcePullbackChart.planeConormalChartSection line 98
  6. lemma OAI.SourcePullbackChart.planeConormalChartSection_isIso line 108
  7. lemma OAI.SourcePullbackChart.planeZeroChart_transition line 125
  8. lemma OAI.SourcePullbackChart.planeConormalChartSection_ratio line 137

    Source documentation

    The conormal chart coordinates are the standard projective ratios.

    lemma planeConormalChartSection_ratio (i j : Fin 3) :
    planeConormalChartSection i j =
      scalar ((Scheme.ΓSpecIso (.of (planeChart i))).inv
        (SectionCompletion.polynomialChartDehom i (MvPolynomial.X j))) ≫
      planeConormalChartSection i i := by
…

    Mentions: OAI.SourcePullbackChart.planeConormalChartSection, OAI.SourcePullbackChart.planeChart, OAI.SectionCompletion.polynomialChartDehom

  9. abbrev OAI.SourcePullbackChart.planeVariables line 182
  10. abbrev OAI.SourcePullbackChart.planePolynomial line 183
  11. def OAI.SourcePullbackChart.planeSubstitution line 185
  12. lemma OAI.SourcePullbackChart.planeSubstitution_self line 187
  13. lemma OAI.SourcePullbackChart.planeSubstitution_other line 190
  14. def OAI.SourcePullbackChart.planeToPolynomial line 194
  15. lemma OAI.SourcePullbackChart.planeToPolynomial_mk line 198
  16. lemma OAI.SourcePullbackChart.planeToPolynomial_ratio line 207
  17. lemma OAI.SourcePullbackChart.planeToPolynomial_scalar line 212
  18. def OAI.SourcePullbackChart.planeToPolynomialAlg line 223
  19. def OAI.SourcePullbackChart.polynomialToPlane line 226
  20. lemma OAI.SourcePullbackChart.polynomialChartDehom_self line 229
  21. lemma OAI.SourcePullbackChart.planeToPolynomial_left line 234
  22. lemma OAI.SourcePullbackChart.planeToPolynomial_right line 242
  23. def OAI.SourcePullbackChart.planePolynomialEquivalence line 262
  24. instance OAI.SourcePullbackChart.planeChart_regular line 266
  25. instance OAI.SourcePullbackChart.planeChart_smooth line 268
  26. instance OAI.SourcePullbackChart.completedBlowupChart_nontrivial line 284
  27. instance OAI.SourcePullbackChart.completedBlowupChart_integral line 286
  28. instance OAI.SourcePullbackChart.completedBlowupChart_domain line 289
  29. def OAI.SourcePullbackChart.completedPlanePrincipalQuotient line 292
  30. instance OAI.SourcePullbackChart.completedPlanePrincipalQuotient_regular line 297
  31. lemma OAI.SourcePullbackChart.completedBlowup_regular_at_fiber line 303

    Source documentation

    Every point of the exceptional fiber has a regular ambient local ring on each of the three completed charts.

    lemma completedBlowup_regular_at_fiber (i : Fin 3) (p : Ideal (completedBlowupChart i))
    [p.IsPrime] (hp : completedBlowupFiber i ∈ p) :
    IsRegularLocalRing (Localization.AtPrime p) := by
…

    Mentions: OAI.SourcePullbackChart.completedBlowupChart, OAI.SourcePullbackChart.completedBlowupFiber

  32. lemma OAI.CoherentChartRank.chart_epi_le line 324
  33. def OAI.CoherentChartRank.chartFreeSectionsIso line 331
  34. lemma OAI.CoherentChartRank.chart_free_rank line 338
  35. abbrev OAI.SourceConeMorphism.planeChartRank line 359
  36. def OAI.SourceConeMorphism.planeConormalChartUnitIso line 362
  37. def OAI.SourceConeMorphism.planeConormalChartIso line 374
  38. lemma OAI.SourceConeMorphism.planeConormal_rank line 382
  39. lemma OAI.SourceConeMorphism.planeConormalPower_rank line 388
  40. lemma OAI.SourceConeMorphism.planeFree_rank line 398
  41. lemma OAI.SourceConeMorphism.planeLayer_rank_le line 402
  42. lemma OAI.CoherentChartRank.chart_iso_rank line 424
  43. def OAI.CoherentChartRank.rankHom line 429
  44. lemma OAI.CoherentChartRank.rankHom_cls line 434
  45. inductive OAI.SourceConeMorphism.ExtensionState.Reachable line 457

    Source documentation

    These are precisely the extensions generated from the double-dual model by finitely many torsion-free divisor quotients.

    inductive Reachable : ExtensionState M → Prop
  | initial : Reachable (initial (M := M))
…

    Mentions: OAI.SourceConeMorphism.ExtensionState, OAI.SourceConeMorphism.ExtensionState.initial

  46. lemma OAI.SourceConeMorphism.ExtensionState.Reachable.rank_eq line 465
  47. lemma OAI.SourceConeMorphism.ExtensionState.Reachable.rank_pos line 473
  48. def OAI.SourceConeMorphism.sourceParameterDegree line 491
  49. lemma OAI.SourceConeMorphism.sourceParameterDegree_pos line 496
  50. lemma OAI.SourceConeMorphism.parameterModule_rank line 507
  51. lemma OAI.SourceConeMorphism.sourceFreeRank_eq line 529
  52. lemma OAI.SourceConeMorphism.sourceFreeRank_rank line 533
  53. lemma OAI.SourceConeMorphism.sourceFreeRank_reached_rank line 537