OAI/AlgebraicGeometry/SurfaceCones/PolynomialRangeTranscendence.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Polynomial.eval₂RingHom_injective_of_range_transcendental line 14
2. def OAI.SourcePullbackChart.blowupCoordinate line 41

   Source documentation

   Affine blowup coordinates inside the original rational function field.

   def blowupCoordinate (i j : Fin 3) : K :=
   …

   Mentions: OAI.SourcePullbackChart.K

3. lemma OAI.SourcePullbackChart.blowupCoordinate_independent line 44
4. lemma OAI.SourcePullbackChart.ratios_adjoin_eq line 61
5. lemma OAI.SourcePullbackChart.radial_transcendental line 80
6. lemma OAI.SourcePullbackChart.planePolynomial_injective line 86
7. abbrev OAI.SourcePullbackChart.surfaceChart line 104
8. instance OAI.SourcePullbackChart.surfaceChartScalar line 106
9. abbrev OAI.SourcePullbackChart.sectionRing line 109
10. abbrev OAI.SourcePullbackChart.parameterMap line 110
11. abbrev OAI.SourcePullbackChart.surfaceDirectionMap line 113
12. instance OAI.SourcePullbackChart.surfaceChartPlaneAlgebra line 117
13. instance OAI.SourcePullbackChart.chartPlaneAlgebra line 119
14. abbrev OAI.SourcePullbackChart.pullbackChart line 122
15. def OAI.SourcePullbackChart.surfaceIn line 124
16. def OAI.SourcePullbackChart.blowupIn line 127
17. lemma OAI.SourcePullbackChart.tensor_balance line 130
18. def OAI.SourcePullbackChart.fiberParameter line 135
19. def OAI.SourcePullbackChart.coneEvaluation line 139

    Source documentation

    The section evaluation, in the coordinate ring of the source's actual fiber product of affine charts.

    def coneEvaluation (i : Fin 3) : sectionRing →+* pullbackChart i :=
    …

    Mentions: OAI.SourcePullbackChart.sectionRing, OAI.SourcePullbackChart.pullbackChart

20. lemma OAI.SourcePullbackChart.coneEvaluation_scalar line 144
21. lemma OAI.SourcePullbackChart.surfaceDirectionMap_ratio line 157
22. lemma OAI.SourcePullbackChart.coneEvaluation_variable line 170
23. lemma OAI.SourcePullbackChart.coneEvaluation_comp_parameters line 191

    Source documentation

    Exact S-compatibility: evaluation commutes with the blowdown variables, including the scalars. It can therefore be base changed by S→C[[x₀,x₁,x₂]].

    lemma coneEvaluation_comp_parameters (i : Fin 3) :
        (coneEvaluation i).comp parameterMap.toRingHom = (blowupIn i).comp (baseMap i) := by
    …

    Mentions: OAI.SourcePullbackChart.coneEvaluation, OAI.SourcePullbackChart.blowupIn, OAI.SourcePullbackChart.baseMap

24. def OAI.SourcePullbackChart.planePolynomialToRees line 216
25. def OAI.SourcePullbackChart.planePolynomialField line 219
26. lemma OAI.SourcePullbackChart.planePolynomialToRees_field line 222
27. lemma OAI.SourcePullbackChart.planePolynomialToRees_injective line 234
28. lemma OAI.SourcePullbackChart.polynomialField_ratio_mem line 244
29. lemma OAI.SourcePullbackChart.polynomialField_coordinate_mem line 250
30. lemma OAI.SourcePullbackChart.polynomialField_base_mem line 257
31. lemma OAI.SourcePullbackChart.polynomialField_scaled_mem line 271
32. lemma OAI.SourcePullbackChart.planePolynomialToRees_surjective line 300
33. def OAI.SourcePullbackChart.planePolynomialEquiv line 311

    Source documentation

    The actual Rees chart is the affine line over its actual plane chart.

    def planePolynomialEquiv (i : Fin 3) : Polynomial (planeChart i) ≃ₐ[planeChart i] chart i :=
    …

    Mentions: OAI.SourcePullbackChart.planeChart, OAI.SourcePullbackChart.chart

34. lemma OAI.SourcePullbackChart.planePolynomialEquiv_C line 319
35. lemma OAI.SourcePullbackChart.planePolynomialEquiv_X line 322
36. def OAI.Polynomial.scalarBaseChangeEquiv line 337
37. lemma OAI.Polynomial.scalarBaseChangeEquiv_tmul_C line 343
38. lemma OAI.Polynomial.scalarBaseChangeEquiv_one_tmul_X line 348
39. lemma OAI.Polynomial.scalarBaseChangeEquiv_symm_C line 352
40. lemma OAI.Polynomial.scalarBaseChangeEquiv_symm_X line 358
41. def OAI.SourcePullbackChart.pullbackPolynomialEquiv line 379

    Source documentation

    The source pullback is locally the affine line over the surface's own homogeneous chart, rather than a merely posited replacement scheme.

    def pullbackPolynomialEquiv (i : Fin 3) :
        pullbackChart i ≃ₐ[surfaceChart i] Polynomial (surfaceChart i) :=
    …

    Mentions: OAI.SourcePullbackChart.pullbackChart, OAI.SourcePullbackChart.surfaceChart

42. lemma OAI.SourcePullbackChart.pullbackPolynomialEquiv_surface line 385
43. lemma OAI.SourcePullbackChart.pullbackPolynomialEquiv_fiber line 389
44. lemma OAI.SourcePullbackChart.pullbackPolynomialEquiv_coefficientMap line 400
45. lemma OAI.SourcePullbackChart.pullbackPolynomialEquiv_eval line 406
46. lemma OAI.SourcePullbackChart.pullbackPolynomialEquiv_coneEvaluation line 414

    Source documentation

    Exact coordinate identity for the geometric map already glued on W₀.

    lemma pullbackPolynomialEquiv_coneEvaluation (i : Fin 3) (b : sectionRing) :
        pullbackPolynomialEquiv i (coneEvaluation i b) =
          SectionCompletion.chartEvaluation ExplicitCone.pieces (ExplicitCone.projectiveParameter i)
            (ExplicitCone.projectiveParameter_mem i) (ExplicitCone.projectiveParameter_ne_zero i) b :=
    …

    Mentions: OAI.SourcePullbackChart.sectionRing, OAI.SourcePullbackChart.pullbackPolynomialEquiv, OAI.SourcePullbackChart.coneEvaluation, OAI.SectionCompletion.chartEvaluation, OAI.ExplicitCone.pieces, OAI.ExplicitCone.projectiveParameter, OAI.ExplicitCone.projectiveParameter_mem, OAI.ExplicitCone.projectiveParameter_ne_zero

47. lemma OAI.Polynomial.awayX_injective line 430
48. abbrev OAI.SectionCompletion.conePuncture line 447
49. abbrev OAI.SectionCompletion.linePuncture line 448
50. def OAI.SectionCompletion.coneCoefficientInclusion line 454
51. def OAI.SectionCompletion.punctureBase line 457
52. lemma OAI.SectionCompletion.punctureBase_section line 461
53. def OAI.SectionCompletion.punctureEvaluation line 467
54. lemma OAI.SectionCompletion.punctureEvaluation_base line 471
55. lemma OAI.SectionCompletion.dehomogenize_homogeneous_mk line 476
56. lemma OAI.SectionCompletion.homogeneousFraction_spec line 484
57. lemma OAI.SectionCompletion.punctureEvaluation_coefficient line 495
58. lemma OAI.SectionCompletion.punctureBase_injective line 512
59. lemma OAI.SectionCompletion.punctureEvaluation_injective line 517
60. def OAI.SectionCompletion.lineToConePolynomial line 528
61. def OAI.SectionCompletion.lineToConePuncture line 532
62. lemma OAI.SectionCompletion.punctureEvaluation_lineToConePolynomial line 538
63. lemma OAI.SectionCompletion.punctureEvaluation_rightInverse line 548
64. def OAI.SectionCompletion.punctureEquiv line 563

    Source documentation

    The actual cone puncture agrees with the actual punctured line chart. This proof makes no degree-one generation assumption.

    def punctureEquiv : conePuncture T c hc ≃+* linePuncture T c hc :=
    …

    Mentions: OAI.SectionCompletion.conePuncture, OAI.SectionCompletion.linePuncture

65. abbrev OAI.SourcePullbackChart.coneSection line 584
66. lemma OAI.SourcePullbackChart.coneSection_eq line 588
67. lemma OAI.SourcePullbackChart.pullbackPolynomialEquiv_coneSection line 591
68. abbrev OAI.SourcePullbackChart.evaluationPuncture line 595
69. abbrev OAI.SourcePullbackChart.polynomialPuncture line 596
70. def OAI.SourcePullbackChart.pullbackPunctureEquiv line 604

    Source documentation

    Localization of the actual line-bundle ring chart.

    def pullbackPunctureEquiv (i : Fin 3) : evaluationPuncture i ≃+* polynomialPuncture i :=
    …

    Mentions: OAI.SourcePullbackChart.evaluationPuncture, OAI.SourcePullbackChart.polynomialPuncture

71. lemma OAI.SourcePullbackChart.pullbackPunctureEquiv_base line 614
72. lemma OAI.SourcePullbackChart.pullbackPunctureEquiv_awayMap line 624
73. lemma OAI.SourcePullbackChart.awayMap_eq_punctureEquiv line 638
74. lemma OAI.SourcePullbackChart.coneEvaluation_restrict_isIso line 651

    Source documentation

    Literal local geometric isomorphism over the actual s_i, not over a hypothetical degree-one generated cone.

    lemma coneEvaluation_restrict_isIso (i : Fin 3) :
        IsIso ((Spec.map (CommRingCat.ofHom (coneEvaluation i))) ∣_
          (PrimeSpectrum.basicOpen (coneSection i))) := by
    …

    Mentions: OAI.SourcePullbackChart.coneEvaluation, OAI.SourcePullbackChart.coneSection

75. def OAI.SourcePullbackChart.planeIota line 678
76. def OAI.SourcePullbackChart.blowupIota line 682
77. def OAI.SourcePullbackChart.surfaceIota line 685
78. instance OAI.SourcePullbackChart.(instance at line 692) line 692
79. instance OAI.SourcePullbackChart.(instance at line 696) line 696
80. instance OAI.SourcePullbackChart.(instance at line 697) line 697
81. lemma OAI.SourcePullbackChart.blowup_chart_square line 704
82. lemma OAI.SourcePullbackChart.surface_chart_square line 711
83. def OAI.SourcePullbackChart.pullbackIota line 734

    Source documentation

    The open chart of the literal source fiber product.

    def pullbackIota (i : Fin 3) : Spec (.of (pullbackChart i)) ⟶ KummerSourceModel.W₀ :=
    …

    Mentions: OAI.SourcePullbackChart.pullbackChart, OAI.KummerSourceModel.W₀

84. instance OAI.SourcePullbackChart.(instance at line 743) line 743
85. lemma OAI.SourcePullbackChart.pullbackIota_surface line 747
86. lemma OAI.SourcePullbackChart.pullbackIota_blowup line 756
87. lemma OAI.SourcePullbackChart.surface_isPullback line 765
88. lemma OAI.SourcePullbackChart.blowup_isPullback line 778
89. def OAI.SourcePullbackChart.planeCover line 789

    Source documentation

    The exact three standard plane charts.

    def planeCover : ExplicitCone.plane.OpenCover :=
    …

90. lemma OAI.SourcePullbackChart.planeCover_f line 795
91. abbrev OAI.SourcePullbackChart.baseChangeCover line 797
92. def OAI.SourcePullbackChart.pullbackChartIso line 802

    Source documentation

    Chartwise comparison with the built-in base-changed open cover.

    def pullbackChartIso (i : Fin 3) : Spec (.of (pullbackChart i)) ≅ baseChangeCover.X i := by
    …

    Mentions: OAI.SourcePullbackChart.pullbackChart

93. lemma OAI.SourcePullbackChart.pullbackChartIso_hom_iota line 825
94. def OAI.SourcePullbackChart.sourceCover line 853

    Source documentation

    An affine open cover of the literal source by the tensor rings on which coneEvaluation was constructed.

    def sourceCover : KummerSourceModel.W₀.OpenCover where
    …