LocalClassFieldTheory.relativeUnramifiedFixedField_eq_sup_standard
The fixed field of the relative degree kernel is the actual compositum with the standard unramified extension of degree residue-degree times m.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomologyLean source · statement
theorem relativeUnramifiedFixedField_eq_sup_standard
(K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
(H : FiniteAbstractField (intrinsicAbsoluteGalois K))
(m : ℕ) (hm : 0 < m) :
abstractFixedField K (SeparableClosure K)
((localResidueDatum K).unramifiedExtensionOfDegree
(H.toFiniteResidueAbstractField (localResidueDatum K)) m hm) =
abstractFixedField K (SeparableClosure K) H.field ⊔
localFiniteUnramifiedField K ((H.residueDegree (localResidueDatum K) : ℕ) * m)
(Nat.mul_pos (H.residueDegree (localResidueDatum K)).property hm)