Module

RationalProjectiveCoordinates.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.RationalProjectiveCoordinates

12 declarations indexed from sourceView source ↗

Module documentation

Primitive integer coordinates of rational projective points

For an actual point of Projectivization ℚ (ℚ × ℚ), the coordinates are (1, 0) at infinity and the reduced numerator and positive denominator of the affine coordinate elsewhere. Their primitivity and their representation of the original projective point are proved from these formulas. Distinct points consequently have nonzero integral coordinate determinant.

The paper's Δ uses a positive denominator when either point is infinity. It therefore differs from the signed coordinate determinant by a minus sign when the second point is infinity. This sign does not change padicValInt.

Source: Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers, the coordinate convention preceding Lemma 2.3 and its use in Lemma 2.4.

Imports9

Nyll.AnabelianGeometry.ProjectiveLine.CrossRatio
Nyll.AnabelianGeometry.ProjectiveLine.CrossRatioSeparation
Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.Determinant
Mathlib.Algebra.Field.Rat
Mathlib.Algebra.Ring.Rat
Mathlib.RingTheory.Coprime.Lemmas
Mathlib.LinearAlgebra.Projectivization.Basic
Mathlib.NumberTheory.Padics.PadicVal.Basic
Mathlib.Tactic.Ring

Imported by11

def

rationalPointNumerator

L42 ↗

ShimizuYamaguchi26BranchedCoverings.rationalPointNumerator

Documentation

The primitive numerator of a rational projective point, equal to 1 at infinity.

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · statement

def rationalPointNumerator (a : Projectivization ℚ (ℚ × ℚ)) : ℤ

def

rationalPointDenominator

L46 ↗

ShimizuYamaguchi26BranchedCoverings.rationalPointDenominator

Documentation

The primitive denominator, equal to 0 at infinity and positive otherwise.

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · statement

def rationalPointDenominator (a : Projectivization ℚ (ℚ × ℚ)) : ℤ

def

rationalPointCoordinates

L50 ↗

ShimizuYamaguchi26BranchedCoverings.rationalPointCoordinates

Documentation

The rational homogeneous vector obtained from the primitive integer coordinates.

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · statement

def rationalPointCoordinates (a : Projectivization ℚ (ℚ × ℚ)) : ℚ × ℚ

theorem

rationalPointCoordinates_isCoprime

L54 ↗

ShimizuYamaguchi26BranchedCoverings.rationalPointCoordinates_isCoprime

Documentation

The coordinates constructed from the point are primitive over the integers.

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · statement

theorem rationalPointCoordinates_isCoprime (a : Projectivization ℚ (ℚ × ℚ)) :
    IsCoprime (rationalPointNumerator a) (rationalPointDenominator a)

theorem

exists_smul_rationalPointCoordinates_eq_rep

L62 ↗

ShimizuYamaguchi26BranchedCoverings.exists_smul_rationalPointCoordinates_eq_rep

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · statement

theorem exists_smul_rationalPointCoordinates_eq_rep
    (a : Projectivization ℚ (ℚ × ℚ)) :
    ∃ c : ℚ, c • rationalPointCoordinates a = a.rep

theorem

rationalPointCoordinates_ne_zero

L94 ↗

ShimizuYamaguchi26BranchedCoverings.rationalPointCoordinates_ne_zero

Documentation

The primitive homogeneous vector is nonzero.

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · statement

theorem rationalPointCoordinates_ne_zero (a : Projectivization ℚ (ℚ × ℚ)) :
    rationalPointCoordinates a ≠ 0

theorem

rationalPointCoordinates_mk

L102 ↗

ShimizuYamaguchi26BranchedCoverings.rationalPointCoordinates_mk

Documentation

The constructed integer coordinates represent the original projective point.

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · statement

theorem rationalPointCoordinates_mk (a : Projectivization ℚ (ℚ × ℚ)) :
    Projectivization.mk ℚ (rationalPointCoordinates a)
      (rationalPointCoordinates_ne_zero a) = a

theorem

rationalPoint_coordinateDeterminant_ne_zero

L114 ↗

ShimizuYamaguchi26BranchedCoverings.rationalPoint_coordinateDeterminant_ne_zero

Documentation

Different rational projective points have nonzero primitive coordinate determinant.

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · statement

theorem rationalPoint_coordinateDeterminant_ne_zero
    (a b : Projectivization ℚ (ℚ × ℚ)) (hab : a ≠ b) :
    coordinateDeterminant (rationalPointNumerator a) (rationalPointDenominator a)
      (rationalPointNumerator b) (rationalPointDenominator b) ≠ 0

def

rationalPointDelta

L130 ↗

ShimizuYamaguchi26BranchedCoverings.rationalPointDelta

Documentation

The integer Δ(a,b) used in the paper, with value 0 when both points are infinity.

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · statement

def rationalPointDelta (a b : Projectivization ℚ (ℚ × ℚ)) : ℤ

theorem

rationalPointDelta_eq_signed_coordinateDeterminant

L137 ↗

ShimizuYamaguchi26BranchedCoverings.rationalPointDelta_eq_signed_coordinateDeterminant

Documentation

The exact sign comparison between the paper's Δ and the homogeneous determinant.

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · full declaration

theorem rationalPointDelta_eq_signed_coordinateDeterminant
    (a b : Projectivization ℚ (ℚ × ℚ)) :
    rationalPointDelta a b =
      if b.rep.2 = 0 then
        -coordinateDeterminant (rationalPointNumerator a) (rationalPointDenominator a)
          (rationalPointNumerator b) (rationalPointDenominator b)
      else coordinateDeterminant (rationalPointNumerator a) (rationalPointDenominator a)
        (rationalPointNumerator b) (rationalPointDenominator b) := by
  by_cases hb : b.rep.2 = 0
  · simp only [rationalPointDelta, coordinateDeterminant,
      rationalPointNumerator, rationalPointDenominator, ite_eq_left hb,
      mul_zero, mul_one, zero_sub, neg_neg]
  · by_cases ha : a.rep.2 = 0
    · simp only [rationalPointDelta, coordinateDeterminant,
        rationalPointNumerator, rationalPointDenominator, ite_eq_left ha, ite_eq_right hb,
        one_mul, zero_mul, sub_zero]
    · simp only [rationalPointDelta, ite_eq_right hb, ite_eq_right ha]

theorem

rationalPointDelta_self

L156 ↗

ShimizuYamaguchi26BranchedCoverings.rationalPointDelta_self

Documentation

The extended determinant vanishes when both rational points coincide.

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · statement

theorem rationalPointDelta_self (a : Projectivization ℚ (ℚ × ℚ)) :
    rationalPointDelta a a = 0

theorem

padicValInt_rationalPointDelta

L162 ↗

ShimizuYamaguchi26BranchedCoverings.padicValInt_rationalPointDelta

Documentation

The paper's integer and the coordinate determinant have the same value at every prime.

Source context 3 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
open AnabelianGeometry.ProjectiveLine

Lean source · statement

theorem padicValInt_rationalPointDelta (p : ℕ)
    (a b : Projectivization ℚ (ℚ × ℚ)) :
    padicValInt p (rationalPointDelta a b) =
      padicValInt p (coordinateDeterminant (rationalPointNumerator a)
        (rationalPointDenominator a) (rationalPointNumerator b)
        (rationalPointDenominator b))

Module documentation

Primitive integer coordinates of rational projective points

Declarations