EssentiallyEtaleBaseChangeInertiaContraction.lean

theorem finiteTypeModel_isFractionRing
    {A C K : Type u}
    [CommRing A] [CommRing C] [IsDomain C] [Algebra A C]
    [Algebra.EssFiniteType A C]
    [Field K] [Algebra C K] [IsFractionRing C K] :
    let T := Algebra.EssFiniteType.subalgebra A C
    IsFractionRing T K := by
  dsimp only
  let T := Algebra.EssFiniteType.subalgebra A C
  let M := Algebra.EssFiniteType.submonoid A C
  let N := IsLocalization.localizationLocalizationSubmodule M
    (nonZeroDivisors C)
  have hN : N = nonZeroDivisors T := by
    ext x
    constructor
    · intro hx
      rw [mem_nonZeroDivisors_iff_ne_zero]
      intro hx0
      have hunit : IsUnit (algebraMap T K x) :=
        IsLocalization.localization_localization_map_units
          M (nonZeroDivisors C) K ⟨x, hx⟩
      rw [hx0, map_zero] at hunit
      exact not_isUnit_zero hunit
    · intro hx
      change x ∈ IsLocalization.localizationLocalizationSubmodule M
        (nonZeroDivisors C)
      rw [IsLocalization.mem_localizationLocalizationSubmodule]
      have hxC : algebraMap T C x ∈ nonZeroDivisors C := by
        rw [mem_nonZeroDivisors_iff_ne_zero, map_ne_zero_iff]
        · exact (mem_nonZeroDivisors_iff_ne_zero.mp hx)
        · exact Subtype.val_injective
      exact ⟨⟨algebraMap T C x, hxC⟩, 1, by simp⟩
  have hloc : IsLocalization N K :=
    IsLocalization.localization_localization_isLocalization
      M (nonZeroDivisors C) K
  rw [hN] at hloc
  exact hloc

theorem finiteTypeModel_isEtaleAt_contraction
    {A C : Type u}
    [CommRing A] [IsNoetherianRing A]
    [CommRing C] [Algebra A C]
    [Algebra.EssFiniteType A C] [Algebra.FormallyEtale A C]
    (P : Ideal C) [P.IsPrime] :
    let T := Algebra.EssFiniteType.subalgebra A C
    let r := P.comap (algebraMap T C)
    Algebra.IsEtaleAt A r := by
  dsimp only
  let T := Algebra.EssFiniteType.subalgebra A C
  let M := Algebra.EssFiniteType.submonoid A C
  let r : Ideal T := P.comap (algebraMap T C)
  let : r.IsPrime := Ideal.IsPrime.comap (algebraMap T C)
  let : IsLocalization.AtPrime (Localization.AtPrime P) r :=
    IsLocalization.isLocalization_isLocalization_atPrime_isLocalization
      M (Localization.AtPrime P) P
  let e : Localization.AtPrime r ≃ₐ[T] Localization.AtPrime P :=
    IsLocalization.algEquiv r.primeCompl _ _
  let eA : Localization.AtPrime r ≃ₐ[A] Localization.AtPrime P :=
    e.restrictScalars A
  exact Algebra.FormallyEtale.of_equiv eA.symm

theorem
normalization_ramificationIdx_eq_at_essentiallyEtale_contraction_of_functionFieldProduct_surjective
    {A C F KC L M : Type u}
    [CommRing A] [IsDomain A] [IsNoetherianRing A]
    [CommRing C] [IsDomain C] [Algebra A C]
    [Algebra.EssFiniteType A C] [Algebra.FormallyEtale A C]
    [Field F] [Algebra A F] [IsFractionRing A F]
    [Field KC] [Algebra C KC] [IsFractionRing C KC]
    [Algebra A KC] [IsScalarTower A C KC]
    [Algebra F KC] [IsScalarTower A F KC]
    [Field L] [Algebra F L] [Algebra A L] [IsScalarTower A F L]
    [Field M] [Algebra KC M] [Algebra C M]
    [Algebra L M] [Algebra F M] [Algebra A M]
    [IsScalarTower C KC M] [IsScalarTower F KC M]
    [IsScalarTower F L M] [IsScalarTower A C M]
    [IsScalarTower A L M]
    (hgeneric : Function.Surjective
      (Algebra.TensorProduct.productMap
        (IsScalarTower.toAlgHom F KC M)
        (IsScalarTower.toAlgHom F L M)))
    (p : Ideal A) [p.IsPrime]
    (P : Ideal C) [P.IsPrime]
    [P.LiesOver p]
    (Q : Ideal (integralClosure C M)) [Q.IsPrime] [Q.LiesOver P] :
    let q := Q.comap
      (integralClosureEtaleBaseChangeHom
        (A := A) (C := C) (L := L) (M := M))
    q.IsPrime ∧ q.LiesOver p ∧
      Q.ramificationIdx C = q.ramificationIdx A := by
  classical
  let T := Algebra.EssFiniteType.subalgebra A C
  let MTC := Algebra.EssFiniteType.submonoid A C
  let r : Ideal T := P.comap (algebraMap T C)
  let : r.IsPrime := Ideal.IsPrime.comap (algebraMap T C)
  let : IsFractionRing T KC :=
    finiteTypeModel_isFractionRing (A := A) (C := C) (K := KC)
  let : Algebra.FinitePresentation A T :=
    Algebra.FinitePresentation.of_finiteType.mp inferInstance
  let : Algebra.IsEtaleAt A r :=
    finiteTypeModel_isEtaleAt_contraction (A := A) (C := C) P
  obtain ⟨f, hfr, hfEtale⟩ :=
    Algebra.IsEtaleAt.exists_isStandardEtale (R := A) r
  have hf0 : f ≠ 0 := fun hf ↦ hfr (hf ▸ r.zero_mem)
  let S := Localization.Away f
  let : Algebra.IsStandardEtale A S := hfEtale
  let : Algebra S KC :=
    localizationAwayToExtensionAlgebra (K := KC) (L := KC) f hf0
  let : IsScalarTower T S KC :=
    localizationAwayToExtension_isScalarTower (K := KC) (L := KC) f hf0
  let : IsDomain S :=
    IsLocalization.isDomain_of_le_nonZeroDivisors S <|
      Submonoid.powers_le.mpr <|
        mem_nonZeroDivisors_iff_ne_zero.mpr hf0
  let : IsFractionRing S KC :=
    IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
      (.powers f) S KC
  let : Algebra S M :=
    ((algebraMap KC M).comp (algebraMap S KC)).toAlgebra
  let : IsScalarTower S KC M := IsScalarTower.of_algebraMap_eq' rfl
  let : IsScalarTower A S KC := IsScalarTower.to₁₃₄ A T S KC
  let : IsScalarTower A KC M := IsScalarTower.to₁₃₄ A C KC M
  let : IsScalarTower A S M := IsScalarTower.to₁₂₄ A S KC M
  have hproductS : Function.Surjective
      (etaleBaseChangeProductMap (A := A) (C := S) (L := L) (M := M)) :=
    etaleBaseChangeProductMap_surjective_of_fractionFieldProductMap_surjective
      (A := A) (C := S) (F := F) (KC := KC) (L := L) (M := M)
      hgeneric
  let CP := Localization.AtPrime P
  let : Algebra CP KC :=
    localizationAtPrimeToFractionFieldAlgebra (K := KC) P
  let : IsScalarTower C CP KC :=
    localizationAtPrimeToFractionField_isScalarTower (K := KC) P
  let : IsFractionRing CP KC :=
    localizationAtPrimeToFractionField_isFractionRing (K := KC) P
  let : Algebra CP M :=
    localizationAtPrimeToExtensionAlgebra (K := KC) (L := M) P
  let : IsScalarTower CP KC M :=
    localizationAtPrimeToFractionFieldToExtension_isScalarTower
      (K := KC) (L := M) P
  let : IsScalarTower C CP M :=
    localizationAtPrimeToExtension_isScalarTower (K := KC) (L := M) P
  let : IsLocalization.AtPrime CP r :=
    IsLocalization.isLocalization_isLocalization_atPrime_isLocalization
      MTC CP P
  have hpow : Submonoid.powers f ≤ r.primeCompl :=
    Submonoid.powers_le.mpr hfr
  let : Algebra S CP :=
    IsLocalization.localizationAlgebraOfSubmonoidLe
      S CP (.powers f) r.primeCompl hpow
  let : IsScalarTower T S CP :=
    IsLocalization.localization_isScalarTower_of_submonoid_le
      S CP (.powers f) r.primeCompl hpow
  let NS : Submonoid S := r.primeCompl.map (algebraMap T S)
  let : IsLocalization NS CP :=
    IsLocalization.isLocalization_of_submonoid_le
      S CP (.powers f) r.primeCompl hpow
  let : IsScalarTower S CP KC := by
    apply IsScalarTower.of_algebraMap_eq'
    apply IsLocalization.ringHom_ext (.powers f)
    ext x
    simp only [RingHom.comp_apply]
    rw [← IsScalarTower.algebraMap_apply T S CP,
      ← IsScalarTower.algebraMap_apply T CP KC,
      ← IsScalarTower.algebraMap_apply T S KC]
  let : IsScalarTower S CP M := by
    apply IsScalarTower.of_algebraMap_eq
    intro x
    change algebraMap S M x = algebraMap CP M (algebraMap S CP x)
    change algebraMap KC M (algebraMap S KC x) =
      algebraMap KC M (algebraMap CP KC (algebraMap S CP x))
    rw [IsScalarTower.algebraMap_apply S CP KC]
  let B := integralClosure A L
  let D := integralClosure C M
  let DS := integralClosure S M
  let E := integralClosure CP M
  let : Algebra B D := integralClosureEtaleBaseChangeAlgebra
  let : IsScalarTower A B D := by
    apply IsScalarTower.of_algebraMap_eq
    intro x
    apply Subtype.ext
    rw [integralClosureEtaleBaseChangeAlgebra_algebraMap_coe]
    simp only [Subalgebra.coe_algebraMap]
    rw [IsScalarTower.algebraMap_apply A L M]
  let : Algebra B DS :=
    integralClosureEtaleBaseChangeAlgebra
  let : IsScalarTower A B DS := by
    apply IsScalarTower.of_algebraMap_eq
    intro x
    apply Subtype.ext
    rw [integralClosureEtaleBaseChangeAlgebra_algebraMap_coe]
    simp only [Subalgebra.coe_algebraMap]
    rw [IsScalarTower.algebraMap_apply A L M]
  let : Algebra.Etale B DS :=
    integralClosure_etale_of_etaleBaseChangeProductMap_surjective hproductS
  let : Algebra D E := integralClosureLocalizationAlgebra (L := M) P
  let : IsScalarTower C D E :=
    IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  let : IsScalarTower D E M :=
    IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  let : IsLocalization
      (Algebra.algebraMapSubmonoid D P.primeCompl) E :=
    isLocalization_integralClosure_localizationAtPrime
      (K := KC) (L := M) P
  let : Algebra DS E :=
    integralClosureEtaleBaseChangeAlgebra
  let : IsScalarTower S DS E := by
    apply IsScalarTower.of_algebraMap_eq
    intro x
    apply Subtype.ext
    rw [integralClosureEtaleBaseChangeAlgebra_algebraMap_coe]
    simp only [Subalgebra.coe_algebraMap]
    rw [IsScalarTower.algebraMap_apply S M M]
    simp
  let : IsScalarTower DS E M :=
    IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  let NDS : Submonoid DS := Algebra.algebraMapSubmonoid DS NS
  let : IsLocalization (Algebra.algebraMapSubmonoid M NS) M :=
    IsLocalization.of_le_isUnit fun x hx ↦ by
      rcases hx with ⟨s, hs, rfl⟩
      change IsUnit (algebraMap S M s)
      simpa only [IsScalarTower.algebraMap_apply S CP M] using
        (IsLocalization.map_units CP ⟨s, hs⟩).map (algebraMap CP M)
  let : IsLocalization NDS E := by
    exact IsLocalization.integralClosure NS
  let Qloc : Ideal E :=
    localizedNormalizationPrime (K := KC) (L := M) P Q
  have hQunder : Q.under C = P := (Q.over_def P).symm
  let : Qloc.IsPrime :=
    localizedNormalizationPrime_isPrime_of_under_le
      (K := KC) (L := M) P Q (hQunder.le)
  have hQlocRam : Qloc.ramificationIdx CP = Q.ramificationIdx C :=
    localizedNormalizationPrime_ramificationIdx
      (K := KC) (L := M) P Q
  have hQDdisj : Disjoint
      ((Algebra.algebraMapSubmonoid D P.primeCompl : Submonoid D) : Set D)
      (Q : Set D) := by
    have hQOver : Q.LiesOver P := inferInstance
    exact Set.disjoint_image_left.mpr
      (Set.disjoint_compl_left_iff_subset.mpr hQOver.over.ge)
  let : Qloc.LiesOver Q := by
    change (Q.map (algebraMap D E)).LiesOver Q
    exact IsLocalization.liesOver_map_of_isPrime_disjoint
      (Algebra.algebraMapSubmonoid D P.primeCompl) E hQDdisj
  let QS : Ideal DS := Qloc.comap (algebraMap DS E)
  let : QS.IsPrime := Ideal.IsPrime.comap (algebraMap DS E)
  let : Qloc.LiesOver QS := ⟨rfl⟩
  have hNDSdisj : Disjoint (NDS : Set DS) (QS : Set DS) :=
    (IsLocalization.disjoint_under_iff NDS E Qloc).2
      (inferInstance : Qloc.IsPrime).ne_top
  have hmapQS : QS.map (algebraMap DS E) = Qloc := by
    exact IsLocalization.map_under NDS E Qloc
  let : CommRing DS := inferInstance
  have hQSRam : Qloc.ramificationIdx CP = Ideal.ramificationIdx (S := DS) QS S := by
    rw [← hmapQS]
    exact ramificationIdx_map_eq_of_isLocalization
      (R := S) (S := DS) (R' := CP) (S' := E)
      NS NDS QS hNDSdisj
  let qS : Ideal B := QS.comap (algebraMap B DS)
  let : qS.IsPrime := Ideal.IsPrime.comap (algebraMap B DS)
  let : QS.LiesOver qS := ⟨rfl⟩
  have hqSRam : Ideal.ramificationIdx (S := DS) QS S = qS.ramificationIdx A :=
    ramificationIdx_eq_of_etale_square
      (R := A) (B := B) (C := S) (S := DS) qS QS
  let hBD := integralClosureEtaleBaseChangeHom
    (A := A) (C := C) (L := L) (M := M)
  let q : Ideal B := Q.comap hBD
  have hmaps :
      (algebraMap DS E).comp
          (algebraMap B DS) =
        (algebraMap D E).comp hBD := by
    ext x
    rfl
  have hqeq : qS = q := by
    have hQeq : Q = Qloc.comap (algebraMap D E) := Qloc.over_def Q
    dsimp only [qS, q, QS]
    rw [hQeq, Ideal.comap_comap, Ideal.comap_comap, hmaps]
  have hqPrime : q.IsPrime := hqeq ▸ inferInstance
  let : q.IsPrime := hqPrime
  have hqOver : q.LiesOver p := by
    have hQp : Q.LiesOver p := Ideal.LiesOver.trans Q P p
    let : Q.LiesOver p := hQp
    change (Q.comap (algebraMap B D)).LiesOver p
    infer_instance
  let : q.LiesOver p := hqOver
  exact ⟨hqPrime, hqOver, hQlocRam.symm.trans <|
    hQSRam.trans <| hqSRam.trans <| hqeq ▸ rfl⟩

theorem
  normalizationInertia_natCard_eq_at_essentiallyEtale_contraction_of_functionFieldProduct_surjective
    {A C F KC L M : Type u}
    [CommRing A] [IsDomain A] [IsNoetherianRing A]
    [IsIntegrallyClosed A]
    [CommRing C] [IsDomain C] [IsNoetherianRing C]
    [IsIntegrallyClosed C] [Algebra A C]
    [Algebra.EssFiniteType A C] [Algebra.FormallyEtale A C]
    [Field F] [Algebra A F] [IsFractionRing A F]
    [Field KC] [Algebra C KC] [IsFractionRing C KC]
    [Algebra A KC] [IsScalarTower A C KC]
    [Algebra F KC] [IsScalarTower A F KC]
    [Field L] [Algebra F L] [Algebra A L] [IsScalarTower A F L]
    [FiniteDimensional F L] [IsGalois F L]
    [Field M] [Algebra KC M] [Algebra C M]
    [FiniteDimensional KC M] [IsGalois KC M]
    [Algebra L M] [Algebra F M] [Algebra A M]
    [IsScalarTower C KC M] [IsScalarTower F KC M]
    [IsScalarTower F L M] [IsScalarTower A C M]
    [IsScalarTower A L M]
    (hgeneric : Function.Surjective
      (Algebra.TensorProduct.productMap
        (IsScalarTower.toAlgHom F KC M)
        (IsScalarTower.toAlgHom F L M)))
    (p : Ideal A) [p.IsPrime] (hpheight : p.height = 1)
    (P : Ideal C) [P.IsPrime] (hPheight : P.height = 1)
    [P.LiesOver p]
    (Q : Ideal (integralClosure C M)) [Q.IsPrime] [Q.LiesOver P]
    [CharZero (A ⧸ p)] [CharZero (C ⧸ P)] :
    let q := Q.comap
      (integralClosureEtaleBaseChangeHom
        (A := A) (C := C) (L := L) (M := M))
    q.IsPrime ∧ q.LiesOver p ∧
      Nat.card (Q.toAddSubgroup.inertia Gal(M/KC)) =
        Nat.card (q.toAddSubgroup.inertia Gal(L/F)) := by
  let q := Q.comap
    (integralClosureEtaleBaseChangeHom
      (A := A) (C := C) (L := L) (M := M))
  obtain ⟨hqPrime, hqOver, hram⟩ :=
    (
normalization_ramificationIdx_eq_at_essentiallyEtale_contraction_of_functionFieldProduct_surjective
      (A := A) (C := C) (F := F) (KC := KC) (L := L) (M := M)
      hgeneric p P Q)
  let : q.IsPrime := hqPrime
  let : q.LiesOver p := hqOver
  refine ⟨hqPrime, hqOver, ?_⟩
  have hQcard :
      Nat.card (Q.toAddSubgroup.inertia Gal(M/KC)) =
        Q.ramificationIdx C :=
    normalizationInertia_card_eq_ramificationIdx_of_normal_noetherian
      (K := KC) (L := M) P hPheight Q
  have hqcard :
      Nat.card (q.toAddSubgroup.inertia Gal(L/F)) =
        q.ramificationIdx A :=
    normalizationInertia_card_eq_ramificationIdx_of_normal_noetherian
      (K := F) (L := L) p hpheight q
  exact hQcard.trans (hram.trans hqcard.symm)