NYLL
Module

IntegralSectionIntersection.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralSectionIntersection
4 declarations indexed from sourceView source ↗

Module documentation

Intersection of the actual rational sections with the infinity section

The intersection ideal is the sum of the stalk ideals of the two actual closed section morphisms. On the infinity chart these ideals are generated by their primitive linear equations. If the second rational point is infinity, the sum is exactly the two-equation ideal already calculated in the actual integral projective stalk.

For distinct original rational points, one of them infinity, the resulting local intersection length is v_p(Δ). This is the infinity case of Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. Transport to an arbitrary pair and the normal-crossing criterion remain separate requirements of the full lemma.

Imports19
Imported by2

Declarations

def

rationalSectionIntersectionIdeal

L52 ↗
ShimizuYamaguchi26BranchedCoverings.rationalSectionIntersectionIdeal
Documentation

The intersection ideal of the two actual rational sections in a projective stalk.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · statement
def rationalSectionIntersectionIdeal
    (a b : Projectivization ℚ (ℚ × ℚ)) (x : ProjectiveLine ℤ) :
    Ideal ((ProjectiveLine ℤ).presheaf.stalk x)
theorem

rationalSection_stalkIdeal_eq

L57 ↗
ShimizuYamaguchi26BranchedCoverings.rationalSection_stalkIdeal_eq
Source context 4 commands

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

noncomputable section
open AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · statement
theorem rationalSection_stalkIdeal_eq
    (a : Projectivization ℚ (ℚ × ℚ)) (q : PrimeSpectrum ℤ[X]) :
    (rationalSection a).ker.stalkIdeal (infinityChartEmbedding ℤ q) =
      (infinitySectionIdeal (rationalPointNumerator a) (rationalPointDenominator a)).map
        (infinityChartGermAt ℤ q)
theorem

rationalSectionIntersectionIdeal_at_infinity

L67 ↗
ShimizuYamaguchi26BranchedCoverings.rationalSectionIntersectionIdeal_at_infinity
Documentation

At infinity, the actual section intersection ideal is the two-equation ideal in the integral projective stalk; the statement also covers primes with empty intersection.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · statement
theorem rationalSectionIntersectionIdeal_at_infinity
    (p : ℕ) [Fact p.Prime] (a b : Projectivization ℚ (ℚ × ℚ))
    (hb : b.rep.2 = 0) :
    rationalSectionIntersectionIdeal a b (integerProjectiveInfinityPoint p) =
      integerProjectiveInfinityIntersectionIdeal p
        (rationalPointNumerator a) (rationalPointDenominator a)
theorem

rationalSectionIntersection_length_at_infinity

L91 ↗
ShimizuYamaguchi26BranchedCoverings.rationalSectionIntersection_length_at_infinity
Documentation

The intersection multiplicity of the original rational sections, with the second point at infinity, is the valuation of the paper's Δ at every prime.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · statement
theorem rationalSectionIntersection_length_at_infinity
    (p : ℕ) [Fact p.Prime] (a b : Projectivization ℚ (ℚ × ℚ))
    (hab : a ≠ b) (hb : b.rep.2 = 0) :
    Module.length (IntegerProjectiveInfinityLocalRing p)
        (IntegerProjectiveInfinityLocalRing p ⧸
          rationalSectionIntersectionIdeal a b (integerProjectiveInfinityPoint p)) =
      (padicValInt p (rationalPointDelta a b) : ℕ∞)

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