AlgebraicNumberTheory.Valuations.maximalUnramifiedSubextension_finiteUnramified
In a finite extension, the maximal unramified subextension is itself a finite unramified extension.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
namespace AlgebraicNumberTheory.Valuations
open scoped IntermediateField
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]Lean source · full declaration
theorem maximalUnramifiedSubextension_finiteUnramified
(v : LubinTate.Valuations.ExponentialValuation K)
(w : LubinTate.Valuations.ExponentialValuation L)
(hExt : ∀ a : K, w (algebraMap K L a) = v a)
(hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
(LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation) :
let T := maximalUnramifiedSubextension v w hExt
let wT := exponentialValuationRestrict w T
let hKT := exponentialValuationRestrict_extends v w hExt T
FiniteUnramifiedExtension v wT hKT := by
classical
let T := maximalUnramifiedSubextension v w hExt
let wT := exponentialValuationRestrict w T
let hKT := exponentialValuationRestrict_extends v w hExt T
have hfg : (⊤ : IntermediateField K T).FG :=
IntermediateField.fg_top K T
obtain ⟨s, hs⟩ := hfg
have hsupport : ∀ x : T, ∃ E : IntermediateField K L,
(x : L) ∈ E ∧ FiniteUnramifiedSubextension v w hExt E := by
intro x
exact exists_finiteUnramifiedSubextension_of_mem_maximal
v w hExt hhens x.property
choose E hxE hE using hsupport
let U : IntermediateField K L :=
⨆ x : T, ⨆ (_hx : x ∈ s), E x
have hUunramified : FiniteUnramifiedSubextension v w hExt U := by
exact finiteUnramifiedSubextension_finset_iSup
v w hExt hhens s E (fun x _hx ↦ hE x)
have hUleT : U ≤ T := by
dsimp [U]
apply iSup_le
intro x
apply iSup_le
intro _hx
exact finiteUnramifiedSubextension_le_maximal v w hExt (hE x)
have hsU : (↑s : Set T) ⊆ U.comap T.val := by
intro x hx
change (x : L) ∈ U
have hExU : E x ≤ U :=
le_iSup_of_le x (le_iSup_of_le hx le_rfl)
exact hExU (hxE x)
have htopLe : (⊤ : IntermediateField K T) ≤ U.comap T.val := by
rw [← hs]
exact IntermediateField.adjoin_le_iff.mpr hsU
have hTleU : T ≤ U := by
intro x hx
let xT : T := ⟨x, hx⟩
have hxComap : xT ∈ U.comap T.val := htopLe (Set.mem_univ xT)
exact hxComap
have hUT : U = T := le_antisymm hUleT hTleU
rw [hUT] at hUunramified
rcases hUunramified with ⟨hfinT, hTunramified⟩
let : FiniteDimensional K T := hfinT
exact hTunramified