CompletedCartierNoetherian.lean`

80 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.finiteType_of_sup_ranges line 7
instance OAI.CompletedCartierChart.sourceAlgebra line 37
instance OAI.CompletedCartierChart.sourceTower line 40
instance OAI.CompletedCartierChart.finiteType line 43
lemma OAI.CompletedCartierChart.noetherian line 47
theorem OAI.RegularCartierLocal.spanFinrank_le_map_add_one line 64
Source documentation
Lifting a minimal generating set through a surjection with principal kernel adds at most one generator. No regularity hypothesis is hidden in this elementary embedding-dimension estimate.
```
theorem spanFinrank_le_map_add_one (f : R →+* S) (hf : Function.Surjective f)
    (I : Ideal R) (hI : I.FG) (x : R) (hxI : x ∈ I)
    (hker : RingHom.ker f = Ideal.span {x}) :
    I.spanFinrank ≤ (I.map f).spanFinrank + 1 := by
…
```

theorem OAI.RegularCartierLocal.isRegularLocalRing_of_quotient line 104

Source documentation

A regular Cartier quotient of a Noetherian local ring lifts regularity to the ambient ring.

theorem isRegularLocalRing_of_quotient [IsLocalRing R] [IsNoetherianRing R]
    (x : R) (hx : x ∈ maximalIdeal R) (hreg : IsSMulRegular R x)
    [IsRegularLocalRing (R ⧸ Ideal.span {x})] : IsRegularLocalRing R := by
…

theorem OAI.RegularCartierLocalization.regular_at_prime line 127
Source documentation
Every point of a regular effective principal divisor in a Noetherian integral scheme is a regular point of the ambient scheme.
```
theorem regular_at_prime (x : R) (hx : x ≠ 0)
    [IsRegularRing (R ⧸ Ideal.span {x})]
    (p : Ideal R) [p.IsPrime] (hxp : x ∈ p) :
    IsRegularLocalRing (Localization.AtPrime p) := by
…
```
abbrev OAI.ExplicitCone.completedAffineChart line 162
Source documentation
The Cartier chart generated by the degreewise completed cone and the constants of its Proj basic open, inside the coefficient power-series ring.
```
abbrev completedAffineChart := CompletedCartierChart.chart pieces sectionChart
…
```
Mentions: OAI.CompletedCartierChart.chart, OAI.ExplicitCone.pieces, OAI.ExplicitCone.sectionChart
instance OAI.ExplicitCone.completedAffineCommRing line 165
instance OAI.ExplicitCone.completedAffineRing line 166
instance OAI.ExplicitCone.completedAffineSemiring line 167
abbrev OAI.ExplicitCone.completedAffineSource line 169
abbrev OAI.ExplicitCone.completedAffineParameter line 173
theorem OAI.ExplicitCone.completedAffineSource_injective line 178
theorem OAI.ExplicitCone.completedAffineParameter_ne_zero line 184
instance OAI.ExplicitCone.completedAffine_finiteType line 189
instance OAI.ExplicitCone.completedAffine_noetherian line 193
def OAI.ExplicitCone.completedAffineExceptionalEquiv line 200
Source documentation
The exceptional divisor on the completed affine chart is isomorphic to the smooth chart of the projective section ring.
```
def completedAffineExceptionalEquiv :
    (completedAffineChart ⧸ Ideal.span {completedAffineParameter}) ≃ₐ[ℂ] sectionChart :=
…
```
Mentions: OAI.ExplicitCone.completedAffineChart, OAI.ExplicitCone.completedAffineParameter, OAI.ExplicitCone.sectionChart
instance OAI.ExplicitCone.completedAffineExceptional_regular line 206
theorem OAI.ExplicitCone.completedAffine_regular_at_exceptional line 213
Source documentation
In particular every prime lying on its exceptional divisor is a genuine regular local ring of the algebraic completed-cone chart.
```
theorem completedAffine_regular_at_exceptional (p : Ideal completedAffineChart) [p.IsPrime]
    (hp : completedAffineParameter ∈ p) : IsRegularLocalRing (Localization.AtPrime p) :=
…
```
Mentions: OAI.ExplicitCone.completedAffineChart, OAI.ExplicitCone.completedAffineParameter
def OAI.ExplicitCone.completedChartMap line 226
Source documentation
The actual completed cone embeds in the formal Cartier chart over the literal z₀z₁z₄ section open. This does NOT assert that the formal chart is the uncompleted affine blowup base change.
```
def completedChartMap : completedRing →ₐ[ℂ] PowerSeries sectionChart :=
…
```
Mentions: OAI.ExplicitCone.completedRing, OAI.ExplicitCone.sectionChart
theorem OAI.ExplicitCone.completedChartMap_injective line 230
lemma OAI.ExplicitCone.completedChartMap_coeff line 234
def OAI.ExplicitCone.completedSection line 241
Source documentation
The original degree-one section, as an element of the degreewise completion used in MainClaim.
```
def completedSection (i : Fin 6 × Fin 3) : completedRing :=
…
```
Mentions: OAI.ExplicitCone.completedRing
lemma OAI.ExplicitCone.completedChartMap_section line 248
lemma OAI.ExplicitCone.completedChartMap_baseSection line 263
def OAI.FractionChartComparison.fieldMap line 278
lemma OAI.FractionChartComparison.fieldMap_algebraMap line 287
def OAI.FractionChartComparison.chart line 292
Source documentation
The literal fraction algebra of an ordinary blowup chart.
```
def chart {ι : Type*} (s : ι → R) (t : R) : Subalgebra R (FractionRing R) :=
…
```
lemma OAI.FractionChartComparison.fieldMap_ratio line 296
lemma OAI.FractionChartComparison.map_chart line 310

def OAI.FractionChartComparison.chartEquiv line 327

Source documentation

A domain generated by actual section ratios is the actual fraction chart, not merely a ring agreeing with it modulo the exceptional equation.

noncomputable def chartEquiv {ι : Type*} (s : ι → R) (t : R) (b : ι → B)
    (hf : Function.Injective (algebraMap R B)) (ht : t ≠ 0)
    (hb : ∀ i, b i * algebraMap R B t = algebraMap R B (s i))
    (hgen : Algebra.adjoin R (Set.range b) = ⊤) : chart s t ≃ₐ[R] B :=
…

Mentions: OAI.FractionChartComparison.chart

lemma OAI.AlgebraGenerators.adjoin_of_sup_ranges line 339
lemma OAI.CompletedCartierChart.adjoin_of_constants line 366
abbrev OAI.ExplicitCone.completedAffineConstant line 378
abbrev OAI.ExplicitCone.completedAffineRatio line 382
lemma OAI.ExplicitCone.completedAffine_section line 385
lemma OAI.ExplicitCone.completedAffine_baseSection line 391
lemma OAI.ExplicitCone.completedSection_base_ne_zero line 396
lemma OAI.ExplicitCone.sectionRatio_generates line 402
lemma OAI.ExplicitCone.completedAffineRatio_generates line 414
abbrev OAI.ExplicitCone.completedFractionChart line 422
Source documentation
The ordinary fraction chart for the original eighteen completed sections. This is the actual affine algebra R[s_i/s_00], not a formal tensor product.
```
abbrev completedFractionChart := FractionChartComparison.chart completedSection
…
```
Mentions: OAI.FractionChartComparison.chart, OAI.ExplicitCone.completedSection
def OAI.ExplicitCone.completedFractionChartEquiv line 427
Source documentation
The algebraic power-series realization coincides with the literal fraction chart of the blowup of the eighteen-section ideal.
```
def completedFractionChartEquiv : completedFractionChart ≃ₐ[completedRing]
    completedAffineChart :=
…
```
Mentions: OAI.ExplicitCone.completedFractionChart, OAI.ExplicitCone.completedRing, OAI.ExplicitCone.completedAffineChart
def OAI.ReesProj.homogeneous line 446
Source documentation
Degree-n polynomials inside the coefficient section algebra.
```
def homogeneous (n : ℕ) : Submodule R (reesAlgebra I) where
…
```
lemma OAI.ReesProj.homogeneous_eq_monomial line 458
instance OAI.ReesProj.homogeneousGradedMonoid line 467
def OAI.ReesProj.homogeneousPart line 475
lemma OAI.ReesProj.homogeneousPart_coe line 479
def OAI.ReesProj.decomposePolynomial line 484
Source documentation
Finite support is the actual polynomial support, not an assumption of a formal infinite homogeneous decomposition.
```
noncomputable def decomposePolynomial (p : reesAlgebra I) :
    ⨁ n, homogeneous I n :=
…
```
Mentions: OAI.ReesProj.homogeneous
lemma OAI.ReesProj.decomposePolynomial_apply line 488
lemma OAI.ReesProj.coeff_recompose line 500
instance OAI.ReesProj.polynomialGradedRing line 515
def OAI.ReesProj.proj line 535
Source documentation
The projective scheme of the section-coefficient algebra.
```
noncomputable def proj : AlgebraicGeometry.Scheme :=
…
```
instance OAI.ReesProj.degreeZeroTower line 539
instance OAI.ReesProj.finiteType_over_degreeZero line 544
instance OAI.ReesProj.projProper line 548
def OAI.ReesProj.zeroEquiv line 552
Source documentation
The degree-zero part of the actual Rees algebra is the original ring.
```
def zeroEquiv : R ≃ₐ[R] homogeneous I 0 :=
…
```
Mentions: OAI.ReesProj.homogeneous
lemma OAI.FractionChartComparison.ratio_mem_of_mem_span line 575
lemma OAI.FractionChartComparison.scaled_mem_of_mem_power line 589
def OAI.ReesProj.linearSection line 614
Source documentation
The actual degree-one Rees element associated to t ∈ I.
```
def linearSection (t : R) (ht : t ∈ I) : reesAlgebra I :=
…
```
lemma OAI.ReesProj.linearSection_homogeneous line 617
abbrev OAI.ReesProj.homogeneousChart line 622
def OAI.ReesProj.evaluateOne line 625
lemma OAI.ReesProj.evaluateOne_linearSection line 629
lemma OAI.ReesProj.mapped_ne_zero line 635
def OAI.ReesProj.homogeneousChartMap line 638
lemma OAI.ReesProj.homogeneousChartMap_mk line 644
lemma OAI.ReesProj.homogeneousChartMap_injective line 661
lemma OAI.ReesProj.scaledCoefficient_mem_range line 685
instance OAI.ReesProj.homogeneousChartScalarAlgebra line 698
lemma OAI.ReesProj.homogeneousChartMap_scalar line 702
def OAI.ReesProj.fractionChart line 728
lemma OAI.ReesProj.ratio_mem_of_mem_span line 732
lemma OAI.ReesProj.scaled_mem_of_mem_power line 747
abbrev OAI.ReesProj.generatedChart line 764
def OAI.ReesProj.generatedChartHom line 766
lemma OAI.ReesProj.generatedChartHom_range line 770
def OAI.ReesProj.generatedChartEquiv line 789
Source documentation
A literal Rees-Proj affine chart is the usual algebra of section fractions.
```
def generatedChartEquiv : generatedChart s t ht ≃ₐ[R] fractionChart (K := K) s t :=
…
```
Mentions: OAI.ReesProj.generatedChart, OAI.ReesProj.fractionChart
def OAI.ReesProj.basicOpenIsoFractionChart line 796