NYLL
Module

LocalizedInfinityIntersection.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.LocalizedInfinityIntersection
12 declarations indexed from sourceView source ↗

Module documentation

The localized intersection with infinity

For a local coefficient ring R, the infinity chart point over its closed point has prime ideal (maximalIdeal R, X) in R[X]. Localizing at this actual ideal and quotienting by the two section equations (X, v-u*X) gives the same algebra as quotienting before localization. The reason is proved concretely: X vanishes in the intersection, so every polynomial outside the point ideal maps to its unit constant coefficient.

Over a DVR, the length over this localized chart ring is therefore the additive valuation of v. This supplies the localization comparison in the infinity-chart calculation of Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. The projective chart/stalk identification and normalization as the integer p-adic valuation are developed in ProjectiveInfinityIntersection. The comparison with global section ideals and normal crossings is separate.

Imports16
  • Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.InfinityIntersection
  • Mathlib.AlgebraicGeometry.Spec
  • Mathlib.RingTheory.DiscreteValuationRing.Basic
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Mathlib.RingTheory.Length
  • Mathlib.Algebra.Algebra.Tower
  • Mathlib.Algebra.Polynomial.AlgebraMap
  • Mathlib.Algebra.Polynomial.Coeff
  • Mathlib.Algebra.Polynomial.Inductions
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.Ideal.Over
  • Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.RingTheory.Localization.Basic
  • Mathlib.RingTheory.Localization.Ideal
  • Mathlib.RingTheory.Polynomial.Ideal
Imported by5

Declarations

theorem

infinityIntersection_polynomial_eq_constantCoeff

L56 ↗
ShimizuYamaguchi26BranchedCoverings.infinityIntersection_polynomial_eq_constantCoeff
Documentation

In the intersection algebra, every polynomial equals its constant 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_polynomial_eq_constantCoeff (u v : R) (f : R[X]) :
    algebraMap R[X] (InfinityIntersectionAlgebra u v) f =
      algebraMap R (InfinityIntersectionAlgebra u v) (Polynomial.constantCoeff f)
def

infinityChartClosedPointIdeal

L77 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartClosedPointIdeal
Documentation

The infinity chart closed point above the closed point of the coefficient ring.

Source context 8 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]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
def infinityChartClosedPointIdeal (R : Type u) [CommRing R] [IsLocalRing R] : Ideal R[X]
instance

infinityChartClosedPointIdeal_isMaximal

L81 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartClosedPointIdeal_isMaximal
Documentation

This concrete chart point is closed.

Source context 8 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]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
instance infinityChartClosedPointIdeal_isMaximal :
    (infinityChartClosedPointIdeal R).IsMaximal
theorem

infinityChartClosedPointIdeal_eq

L86 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartClosedPointIdeal_eq
Documentation

The evaluation description is exactly the coordinate ideal (maximalIdeal R, X).

Source context 8 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]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
theorem infinityChartClosedPointIdeal_eq :
    infinityChartClosedPointIdeal R =
      (IsLocalRing.maximalIdeal R).map Polynomial.C ⊔ Ideal.span {Polynomial.X}
abbrev

InfinityChartLocalRing

L100 ↗
ShimizuYamaguchi26BranchedCoverings.InfinityChartLocalRing
Documentation

The actual local ring of the polynomial chart at the infinity section point.

Source context 8 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]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
abbrev InfinityChartLocalRing (R : Type u) [CommRing R] [IsLocalRing R]
abbrev

LocalizedInfinityIntersectionAlgebra

L104 ↗
ShimizuYamaguchi26BranchedCoverings.LocalizedInfinityIntersectionAlgebra
Documentation

The two section equations in the localized chart ring.

Source context 8 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]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
abbrev LocalizedInfinityIntersectionAlgebra (u v : R)
theorem

infinityIntersection_denominators_are_units

L108 ↗
ShimizuYamaguchi26BranchedCoverings.infinityIntersection_denominators_are_units
Source context 8 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]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
theorem infinityIntersection_denominators_are_units (u v : R) :
    Algebra.algebraMapSubmonoid (InfinityIntersectionAlgebra u v)
        (infinityChartClosedPointIdeal R).primeCompl ≤
      IsUnit.submonoid (InfinityIntersectionAlgebra u v)
def

localizedInfinityIntersectionEquiv

L121 ↗
ShimizuYamaguchi26BranchedCoverings.localizedInfinityIntersectionEquiv
Documentation

Localizing the actual intersection quotient does not change it. Every inverted polynomial has a unit constant coefficient in the quotient.

Source context 8 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]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
def localizedInfinityIntersectionEquiv (u v : R) :
    LocalizedInfinityIntersectionAlgebra u v ≃ₐ[R[X]] InfinityIntersectionAlgebra u v
def

localizedInfinityIntersectionIso

L132 ↗
ShimizuYamaguchi26BranchedCoverings.localizedInfinityIntersectionIso
Documentation

The scheme of the localized intersection is the spectrum of the denominator quotient.

Source context 8 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]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
def localizedInfinityIntersectionIso (u v : R) :
    Spec (CommRingCat.of (LocalizedInfinityIntersectionAlgebra u v)) ≅
      Spec (CommRingCat.of (R ⧸ Ideal.span {v}))
theorem

localizedInfinityIntersection_algebraMap_surjective

L140 ↗
ShimizuYamaguchi26BranchedCoverings.localizedInfinityIntersection_algebraMap_surjective
Documentation

The chart polynomial ring already surjects onto the localized intersection.

Source context 8 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]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
theorem localizedInfinityIntersection_algebraMap_surjective (u v : R) :
    Function.Surjective (algebraMap R[X] (LocalizedInfinityIntersectionAlgebra u v))
theorem

localizedInfinityIntersection_length_eq

L150 ↗
ShimizuYamaguchi26BranchedCoverings.localizedInfinityIntersection_length_eq
Documentation

The length over the actual localized chart equals the affine intersection length.

Source context 8 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]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
theorem localizedInfinityIntersection_length_eq (u v : R) :
    Module.length (InfinityChartLocalRing R) (LocalizedInfinityIntersectionAlgebra u v) =
      Module.length R[X] (InfinityIntersectionAlgebra u v)
theorem

localizedInfinityIntersection_length

L170 ↗
ShimizuYamaguchi26BranchedCoverings.localizedInfinityIntersection_length
Documentation

The localized infinity-chart intersection multiplicity over a DVR is the valuation of 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
theorem localizedInfinityIntersection_length [IsDomain R] [IsDiscreteValuationRing R] (u v : R) :
    Module.length (InfinityChartLocalRing R) (LocalizedInfinityIntersectionAlgebra u v) =
      IsDiscreteValuationRing.addVal R v

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.