EtaleFundamentalGroups.Kummer.galoisFullRootCover_selectedComponent_exactPrimeSource_constructed
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe uA uK uL
Lean source · full declarationtheorem
galoisFullRootCover_selectedComponent_exactPrimeSource_constructed
{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]
[Module.Finite A (integralClosure A 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 : ∀ j, j.1 < r →
CharZero (A ⧸ Ideal.span ({t j} : Set A)))
(hAway : (Localization.awayMap
(algebraMap A (integralClosure A L)) f).Etale) :
let e := heightTwoOtherBranchGaloisRamificationIndex
(K := K) (L := L) t hNC i
let N := heightTwoSelectedBranchGaloisRamificationIndex
(K := K) (L := L) t hNC i
∃ σ : Equiv.Perm (Fin d),
let R := Localization.AtPrime P
let n := heightTwoConditionalOtherExponent t i r P e σ
let a : Fin d → R := heightTwoConditionalOtherRadicand t i P σ
let B := iteratedRadical R d n a
let y : R := algebraMap A R (t i)
let yB : B := algebraMap R B y
let F : B[X] := X ^ N - C yB
let D := AdjoinRoot F
∃ hgeometryB : IsRegularLocalRing B ∧ IsDomain B ∧
ringKrullDim B = ((2 : ℕ∞) : WithBot ℕ∞) ∧ Prime yB ∧
IsDomain (B ⧸ Ideal.span ({yB} : Set B)) ∧
IsRegularLocalRing (B ⧸ Ideal.span ({yB} : Set B)),
∃ hgeometryD : IsRegularLocalRing D ∧ IsDomain D ∧
ringKrullDim D = ((2 : ℕ∞) : WithBot ℕ∞) ∧
Prime (AdjoinRoot.root F),
let : IsRegularLocalRing B := hgeometryB.1
let : IsDomain B := hgeometryB.2.1
let : IsIntegrallyClosed B :=
SpecialLocalPurity.isIntegrallyClosed_of_isRegularLocalRing_dimension_two
hgeometryB.2.2.1
let : IsRegularLocalRing D := hgeometryD.1
let : IsDomain D := hgeometryD.2.1
let : IsIntegrallyClosed D :=
SpecialLocalPurity.isIntegrallyClosed_of_isRegularLocalRing_dimension_two
hgeometryD.2.2.1
let hn : ∀ k, 0 < n k :=
heightTwoConditionalOtherExponent_pos_of_pos t i r P e
(heightTwoOtherBranchGaloisRamificationIndex_pos
(K := K) (L := L) t hNC i) σ
let hN : 0 < N :=
heightTwoSelectedBranchGaloisRamificationIndex_pos
(K := K) (L := L) t hNC i
let : Module.Finite B D := by
simpa only [D, F] using
(monic_X_pow_sub_C yB hN.ne').finite_adjoinRoot
let : Algebra.IsIntegral B D := Algebra.IsIntegral.of_finite B D
let : Module.FaithfullyFlat R B :=
faithfullyFlat_iteratedRadical n a hn
let : FaithfulSMul R B := Module.FaithfullyFlat.faithfulSMul
let : Module.FaithfullyFlat B D :=
faithfullyFlat_adjoinRoot_X_pow_sub_C hN yB
let : FaithfulSMul B D := Module.FaithfullyFlat.faithfulSMul
let : FaithfulSMul R D := FaithfulSMul.trans R B D
let : Algebra R K :=
localizationAtPrimeToFractionFieldAlgebra (K := K) P
let : IsFractionRing R K :=
localizationAtPrimeToFractionField_isFractionRing (K := K) P
let KB := FractionRing B
let KD := FractionRing D
let : FaithfulSMul R KB := FaithfulSMul.trans R B KB
let : FaithfulSMul R KD := FaithfulSMul.trans R D KD
let : FaithfulSMul B KD := FaithfulSMul.trans B D KD
let : Algebra K KB :=
chosenFractionFieldToFaithfulFieldAlgebra
(R := R) (K := K) (F := KB)
let : Algebra K KD :=
galoisFullRootCoverFractionFieldAlgebra n a hn N hN y
let : Algebra KB KD := FractionRing.liftAlgebra B KD
∃ hTower : IsScalarTower K KB KD,
let : IsScalarTower K KB KD := hTower
∃ hFin : FiniteDimensional KB KD,
let : FiniteDimensional KB KD := hFin
let m := genericTensorMaximalIdeal
(K := K) (K' := KD) (L := L)
let : m.IsMaximal := genericTensorMaximalIdeal_isMaximal
let n₀ := genericTensorTowerIntermediateIdeal
(K := K) (F := KB) (F' := KD) (L := L) m
let : n₀.IsMaximal :=
genericTensorTowerIntermediateIdeal_isMaximal
(K := K) (F := KB) (F' := KD) (L := L) m
let M₀ := GenericTensorFieldComponent n₀
let : Algebra B M₀ :=
genericTensorFieldComponentLeftScalarAlgebra (R := B) n₀
let : SMul B M₀ :=
(genericTensorFieldComponentLeftScalarAlgebra
(R := B) n₀).toSMul
let : IsScalarTower B KB M₀ :=
IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
let M := GenericTensorFieldComponent m
let : Algebra D M :=
genericTensorFieldComponentLeftScalarAlgebra (R := D) m
let : SMul D M :=
(genericTensorFieldComponentLeftScalarAlgebra
(R := D) m).toSMul
let : IsScalarTower D KD M :=
IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
let pR := (Ideal.span ({t i} : Set A)).map
(algebraMap A R)
let qB := Ideal.span ({yB} : Set B)
let qD := Ideal.span ({AdjoinRoot.root F} : Set D)
let : pR.IsPrime := by
let : (Ideal.span ({t i} : Set A)).IsPrime :=
Ideal.isPrime_span_singleton_of_prime
(hNC.2.2.2.1 i hi)
exact Ideal.isPrime_map_of_isLocalizationAtPrime P
(P.span_singleton_le_iff_mem.mpr htiP)
let : qB.IsPrime :=
Ideal.isPrime_span_singleton_of_prime hgeometryB.2.2.2.1
let : qD.IsPrime :=
Ideal.isPrime_span_singleton_of_prime hgeometryD.2.2.2
let : qB.LiesOver pR := by
constructor
simpa only [pR, qB, yB, y, Ideal.map_span,
Ideal.map_map, Set.image_singleton,
RingHom.comp_apply] using
(Ideal.comap_map_eq_self_of_faithfullyFlat
(B := B) pR).symm
let : qD.LiesOver qB :=
span_root_liesOver_span_radicand hN hgeometryB.2.2.2.1
let : qD.LiesOver pR := Ideal.LiesOver.trans qD qB pR
let V := Localization.AtPrime pR
let W := Localization.AtPrime qD
let : Algebra V W :=
Localization.AtPrime.algebraOfLiesOver pR qD
let : IsLocalHom (algebraMap V W) := inferInstance
let : Algebra V K :=
localizationAtPrimeToFractionFieldAlgebra (K := K) pR
let : Algebra V L :=
localizationAtPrimeToExtensionAlgebra
(K := K) (L := L) pR
let : Algebra W KD :=
localizationAtPrimeToFractionFieldAlgebra (K := KD) qD
let : Algebra W M :=
localizationAtPrimeToExtensionAlgebra
(K := KD) (L := M) qD
let : Algebra L M := genericTensorFieldComponentRightAlgebra m
let : Algebra V M :=
((algebraMap W M).comp (algebraMap V W)).toAlgebra
let Csel := integralClosure V L
let Cpost := integralClosure W M
let Cglobal := integralClosure D M
let : Algebra B Cglobal :=
((algebraMap D Cglobal).comp (algebraMap B D)).toAlgebra
let : Algebra V Cpost :=
((algebraMap W Cpost).comp (algebraMap V W)).toAlgebra
∃ qPost : (IsLocalRing.maximalIdeal W).primesOver Cpost,
∃ qGlobal p : Ideal Cglobal,
qGlobal.IsPrime ∧ qGlobal.LiesOver qD ∧
localizedNormalizationPrime
(K := KD) (L := M) qD qGlobal = qPost.1 ∧
qGlobal.ramificationIdx D =
qPost.1.ramificationIdx W ∧
qGlobal.ramificationIdx B = N ∧
qGlobal ≤ p ∧ p.IsMaximal ∧
p.LiesOver (IsLocalRing.maximalIdeal D) ∧
let qPrefix :=
genericTensorTowerIntermediateNormalizationPrime
(A := B) (B := D) (K := K) (F := KB)
(F' := KD) (L := L) m qGlobal
let qClosed :=
genericTensorTowerIntermediateNormalizationPrime
(A := B) (B := D) (K := K) (F := KB)
(F' := KD) (L := L) m p
qGlobal.comap
(genericTensorTowerIntermediateNormalizationAlgHom
(A := B) (B := D) (K := K) (F := KB)
(F' := KD) (L := L) m).toRingHom = qPrefix ∧
qPrefix.IsPrime ∧ qPrefix.LiesOver qB ∧
qPrefix.ramificationIdx B = N ∧
qPrefix ≤ qClosed ∧ qClosed.IsMaximal ∧
qClosed.LiesOver (IsLocalRing.maximalIdeal B) ∧
∃ φ : Csel →ₐ[V] Cpost,
∃ Q : (IsLocalRing.maximalIdeal V).primesOver Csel,
qPost.1.comap φ.toRingHom = Q.1 ∧
(∀ z : Csel,
(((φ z : Cpost) : M)) =
algebraMap L M (z : L)) ∧
Ideal.ramificationIdx (S := Csel) Q.1 V = N ∧
(Localization.awayMap
(algebraMap B (integralClosure B M₀)) yB).Etale ∧
Module.Finite D (integralClosure D M) ∧
Algebra.Etale D (integralClosure D M) := by
classical
intro e N
obtain ⟨σ, hgeometryB, hgeometryD, _hTowerCombined,
_hFinCombined, hcomponentForAll⟩ :=
splitStrictNormalCrossings_heightTwo_galoisPrefix_selectedAway_fullRoot_fixedComponent_etale
(A := A) (K := K) (L := L) (d := d) (r := r)
(f := f) (t := t) hNC i hi P hP htiP hCharZero hAway
refine ⟨σ, ?_⟩
intro R n a B y yB F D
refine ⟨hgeometryB, hgeometryD, ?_⟩
intro regB domainB closedB regD domainD closedD hn hN
finiteBD integralBD ffRB faithfulRB ffBD faithfulBD faithfulRD
algRK fracRK KB KD faithfulRKB faithfulRKD faithfulBKD algKKB algKKD algKBKD
let : IsScalarTower A R K :=
localizationAtPrimeToFractionField_isScalarTower (K := K) P
let : IsScalarTower R K KB :=
chosenFractionFieldToFaithfulField_isScalarTower
(R := R) (K := K) (F := KB)
let : IsScalarTower R K KD :=
galoisFullRootCoverFractionField_isScalarTower n a hn N hN y
let : IsScalarTower R B KB := IsScalarTower.of_algebraMap_eq' rfl
let : IsScalarTower R B D := IsScalarTower.of_algebraMap_eq' rfl
let : IsScalarTower B D KD := IsScalarTower.of_algebraMap_eq' rfl
let : IsScalarTower R D KD := IsScalarTower.of_algebraMap_eq' rfl
let : IsScalarTower R B KD := IsScalarTower.of_algebraMap_eq' rfl
let : IsScalarTower B KB KD :=
FractionRing.isScalarTower_liftAlgebra B KD
refine ⟨_hTowerCombined, ?_⟩
intro towerKKBKD
refine ⟨_hFinCombined, ?_⟩
intro finiteKBKD m hm n₀ hn₀ M₀ algBM₀ smulBM₀ towerBKBM₀
M algDM smulDM towerDKDM
have hcomponent :
(Localization.awayMap
(algebraMap B (integralClosure B M₀)) yB).Etale ∧
Module.Finite D (integralClosure D M) ∧
Algebra.Etale D (integralClosure D M) :=
hcomponentForAll m inferInstance
intro pR qB qD hpR hqB hqD hqBpR hqDqB hqDpR V W
algVW localVW algVK algVL algWKD algWM algLM algVM
have hPrefixRamification :
∀ qPrefix : Ideal (integralClosure B M₀), qPrefix.IsPrime →
qPrefix.LiesOver qB → qPrefix.ramificationIdx B = N :=
prefixNormalizationRamification_exactPrimeSource
(K := K) (L := L) hNC i hi P hP htiP (hCharZero i hi) σ hgeometryB
n₀ inferInstance
intro Csel Cpost Cglobal algBCglobal algVCpost
let : IsScalarTower B D Cglobal := IsScalarTower.of_algebraMap_eq' rfl
let : Module.Finite D Cglobal := hcomponent.2.1
obtain ⟨qPost, qGlobal, p, hqGlobalPrime, hqGlobalOver,
hqGlobalLocal, hqGlobalRam, hqGlobalLe, hpMax, hpOver⟩ :=
postRootNormalizationPrimes_exactPrimeSource (D := D) (KD := KD) (M := M) qD
have hqDRam : qD.ramificationIdx B = N := by
let : IsRegularRing B :=
EtaleFundamentalGroups.isRegularRing_of_isRegularLocalRing_dimension_two
hgeometryB.2.2.1
let U := Localization.AtPrime qB
let : Algebra U W :=
Localization.AtPrime.algebraOfLiesOver qB qD
let : IsDomain W := by
simpa only [W, qD, D, F] using
(adjoinRootLocalizationAtRootPrime_isDomain
(R := B) hN hgeometryB.2.2.2.1)
let hWDVR : IsDiscreteValuationRing W := by
simpa only [W, qD, D, F] using
(adjoinRootLocalizationAtRootPrime_isDiscreteValuationRing
(R := B) hN hgeometryB.2.2.2.1)
have hqBMapW : qB.map (algebraMap B W) =
IsLocalRing.maximalIdeal W ^ N := by
calc
qB.map (algebraMap B W) =
(qB.map (algebraMap B U)).map (algebraMap U W) := by
rw [Ideal.map_map, IsScalarTower.algebraMap_eq B U W]
_ = (IsLocalRing.maximalIdeal U).map (algebraMap U W) := by
rw [Localization.AtPrime.map_eq_maximalIdeal]
_ = IsLocalRing.maximalIdeal W ^ N := by
simpa only [U, W, qB, qD, D, F] using
(adjoinRootLocalizationAtRootPrime_maximalIdeal_map_eq_pow
(R := B) hN hgeometryB.2.2.2.1)
rw [Ideal.ramificationIdx_eq qB qD, hqBMapW,
hWDVR.length_quotient_pow_maximalIdeal, ENat.toNat_natCast]
let : Algebra.Etale D Cglobal := hcomponent.2.2
have hqGlobalRamDOne : qGlobal.ramificationIdx D = 1 :=
Ideal.ramificationIdx_eq_one qGlobal D
have hqGlobalRamB : qGlobal.ramificationIdx B = N := by
calc
qGlobal.ramificationIdx B =
qD.ramificationIdx B * qGlobal.ramificationIdx D :=
Ideal.ramificationIdx_tower qD qGlobal
_ = N := by rw [hqDRam, hqGlobalRamDOne, mul_one]
refine ⟨qPost, qGlobal, p, hqGlobalPrime, hqGlobalOver,
hqGlobalLocal, hqGlobalRam, hqGlobalRamB, hqGlobalLe, hpMax, hpOver, ?_⟩
intro qPrefix qClosed
have hqPrefixPrime : qPrefix.IsPrime :=
genericTensorTowerIntermediateNormalizationPrime_isPrime
(A := B) (B := D) (K := K) (F := KB) (F' := KD) (L := L)
m qGlobal
have hqClosedMax : qClosed.IsMaximal :=
genericTensorTowerIntermediateNormalizationPrime_isMaximal
(A := B) (B := D) (K := K) (F := KB) (F' := KD) (L := L)
m p
have hqClosedOver : qClosed.LiesOver (IsLocalRing.maximalIdeal B) :=
genericTensorTowerIntermediateNormalizationPrime_liesOver_maximalIdeal
(A := B) (B := D) (K := K) (F := KB) (F' := KD) (L := L)
m p
let g := genericTensorTowerIntermediateNormalizationAlgHom
(A := B) (B := D) (K := K) (F := KB) (F' := KD) (L := L) m
have hqGlobalComap : qGlobal.comap g.toRingHom = qPrefix :=
genericTensorTowerIntermediateNormalizationAlgHom_comap_eq_prime
(A := B) (B := D) (K := K) (F := KB) (F' := KD) (L := L)
m qGlobal
have hqGlobalOverB : qGlobal.LiesOver qB :=
Ideal.LiesOver.trans qGlobal qD qB
have hqPrefixOver : qPrefix.LiesOver qB := by
have hmap :
g.toRingHom.comp (algebraMap B (integralClosure B M₀)) =
algebraMap B Cglobal := by
apply RingHom.ext
intro b
exact g.commutes b
constructor
rw [Ideal.under_def, ← hqGlobalComap, Ideal.comap_comap, hmap]
exact hqGlobalOverB.over
have hqPrefixLe : qPrefix ≤ qClosed := by
change qGlobal.comap g.toRingHom ≤ p.comap g.toRingHom
exact Ideal.comap_mono hqGlobalLe
have hBaseRing :
(algebraMap K KD).comp (algebraMap R K) =
(algebraMap D KD).comp (algebraMap R D) := by
ext z
simp only [RingHom.comp_apply]
rw [← IsScalarTower.algebraMap_apply R K KD,
IsScalarTower.algebraMap_apply R D KD]
have hTensorRing :
(genericTensorFieldComponentLeft m).toRingHom.comp (algebraMap K KD) =
(genericTensorFieldComponentRight m).toRingHom.comp (algebraMap K L) := by
ext z
exact ((genericTensorFieldComponentLeft m).commutes z).trans
((genericTensorFieldComponentRight m).commutes z).symm
have hLocalRing := localizedComponentMaps_commute_exactPrimeSource
(R := R) (D := D) (K := K) (KD := KD) (L := L) (M := M)
pR qD (genericTensorFieldComponentLeft m).toRingHom
(genericTensorFieldComponentRight m).toRingHom hBaseRing hTensorRing
obtain ⟨φ, Q, hQComap, hQCoe, hExact⟩ :=
selectedPrimeContraction_exactPrimeSource (N := N)
(V := V) (W := W) (L := L) (M := M)
(algVW := Localization.AtPrime.algebraOfLiesOver pR qD)
(algVL := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) pR)
(algWM := localizationAtPrimeToExtensionAlgebra (K := KD) (L := M) qD)
(genericTensorFieldComponentRight m).toRingHom
(RingHom.ext fun z ↦ (DFunLike.congr_fun hLocalRing z).symm)
qPost (fun Qauto ↦ by
simpa only [N, R, pR, V, Csel,
heightTwoSelectedBranchGaloisRamificationIndex] using
(
localNormalizationPrime_ramificationIdx_eq_splitStrictNormalCrossingsGaloisIndex_at_largerPrime
(K := K) (L := L) hNC i hi P htiP Qauto))
refine ⟨hqGlobalComap, hqPrefixPrime, hqPrefixOver, ?_, hqPrefixLe,
hqClosedMax, hqClosedOver,
φ, Q, hQComap, ?_, hExact, hcomponent.1,
hcomponent.2.1, hcomponent.2.2⟩
· exact hPrefixRamification qPrefix hqPrefixPrime hqPrefixOver
intro z
exact hQCoe z