OAI/AlgebraicGeometry/SurfaceCones/ConeMorphism.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's actual source evaluation p : W → Spec R, where W is literally X ×[P²] (Bl₀(A³) ×[A³] Spec C[[x₀,x₁,x₂]]). The construction uses the proved canonical scalar-completion comparison; no identification with an ordinary Rees blowup of R is assumed.

  1. abbrev OAI.SourceConeMorphism.sectionRing line 15
  2. abbrev OAI.SourceConeMorphism.parameterMap line 16
  3. def OAI.SourceConeMorphism.forgetCompletion line 22

    Source documentation

    The literal source's forget-completion morphism.

    def forgetCompletion : W ⟶ W₀ :=
…
  4. lemma OAI.SourceConeMorphism.forgetCompletion_surface line 28
  5. lemma OAI.SourceConeMorphism.forgetCompletion_blowup line 31
  6. lemma OAI.SourceConeMorphism.forgetCompletion_base line 34
  7. def OAI.SourceConeMorphism.tensorEvaluation line 41

    Source documentation

    Evaluation into the exact scalar-extended affine cone.

    def tensorEvaluation : W ⟶
    pullback completionToPolynomial (Spec.map (CommRingCat.ofHom parameterMap.toRingHom)) :=
…
  8. def OAI.SourceConeMorphism.p line 50

    Source documentation

    The source map in the obstruction proof, with its faithful completed section-cone target.

    def p : W ⟶ Spec (.of ExplicitCone.completedRing) :=
…

    Mentions: OAI.ExplicitCone.completedRing

  9. lemma OAI.SourceConeMorphism.completion_parameter_identity line 54
  10. lemma OAI.SourceConeMorphism.p_parameters line 61
  11. instance OAI.SourceConeMorphism.(instance at line 77) line 77

    Source documentation

    Properness of the actual source map, using the actual S-compatible completion and the already proved properness over Spec A.

    instance : IsProper p := by
…

    Mentions: OAI.SourceConeMorphism.p

  12. lemma OAI.SourceConeMorphism.forgetCompletion_isPullback line 99
  13. lemma OAI.SourceConeMorphism.sourceCompletion_isPullback line 108
  14. def OAI.SourceConeMorphism.completionSpecIso line 114

    Source documentation

    Exact affine-cone base-change comparison.

    def completionSpecIso : Spec (.of ExplicitCone.completedRing) ≅
    pullback completionToPolynomial (Spec.map (CommRingCat.ofHom parameterMap.toRingHom)) :=
…

    Mentions: OAI.ExplicitCone.completedRing

  15. def OAI.SourceConeMorphism.toUncompleted line 120

    Source documentation

    The canonical map from the completed cone to the uncompleted cone.

    def toUncompleted : Spec (.of ExplicitCone.completedRing) ⟶ Spec (.of sectionRing) :=
…

    Mentions: OAI.ExplicitCone.completedRing, OAI.SourceConeMorphism.sectionRing

  16. def OAI.SourceConeMorphism.toPowerSeries line 123
  17. lemma OAI.SourceConeMorphism.tensor_right_identity line 126
  18. lemma OAI.SourceConeMorphism.toUncompleted_eq line 137
  19. lemma OAI.SourceConeMorphism.p_eq_comparison line 146
  20. lemma OAI.SourceConeMorphism.p_toUncompleted line 148
  21. lemma OAI.SourceConeMorphism.p_toPowerSeries line 153
  22. lemma OAI.SourceConeMorphism.coneCompletion_isPullback line 157
  23. lemma OAI.SourceConeMorphism.p_isPullback line 170

    Source documentation

    The actual source completion square is cartesian, hence the punctured isomorphism can be transferred without any assumptions about flatness.

    lemma p_isPullback : IsPullback p forgetCompletion toUncompleted
    SourcePullbackChart.coneMorphism := by
…

    Mentions: OAI.SourceConeMorphism.p, OAI.SourceConeMorphism.forgetCompletion, OAI.SourceConeMorphism.toUncompleted, OAI.SourcePullbackChart.coneMorphism

  24. def OAI.SourceZeroSections.planeZero line 191
  25. def OAI.SourceZeroSections.planeScalar line 192
  26. lemma OAI.SourceZeroSections.planeZero_direction line 194
  27. lemma OAI.SourceZeroSections.planeZero_blowdown line 198
  28. lemma OAI.SourceZeroSections.planeZero_isPullback line 201
  29. instance OAI.SourceZeroSections.originPoint_closed line 209
  30. instance OAI.SourceZeroSections.planeZero_closed line 213
  31. def OAI.SourceZeroSections.sourceZero line 217
  32. lemma OAI.SourceZeroSections.sourceZero_fst line 221
  33. lemma OAI.SourceZeroSections.sourceZero_g₀ line 222
  34. lemma OAI.SourceZeroSections.sourceZero_isPullback line 225
  35. instance OAI.SourceZeroSections.sourceZero_closed line 233
  36. abbrev OAI.SourceZeroSections.seriesOrigin line 237
  37. lemma OAI.SourceZeroSections.seriesOrigin_toPolynomial line 240
  38. instance OAI.SourceZeroSections.seriesOrigin_closed line 252
  39. def OAI.SourceZeroSections.completedPlaneZero line 256
  40. lemma OAI.SourceZeroSections.completedPlaneZero_fst line 260
  41. lemma OAI.SourceZeroSections.completedPlaneZero_blowdown line 262
  42. lemma OAI.SourceZeroSections.completedPlaneZero_direction line 264
  43. lemma OAI.SourceZeroSections.completedPlaneZero_isPullback line 267
  44. instance OAI.SourceZeroSections.completedPlaneZero_closed line 276
  45. def OAI.SourceZeroSections.completedSourceZero line 280
  46. lemma OAI.SourceZeroSections.completedSourceZero_fst line 284
  47. lemma OAI.SourceZeroSections.completedSourceZero_g line 286
  48. lemma OAI.SourceZeroSections.completedSourceZero_isPullback line 290

    Source documentation

    The exact left-hand square in the manuscript, lines 275--277.

    lemma completedSourceZero_isPullback :
    IsPullback completedSourceZero ExplicitCone.projectiveNormalization g completedPlaneZero := by
…

    Mentions: OAI.SourceZeroSections.completedSourceZero, OAI.ExplicitCone.projectiveNormalization, OAI.SourceZeroSections.completedPlaneZero

  49. instance OAI.SourceZeroSections.completedSourceZero_closed line 299
  50. lemma OAI.SourceZeroSections.completedSourceZero_origin_isPullback line 304

    Source documentation

    The entire actual closed fiber of W over A, with no extra components.

    lemma completedSourceZero_origin_isPullback :
    IsPullback completedSourceZero (ExplicitCone.projectiveNormalization ≫ planeScalar)
      (g ≫ completedBlowdown) seriesOrigin :=
…

    Mentions: OAI.SourceZeroSections.completedSourceZero, OAI.ExplicitCone.projectiveNormalization, OAI.SourceZeroSections.planeScalar, OAI.SourceZeroSections.seriesOrigin

  51. lemma OAI.ExplicitCone.projectiveCompletedParameterHom_finite line 316
  52. lemma OAI.ExplicitCone.projectiveCompletedParameterHom_injective line 322
  53. lemma OAI.ExplicitCone.projectiveCompletedParameterHom_polynomial line 342

    Source documentation

    The original polynomial cone and the actual projective-parameter power-series map have a commuting square, not just abstract isomorphic bases.

    lemma projectiveCompletedParameterHom_polynomial :
    (SectionCompletion.polynomialToSeries pieces).comp
      (SectionCompletion.linearPolynomialMap pieces projectiveParameter projectiveParameter_mem) =
      projectiveCompletedParameterHom.comp (MvPolynomial.aeval MvPowerSeries.X) := by
…

    Mentions: OAI.SectionCompletion.polynomialToSeries, OAI.ExplicitCone.pieces, OAI.SectionCompletion.linearPolynomialMap, OAI.ExplicitCone.projectiveParameter, OAI.ExplicitCone.projectiveParameter_mem

  54. theorem OAI.ExplicitCone.projective_parameters_free_of_CM line 354

    Source documentation

    For every arbitrary hypothetical CM module, source freeness holds over this compatible parameter base as well. The module is not assumed graded, and no equality with another chosen parameter homomorphism is asserted.

    theorem projective_parameters_free_of_CM
    (M : Type) [AddCommGroup M] [Module completedRing M]
    [Module.Finite completedRing M] [Nontrivial M]
    (hdepth : SmallCM.localDepth completedRing M = 3) :
    letI : Algebra (MvPowerSeries (Fin 3) ℂ) completedRing :=
…

    Mentions: OAI.ExplicitCone.completedRing, OAI.SmallCM.localDepth

  55. abbrev OAI.ExplicitCone.completedProjectiveSection line 382
  56. lemma OAI.ExplicitCone.completedProjectiveSection_eq line 385
  57. lemma OAI.ExplicitCone.completedProjectiveIdeal_radical line 390
  58. lemma OAI.ExplicitCone.completedProjectiveSection_mem_maximal line 407
  59. lemma OAI.ExplicitCone.exists_completedProjectiveSection_notMem line 412
  60. lemma OAI.ExplicitCone.completedProjectiveCover line 425
  61. lemma OAI.ExplicitCone.completedProjectiveOpen_eq line 439
  62. lemma OAI.AlgebraicGeometry.Scheme.Hom.isIso_restrict_of_isPullback line 457
  63. lemma OAI.SourceConeMorphism.toUncompleted_preimage_puncture line 476
  64. instance OAI.SourceConeMorphism.p_puncture_isIso line 482

    Source documentation

    Literal completed source isomorphism off the actual closed cone point.

    instance p_puncture_isIso : IsIso (p ∣_ ExplicitCone.completedPunctureOpen) := by
…

    Mentions: OAI.SourceConeMorphism.p, OAI.ExplicitCone.completedPunctureOpen

  65. def OAI.SourceConeMorphism.puncturedIso line 487
  66. lemma OAI.SourceConeMorphism.puncturedIso_hom_ι line 490
  67. lemma OAI.AlgebraicGeometry.IsSchemeTheoreticallyDominant.isIntegral line 506
  68. instance OAI.SourceConeMorphism.completion_flat line 530
  69. instance OAI.SourceConeMorphism.sourceCompletion_flat line 534
  70. instance OAI.SourceConeMorphism.completed_noetherian line 538
  71. lemma OAI.SourceConeMorphism.sourcePuncture_preimage line 542
  72. instance OAI.SourceConeMorphism.completedPuncture_schematicallyDominant line 550
  73. instance OAI.SourceConeMorphism.completedConePuncture_nonempty line 556
  74. instance OAI.SourceConeMorphism.completedConePuncture_integral line 573
  75. instance OAI.SourceConeMorphism.sourcePuncture_integral line 576
  76. instance OAI.SourceConeMorphism.completed_integral line 580

    Source documentation

    The completed cone model supporting the pullback double dual is integral and Noetherian.

    instance completed_integral : IsIntegral W :=
…
  77. def OAI.SourcePullbackChart.completedChartFirst line 600
  78. def OAI.SourcePullbackChart.completedChartSecond line 603
  79. lemma OAI.SourcePullbackChart.completedChartTensor_isPullback line 606
  80. def OAI.SourcePullbackChart.completedIota line 619
  81. lemma OAI.SourcePullbackChart.completedIota_forget line 624
  82. lemma OAI.SourcePullbackChart.completedIota_base line 628
  83. lemma OAI.SourcePullbackChart.completedIota_isPullback line 632
  84. instance OAI.SourcePullbackChart.(instance at line 640) line 640
  85. lemma OAI.SourcePullbackChart.completedIota_opensRange line 644
  86. def OAI.SourcePullbackChart.completedCover line 652
  87. lemma OAI.SourceZeroSections.planeIota_originFiber line 691
  88. lemma OAI.SourceZeroSections.planeIota_zero line 704
  89. lemma OAI.SourceZeroSections.planeIota_scalar line 715
  90. lemma OAI.SourceZeroSections.zeroEvaluation_blowup line 726
  91. lemma OAI.SourceZeroSections.surfaceIota_sourceZero line 752
  92. lemma OAI.SourceZeroSections.surfaceIota_scalar line 781
  93. lemma OAI.SourceZeroSections.completedSourceZero_forget line 790
  94. lemma OAI.SourcePullbackChart.completedZeroEvaluation_left line 815
  95. lemma OAI.SourcePullbackChart.completedZeroEvaluation_right line 824
  96. abbrev OAI.SourcePullbackChart.completedZeroChart line 834
  97. lemma OAI.SourcePullbackChart.completedZeroChart_first line 837
  98. lemma OAI.SourcePullbackChart.completedZeroChart_second line 842
  99. lemma OAI.SourcePullbackChart.surfaceIota_completedSourceZero line 849

    Source documentation

    Exact commutative square for the actual completed zero immersion.

    @[reassoc] lemma surfaceIota_completedSourceZero (i : Fin 3) :
    surfaceIota i ≫ completedSourceZero = completedZeroChart i ≫ completedIota i := by
…

    Mentions: OAI.SourcePullbackChart.surfaceIota, OAI.SourcePullbackChart.completedZeroChart, OAI.SourcePullbackChart.completedIota

  100. lemma OAI.SourcePullbackChart.surfaceIota_opensRange line 857
  101. lemma OAI.SourcePullbackChart.surfaceIota_cover line 864
  102. lemma OAI.SourcePullbackChart.surfaceZero_chart_preimage line 871
  103. lemma OAI.SourcePullbackChart.completedZero_isPullback line 882
  104. instance OAI.SourcePullbackChart.completedSourceChart_noetherian line 889