NYLL
Module

ProjectiveInfinityIntersection.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.ProjectiveInfinityIntersection
9 declarations indexed from sourceView source ↗

Module documentation

Intersection equations in the actual projective local ring

The equations w and v-u*w are sent to the stalk of the projective line through the genuine chart germ map. The chart stalk isomorphism carries their generated ideal to the localized polynomial intersection ideal. Consequently the quotient of the actual projective stalk is isomorphic to the previously computed localized quotient, and their module lengths agree. The length comparison uses the order isomorphism on ideals, without changing or reconstructing the scalar structures of either quotient.

Over the integers localized at a rational prime, this length is the integer p-adic valuation of the nonzero denominator. This is the projective-stalk calculation needed in Lemma 2.3 of Shimizu and Yamaguchi, On branched coverings of the projective line over the integers. The comparison with the global integral section ideals through coefficient localization and the normal-crossing criterion are separate requirements.

Imports17
Imported by2

Declarations

abbrev

ProjectiveInfinityLocalRing

L59 ↗
ShimizuYamaguchi26BranchedCoverings.ProjectiveInfinityLocalRing
Documentation

The actual local ring at the infinity-chart point of the projective line.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
abbrev ProjectiveInfinityLocalRing (R : Type u) [CommRing R] [IsLocalRing R]
def

projectiveInfinityIntersectionIdeal

L63 ↗
ShimizuYamaguchi26BranchedCoverings.projectiveInfinityIntersectionIdeal
Documentation

The ideal generated by the germs of the two explicit chart equations.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
def projectiveInfinityIntersectionIdeal (u v : R) : Ideal (ProjectiveInfinityLocalRing R)
theorem

projectiveInfinityIntersectionIdeal_eq

L67 ↗
ShimizuYamaguchi26BranchedCoverings.projectiveInfinityIntersectionIdeal_eq
Documentation

The stalk ideal is generated by the coordinate germ and the second section equation.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
theorem projectiveInfinityIntersectionIdeal_eq (u v : R) :
    projectiveInfinityIntersectionIdeal u v =
      Ideal.span {infinityChartGerm R Polynomial.X,
        infinityChartGerm R (Polynomial.C v) -
          infinityChartGerm R (Polynomial.C u) * infinityChartGerm R Polynomial.X}
theorem

map_projectiveInfinityIntersectionIdeal

L76 ↗
ShimizuYamaguchi26BranchedCoverings.map_projectiveInfinityIntersectionIdeal
Documentation

The actual chart stalk isomorphism identifies the two generated ideals.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
theorem map_projectiveInfinityIntersectionIdeal (u v : R) :
    (projectiveInfinityIntersectionIdeal u v).map
        (projectiveInfinityStalkEquiv R).toRingHom =
      (infinityIntersectionIdeal u v).map (algebraMap R[X] (InfinityChartLocalRing R))
abbrev

ProjectiveInfinityIntersectionAlgebra

L90 ↗
ShimizuYamaguchi26BranchedCoverings.ProjectiveInfinityIntersectionAlgebra
Documentation

The quotient by the two equation germs in the projective local ring.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
abbrev ProjectiveInfinityIntersectionAlgebra (u v : R)
def

projectiveInfinityIntersectionEquiv

L94 ↗
ShimizuYamaguchi26BranchedCoverings.projectiveInfinityIntersectionEquiv
Documentation

The explicit chart isomorphism descends to the actual local intersection quotients.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
def projectiveInfinityIntersectionEquiv (u v : R) :
    ProjectiveInfinityIntersectionAlgebra u v ≃+* LocalizedInfinityIntersectionAlgebra u v
theorem

projectiveInfinityIntersection_length_eq

L101 ↗
ShimizuYamaguchi26BranchedCoverings.projectiveInfinityIntersection_length_eq
Documentation

The projective stalk quotient and its polynomial localization model have equal length.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]
section LocalRing
variable [IsLocalRing R]
Lean source · statement
theorem projectiveInfinityIntersection_length_eq (u v : R) :
    Module.length (ProjectiveInfinityLocalRing R) (ProjectiveInfinityIntersectionAlgebra u v) =
      Module.length (InfinityChartLocalRing R) (LocalizedInfinityIntersectionAlgebra u v)
theorem

projectiveInfinityIntersection_length

L114 ↗
ShimizuYamaguchi26BranchedCoverings.projectiveInfinityIntersection_length
Documentation

Over a DVR, the length of the two equation germs in the projective stalk is the valuation.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem projectiveInfinityIntersection_length [IsDomain R] [IsDiscreteValuationRing R]
    (u v : R) :
    Module.length (ProjectiveInfinityLocalRing R) (ProjectiveInfinityIntersectionAlgebra u v) =
      IsDiscreteValuationRing.addVal R v
theorem

projectiveInfinityIntersection_length_int

L122 ↗
ShimizuYamaguchi26BranchedCoverings.projectiveInfinityIntersection_length_int
Documentation

Over the integers localized at p, the projective stalk calculation has exactly the normalization v_p(v) used for the denominator in Lemma 2.3.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem projectiveInfinityIntersection_length_int (p : ℕ) [Fact p.Prime]
    (u v : ℤ) (hv : v ≠ 0) :
    Module.length (ProjectiveInfinityLocalRing (IntegerPrimeLocalization p))
        (ProjectiveInfinityIntersectionAlgebra
          (algebraMap ℤ (IntegerPrimeLocalization p) u)
          (algebraMap ℤ (IntegerPrimeLocalization p) v)) =
      (padicValInt p v : ℕ∞)

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