KummerCompletedBlowup.lean`

81 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExplicitCone.completedSectionIdeal line 13
Source documentation
The ideal generated by the eighteen degree-one sections of the polarization in the completed cone.
```
def completedSectionIdeal : Ideal completedRing := Ideal.span (Set.range completedSection)
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedSection
lemma OAI.ExplicitCone.completedSection_mem_ideal line 15
abbrev OAI.ExplicitCone.completedBlowup line 18
def OAI.ExplicitCone.completedReesZeroSpecIso line 20
def OAI.ExplicitCone.completedBlowupMap line 26
Source documentation
The actual projective Rees model over the actual completed ring.
```
def completedBlowupMap : completedBlowup ⟶ Spec (.of completedRing) :=
…
```
Mentions: OAI.ExplicitCone.completedBlowup, OAI.ExplicitCone.completedRing
instance OAI.ExplicitCone.completedBlowup_proper line 29
abbrev OAI.ExplicitCone.completedBlowupSection line 35
abbrev OAI.ExplicitCone.completedBlowupChart line 38
instance OAI.ExplicitCone.completedBlowupChart_algebra line 41
def OAI.ExplicitCone.completedBlowupChartEquiv line 47
Source documentation
The affine Rees–Proj chart is the algebraic power-series realization of the completed cone.
```
def completedBlowupChartEquiv : completedBlowupChart ≃ₐ[completedRing] completedAffineChart := by
…
```
Mentions: OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedAffineChart
def OAI.ExplicitCone.completedBlowupOpenIso line 53
abbrev OAI.ExplicitCone.completedBlowupParameter line 60
lemma OAI.ExplicitCone.completedBlowupChartEquiv_parameter line 64
lemma OAI.ExplicitCone.completedBlowupParameter_ne_zero line 69
def OAI.ExplicitCone.completedBlowupExceptionalEquiv line 79
instance OAI.ExplicitCone.completedBlowupChart_noetherian line 89
instance OAI.ExplicitCone.completedBlowupChart_domain line 92
instance OAI.ExplicitCone.completedBlowupExceptional_regular line 95
theorem OAI.ExplicitCone.completedBlowupChart_regular_at_exceptional line 102
Source documentation
The local rings on the exceptional divisor of the distinguished projective blowup chart are regular.
```
theorem completedBlowupChart_regular_at_exceptional (p : Ideal completedBlowupChart) [p.IsPrime]
    (hp : completedBlowupParameter ∈ p) : IsRegularLocalRing (Localization.AtPrime p) :=
…
```
Mentions: OAI.ExplicitCone.completedBlowupChart, OAI.ExplicitCone.completedBlowupParameter
def OAI.SectionCompletion.polynomialToSeries line 120
lemma OAI.SectionCompletion.substHom_variable line 133
lemma OAI.SectionCompletion.substHom_variables_span_maximal line 146
lemma OAI.SmallCM.integral_eq_scalar_of_algClosed line 168
lemma OAI.SmallCM.integral_maximal_nilpotent line 177

lemma OAI.SmallCM.integral_image_of_base_scalars line 204

Source documentation

Integrality descends to the ground field when the image of the coefficient algebra consists of scalars. This is used after killing the original cone sections, not as an assumed finiteness of the completed closed fiber.

lemma integral_image_of_base_scalars
    {k B N Q : Type*} [Field k] [CommRing B] [CommRing N] [CommRing Q] [Nontrivial Q]
    [Algebra k B] [Algebra k N] [Algebra B N] [IsScalarTower k B N] [Algebra k Q]
    (f : N →ₐ[k] Q)
    (hf : ∀ b : B, f (algebraMap B N b) ∈ (⊥ : Subalgebra k Q))
    {x : N} (hx : IsIntegral B x) : IsIntegral k (f x) := by
…

lemma OAI.SmallCM.adjoin_hom_mem_bot line 224
lemma OAI.SmallCM.integralClosure_image_of_base_scalars line 250
abbrev OAI.ExplicitCone.normalizedPolynomials line 270
def OAI.ExplicitCone.normalizedPolynomialEquiv line 272
def OAI.ExplicitCone.normalizedPolynomialToSeries line 277
lemma OAI.ExplicitCone.normalizedPolynomialToSeries_val line 280
lemma OAI.ExplicitCone.completedSection_mem_maximal line 283
lemma OAI.ExplicitCone.completedSectionIdeal_le_maximal line 290
lemma OAI.ExplicitCone.completedSectionIdeal_ne_top line 296
instance OAI.ExplicitCone.completedSectionQuotient_nontrivial line 300
instance OAI.ExplicitCone.completedSectionQuotient_local line 303
lemma OAI.ExplicitCone.normalized_original_section line 307
def OAI.ExplicitCone.normalizedClosedFiber line 316
lemma OAI.ExplicitCone.normalizedClosedFiber_base_scalars line 319
lemma OAI.ExplicitCone.normalizedClosedFiber_integral line 336
lemma OAI.ExplicitCone.normalizedClosedFiber_polynomial_integral line 343
theorem OAI.ExplicitCone.completedSectionIdeal_radical line 352
Source documentation
The eighteen literal source sections cut out only the closed point, including in the actual completed and normalized cone. No primaryness is assumed.
```
theorem completedSectionIdeal_radical :
    completedSectionIdeal.radical = IsLocalRing.maximalIdeal completedRing := by
…
```
Mentions: OAI.ExplicitCone.completedRing
abbrev OAI.ReesProj.sectionIdeal line 404
def OAI.ReesProj.chartSection line 405
lemma OAI.ReesProj.chartSections_generate line 408
lemma OAI.ReesProj.chartSections_generate_over_zero line 425
theorem OAI.ReesProj.chartSections_cover line 431
lemma OAI.ExplicitCone.completedSection_ne_zero line 450
theorem OAI.ExplicitCone.exists_completedSection_notMem line 460
Source documentation
The actual source sections cover every point of the punctured local spectrum.
```
theorem exists_completedSection_notMem (p : Ideal completedRing) [p.IsPrime]
    (hp : p ≠ IsLocalRing.maximalIdeal completedRing) :
    ∃ i : Fin 6 × Fin 3, completedSection i ∉ p := by
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedSection
def OAI.ExplicitCone.completedClosedPoint line 473
theorem OAI.ExplicitCone.completedPuncture_sectionCover line 476
abbrev OAI.ExplicitCone.completedBlowupSectionAt line 491
theorem OAI.ExplicitCone.completedBlowup_sectionCover line 496
Source documentation
A finite affine cover of the genuine eighteen-section blowup, not an assumed cover of a surrogate formal scheme.
```
theorem completedBlowup_sectionCover :
    ⨆ i : Fin 6 × Fin 3, Proj.basicOpen (ReesProj.homogeneous completedSectionIdeal)
      (completedBlowupSectionAt i) = ⊤ :=
…
```
Mentions: OAI.ReesProj.homogeneous, OAI.ExplicitCone.completedSectionIdeal, OAI.ExplicitCone.completedBlowupSectionAt
abbrev OAI.ExplicitCone.completedFractionChartAt line 501
def OAI.ExplicitCone.completedBlowupOpenIsoAt line 504
def OAI.FractionalAlgebraAway.denominatorAlgebra line 522
Source documentation
The elements whose denominator is a power of the given source element.
```
def denominatorAlgebra : Subalgebra R B where
…
```
lemma OAI.FractionalAlgebraAway.denominator_of_generators line 545

theorem OAI.FractionalAlgebraAway.over_closedPoint_iff line 558

Source documentation

A principal pullback of a maximal-primary ideal cuts out exactly the fiber over the closed point.

theorem over_closedPoint_iff [IsLocalRing R] (I : Ideal R)
    (hI : I.radical = IsLocalRing.maximalIdeal R) (htI : t ∈ I)
    (hmap : Ideal.map (algebraMap R B) I =
      Ideal.span ({algebraMap R B t} : Set B)) (p : Ideal B) [p.IsPrime] :
    Ideal.comap (algebraMap R B) p = IsLocalRing.maximalIdeal R ↔ algebraMap R B t ∈ p := by
…

theorem OAI.FractionalAlgebraAway.source_isLocalization line 585

Source documentation

Inverting the divisor equation in a fraction-generated algebra recovers exactly the corresponding source localization.

theorem source_isLocalization {ι : Type*} (v : ι → B) (s : ι → R)
    (hgen : Algebra.adjoin R (Set.range v) = ⊤)
    (hrel : ∀ i, v i * algebraMap R B t = algebraMap R B (s i)) :
    IsLocalization.Away t (Localization.Away (algebraMap R B t)) := by
…

def OAI.FractionalAlgebraAway.sourceAwayEquiv line 617
def OAI.ReesProj.fractionChartRatio line 638
lemma OAI.ReesProj.fractionChartRatio_generate line 642
lemma OAI.ReesProj.fractionChartRatio_relation line 658
lemma OAI.ReesProj.fractionChartScalar_injective line 669
lemma OAI.ReesProj.fractionChart_sectionIdeal line 677
Source documentation
On every chart the pulled-back section ideal is the principal ideal of that chart's distinguished section.
```
lemma fractionChart_sectionIdeal (htI : t ∈ Ideal.span (Set.range s)) (ht : t ≠ 0) :
    Ideal.map (algebraMap R (fractionChart (K := K) s t))
…
```
Mentions: OAI.ReesProj.fractionChart
def OAI.ReesProj.fractionChartAwayEquiv line 695
Source documentation
Each genuine section-fraction chart is unchanged over the source principal open where its selected section is invertible.
```
def fractionChartAwayEquiv (ht : t ≠ 0) :
    Localization.Away (algebraMap R (fractionChart (K := K) s t) t) ≃ₐ[R]
…
```
Mentions: OAI.ReesProj.fractionChart
abbrev OAI.ExplicitCone.completedFractionParameterAt line 714
lemma OAI.ExplicitCone.completedFractionParameterAt_ne_zero line 717
lemma OAI.ExplicitCone.completedFractionChart_exceptionalIdeal line 725
Source documentation
The exceptional ideal is Cartier on every one of the eighteen genuine blowup charts; the displayed local equation is a nonzerodivisor.
```
lemma completedFractionChart_exceptionalIdeal (i : Fin 6 × Fin 3) :
    Ideal.map (algebraMap completedRing (completedFractionChartAt i))
      completedSectionIdeal = Ideal.span ({completedFractionParameterAt i} :
        Set (completedFractionChartAt i)) :=
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedFractionChartAt, OAI.ExplicitCone.completedSectionIdeal, OAI.ExplicitCone.completedFractionParameterAt
def OAI.ExplicitCone.completedFractionChartAwayEquiv line 734
Source documentation
Away from its exceptional equation, every actual fraction chart is the literal completed-cone principal open. These opens cover the puncture.
```
def completedFractionChartAwayEquiv (i : Fin 6 × Fin 3) :
    Localization.Away (completedFractionParameterAt i) ≃ₐ[completedRing]
      Localization.Away (completedSection i) :=
…
```
Mentions: OAI.ExplicitCone.completedFractionParameterAt, OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedSection
instance OAI.ExplicitCone.completedFractionChartAt_finiteType line 740
instance OAI.ExplicitCone.completedFractionChartAt_noetherian line 744
lemma OAI.ExplicitCone.completedFractionParameterAt_regular line 749
theorem OAI.ExplicitCone.completedFractionChart_over_closedPoint_iff line 756
Source documentation
The exceptional equation vanishes precisely over the closed point of our fixed completed cone. This uses the proved primaryness, not a supplied assumption about the chosen degree-one sections.
```
theorem completedFractionChart_over_closedPoint_iff (i : Fin 6 × Fin 3)
    (p : Ideal (completedFractionChartAt i)) [p.IsPrime] :
    Ideal.comap (algebraMap completedRing (completedFractionChartAt i)) p =
      IsLocalRing.maximalIdeal completedRing ↔ completedFractionParameterAt i ∈ p :=
…
```
Mentions: OAI.ExplicitCone.completedFractionChartAt, OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedFractionParameterAt
def OAI.ReesProj.structuralMap line 780
def OAI.ReesProj.fractionChartInclusion line 787
instance OAI.ReesProj.(instance at line 795) line 795
lemma OAI.ReesProj.fractionChartInclusion_structuralMap line 806
Source documentation
The genuine fraction-chart presentation respects the structural map to Spec R, not just the abstract coordinate rings.
```
lemma fractionChartInclusion_structuralMap :
    fractionChartInclusion (K := K) s t ht hn ≫
…
```
Mentions: OAI.ReesProj.fractionChartInclusion
lemma OAI.ProjZeroPoints.basicOpenToSpec_apply line 844
lemma OAI.ProjZeroPoints.fromZero_mem_basicOpenToSpec line 850
lemma OAI.ProjZeroPoints.toSpecZero_mem line 858