Module

DyadicCollision.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.DyadicCollision

3 declarations indexed from sourceView source ↗

Module documentation

The dyadic collision of three rational sections

After moving their common reduction to zero, three rational sections have even numerators and odd denominators. Some pair has determinant divisible by four. The statement below is the coordinate calculation in Lemma 2.4; it does not assume or assert the unconstructed comparison with intersection multiplicities.

Source: Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers, Lemma 2.4 and the sign choice in Proposition 2.5.

Imports6

Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.Determinant
Mathlib.Algebra.Ring.Int.Parity
Mathlib.Data.Fintype.Pigeonhole
Mathlib.Tactic.NormNum
Lean.Elab.Tactic.Omega
Mathlib.Tactic.Ring

Imported by4

theorem

four_dvd_coordinateDeterminant_of_even_odd

L31 ↗

ShimizuYamaguchi26BranchedCoverings.four_dvd_coordinateDeterminant_of_even_odd

Documentation

Two even numerators congruent modulo four, with odd denominators, have determinant divisible by four.

Source context 1 command

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

namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem four_dvd_coordinateDeterminant_of_even_odd
    (u v u' v' : ℤ) (hu' : Even u') (hv : Odd v) (hv' : Odd v')
    (hnum : (4 : ℤ) ∣ u - u') :
    (4 : ℤ) ∣ coordinateDeterminant u v u' v'

theorem

exists_four_dvd_coordinateDeterminant_of_three

L52 ↗

ShimizuYamaguchi26BranchedCoverings.exists_four_dvd_coordinateDeterminant_of_three

Documentation

The arithmetic content of Lemma 2.4 in an affine chart: among three sections reducing to zero modulo two, two have determinant divisible by four.

Source context 1 command

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

namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem exists_four_dvd_coordinateDeterminant_of_three
    (u v : Fin 3 → ℤ) (hu : ∀ i : Fin 3, Even (u i))
    (hv : ∀ i : Fin 3, Odd (v i)) :
    ∃ i j : Fin 3, i ≠ j ∧ (4 : ℤ) ∣ coordinateDeterminant (u i) (v i) (u j) (v j)

theorem

exists_sign_four_dvd_one_add

L77 ↗

ShimizuYamaguchi26BranchedCoverings.exists_sign_four_dvd_one_add

Documentation

For an odd numerator, one of the two signs makes 1 + ε * u divisible by four, as required for the integral quadratic equation of Proposition 2.5.

Source context 1 command

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

namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem exists_sign_four_dvd_one_add (u : ℤ) (hu : Odd u) :
    ∃ ε : ℤ, (ε = 1 ∨ ε = -1) ∧ (4 : ℤ) ∣ 1 + ε * u

Module documentation

The dyadic collision of three rational sections

Declarations

four_dvd_coordinateDeterminant_of_even_odd

exists_four_dvd_coordinateDeterminant_of_three

exists_sign_four_dvd_one_add