NYLL
Module

Theorem2Dot3IntersectionMultiplicity.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Theorem2Dot3IntersectionMultiplicity
4 declarations indexed from sourceView source ↗

Module documentation

Lemma 2.3: intersection multiplicity for rational sections

The corresponding Lean declaration is rationalSectionIntersection_length.

The integral Bezout coordinate isomorphism sends the second original section point over p to the infinity-chart point (p,w). Pullback carries the actual kernel ideal sheaves to the sections with the explicitly transformed primitive coordinates. Its stalk isomorphism therefore carries the original intersection ideal to the pair of equations whose quotient length was computed at infinity.

The resulting length is the valuation of the original coordinate determinant, and hence of the paper's Delta. The statement is at the actual point of the original second section over p; it applies to every prime, with length zero when the sections do not meet there. This proves the multiplicity assertion of Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. The normal-crossing criterion is a further assertion of that lemma.

Imports38
Imported by2

Declarations

theorem

integralSection_stalkIdeal_map_coordinateChange_inv

L73 ↗
ShimizuYamaguchi26BranchedCoverings.integralSection_stalkIdeal_map_coordinateChange_inv
Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · statement
theorem integralSection_stalkIdeal_map_coordinateChange_inv
    (u v a b u' v' c d : ℤ) (hab : a * u + b * v = 1)
    (hcd : c * u' + d * v' = 1) (q : PrimeSpectrum ℤ[X]) :
    ((integralSection u' v' c d hcd).ker.stalkIdeal
        ((integralCoordinateChange u v a b hab).inv (infinityChartEmbedding ℤ q))).map
      ((integralCoordinateChange u v a b hab).inv.stalkMap
        (infinityChartEmbedding ℤ q)).hom =
      (infinitySectionIdeal (-(a * u' + b * v')) (coordinateDeterminant u v u' v')).map
        (infinityChartGermAt ℤ q)
theorem

integralSectionIntersection_length_coordinateChange

L89 ↗
ShimizuYamaguchi26BranchedCoverings.integralSectionIntersection_length_coordinateChange
Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · full declaration
theorem integralSectionIntersection_length_coordinateChange
    (p : ℕ) [Fact p.Prime] (u v c d u' v' c' d' : ℤ)
    (hcd : c * u + d * v = 1) (hcd' : c' * u' + d' * v' = 1)
    (hdet : coordinateDeterminant u' v' u v ≠ 0) :
    let x : ProjectiveLine ℤ :=
      (integralCoordinateChange u' v' c' d' hcd').inv (integerProjectiveInfinityPoint p)
    Module.length ((ProjectiveLine ℤ).presheaf.stalk x)
      ((ProjectiveLine ℤ).presheaf.stalk x ⧸
        ((integralSection u v c d hcd).ker.stalkIdeal x ⊔
          (integralSection u' v' c' d' hcd').ker.stalkIdeal x)) =
      (padicValInt p (coordinateDeterminant u' v' u v) : ℕ∞) := by
  let e : ProjectiveLine ℤ ≅ ProjectiveLine ℤ :=
    integralCoordinateChange u' v' c' d' hcd'
  let y : ProjectiveLine ℤ := integerProjectiveInfinityPoint p
  let I : Ideal ((ProjectiveLine ℤ).presheaf.stalk (e.inv y)) :=
    (integralSection u v c d hcd).ker.stalkIdeal (e.inv y) ⊔
      (integralSection u' v' c' d' hcd').ker.stalkIdeal (e.inv y)
  let U : ℤ := -(c' * u + d' * v)
  let V : ℤ := coordinateDeterminant u' v' u v
  let J : Ideal (IntegerProjectiveInfinityLocalRing p) :=
    integerProjectiveInfinityIntersectionIdeal p U V
  let F : (ProjectiveLine ℤ).presheaf.stalk (e.inv y) ≃+*
      IntegerProjectiveInfinityLocalRing p :=
    (asIso (e.inv.stalkMap y)).commRingCatIsoToRingEquiv
  have hmap : I.map F.toRingHom = J := by
    change (((integralSection u v c d hcd).ker.stalkIdeal
          (e.inv (infinityChartEmbedding ℤ (integerInfinityChartPoint p)))) ⊔
        ((integralSection u' v' c' d' hcd').ker.stalkIdeal
          (e.inv (infinityChartEmbedding ℤ (integerInfinityChartPoint p))))).map
        (e.inv.stalkMap (infinityChartEmbedding ℤ (integerInfinityChartPoint p))).hom = J
    rw [Ideal.map_sup,
      integralSection_stalkIdeal_map_coordinateChange_inv u' v' c' d' u v c d hcd' hcd,
      integralSection_stalkIdeal_map_coordinateChange_inv u' v' c' d' u' v' c' d' hcd' hcd']
    have hself : coordinateDeterminant u' v' u' v' = 0 := by
      unfold coordinateDeterminant
      ring
    rw [hcd', hself]
    change (infinitySectionIdeal U V).map (infinityChartGermAt ℤ (integerInfinityChartPoint p)) ⊔
        (infinitySectionIdeal (-1) 0).map (infinityChartGermAt ℤ (integerInfinityChartPoint p)) =
      (infinityIntersectionIdeal U V).map (infinityChartGermAt ℤ (integerInfinityChartPoint p))
    rw [← Ideal.map_sup]
    apply congrArg (Ideal.map (infinityChartGermAt ℤ (integerInfinityChartPoint p)))
    simp only [infinitySectionIdeal, map_zero, map_neg, map_one, neg_one_mul, zero_sub, neg_neg]
    rw [infinityIntersectionIdeal, Ideal.span_insert, sup_comm]
  have hlength : Module.length ((ProjectiveLine ℤ).presheaf.stalk (e.inv y))
        ((ProjectiveLine ℤ).presheaf.stalk (e.inv y) ⧸ I) =
      Module.length (IntegerProjectiveInfinityLocalRing p)
        (IntegerProjectiveInfinityLocalRing p ⧸ J) := by
    rw [Module.length_quotient, Module.length_quotient, ← hmap]
    simpa only [RingEquiv.idealComapOrderIso_symm_apply,
      RingEquiv.toRingHom_eq_coe, Ideal.map_coe] using
      (Order.coheight_orderIso F.idealComapOrderIso.symm I).symm
  exact hlength.trans (integerProjectiveInfinityIntersection_length p U V hdet)
theorem

rationalSectionIntersection_length

L145 ↗
ShimizuYamaguchi26BranchedCoverings.rationalSectionIntersection_length
Documentation

For distinct original rational points, the quotient of the actual projective local ring by their two section ideals has length v_p(Delta) at the second section's point over p.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · statement
theorem rationalSectionIntersection_length
    (p : ℕ) [Fact p.Prime] (a b : Projectivization ℚ (ℚ × ℚ)) (hab : a ≠ b) :
    Module.length ((ProjectiveLine ℤ).presheaf.stalk (rationalSection b (integerPrimePoint p)))
      ((ProjectiveLine ℤ).presheaf.stalk (rationalSection b (integerPrimePoint p)) ⧸
        rationalSectionIntersectionIdeal a b (rationalSection b (integerPrimePoint p))) =
      (padicValInt p (rationalPointDelta a b) : ℕ∞)
theorem

rationalSection_stalkIdeal_eq_top_of_not_dvd

L168 ↗
ShimizuYamaguchi26BranchedCoverings.rationalSection_stalkIdeal_eq_top_of_not_dvd
Documentation

If the determinant is not divisible by p, the first section has unit ideal in the actual local ring at the second section's point over p.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · statement
theorem rationalSection_stalkIdeal_eq_top_of_not_dvd
    (p : ℕ) [Fact p.Prime] (a b : Projectivization ℚ (ℚ × ℚ)) (hab : a ≠ b)
    (hnot : ¬ (p : ℤ) ∣ rationalPointDelta a b) :
    (rationalSection a).ker.stalkIdeal (rationalSection b (integerPrimePoint p)) = ⊤

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