OtherPrefixEtale.lean

theorem prime_algebraMap_localizationAtPrime_of_mem
    {A : Type u} [CommRing A] [IsDomain A]
    (P : Ideal A) [P.IsPrime] {t : A} (ht : Prime t) (htP : t ∈ P) :
    Prime (algebraMap A (Localization.AtPrime P) t)

theorem iteratedRadical_etale_of_exponents_radicands_isUnit
    {A : Type u} [CommRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (hnUnit : ∀ i, IsUnit (n i : A))
    (haUnit : ∀ i, IsUnit (a i)) :
    Algebra.Etale A (iteratedRadical A r n a)

theorem heightTwoConditionalOtherRadicand_isUnit_at_selectedBranch
    {A : Type uA} [CommRing A] [IsDomain A] [IsLocalRing A]
    [IsRegularRing A]
    {d r : ℕ} {f : A} {t : Fin (d + 1) → A}
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (i : Fin (d + 1)) (hi : i.1 < r)
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    (htiP : t i ∈ P) (sigma : Equiv.Perm (Fin d)) :
    let R := Localization.AtPrime P
    let y : R := algebraMap A R (t i)
    let hy : Prime y :=
      prime_algebraMap_localizationAtPrime_of_mem P
        (hNC.2.2.2.1 i hi) htiP
    let pR := Ideal.span ({y} : Set R)
    letI : pR.IsPrime := Ideal.isPrime_span_singleton_of_prime hy
    let V := Localization.AtPrime pR
    ∀ k,
      IsUnit (algebraMap R V
        (heightTwoConditionalOtherRadicand t i P sigma k)) := by
  dsimp only
  let R := Localization.AtPrime P
  let y : R := algebraMap A R (t i)
  have hy : Prime y :=
    prime_algebraMap_localizationAtPrime_of_mem P
      (hNC.2.2.2.1 i hi) htiP
  let pR := Ideal.span ({y} : Set R)
  let : pR.IsPrime := Ideal.isPrime_span_singleton_of_prime hy
  let V := Localization.AtPrime pR
  intro k
  let j : Fin (d + 1) := i.succAbove (sigma k)
  let aR : R := heightTwoConditionalOtherRadicand t i P sigma k
  by_cases htjP : t j ∈ P
  · have hij : i ≠ j := (Fin.succAbove_ne i (sigma k)).symm
    have hregular : IsRegular R [y, aR] := by
      simpa only [R, y, aR, j,
        heightTwoConditionalOtherRadicand] using
        (regular_pair_localizationAtPrime_of_two_splitStrictNormalCrossingsParameters
          hNC i j hij P hP htiP htjP).1
    have hrel : IsRelPrime y aR :=
      (SpecialLocalPurity.regular_pair_nonzero_and_isRelPrime
        hregular).2.2
    have hyMem : y ∈ IsLocalRing.maximalIdeal R :=
      (IsLocalization.AtPrime.to_map_mem_maximal_iff R P (t i)).mpr htiP
    have haNot : aR ∉ pR := by
      intro ha
      have hyDvd : y ∣ aR := Ideal.mem_span_singleton.mp ha
      have hyUnit : IsUnit y := hrel.isUnit_of_dvd hyDvd
      exact ((IsLocalRing.notMem_maximalIdeal).mpr hyUnit) hyMem
    exact
      (IsLocalization.AtPrime.isUnit_to_map_iff V pR aR).mpr haNot
  · have haRUnit : IsUnit aR := by
      change IsUnit (algebraMap A R (t j))
      exact
        (IsLocalization.AtPrime.isUnit_to_map_iff R P (t j)).mpr htjP
    exact haRUnit.map (algebraMap R V)

theorem heightTwoConditionalOtherExponent_isUnit_at_selectedBranch
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [IsGalois K L]
    {d r : ℕ} {f : A} {t : Fin (d + 1) → A}
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (i : Fin (d + 1)) (hi : i.1 < r)
    (P : Ideal A) [P.IsPrime] (htiP : t i ∈ P)
    (hCharZero : CharZero (A ⧸ Ideal.span ({t i} : Set A)))
    (sigma : Equiv.Perm (Fin d)) :
    let e := heightTwoOtherBranchGaloisRamificationIndex
      (K := K) (L := L) t hNC i
    let n := heightTwoConditionalOtherExponent t i r P e sigma
    let R := Localization.AtPrime P
    let y : R := algebraMap A R (t i)
    let hy : Prime y :=
      prime_algebraMap_localizationAtPrime_of_mem P
        (hNC.2.2.2.1 i hi) htiP
    let pR := Ideal.span ({y} : Set R)
    letI : pR.IsPrime := Ideal.isPrime_span_singleton_of_prime hy
    let V := Localization.AtPrime pR
    ∀ k, IsUnit (n k : V) := by
  dsimp only
  let e := heightTwoOtherBranchGaloisRamificationIndex
    (K := K) (L := L) t hNC i
  let n := heightTwoConditionalOtherExponent t i r P e sigma
  let R := Localization.AtPrime P
  let y : R := algebraMap A R (t i)
  have hy : Prime y :=
    prime_algebraMap_localizationAtPrime_of_mem P
      (hNC.2.2.2.1 i hi) htiP
  let pR := Ideal.span ({y} : Set R)
  let : pR.IsPrime := Ideal.isPrime_span_singleton_of_prime hy
  let V := Localization.AtPrime pR
  let : CharZero (V ⧸ IsLocalRing.maximalIdeal V) := by
    simpa only [R, y, pR, V] using
      (charZero_twiceLocalized_splitStrictNormalCrossingsBranchResidue
        hNC i hi P htiP hCharZero)
  have hn : ∀ k, 0 < n k := by
    intro k
    by_cases hk : (i.succAbove (sigma k)).1 < r ∧
        t (i.succAbove (sigma k)) ∈ P
    · simpa [n, e, heightTwoConditionalOtherExponent, hk] using
        (heightTwoOtherBranchGaloisRamificationIndex_pos
          (K := K) (L := L) t hNC i (sigma k))
    · simp [n, heightTwoConditionalOtherExponent, hk]
  intro k
  apply (IsLocalRing.residue_ne_zero_iff_isUnit (n k : V)).mp
  change ((n k : ℕ) :
    (V ⧸ IsLocalRing.maximalIdeal V)) ≠ 0
  exact Nat.cast_ne_zero.mpr (Nat.ne_of_gt (hn k))

theorem heightTwoGaloisOtherRootPrefix_finiteEtale_at_selectedBranch
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [IsGalois K L]
    {d r : ℕ} {f : A} {t : Fin (d + 1) → A}
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (i : Fin (d + 1)) (hi : i.1 < r)
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    (htiP : t i ∈ P)
    (hCharZero : CharZero (A ⧸ Ideal.span ({t i} : Set A)))
    (sigma : Equiv.Perm (Fin d)) :
    let e := heightTwoOtherBranchGaloisRamificationIndex
      (K := K) (L := L) t hNC i
    let n := heightTwoConditionalOtherExponent t i r P e sigma
    let R := Localization.AtPrime P
    letI : Algebra R K :=
      localizationAtPrimeToFractionFieldAlgebra (K := K) P
    letI : Algebra R L :=
      localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
    letI : IsScalarTower R K L :=
      localizationAtPrimeToFractionFieldToExtension_isScalarTower
        (K := K) (L := L) P
    letI : IsFractionRing R K :=
      localizationAtPrimeToFractionField_isFractionRing (K := K) P
    let aR : Fin d → R :=
      heightTwoConditionalOtherRadicand t i P sigma
    let y : R := algebraMap A R (t i)
    let hy : Prime y :=
      prime_algebraMap_localizationAtPrime_of_mem P
        (hNC.2.2.2.1 i hi) htiP
    let pR := Ideal.span ({y} : Set R)
    letI : pR.IsPrime := Ideal.isPrime_span_singleton_of_prime hy
    let V := Localization.AtPrime pR
    let aV : Fin d → V := fun k ↦ algebraMap R V (aR k)
    let E := iteratedRadical V d n aV
    Module.Finite V E ∧
      Module.FaithfullyFlat V E ∧ Algebra.Etale V E := by
  dsimp only
  let e := heightTwoOtherBranchGaloisRamificationIndex
    (K := K) (L := L) t hNC i
  let n := heightTwoConditionalOtherExponent t i r P e sigma
  let R := Localization.AtPrime P
  let : Algebra R K :=
    localizationAtPrimeToFractionFieldAlgebra (K := K) P
  let : Algebra R L :=
    localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
  let : IsScalarTower R K L :=
    localizationAtPrimeToFractionFieldToExtension_isScalarTower
      (K := K) (L := L) P
  let : IsFractionRing R K :=
    localizationAtPrimeToFractionField_isFractionRing (K := K) P
  let aR : Fin d → R :=
    heightTwoConditionalOtherRadicand t i P sigma
  let y : R := algebraMap A R (t i)
  have hy : Prime y :=
    prime_algebraMap_localizationAtPrime_of_mem P
      (hNC.2.2.2.1 i hi) htiP
  let pR := Ideal.span ({y} : Set R)
  let : pR.IsPrime := Ideal.isPrime_span_singleton_of_prime hy
  let V := Localization.AtPrime pR
  let aV : Fin d → V := fun k ↦ algebraMap R V (aR k)
  let E := iteratedRadical V d n aV
  have hn : ∀ k, 0 < n k := by
    intro k
    by_cases hk : (i.succAbove (sigma k)).1 < r ∧
        t (i.succAbove (sigma k)) ∈ P
    · simpa [n, e, heightTwoConditionalOtherExponent, hk] using
        (heightTwoOtherBranchGaloisRamificationIndex_pos
          (K := K) (L := L) t hNC i (sigma k))
    · simp [n, heightTwoConditionalOtherExponent, hk]
  have hnUnit : ∀ k, IsUnit (n k : V) := by
    simpa only [e, n, R, y, pR, V] using
      (heightTwoConditionalOtherExponent_isUnit_at_selectedBranch
        (K := K) (L := L) hNC i hi P htiP hCharZero sigma)
  have haUnit : ∀ k, IsUnit (aV k) := by
    simpa only [R, aR, y, pR, V, aV] using
      (heightTwoConditionalOtherRadicand_isUnit_at_selectedBranch
        hNC i hi P hP htiP sigma)
  have hFinite : Module.Finite V E :=
    finite_iteratedRadical n aV hn
  have hFaithful : Module.FaithfullyFlat V E :=
    faithfullyFlat_iteratedRadical n aV hn
  have hEtale : Algebra.Etale V E :=
    iteratedRadical_etale_of_exponents_radicands_isUnit
      n aV hn hnUnit haUnit
  exact ⟨hFinite, hFaithful, hEtale⟩

theorem exists_tensorProduct_prime_over_right_ramificationIdx_eq_of_etale
    {R B E : Type*} [CommRing R] [CommRing B] [CommRing E]
    [Algebra R B] [Algebra R E]
    [Algebra.Etale R E] [Module.FaithfullyFlat R E]
    (q : Ideal B) [q.IsPrime] :
    ∃ Q : Ideal (E ⊗[R] B),
      Q.IsPrime ∧
        Q.comap Algebra.TensorProduct.includeRight.toRingHom = q ∧
          Q.ramificationIdx E = q.ramificationIdx R