SchemeArithmeticCanonicalFundamentalGroup.lean

def CanonicalGaloisCoverInertiaRangeAndCoprime
    {V : Type u} [CommRing V] [IsDomain V] [IsLocalRing V] [IsRegularRing V]
    [IsIntegrallyClosed V]
    {r : ℕ} {t : Fin 2 → V}
    (hNC : IsSplitStrictNormalCrossingsAt (boundaryProduct t r) t r)
    (i : Fin 2) (hi : i.1 < r) (p : ℕ) : Prop

theorem
    exists_arithmeticLocalSplitChart_galoisCover_canonicalFundamentalGroupInertia_range_and_coprime
    {X : Scheme.{u}} {I : X.IdealSheafData} {x : X}
    (hI : I.IsStrictNormalCrossings)
    (hCharZero : I.HasCharacteristicZeroBranchesAt x)
    (q : Ideal (X.presheaf.stalk x)) [q.IsPrime]
    (hqheight : q.height = 1)
    (hIq : I.stalkIdeal x ≤ q)
    {k : Type uk} [CommRing k] [Nontrivial k]
    (phi : (X.presheaf.stalk x ⧸ q) →+* k)
    (p : ℕ) [CharP k p] (hp : p.Prime) :
    let A := X.presheaf.stalk x
    ∃ P : AlgebraicGeometry.Spec A,
      q < P.asIdeal ∧ P.asIdeal.height = 2 ∧
        let : P.asIdeal.IsPrime := P.isPrime
        let V := Localization.AtPrime P.asIdeal
        let qV := q.map (algebraMap A V)
        ∃ (r : ℕ) (t : Fin 2 → V) (i : Fin 2)
          (hVdomain : IsDomain V) (hVregular : IsRegularRing V)
          (hVnormal : IsIntegrallyClosed V)
          (_hboundary : (I.stalkIdeal x).map (algebraMap A V) =
            Ideal.span {boundaryProduct t r})
          (hNC : IsSplitStrictNormalCrossingsAt
            (boundaryProduct t r) t r)
          (hi : i.1 < r)
          (_hqi : qV = Ideal.span {t i})
          (_hlocalizedCharZero : ∀ j : Fin 2, j.1 < r →
            CharZero (V ⧸ Ideal.span {t j}))
          (_hpV : CharP (V ⧸ maximalIdeal V) p),
            let : IsDomain V := hVdomain
            let : IsRegularRing V := hVregular
            let : IsIntegrallyClosed V := hVnormal
            CanonicalGaloisCoverInertiaRangeAndCoprime hNC i hi p := by
  intro A
  obtain ⟨P, hPprime, hqP, hPheight, r, t, i, hVdomain,
      hVregular, hboundary, hNC, hi, hqi, hlocalizedCharZero, hpV⟩ :=
    hI.exists_heightTwo_localSplitChart_of_branch_residueCharacteristic
      hCharZero q hqheight hIq phi p hp
  let Pspec : AlgebraicGeometry.Spec A := ⟨P, hPprime⟩
  refine ⟨Pspec, ?_⟩
  change q < P ∧ P.height = 2 ∧ _
  refine ⟨hqP, hPheight, ?_⟩
  intro hPPrime V qV
  let : IsDomain V := hVdomain
  let : IsRegularRing V := hVregular
  let : IsRegularLocalRing V :=
    IsRegularLocalRing.of_isRegularRing_of_isLocalRing V
  have hdimV : ringKrullDim V = ((2 : ℕ∞) : WithBot ℕ∞) := by
    calc
      ringKrullDim V = (P.height : WithBot ℕ∞) :=
        IsLocalization.AtPrime.ringKrullDim_eq_height P V
      _ = ((2 : ℕ∞) : WithBot ℕ∞) :=
        congrArg (fun n : ℕ∞ ↦ (n : WithBot ℕ∞)) hPheight
  have hVnormal : IsIntegrallyClosed V :=
    SpecialLocalPurity.isIntegrallyClosed_of_isRegularLocalRing_dimension_two
      hdimV
  let : IsIntegrallyClosed V := hVnormal
  refine ⟨r, t, i, hVdomain, hVregular,
    hVnormal, hboundary, hNC, hi, hqi, hlocalizedCharZero, hpV, ?_⟩
  intro domainV regularV normalV Y
  let hcanonical :=
    EtaleFundamentalGroups.Kummer.finiteEtaleGaloisCover_canonicalInertia_range_and_coprime
      (A := V) (k := V ⧸ maximalIdeal V)
      hNC i hi hlocalizedCharZero Y
  intro f hf S domainS normalS hY galoisY integralY K L algebraKL algebraVK
    algebraVL towerVKL fractionVK finiteKL galoisKL Q hQprime hQbranch primeBranch
  let phiV : (V ⧸ Ideal.span ({t i} : Set V)) →+*
      (V ⧸ maximalIdeal V) :=
    (localizationAtPrimeBranchQuotientToResidue q P hqP.le).comp
      (Ideal.quotEquivOfEq hqi.symm).toRingHom
  exact hcanonical hY Q hQprime hQbranch phiV p hpV hp