Module

RationalSection.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.RationalSection

9 declarations indexed from sourceView source ↗

Module documentation

Rational points and their integral section closures

The primitive numerator and denominator of an actual rational projective point supply Bezout coefficients. These construct a section of the integral projective line, whose image is the homogeneous linear zero locus already used for special fibre intersections. The image of the original point over the rational numbers is exactly the generic point of this section. Consequently its Zariski closure is that same zero locus, as in the definition of the divisors in Lemma 2.3 of Shimizu and Yamaguchi, On branched coverings of the projective line over the integers.

Imports27

Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.RationalProjectiveCoordinates
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.FieldSectionPoint
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralSection
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.RationalSectionSupport
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.StandardAffineChart
Nyll.SchemeTheory.Divisors.LocalComplement
Nyll.SchemeTheory.ProjectiveSpace.Basic
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.ConcreteCategory.Basic
Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Mathlib.Data.Finset.Lattice.Fold
Mathlib.Data.Int.Cast.Lemmas
Mathlib.Data.Set.Image
Mathlib.RingTheory.MvPolynomial.Homogeneous
Mathlib.LinearAlgebra.Projectivization.Basic
Mathlib.RingTheory.Coprime.Basic
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Spectrum.Prime.Basic
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.Topology.Maps.Basic
Mathlib.Topology.Sets.Closeds

Imported by7

def

rationalSection

L58 ↗

ShimizuYamaguchi26BranchedCoverings.rationalSection

Documentation

The actual integral section obtained from a rational projective point's primitive coordinates and their Bezout identity.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

def rationalSection (a : Projectivization ℚ (ℚ × ℚ)) :
    Spec (CommRingCat.of ℤ) ⟶ ProjectiveLine ℤ

theorem

rationalSection_comp_π

L65 ↗

ShimizuYamaguchi26BranchedCoverings.rationalSection_comp_π

Documentation

The constructed morphism is a section of the integral projective line.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem rationalSection_comp_π (a : Projectivization ℚ (ℚ × ℚ)) :
    rationalSection a ≫ ProjSpace.π ℤ 1 = 𝟙 (Spec (CommRingCat.of ℤ))

instance

(anonymous instance)

L69 ↗

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

instance (a : Projectivization ℚ (ℚ × ℚ)) : IsClosedImmersion (rationalSection a)

theorem

range_rationalSection

L75 ↗

ShimizuYamaguchi26BranchedCoverings.range_rationalSection

Documentation

The actual section image equals the homogeneous support used in the special-fibre intersection calculations.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem range_rationalSection (a : Projectivization ℚ (ℚ × ℚ)) :
    Set.range (rationalSection a) = rationalSectionSupport a

def

rationalProjectiveSchemePoint

L82 ↗

ShimizuYamaguchi26BranchedCoverings.rationalProjectiveSchemePoint

Documentation

The rational projective-scheme point represented by the primitive coordinates of the given point of Projectivization ℚ (ℚ × ℚ).

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

def rationalProjectiveSchemePoint (a : Projectivization ℚ (ℚ × ℚ)) : ProjectiveLine ℚ

def

rationalSectionGenericPoint

L87 ↗

ShimizuYamaguchi26BranchedCoverings.rationalSectionGenericPoint

Documentation

The original rational point, viewed as a point of the integral projective line.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

def rationalSectionGenericPoint (a : Projectivization ℚ (ℚ × ℚ)) : ProjectiveLine ℤ

theorem

rationalSectionGenericPoint_eq

L92 ↗

ShimizuYamaguchi26BranchedCoverings.rationalSectionGenericPoint_eq

Documentation

The point over the rational numbers is the image of the generic point of Spec ℤ under the constructed integral section.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem rationalSectionGenericPoint_eq (a : Projectivization ℚ (ℚ × ℚ)) :
    rationalSectionGenericPoint a = rationalSection a (⊥ : PrimeSpectrum ℤ)

theorem

closure_rationalSectionGenericPoint

L128 ↗

ShimizuYamaguchi26BranchedCoverings.closure_rationalSectionGenericPoint

Documentation

The homogeneous support is precisely the Zariski closure of the original rational point in the integral projective line.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem closure_rationalSectionGenericPoint (a : Projectivization ℚ (ℚ × ℚ)) :
    closure ({rationalSectionGenericPoint a} : Set (ProjectiveLine ℤ)) =
      rationalSectionSupport a

theorem

rationalSectionFamily_supportComplement

L151 ↗

ShimizuYamaguchi26BranchedCoverings.rationalSectionFamily_supportComplement

Documentation

The support complement of the actual product of section kernel ideals is the finite intersection of the nonvanishing opens of their equations.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · full declaration

theorem rationalSectionFamily_supportComplement
    (A : Finset (Projectivization ℚ (ℚ × ℚ))) :
    (∏ a ∈ A, (rationalSection a).ker).supportComplement =
      A.inf (fun a =>
        Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
          (linearSectionEquation (rationalPointNumerator a)
            (rationalPointDenominator a))) := by
  have hsingle (a : Projectivization ℚ (ℚ × ℚ)) :
      (rationalSection a).ker.supportComplement =
        Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
          (linearSectionEquation (rationalPointNumerator a)
            (rationalPointDenominator a)) := by
    apply TopologicalSpace.Opens.ext
    change ((rationalSection a).ker.support : Set (ProjectiveLine ℤ))ᶜ = _
    have hker : ((rationalSection a).ker.support : Set (ProjectiveLine ℤ)) =
        closure (Set.range (rationalSection a)) :=
      Scheme.Hom.support_ker (rationalSection a)
    have hclosed : closure (Set.range (rationalSection a)) =
        Set.range (rationalSection a) :=
      (rationalSection a).isClosedEmbedding.isClosed_range.closure_eq
    have hopen :
        (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
          (linearSectionEquation (rationalPointNumerator a)
            (rationalPointDenominator a)) : Set (ProjectiveLine ℤ)) =
          (rationalSectionSupport a)ᶜ :=
      ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl
        (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        (linearSectionEquation (rationalPointNumerator a)
          (rationalPointDenominator a))
    exact (congrArg (fun Z : Set (ProjectiveLine ℤ) => Zᶜ)
      (hker.trans (hclosed.trans (range_rationalSection a)))).trans hopen.symm
  have hfinite : (∏ a ∈ A, (rationalSection a).ker).supportComplement =
      A.inf (fun a => (rationalSection a).ker.supportComplement) := by
    change (∏ a ∈ A, (rationalSection a).ker).support.compl =
      A.inf (fun a => (rationalSection a).ker.support.compl)
    rw [Scheme.IdealSheafData.support_finset_prod]
    exact map_finset_sup
      (TopologicalSpace.Closeds.complOrderIso (ProjectiveLine ℤ)) A
      (fun a => (rationalSection a).ker.support)
  exact hfinite.trans (Finset.inf_congr rfl fun a _ => hsingle a)

Module documentation

Rational points and their integral section closures

Declarations