EtaleFundamentalGroups.Kummer.exists_higherRadicalActualFactorData_of_completeBase
A specified uniformizer of a complete DVF has an actual finite-etale higher-radical factor in every finite separable field extension, at the intrinsic ramification exponent of the canonical target valuation.
The target complete valuation, finite extension of valuation rings, target uniformizer and unit decomposition, and the required root in the algebraic closure are all constructed in the proof.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v wLean source · full declaration
theorem exists_higherRadicalActualFactorData_of_completeBase
{K : Type u} {L : Type w} [Field K] [Field L]
[Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
(base : CompleteDVF.{u, v} K)
[CharZero base.residueField]
(varpi : base.valuationSubring)
(hvarpi : base.valuation.IsUniformizer (varpi : K)) :
∃ target : CompleteDVF.{w, 0} L,
∃ hExt : base.valuation.HasExtension target.valuation,
letI : base.valuation.HasExtension target.valuation := hExt
let e := ramificationIndex base.toDVF target.toDVF
∃ (pi : target.valuationSubring)
(unit : target.valuationSubringˣ)
(beta : AlgebraicClosure L),
target.valuation.IsUniformizer (pi : L) ∧
integerMap base.toDVF target.toDVF varpi =
(unit : target.valuationSubring) * pi ^ e ∧
beta ^ e =
algebraMap K (AlgebraicClosure L) (varpi : K) ∧
Nonempty
(HigherRadicalActualFactorData
base.toDVF target.toDVF varpi e beta) := by
obtain ⟨target, hExt, hIntegralClosure, _hFundamental⟩ :=
exists_integralClosure_standard_fundamental_identity
(K := K) (L := L) base
refine ⟨target, hExt, ?_⟩
let : base.valuation.HasExtension target.valuation := hExt
let : IsScalarTower base.valuationSubring target.valuationSubring L :=
IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
let : IsIntegralClosure target.valuationSubring
base.valuationSubring L := hIntegralClosure
let : Module.Finite base.valuationSubring target.valuationSubring :=
moduleFinite_target_valuationSubring_of_isIntegralClosure
(K := K) (L := L) base target
let : Module.IsTorsionFree base.valuationSubring
target.valuationSubring :=
Module.isTorsionFree_iff_algebraMap_injective.mpr
(integerMap_injective base.toDVF target.toDVF)
obtain ⟨pi, hpi⟩ := target.exists_uniformizer
obtain ⟨unit, hdecomp⟩ :=
exists_unit_mul_target_uniformizer_pow_eq_base_uniformizer_image_of_dvf
base.toDVF target.toDVF hvarpi hpi
let e := ramificationIndex base.toDVF target.toDVF
have he : 0 < e := by
exact Nat.pos_of_ne_zero
(ramificationIndex_ne_zero (base := base) (target := target))
obtain ⟨beta, hbeta⟩ :=
IsAlgClosed.exists_pow_nat_eq
(algebraMap K (AlgebraicClosure L) (varpi : K)) he
refine ⟨pi, unit, beta, hpi, hdecomp, hbeta, ?_⟩
exact higherRadicalActualFactorData
base.toDVF target.toDVF varpi hvarpi pi unit hpi hdecomp
e (dvd_refl e) beta hbeta