Module

SpecialFiberIntersection.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.SpecialFiberIntersection

8 declarations indexed from sourceView source ↗

Module documentation

Rational section intersections in a prime special fibre

A common point of two homogeneous linear equations over a field forces the coordinate determinant to vanish: two explicit linear combinations put the determinant times both coordinates in its homogeneous prime ideal, and an invertible determinant would put the irrelevant ideal there.

Conversely, the homogeneous core of evaluation at the reduction of the first primitive pair constructs the intersection point. Its evaluation formula identifies meeting with divisibility of the integer determinant, with the paper's sign convention at infinity. The zero locus of either individual section in the special fibre is a singleton closed point.

These are the incidence and unique-closed-point assertions of Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. The local intersection-length and normal-crossing assertions of that lemma are separate requirements.

Imports15

Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.Determinant
Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.RationalProjectiveCoordinates
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.FieldSectionPoint
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.FieldSectionPointUniqueness
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.RationalSectionSupport
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.StandardAffineChart
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.TwoSectionComplement
Nyll.SchemeTheory.ProjectiveSpace.Basic
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Mathlib.Algebra.Field.ZMod
Mathlib.Data.ZMod.Basic
Mathlib.LinearAlgebra.Projectivization.Basic
Mathlib.RingTheory.Coprime.Basic
Mathlib.RingTheory.Ideal.Defs
Mathlib.Tactic.Ring

Imported by2

theorem

determinant_eq_zero_of_common_field_section_point

L55 ↗

ShimizuYamaguchi26BranchedCoverings.determinant_eq_zero_of_common_field_section_point

Documentation

A common point of two linear equations over a field forces their determinant to vanish.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem determinant_eq_zero_of_common_field_section_point
    {k : Type u} [Field k] (u v s t : k) (x : ProjectiveLine k)
    (hfirst : linearSectionEquation u v ∈ x.asHomogeneousIdeal)
    (hsecond : linearSectionEquation s t ∈ x.asHomogeneousIdeal) : u * t - v * s = 0

theorem

reduced_rationalPointCoordinates_ne_zero

L92 ↗

ShimizuYamaguchi26BranchedCoverings.reduced_rationalPointCoordinates_ne_zero

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem reduced_rationalPointCoordinates_ne_zero (p : ℕ) [Fact p.Prime]
    (a : Projectivization ℚ (ℚ × ℚ)) :
    (rationalPointNumerator a : ZMod p) ≠ 0 ∨ (rationalPointDenominator a : ZMod p) ≠ 0

def

rationalSectionSpecialFiberPoint

L98 ↗

ShimizuYamaguchi26BranchedCoverings.rationalSectionSpecialFiberPoint

Documentation

The actual point of the prime special fibre selected by a rational section.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

def rationalSectionSpecialFiberPoint (p : ℕ) [Fact p.Prime]
    (a : Projectivization ℚ (ℚ × ℚ)) : ProjectiveLine (ZMod p)

theorem

prime_dvd_delta_iff

L103 ↗

ShimizuYamaguchi26BranchedCoverings.prime_dvd_delta_iff

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem prime_dvd_delta_iff (p : ℕ)
    (a b : Projectivization ℚ (ℚ × ℚ)) :
    (p : ℤ) ∣ rationalPointDelta a b ↔
      (p : ℤ) ∣ coordinateDeterminant (rationalPointNumerator a) (rationalPointDenominator a)
        (rationalPointNumerator b) (rationalPointDenominator b)

theorem

rationalSectionSpecialFiberPoint_mem_iff

L116 ↗

ShimizuYamaguchi26BranchedCoverings.rationalSectionSpecialFiberPoint_mem_iff

Documentation

The reduction point of the first section belongs to the second section exactly when the prime divides the paper's integer Δ.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem rationalSectionSpecialFiberPoint_mem_iff (p : ℕ) [Fact p.Prime]
    (a b : Projectivization ℚ (ℚ × ℚ)) :
    (ProjSpace.map ℤ (ZMod p) 1) (rationalSectionSpecialFiberPoint p a) ∈
        rationalSectionSupport b ↔ (p : ℤ) ∣ rationalPointDelta a b

theorem

rationalSectionSpecialFiberPoint_mem

L129 ↗

ShimizuYamaguchi26BranchedCoverings.rationalSectionSpecialFiberPoint_mem

Documentation

The constructed reduction point lies on its original rational section.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem rationalSectionSpecialFiberPoint_mem (p : ℕ) [Fact p.Prime]
    (a : Projectivization ℚ (ℚ × ℚ)) :
    (ProjSpace.map ℤ (ZMod p) 1) (rationalSectionSpecialFiberPoint p a) ∈
      rationalSectionSupport a

theorem

specialFiber_intersection_nonempty_iff

L140 ↗

ShimizuYamaguchi26BranchedCoverings.specialFiber_intersection_nonempty_iff

Documentation

The incidence assertion of Lemma 2.3: the two actual integral section supports meet in the prime special fibre if and only if the prime divides Δ. This holds also for equal rational points, where both sides hold.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem specialFiber_intersection_nonempty_iff (p : ℕ) [Fact p.Prime]
    (a b : Projectivization ℚ (ℚ × ℚ)) :
    (∃ x : ProjectiveLine (ZMod p), (ProjSpace.map ℤ (ZMod p) 1) x ∈ rationalSectionSupport a ∧
      (ProjSpace.map ℤ (ZMod p) 1) x ∈ rationalSectionSupport b) ↔
        (p : ℤ) ∣ rationalPointDelta a b

theorem

specialFiber_intersection_singleton_closed

L162 ↗

ShimizuYamaguchi26BranchedCoverings.specialFiber_intersection_singleton_closed

Documentation

When the prime divides Δ, the entire intersection in the actual special fibre is the singleton constructed from the first section, and this point is closed. This is the unique-closed-point assertion of Lemma 2.3.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem specialFiber_intersection_singleton_closed (p : ℕ) [Fact p.Prime]
    (a b : Projectivization ℚ (ℚ × ℚ)) (hdiv : (p : ℤ) ∣ rationalPointDelta a b) :
    {x : ProjectiveLine (ZMod p) |
      (ProjSpace.map ℤ (ZMod p) 1) x ∈ rationalSectionSupport a ∧
        (ProjSpace.map ℤ (ZMod p) 1) x ∈ rationalSectionSupport b} =
      {rationalSectionSpecialFiberPoint p a} ∧
        IsClosed ({rationalSectionSpecialFiberPoint p a} : Set (ProjectiveLine (ZMod p)))

Module documentation

Rational section intersections in a prime special fibre

Declarations