SchemeArithmeticQuotientInertia.lean

def PointedGaloisQuotientInertiaCoprime
    {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)
    (qV : Ideal V) (p : ℕ) : Prop

theorem
  IsStrictNormalCrossings.exists_arithmeticLocalSplitChart_galoisCover_quotientIdealInertia_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),
            letI : IsDomain V := hVdomain
            letI : IsRegularRing V := hVregular
            letI : IsIntegrallyClosed V := hVnormal
            PointedGaloisQuotientInertiaCoprime hNC qV 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 : 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
  refine ⟨r, t, i, hVdomain, hVregular,
    hVnormal, hboundary, hNC, hi, hqi, hlocalizedCharZero, hpV, ?_⟩
  dsimp only [PointedGaloisQuotientInertiaCoprime]
  intro Y
  let hquotient :=
    Kummer.splitStrictNormalCrossings_finiteEtaleGaloisCover_quotientIdealInertia_coprime
      (A := V) (k := V ⧸ maximalIdeal V)
      hNC i hi hlocalizedCharZero Y
  let f := boundaryProduct t r
  have hf : f ≠ 0 :=
    EtaleFundamentalGroups.Kummer.splitStrictNormalCrossings_boundaryEquation_ne_zero
      hNC
  let S := Localization.Away f
  let : IsDomain S := IsLocalization.Away.isDomain S hf
  let : IsIntegrallyClosed S :=
    isIntegrallyClosed_of_isLocalization S (Submonoid.powers f)
      (Submonoid.powers_le.mpr
        (mem_nonZeroDivisors_iff_ne_zero.mpr hf))
  intro hY
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let K : Type u := (Spec (.of S)).functionField
  let L : Type u := Y.left.functionField
  let : Algebra K L := finiteEtaleFunctionFieldAlgebra Y
  let : Algebra V K := localizationAwaySpecFunctionFieldAlgebra f hf
  let : Algebra V L := finiteEtaleAwayFunctionFieldAlgebra f hf Y
  let : IsScalarTower V K L :=
    finiteEtaleAway_functionField_isScalarTower f hf Y
  let : IsFractionRing V K :=
    localizationAwaySpecFunctionField_isFractionRing f hf
  let : FiniteDimensional K L :=
    finiteDimensional_functionField_of_finiteEtale_isConnected Y
  let : _root_.IsGalois K L :=
    isGalois_functionField_of_isGalois_finiteEtale Y hY
  intro Omega instField instSepClosed xi y Q hQprime hQq
  have hQbranch : Q.LiesOver (Ideal.span ({t i} : Set V)) := by
    rw [← hqi]
    exact hQq
  let phiV : (V ⧸ Ideal.span ({t i} : Set V)) →+*
      (V ⧸ maximalIdeal V) :=
    (localizationAtPrimeBranchQuotientToResidue q P hqP.le).comp
      (Ideal.quotEquivOfEq hqi.symm).toRingHom
  exact hquotient hY xi y Q hQprime hQbranch phiV p hpV hp