NYLL
Module

IntegralSectionPrimePoint.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralSectionPrimePoint
2 declarations indexed from sourceView source ↗

Module documentation

The integral section point above a prime

The closed point of Spec ℤ defined by p maps under evaluation at zero in the polynomial chart to the prime (p, X). The actual integral section is the zero section followed by a coordinate swap and the inverse Bézout coordinate change. The same coordinate swap defines the infinity chart. Thus the section point is exactly the inverse image of the integral infinity point under that change of coordinates.

This identifies the point used for the general local intersection calculation in Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers.

Imports18
Imported by4

Declarations

def

integerPrimePoint

L50 ↗
ShimizuYamaguchi26BranchedCoverings.integerPrimePoint
Documentation

The point of the integer spectrum defined by the prime p.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def integerPrimePoint (p : ℕ) [Fact p.Prime] : PrimeSpectrum ℤ
theorem

integralSection_at_integerPrimePoint

L55 ↗
ShimizuYamaguchi26BranchedCoverings.integralSection_at_integerPrimePoint
Documentation

The actual integral section point over p is obtained by transporting its infinity-chart point along the inverse Bézout coordinate change.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem integralSection_at_integerPrimePoint
    (u v a b : ℤ) (hab : a * u + b * v = 1) (p : ℕ) [Fact p.Prime] :
    integralSection u v a b hab (integerPrimePoint p) =
      (integralCoordinateChange u v a b hab).inv (integerProjectiveInfinityPoint p)

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