Module

InfinityIntersection.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.InfinityIntersection

9 declarations indexed from sourceView source ↗

Module documentation

Intersection with the section at infinity

On the affine chart with coordinate w = T₁ / T₀, the equations of the section at infinity and a section given by a primitive pair (u,v) are w and v - u*w. The affine intersection of these equations has coordinate ring R[w] / (w, v-u*w).

The actual quotient algebra is identified with R / (v). When the coefficient ring is a DVR, its length as an R[w]-module is the additive valuation of v. Both the isomorphism and the equality of lengths are proved from the two equations; no intersection comparison is supplied as an assumption.

This is the affine algebra calculation in Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. The projective-stalk calculation and the integer p-adic normalization are developed in ProjectiveInfinityIntersection; the primitive section images are constructed in RationalSection. Identifying the original global section ideals in the local chart and the normal-crossing criterion remains separate.

Imports13

Mathlib.Algebra.Polynomial.Basic
Mathlib.Algebra.Polynomial.Eval.Defs
Mathlib.AlgebraicGeometry.Scheme
Mathlib.Data.Set.Image
Mathlib.Order.KrullDimension
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.Length
Mathlib.RingTheory.Polynomial.Quotient
Mathlib.RingTheory.PrincipalIdealDomain
Mathlib.Tactic.Ring

Imported by7

def

infinityIntersectionIdeal

L55 ↗

ShimizuYamaguchi26BranchedCoverings.infinityIntersectionIdeal

Documentation

The ideal of the two section equations on the chart with coordinate w.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

def infinityIntersectionIdeal (u v : R) : Ideal R[X]

theorem

infinityIntersectionIdeal_map

L59 ↗

ShimizuYamaguchi26BranchedCoverings.infinityIntersectionIdeal_map

Documentation

Extending coefficients preserves the two concrete intersection equations.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem infinityIntersectionIdeal_map {S : Type*} [CommRing S] (f : R →+* S) (u v : R) :
    (infinityIntersectionIdeal u v).map (Polynomial.mapRingHom f) =
      infinityIntersectionIdeal (f u) (f v)

theorem

infinityIntersectionIdeal_eq

L67 ↗

ShimizuYamaguchi26BranchedCoverings.infinityIntersectionIdeal_eq

Documentation

Eliminating the chart coordinate leaves exactly the denominator equation.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem infinityIntersectionIdeal_eq (u v : R) :
    infinityIntersectionIdeal u v = Ideal.span {Polynomial.C v, Polynomial.X}

abbrev

InfinityIntersectionAlgebra

L75 ↗

ShimizuYamaguchi26BranchedCoverings.InfinityIntersectionAlgebra

Documentation

The actual affine intersection algebra of the two section equations.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

abbrev InfinityIntersectionAlgebra (u v : R)

def

infinityIntersectionEquiv

L78 ↗

ShimizuYamaguchi26BranchedCoverings.infinityIntersectionEquiv

Documentation

Evaluation at zero constructs the affine intersection algebra as R / (v).

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

def infinityIntersectionEquiv (u v : R) :
    InfinityIntersectionAlgebra u v ≃ₐ[R] R ⧸ Ideal.span {v}

def

infinityIntersectionIso

L87 ↗

ShimizuYamaguchi26BranchedCoverings.infinityIntersectionIso

Documentation

The affine intersection is the spectrum of the actual denominator quotient.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

def infinityIntersectionIso (u v : R) :
    Spec (CommRingCat.of (InfinityIntersectionAlgebra u v)) ≅
      Spec (CommRingCat.of (R ⧸ Ideal.span {v}))

theorem

infinityIntersection_algebraMap_surjective

L93 ↗

ShimizuYamaguchi26BranchedCoverings.infinityIntersection_algebraMap_surjective

Documentation

Every intersection-algebra element is the image of a coefficient.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem infinityIntersection_algebraMap_surjective (u v : R) :
    Function.Surjective (algebraMap R (InfinityIntersectionAlgebra u v))

theorem

infinityIntersection_length_eq_base

L104 ↗

ShimizuYamaguchi26BranchedCoverings.infinityIntersection_length_eq_base

Documentation

The polynomial-ring length of the affine intersection equals its coefficient-ring length. The comparison follows from the two actual surjective coefficient maps.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem infinityIntersection_length_eq_base (u v : R) :
    Module.length R[X] (InfinityIntersectionAlgebra u v) =
      Module.length R (InfinityIntersectionAlgebra u v)

theorem

infinityIntersection_length

L121 ↗

ShimizuYamaguchi26BranchedCoverings.infinityIntersection_length

Documentation

On a DVR coefficient ring, the affine intersection length is the valuation of v. This includes the infinite length when v = 0, so no hidden distinctness assumption is needed for the algebra calculation.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem infinityIntersection_length [IsDomain R] [IsDiscreteValuationRing R] (u v : R) :
    Module.length R[X] (InfinityIntersectionAlgebra u v) =
      IsDiscreteValuationRing.addVal R v

Module documentation

Intersection with the section at infinity

Declarations