Module

IntegerProjectiveIntersection.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegerProjectiveIntersection

10 declarations indexed from sourceView source ↗

Module documentation

The intersection calculation in the integral projective line

The actual point of ℙ¹_ℤ represented by (p,w) in the infinity chart has local ring ℤ[w]_(p,w). The chart stalk isomorphism and the coefficient localization comparison identify this ring with the local chart ring over ℤ_(p), preserving the germs of every integral polynomial.

The ideal generated by the actual germs of w and v-u*w is consequently carried to the same two equations over ℤ_(p). Its quotient is isomorphic to the projective-stalk intersection quotient already constructed over the local coefficient ring, and has length v_p(v) when v is nonzero.

This supplies the integral projective-stalk calculation in Lemma 2.3 of Shimizu and Yamaguchi, On branched coverings of the projective line over the integers. Identifying these equation ideals with the original integral section ideals, transporting a general pair by the Bezout coordinate change, and proving the normal-crossing criterion remain separate requirements.

Imports20

Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.IntegerLocalizationValuation
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.InfinityChartStalk
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.InfinityIntersection
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegerChartLocalization
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.LocalizedInfinityIntersection
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.ProjectiveInfinityIntersection
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.StandardAffineChart
Mathlib.Algebra.Algebra.Tower
Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.Algebra.Ring.Equiv
Mathlib.Algebra.Ring.Hom.Defs
Mathlib.AlgebraicGeometry.Scheme
Mathlib.AlgebraicGeometry.Spec
Mathlib.Data.ENat.Basic
Mathlib.NumberTheory.Padics.PadicVal.Basic
Mathlib.Order.KrullDimension
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Length
Mathlib.RingTheory.PolynomialAlgebra

Imported by6

def

integerProjectiveInfinityPoint

L58 ↗

ShimizuYamaguchi26BranchedCoverings.integerProjectiveInfinityPoint

Documentation

The actual point (p,w) of the integral projective line in the infinity chart.

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 integerProjectiveInfinityPoint (p : ℕ) [Fact p.Prime] : ProjectiveLine ℤ

abbrev

IntegerProjectiveInfinityLocalRing

L62 ↗

ShimizuYamaguchi26BranchedCoverings.IntegerProjectiveInfinityLocalRing

Documentation

The actual local ring of the integral projective line at this point.

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 IntegerProjectiveInfinityLocalRing (p : ℕ) [Fact p.Prime]

def

integerProjectiveInfinityStalkEquiv

L66 ↗

ShimizuYamaguchi26BranchedCoverings.integerProjectiveInfinityStalkEquiv

Documentation

The integral projective stalk equals the chart local ring after coefficient localization.

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 integerProjectiveInfinityStalkEquiv (p : ℕ) [Fact p.Prime] :
    IntegerProjectiveInfinityLocalRing p ≃+* InfinityChartLocalRing (IntegerPrimeLocalization p)

theorem

integerProjectiveInfinityStalkEquiv_germ

L72 ↗

ShimizuYamaguchi26BranchedCoverings.integerProjectiveInfinityStalkEquiv_germ

Documentation

The comparison preserves the actual germ of each 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 integerProjectiveInfinityStalkEquiv_germ
    (p : ℕ) [Fact p.Prime] (f : ℤ[X]) :
    integerProjectiveInfinityStalkEquiv p
        (infinityChartGermAt ℤ (integerInfinityChartPoint p) f) =
      algebraMap ℤ[X] (InfinityChartLocalRing (IntegerPrimeLocalization p)) f

def

integerProjectiveInfinityIntersectionIdeal

L85 ↗

ShimizuYamaguchi26BranchedCoverings.integerProjectiveInfinityIntersectionIdeal

Documentation

The ideal of the two equation germs in the actual integral projective stalk.

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 integerProjectiveInfinityIntersectionIdeal (p : ℕ) [Fact p.Prime] (u v : ℤ) :
    Ideal (IntegerProjectiveInfinityLocalRing p)

theorem

map_integerProjectiveInfinityIntersectionIdeal

L90 ↗

ShimizuYamaguchi26BranchedCoverings.map_integerProjectiveInfinityIntersectionIdeal

Documentation

The stalk comparison carries the two integral equations to their coefficient-localized forms.

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 map_integerProjectiveInfinityIntersectionIdeal
    (p : ℕ) [Fact p.Prime] (u v : ℤ) :
    (integerProjectiveInfinityIntersectionIdeal p u v).map
        (integerProjectiveInfinityStalkEquiv p).toRingHom =
      (infinityIntersectionIdeal (algebraMap ℤ (IntegerPrimeLocalization p) u)
        (algebraMap ℤ (IntegerPrimeLocalization p) v)).map
          (algebraMap (IntegerPrimeLocalization p)[X]
            (InfinityChartLocalRing (IntegerPrimeLocalization p)))

abbrev

IntegerProjectiveInfinityIntersectionAlgebra

L117 ↗

ShimizuYamaguchi26BranchedCoverings.IntegerProjectiveInfinityIntersectionAlgebra

Documentation

The quotient by the two equation germs in the integral projective stalk.

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 IntegerProjectiveInfinityIntersectionAlgebra (p : ℕ) [Fact p.Prime] (u v : ℤ)

def

integerProjectiveInfinityIntersectionEquiv

L122 ↗

ShimizuYamaguchi26BranchedCoverings.integerProjectiveInfinityIntersectionEquiv

Documentation

The two projective-stalk intersection quotients agree before and after coefficient localization.

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 integerProjectiveInfinityIntersectionEquiv (p : ℕ) [Fact p.Prime] (u v : ℤ) :
    IntegerProjectiveInfinityIntersectionAlgebra p u v ≃+*
      ProjectiveInfinityIntersectionAlgebra (algebraMap ℤ (IntegerPrimeLocalization p) u)
        (algebraMap ℤ (IntegerPrimeLocalization p) v)

theorem

integerProjectiveInfinityIntersection_length_eq

L137 ↗

ShimizuYamaguchi26BranchedCoverings.integerProjectiveInfinityIntersection_length_eq

Documentation

Coefficient localization preserves the length of the quotient of the actual projective stalk.

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 integerProjectiveInfinityIntersection_length_eq
    (p : ℕ) [Fact p.Prime] (u v : ℤ) :
    Module.length (IntegerProjectiveInfinityLocalRing p)
        (IntegerProjectiveInfinityIntersectionAlgebra p u v) =
      Module.length (ProjectiveInfinityLocalRing (IntegerPrimeLocalization p))
        (ProjectiveInfinityIntersectionAlgebra (algebraMap ℤ (IntegerPrimeLocalization p) u)
          (algebraMap ℤ (IntegerPrimeLocalization p) v))

theorem

integerProjectiveInfinityIntersection_length

L153 ↗

ShimizuYamaguchi26BranchedCoverings.integerProjectiveInfinityIntersection_length

Documentation

The two equation germs in the original integral projective stalk have length v_p(v).

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 integerProjectiveInfinityIntersection_length
    (p : ℕ) [Fact p.Prime] (u v : ℤ) (hv : v ≠ 0) :
    Module.length (IntegerProjectiveInfinityLocalRing p)
        (IntegerProjectiveInfinityIntersectionAlgebra p u v) =
      (padicValInt p v : ℕ∞)

Module documentation

The intersection calculation in the integral projective line

Declarations