IntegralSectionNormalCrossings.lean

theorem infinitySection_stalkIdeal_eq
    (p : ℕ) [Fact p.Prime] :
    (integralSection 1 0 1 0 (by decide)).ker.stalkIdeal
      (integerProjectiveInfinityPoint p) =
      Ideal.span ({infinityChartGermAt ℤ (integerInfinityChartPoint p) Polynomial.X} :
        Set (IntegerProjectiveInfinityLocalRing p)) := by
  let q : Spec (CommRingCat.of ℤ[X]) := integerInfinityChartPoint p
  let g : ℤ[X] →+* IntegerProjectiveInfinityLocalRing p := infinityChartGermAt ℤ q
  have hstalk : (integralSection 1 0 1 0 (by decide)).ker.stalkIdeal
      (integerProjectiveInfinityPoint p) = (infinitySectionIdeal 1 0).map g :=
    integralSection_stalkIdeal_eq 1 0 1 0 (by decide) q
  have hspan : (infinitySectionIdeal 1 0).map g = Ideal.span {g Polynomial.X} := by
    simp only [infinitySectionIdeal, map_zero, map_one, one_mul, zero_sub,
      Ideal.span_singleton_neg, Ideal.map_span, Set.image_singleton]
  exact hstalk.trans hspan

theorem integralSectionPair_isStrictNormalCrossingsAt_infinity
    (p : ℕ) [Fact p.Prime] (u v a b : ℤ) (hab : a * u + b * v = 1)
    (hv : v ≠ 0) (hval : padicValInt p v = 1) :
    ((integralSection 1 0 1 0 (by decide)).ker *
      (integralSection u v a b hab).ker).IsStrictNormalCrossingsAt
        (integerProjectiveInfinityPoint p) := by
  let S : Type := IntegerProjectiveInfinityLocalRing p
  let q : Spec (CommRingCat.of ℤ[X]) := integerInfinityChartPoint p
  let e : S ≃+* IntegerInfinityChartLocalRing p := infinityChartStalkEquiv ℤ q
  have : IsNoetherianRing S :=
    isNoetherianRing_of_ringEquiv (IntegerInfinityChartLocalRing p) e.symm
  let g : ℤ[X] →+* S := infinityChartGermAt ℤ q
  let t : Fin 2 → S :=
    ![g Polynomial.X, g (Polynomial.C v - Polynomial.C u * Polynomial.X)]
  have hparameters : Scheme.IsRegularSystemOfParameters t :=
    integerProjectiveInfinitySection_isRegularSystemOfParameters p u v hv hval
  have hregular : (ProjectiveLine ℤ).IsRegularAt (integerProjectiveInfinityPoint p) :=
    EtaleFundamentalGroups.Kummer.isRegularLocalRing_of_regularSystem
      (List.ofFn t) hparameters.1 hparameters.2
  have hinfinity : (integralSection 1 0 1 0 (by decide)).ker.stalkIdeal
      (integerProjectiveInfinityPoint p) = Ideal.span {g Polynomial.X} :=
    infinitySection_stalkIdeal_eq p
  have hsection : (integralSection u v a b hab).ker.stalkIdeal
      (integerProjectiveInfinityPoint p) =
      Ideal.span {g (Polynomial.C v - Polynomial.C u * Polynomial.X)} := by
    have hstalk : (integralSection u v a b hab).ker.stalkIdeal
        (integerProjectiveInfinityPoint p) = (infinitySectionIdeal u v).map g :=
      integralSection_stalkIdeal_eq u v a b hab q
    have hspan : (infinitySectionIdeal u v).map g =
        Ideal.span {g (Polynomial.C v - Polynomial.C u * Polynomial.X)} := by
      rw [infinitySectionIdeal, Ideal.map_span, Set.image_singleton]
    exact hstalk.trans hspan
  have hproduct : Scheme.initialParameterProduct t 2 (Nat.le_refl 2) =
      g Polynomial.X * g (Polynomial.C v - Polynomial.C u * Polynomial.X) := by
    simp only [Scheme.initialParameterProduct, Fin.castLE_rfl, id_eq,
      Fin.prod_univ_two, t, Matrix.cons_val_zero, Matrix.cons_val_one]
  refine ⟨hregular, 2, 2, t, by decide, Nat.le_refl 2, hparameters, ?_⟩
  rw [Scheme.IdealSheafData.stalkIdeal_mul, hinfinity, hsection,
    Ideal.span_singleton_mul_span_singleton, hproduct]

theorem infinitySection_isStrictNormalCrossingsAt
    (p : ℕ) [hp : Fact p.Prime] :
    (integralSection 1 0 1 0 (by decide)).ker.IsStrictNormalCrossingsAt
      (integerProjectiveInfinityPoint p) := by
  have hp0 : (p : ℤ) ≠ 0 := Int.natCast_ne_zero.mpr hp.out.ne_zero
  let S : Type := IntegerProjectiveInfinityLocalRing p
  let q : Spec (CommRingCat.of ℤ[X]) := integerInfinityChartPoint p
  let g : ℤ[X] →+* S := infinityChartGermAt ℤ q
  let t : Fin 2 → S :=
    ![g Polynomial.X, g (Polynomial.C (p : ℤ) - Polynomial.C 1 * Polynomial.X)]
  have hparameters : Scheme.IsRegularSystemOfParameters t :=
    integerProjectiveInfinitySection_isRegularSystemOfParameters p 1 p hp0 padicValInt_self
  have hregular : (ProjectiveLine ℤ).IsRegularAt (integerProjectiveInfinityPoint p) :=
    (integralSectionPair_isStrictNormalCrossingsAt_infinity p 1 p 1 0
      (by simp only [one_mul, zero_mul, add_zero]) hp0 padicValInt_self).1
  have hproduct : Scheme.initialParameterProduct t 1 (by decide) = g Polynomial.X := by
    simp only [Scheme.initialParameterProduct, Fin.prod_univ_one,
      Fin.castLE_zero, t, Matrix.cons_val_zero]
  have hinfinity : (integralSection 1 0 1 0 (by decide)).ker.stalkIdeal
      (integerProjectiveInfinityPoint p) = Ideal.span {g Polynomial.X} :=
    infinitySection_stalkIdeal_eq p
  refine ⟨hregular, 2, 1, t, by decide, by decide, hparameters, ?_⟩
  exact hinfinity.trans (congrArg (fun z : S => Ideal.span {z}) hproduct.symm)

theorem rationalSection_isStrictNormalCrossingsAt
    (p : ℕ) [Fact p.Prime] (a : Projectivization ℚ (ℚ × ℚ)) :
    (rationalSection a).ker.IsStrictNormalCrossingsAt
      (rationalSection a (integerPrimePoint p))

theorem integralSectionPair_isStrictNormalCrossingsAt_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)
    (hval : padicValInt p (coordinateDeterminant u' v' u v) = 1) :
    ((integralSection u v c d hcd).ker *
      (integralSection u' v' c' d' hcd').ker).IsStrictNormalCrossingsAt
        ((integralCoordinateChange u' v' c' d' hcd').inv
          (integerProjectiveInfinityPoint p))

theorem rationalSectionPair_isStrictNormalCrossingsAt
    (p : ℕ) [Fact p.Prime] (a b : Projectivization ℚ (ℚ × ℚ)) (hab : a ≠ b)
    (hval : padicValInt p (rationalPointDelta a b) = 1) :
    ((rationalSection a).ker * (rationalSection b).ker).IsStrictNormalCrossingsAt
      (rationalSection b (integerPrimePoint p))