EtaleFundamentalGroups.Kummer.exists_finiteEtale_unitAbsorption_uniformizerRadical
In residue characteristic zero, a bare extension of discrete valuation fields becomes a pure uniformizer radical after passing to one generic field factor of a finite etale unit-root algebra on the target.
The two displayed AdjoinRoot equivalences use the same chosen root delta: the first presents its generic factor over the target field, while the second presents only the pure radical subfield generated by alpha = delta * pi over the base field. No equivalence between the whole generic factor and the pure radical subfield is asserted.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v w xLean source · full declaration
theorem exists_finiteEtale_unitAbsorption_uniformizerRadical
{K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
(base : DVF.{u, v} K) (target : DVF.{w, x} L)
[base.valuation.HasExtension target.valuation]
[CharZero base.residueField] :
let n := ramificationIndex base target
exists (varpi : base.valuationSubring) (pi : target.valuationSubring)
(unit : target.valuationSubringˣ)
(delta alpha : AlgebraicClosure L)
(factorEquiv :
AdjoinRoot (minpoly L delta) ≃ₐ[L]
IntermediateField.adjoin L ({delta} : Set (AlgebraicClosure L)))
(radicalEquiv :
AdjoinRoot (X ^ n - C (varpi : K)) ≃ₐ[K]
IntermediateField.adjoin K ({alpha} : Set (AlgebraicClosure L))),
base.valuation.IsUniformizer (varpi : K) ∧
target.valuation.IsUniformizer (pi : L) ∧
Prime varpi ∧
integerMap base target varpi =
(unit : target.valuationSubring) * pi ^ n ∧
Algebra.Etale target.valuationSubring
(AdjoinRoot
(X ^ n - C (unit : target.valuationSubring))) ∧
Module.Finite target.valuationSubring
(AdjoinRoot
(X ^ n - C (unit : target.valuationSubring))) ∧
delta ^ n = algebraMap L (AlgebraicClosure L) (unit : L) ∧
minpoly L delta ∣ X ^ n - C (unit : L) ∧
IsSeparable L delta ∧
alpha = delta * algebraMap L (AlgebraicClosure L) (pi : L) ∧
alpha ^ n =
algebraMap K (AlgebraicClosure L) (varpi : K) ∧
factorEquiv (AdjoinRoot.root (minpoly L delta)) =
IntermediateField.AdjoinSimple.gen L delta ∧
radicalEquiv
(AdjoinRoot.root (X ^ n - C (varpi : K))) =
IntermediateField.AdjoinSimple.gen K alpha := by
let n := ramificationIndex base target
have hn_ne : n ≠ 0 := by
simpa [n, ramificationIndex] using
(Ideal.IsDedekindDomain.ramificationIdx'_ne_zero
(maximalIdeal_map_integerMap_ne_bot base target)
(IsLocalRing.maximalIdeal.isMaximal target.valuationSubring).isPrime
(maximalIdeal_map_integerMap_le base target))
have hn : 0 < n := Nat.pos_of_ne_zero hn_ne
have hnBase : IsUnit (n : base.valuationSubring) := by
apply (base.residue_ne_zero_iff_isUnit (n : base.valuationSubring)).mp
simpa using (Nat.cast_ne_zero.mpr hn_ne : (n : base.residueField) ≠ 0)
have hnTarget : IsUnit (n : target.valuationSubring) := by
simpa using hnBase.map (integerMap base target)
obtain ⟨varpi, pi, unit, hvarpi, hpi, hdecomp⟩ :=
exists_uniformizers_unit_mul_target_uniformizer_pow_eq_base_uniformizer_image
base target
let targetPolynomial : target.valuationSubring[X] :=
X ^ n - C (unit : target.valuationSubring)
have hFormal :
Algebra.FormallyEtale target.valuationSubring
(AdjoinRoot targetPolynomial) := by
exact formallyEtale_adjoinRoot_X_pow_sub_C hn hnTarget unit.isUnit
have hEtale :
Algebra.Etale target.valuationSubring
(AdjoinRoot targetPolynomial) :=
{ formallyEtale := hFormal
finitePresentation := inferInstance }
have hFinite :
Module.Finite target.valuationSubring
(AdjoinRoot targetPolynomial) :=
(Polynomial.monic_X_pow_sub_C
(unit : target.valuationSubring) hn.ne').finite_adjoinRoot
let Omega := AlgebraicClosure L
obtain ⟨delta, hdelta⟩ :=
IsAlgClosed.exists_pow_nat_eq
(algebraMap L Omega (unit : L)) hn
let fieldPolynomial : L[X] := X ^ n - C (unit : L)
have hFieldRoot : aeval delta fieldPolynomial = 0 := by
simp [fieldPolynomial, hdelta]
have hMinpolyDvd : minpoly L delta ∣ fieldPolynomial :=
minpoly.dvd L delta hFieldRoot
have hnL : IsUnit (n : L) := by
simpa using hnTarget.map (algebraMap target.valuationSubring L)
have hunitL : IsUnit (unit : L) :=
unit.isUnit.map (algebraMap target.valuationSubring L)
have hFieldSeparable : fieldPolynomial.Separable := by
exact Polynomial.separable_X_pow_sub_C (unit : L) hnL.ne_zero hunitL.ne_zero
have hdeltaSeparable : IsSeparable L delta := by
exact hFieldSeparable.of_dvd hMinpolyDvd
have hdeltaIntegral : IsIntegral L delta :=
Algebra.IsIntegral.isIntegral delta
let factorEquiv :
AdjoinRoot (minpoly L delta) ≃ₐ[L]
IntermediateField.adjoin L ({delta} : Set Omega) :=
IntermediateField.adjoinRootEquivAdjoin L hdeltaIntegral
have hvarpi_ne : varpi ≠ 0 := by
intro hzero
apply hvarpi.ne_zero
exact congrArg Subtype.val hzero
have hvarpiPrime : Prime varpi := by
apply (Ideal.span_singleton_prime hvarpi_ne).mp
exact (base.maximalIdeal_eq_span_uniformizer hvarpi).symm ▸
(IsLocalRing.maximalIdeal.isMaximal base.valuationSubring).isPrime
have hdecompL :
algebraMap K L (varpi : K) = (unit : L) * (pi : L) ^ n := by
have h := congrArg (fun z : target.valuationSubring ↦ (z : L)) hdecomp
simpa using h
let alpha : Omega :=
delta * algebraMap L Omega (pi : L)
have halphaPow :
alpha ^ n = algebraMap K Omega (varpi : K) := by
calc
alpha ^ n =
delta ^ n * (algebraMap L Omega (pi : L)) ^ n := by
simp [alpha, mul_pow]
_ = algebraMap L Omega (unit : L) *
algebraMap L Omega ((pi : L) ^ n) := by
rw [hdelta, map_pow]
_ = algebraMap L Omega ((unit : L) * (pi : L) ^ n) := by
rw [map_mul]
_ = algebraMap L Omega (algebraMap K L (varpi : K)) := by
rw [hdecompL]
_ = algebraMap K Omega (varpi : K) := by
rw [IsScalarTower.algebraMap_apply K L Omega]
let : IsFractionRing base.valuationSubring K :=
base.valuationSubring_isFractionRing
let : IsIntegrallyClosed base.valuationSubring :=
base.valuationSubring_isIntegrallyClosed
let radicalPolynomial : K[X] := X ^ n - C (varpi : K)
have hRadicalIrreducible : Irreducible radicalPolynomial := by
exact irreducible_X_pow_sub_C_fractionRing_of_prime hvarpiPrime hn
have hRadicalMonic : radicalPolynomial.Monic := by
exact monic_X_pow_sub_C (varpi : K) hn.ne'
have hRadicalRoot : aeval alpha radicalPolynomial = 0 := by
simp [radicalPolynomial, halphaPow]
have hRadicalMinpoly : radicalPolynomial = minpoly K alpha :=
minpoly.eq_of_irreducible_of_monic
hRadicalIrreducible hRadicalRoot hRadicalMonic
have halphaIntegral : IsIntegral K alpha :=
⟨radicalPolynomial, hRadicalMonic, hRadicalRoot⟩
let radicalEquiv :
AdjoinRoot radicalPolynomial ≃ₐ[K]
IntermediateField.adjoin K ({alpha} : Set Omega) :=
(AdjoinRoot.algEquivOfEq K radicalPolynomial (minpoly K alpha)
hRadicalMinpoly).trans
(IntermediateField.adjoinRootEquivAdjoin K halphaIntegral)
have hFactorRoot :
factorEquiv (AdjoinRoot.root (minpoly L delta)) =
IntermediateField.AdjoinSimple.gen L delta :=
IntermediateField.adjoinRootEquivAdjoin_apply_root L hdeltaIntegral
have hRadicalEquivRoot :
radicalEquiv (AdjoinRoot.root radicalPolynomial) =
IntermediateField.AdjoinSimple.gen K alpha := by
simp [radicalEquiv, AdjoinRoot.algEquivOfEq_root,
IntermediateField.adjoinRootEquivAdjoin_apply_root]
refine ⟨varpi, pi, unit, delta, alpha, factorEquiv, radicalEquiv,
hvarpi, hpi, hvarpiPrime, hdecomp, ?_, ?_, hdelta, ?_,
hdeltaSeparable, rfl, halphaPow, hFactorRoot, ?_⟩
· simpa [targetPolynomial] using hEtale
· simpa [targetPolynomial] using hFinite
· simpa [fieldPolynomial] using hMinpolyDvd
· simpa [radicalPolynomial] using hRadicalEquivRoot