OAI/AlgebraicGeometry/SurfaceCones/SectionFiniteChart.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

Required local cone-evaluation maps for the manuscript, lines 243–268. These maps use the actual homogeneous Proj chart, not a postulated coordinate ring.

  1. abbrev OAI.SectionCompletion.polynomialChart line 13
  2. instance OAI.SectionCompletion.polynomialChartScalarAlgebra line 15
  3. def OAI.SectionCompletion.polynomialChartDehom line 19
  4. lemma OAI.SectionCompletion.linearGradedMap_X line 24
  5. def OAI.SectionCompletion.linearChartMap line 28
  6. lemma OAI.SectionCompletion.linearChartMap_scalar line 36
  7. def OAI.SectionCompletion.linearChartAlgMap line 60

    Source documentation

    The actual ring map on an affine chart, including its scalar structure.

    def linearChartAlgMap : polynomialChart (k := k) i →ₐ[k] homogeneousChart T (w i) (hw i) :=
…

    Mentions: OAI.SectionCompletion.polynomialChart, OAI.SectionCompletion.homogeneousChart

  8. lemma OAI.SectionCompletion.linearChartMap_dehom line 63
  9. theorem OAI.SectionCompletion.linearChartMap_finite line 84

    Source documentation

    Every actual projective chart map of the finite normalized linear cone is FINITE, proved through surjective dehomogenization of the section ring.

    theorem linearChartMap_finite (hn : w i ≠ 0)
    (hfin : (linearPolynomialMap T w hw).Finite) : (linearChartMap T w hw i).Finite := by
…

    Mentions: OAI.SectionCompletion.linearPolynomialMap, OAI.SectionCompletion.linearChartMap

  10. lemma OAI.SectionCompletion.polynomial_irrelevant_le line 104
  11. lemma OAI.SectionCompletion.awayMap_finite line 120
  12. theorem OAI.SectionCompletion.linearProjectiveMap_finite line 139

    Source documentation

    Finiteness of the actual projective scheme map, from the finite normalized homogeneous cone and chartwise surjective dehomogenization.

    theorem linearProjectiveMap_finite (hn : ∀ i, w i ≠ 0)
    (hfin : (linearPolynomialMap T w hw).Finite) :
    IsFinite (linearProjectiveMap T w hw hfin) := by
…

    Mentions: OAI.SectionCompletion.linearPolynomialMap, OAI.SectionCompletion.linearProjectiveMap

  13. lemma OAI.ExplicitCone.projectiveParameter_injective line 179
  14. lemma OAI.ExplicitCone.projectiveParameter_ne_zero line 184
  15. theorem OAI.ExplicitCone.projectiveNormalization_finite line 193

    Source documentation

    The morphism from the normalized Kummer section-cone Proj to the projective plane is finite.

    theorem projectiveNormalization_finite : IsFinite projectiveNormalization :=
…

    Mentions: OAI.ExplicitCone.projectiveNormalization

  16. lemma OAI.ExplicitCone.projectiveParameter_section_ne_zero line 206
  17. instance OAI.ExplicitCone.projectiveSurface_integral line 215

    Source documentation

    Integrality is proved for the actual normalized section-cone Proj. This still makes no unsupported claim of all-chart smoothness.

    instance projectiveSurface_integral : IsIntegral projectiveSurface :=
…

    Mentions: OAI.ExplicitCone.projectiveSurface

  18. theorem OAI.ExplicitCone.projectiveNormalization_surjective line 224

    Source documentation

    The genuine projective normalization covers P², including every closed point. Its generic-point dominance follows from the injective homogeneous normalization, and finite closedness supplies surjectivity.

    theorem projectiveNormalization_surjective : Function.Surjective projectiveNormalization := by
…

    Mentions: OAI.ExplicitCone.projectiveNormalization

  19. abbrev OAI.KummerSourceModel.S line 254
  20. abbrev OAI.KummerSourceModel.A line 255
  21. abbrev OAI.KummerSourceModel.m line 256
  22. abbrev OAI.KummerSourceModel.B line 257
  23. instance OAI.KummerSourceModel.(instance at line 258) line 258
  24. instance OAI.KummerSourceModel.(instance at line 259) line 259
  25. abbrev OAI.KummerSourceModel.grades line 260
  26. abbrev OAI.KummerSourceModel.V₀ line 261
  27. def OAI.KummerSourceModel.projectionGradedMap line 263
  28. lemma OAI.KummerSourceModel.sourceSections_cover line 268
  29. lemma OAI.KummerSourceModel.irrelevant_le_radical line 280
  30. def OAI.KummerSourceModel.direction line 314

    Source documentation

    The projective direction of the literal blowup of affine 3-space at its origin; no line-bundle or regularity identification is assumed.

    def direction : V₀ ⟶ ExplicitCone.plane :=
…

    Mentions: OAI.KummerSourceModel.V₀, OAI.ExplicitCone.plane

  31. def OAI.KummerSourceModel.zeroSpecIso line 317
  32. def OAI.KummerSourceModel.blowdown line 320
  33. instance OAI.KummerSourceModel.(instance at line 321) line 321
  34. def OAI.KummerSourceModel.completionToPolynomial line 327
  35. abbrev OAI.KummerSourceModel.W₀ line 331

    Source documentation

    The literal uncompleted fiber-product model, not a postulated total space.

    abbrev W₀ : Scheme := pullback ExplicitCone.projectiveNormalization direction

    Mentions: OAI.ExplicitCone.projectiveNormalization, OAI.KummerSourceModel.direction

  36. def OAI.KummerSourceModel.g₀ line 333
  37. theorem OAI.KummerSourceModel.g₀_finite line 335
  38. abbrev OAI.KummerSourceModel.V line 341

    Source documentation

    The source's completed polynomial blowup V, as literal base change.

    abbrev V : Scheme := pullback blowdown completionToPolynomial

    Mentions: OAI.KummerSourceModel.blowdown, OAI.KummerSourceModel.completionToPolynomial

  39. def OAI.KummerSourceModel.completedBlowdown line 343
  40. instance OAI.KummerSourceModel.(instance at line 344) line 344
  41. def OAI.KummerSourceModel.completedDirection line 346
  42. abbrev OAI.KummerSourceModel.W line 349

    Source documentation

    The completed model is the fiber product of the normalized section-cone Proj with the completed polynomial blowup over the projective plane.

    abbrev W : Scheme := pullback ExplicitCone.projectiveNormalization completedDirection

    Mentions: OAI.ExplicitCone.projectiveNormalization, OAI.KummerSourceModel.completedDirection

  43. def OAI.KummerSourceModel.g line 351
  44. theorem OAI.KummerSourceModel.g_finite line 353
  45. instance OAI.KummerSourceModel.(instance at line 358) line 358
  46. theorem OAI.KummerSourceModel.g_surjective line 362
  47. theorem OAI.KummerSourceModel.W_proper line 369

    Source documentation

    The completed fiber-product model is proper.

    theorem W_proper : IsProper (g ≫ completedBlowdown) := inferInstance
…

    Mentions: OAI.KummerSourceModel.g, OAI.KummerSourceModel.completedBlowdown

  48. def OAI.SectionCompletion.scaledPolynomialMap line 387

    Source documentation

    Homogeneous rescaling of the literal section polynomial.

    def scaledPolynomialMap : polynomials T →ₐ[k] Polynomial K :=
…

    Mentions: OAI.SectionCompletion.polynomials

  49. lemma OAI.SectionCompletion.coeff_scaledPolynomialMap line 390
  50. lemma OAI.SectionCompletion.scaledPolynomialMap_mem_range line 396
  51. def OAI.SectionCompletion.chartEvaluation line 408

    Source documentation

    The line-bundle-chart evaluation of the section ring, rescaling each pure section by c^degree and retaining the fiber parameter X.

    def chartEvaluation : polynomials T →ₐ[k] Polynomial (homogeneousChart T c hc) :=
…

    Mentions: OAI.SectionCompletion.polynomials, OAI.SectionCompletion.homogeneousChart

  52. lemma OAI.SectionCompletion.map_chartEvaluation line 413
  53. lemma OAI.SectionCompletion.coeff_chartEvaluation line 421
  54. lemma OAI.SectionCompletion.chartEvaluation_injective line 426
  55. lemma OAI.SectionCompletion.chartEvaluation_homogeneous line 435
  56. lemma OAI.SectionCompletion.chartEvaluation_parameter line 451
  57. lemma OAI.SectionCompletion.chartEvaluation_linearSection line 463

    Source documentation

    Every degree-one section is its direction ratio times the fiber parameter.

    lemma chartEvaluation_linearSection (a : K) (ha : a ∈ T 1) :
    chartEvaluation T c hc hn (linearSection T a ha) =
      C (dehomogenize T c hc hn (linearSection T a ha)) * X := by
…

    Mentions: OAI.SectionCompletion.chartEvaluation, OAI.SectionCompletion.linearSection, OAI.SectionCompletion.dehomogenize

  58. lemma OAI.HomogeneousLocalization.ratio_mul_fromZero line 482
  59. abbrev OAI.SourcePullbackChart.S line 502
  60. abbrev OAI.SourcePullbackChart.origin line 503
  61. abbrev OAI.SourcePullbackChart.Rees line 504
  62. abbrev OAI.SourcePullbackChart.grades line 505
  63. abbrev OAI.SourcePullbackChart.projectionGradedMap line 506
  64. abbrev OAI.SourcePullbackChart.sourceSection line 509
  65. lemma OAI.SourcePullbackChart.sourceSection_eq line 510
  66. lemma OAI.SourcePullbackChart.sourceSection_homogeneous line 512
  67. abbrev OAI.SourcePullbackChart.chart line 515
  68. abbrev OAI.SourcePullbackChart.planeChart line 516
  69. def OAI.SourcePullbackChart.directionMap line 518
  70. def OAI.SourcePullbackChart.baseToZero line 522

    Source documentation

    Blowdown's exact degree-zero ring map on this Rees chart.

    def baseToZero : S →+* grades 0 :=
…

    Mentions: OAI.SourcePullbackChart.S, OAI.SourcePullbackChart.grades

  71. def OAI.SourcePullbackChart.baseMap line 525
  72. lemma OAI.SourcePullbackChart.directionMap_ratio line 528
  73. lemma OAI.SourcePullbackChart.directionMap_scalar line 539
  74. lemma OAI.SourcePullbackChart.baseMap_mk line 560
  75. lemma OAI.SourcePullbackChart.baseToZero_coe line 563
  76. lemma OAI.SourcePullbackChart.sourceSection_cross line 565
  77. lemma OAI.SourcePullbackChart.ratio_relation line 574
  78. lemma OAI.MvPolynomial.homogeneous_aeval_div line 597
  79. abbrev OAI.SourcePullbackChart.K line 623
  80. def OAI.SourcePullbackChart.coordinate line 625
  81. lemma OAI.SourcePullbackChart.coordinate_ne_zero line 626
  82. def OAI.SourcePullbackChart.planeField line 629
  83. lemma OAI.SourcePullbackChart.planeField_mk line 634
  84. lemma OAI.SourcePullbackChart.planeField_injective line 644
  85. lemma OAI.SourcePullbackChart.planeField_scalar line 661
  86. def OAI.SourcePullbackChart.planeFieldAlg line 674
  87. lemma OAI.SourcePullbackChart.planeField_ratio line 677
  88. lemma OAI.SourcePullbackChart.planeField_dehom line 683
  89. lemma OAI.SourcePullbackChart.polynomialChartDehom_surjective line 695
  90. lemma OAI.SourcePullbackChart.planeField_range line 709
  91. lemma OAI.SourcePullbackChart.sourceSection_literal line 739
  92. lemma OAI.SourcePullbackChart.evaluateOne_sourceSection line 743
  93. def OAI.SourcePullbackChart.reesField line 749
  94. lemma OAI.SourcePullbackChart.reesField_mk line 754
  95. lemma OAI.SourcePullbackChart.reesField_injective line 766
  96. lemma OAI.SourcePullbackChart.reesField_base line 790
  97. lemma OAI.SourcePullbackChart.reesField_direction line 805