Module

IntegerChartLocalization.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegerChartLocalization

8 declarations indexed from sourceView source ↗

Module documentation

The integral infinity chart and localization of the coefficient ring

The point (p, X) in Spec ℤ[X] is defined by pulling the prime ideal (p) back along the constant-coefficient map. Its ideal is the inverse image of the infinity chart closed point after localizing the coefficient ring at p.

The polynomial ring over ℤ_(p) is the localization of ℤ[X] at constant denominators prime to p. Localizing again at the chart point therefore gives the same algebra as localizing ℤ[X] directly at (p, X). The algebra isomorphism commutes with the actual polynomial localization maps.

This supplies the comparison of integral and localized chart rings used in Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers.

Imports18

Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.IntegerLocalizationValuation
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.LocalizedInfinityIntersection
Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Polynomial.Basic
Mathlib.Algebra.Polynomial.Coeff
Mathlib.Algebra.Polynomial.Eval.Coeff
Mathlib.Data.Set.Image
Mathlib.RingTheory.Ideal.Int
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Localization.Algebra
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.Basic
Mathlib.RingTheory.Localization.LocalizationLocalization
Mathlib.RingTheory.Polynomial.Ideal
Mathlib.RingTheory.PolynomialAlgebra
Mathlib.RingTheory.Spectrum.Prime.Basic

Imported by7

def

integerInfinityChartIdeal

L52 ↗

ShimizuYamaguchi26BranchedCoverings.integerInfinityChartIdeal

Documentation

The point ideal in the integral infinity chart, defined by its constant term.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] Polynomial.algebra

Lean source · statement

def integerInfinityChartIdeal (p : ℕ) : Ideal ℤ[X]

instance

(anonymous instance)

L55 ↗

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] Polynomial.algebra

Lean source · statement

instance (p : ℕ) [Fact p.Prime] : (integerInfinityChartIdeal p).IsMaximal

theorem

integerInfinityChartIdeal_eq_span

L59 ↗

ShimizuYamaguchi26BranchedCoverings.integerInfinityChartIdeal_eq_span

Documentation

The evaluation description of the integral chart point is exactly (p, X).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] Polynomial.algebra

Lean source · statement

theorem integerInfinityChartIdeal_eq_span (p : ℕ) :
    integerInfinityChartIdeal p = Ideal.span {Polynomial.C (p : ℤ), Polynomial.X}

def

integerInfinityChartPoint

L73 ↗

ShimizuYamaguchi26BranchedCoverings.integerInfinityChartPoint

Documentation

The actual prime-spectrum point of the integral chart above the prime p.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] Polynomial.algebra

Lean source · statement

def integerInfinityChartPoint (p : ℕ) [Fact p.Prime] : PrimeSpectrum ℤ[X]

abbrev

IntegerInfinityChartLocalRing

L77 ↗

ShimizuYamaguchi26BranchedCoverings.IntegerInfinityChartLocalRing

Documentation

The local ring of the integral affine chart at (p, X).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] Polynomial.algebra

Lean source · statement

abbrev IntegerInfinityChartLocalRing (p : ℕ) [Fact p.Prime] : Type

theorem

infinityChartClosedPointIdeal_comap

L81 ↗

ShimizuYamaguchi26BranchedCoverings.infinityChartClosedPointIdeal_comap

Documentation

The closed point after coefficient localization lies over the integral point (p, X).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] Polynomial.algebra

Lean source · statement

theorem infinityChartClosedPointIdeal_comap (p : ℕ) [Fact p.Prime] :
    (infinityChartClosedPointIdeal (IntegerPrimeLocalization p)).comap
        (algebraMap ℤ[X] (IntegerPrimeLocalization p)[X]) =
      integerInfinityChartIdeal p

def

integerInfinityChartLocalizationEquiv

L98 ↗

ShimizuYamaguchi26BranchedCoverings.integerInfinityChartLocalizationEquiv

Documentation

Localizing coefficients and then the chart point gives its integral chart local ring.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] Polynomial.algebra

Lean source · statement

def integerInfinityChartLocalizationEquiv (p : ℕ) [Fact p.Prime] :
    IntegerInfinityChartLocalRing p ≃ₐ[ℤ[X]]
      InfinityChartLocalRing (IntegerPrimeLocalization p)

theorem

integerInfinityChartLocalizationEquiv_algebraMap

L119 ↗

ShimizuYamaguchi26BranchedCoverings.integerInfinityChartLocalizationEquiv_algebraMap

Documentation

The comparison preserves the image of every integral polynomial.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] Polynomial.algebra

Lean source · statement

theorem integerInfinityChartLocalizationEquiv_algebraMap
    (p : ℕ) [Fact p.Prime] (f : ℤ[X]) :
    integerInfinityChartLocalizationEquiv p
        (algebraMap ℤ[X] (IntegerInfinityChartLocalRing p) f) =
      algebraMap ℤ[X] (InfinityChartLocalRing (IntegerPrimeLocalization p)) f

Module documentation

The integral infinity chart and localization of the coefficient ring

Declarations