LocalClassFieldTheory.map_intrinsicExtensionInertia_eq_ambientFixedField
The separable-closure equivalence identifies the intrinsic extension inertia subgroup of a fixed field with its ambient extension inertia subgroup.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRelLean source · full declaration
theorem map_intrinsicExtensionInertia_eq_ambientFixedField
(K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
(H : FiniteAbstractField
Gal(SeparableClosure K/K))
(J : ClosedSubgroup Gal(SeparableClosure K/K))
(hJH : J.toSubgroup ≤ H.field.toSubgroup)
[hJnormal : (extensionSubgroup H.field J hJH).Normal]
[hJfinite : Finite
(H.field.toSubgroup ⧸ extensionSubgroup H.field J hJH)] :
let F := abstractFixedField K (SeparableClosure K) H.field
letI : Algebra F (SeparableClosure F) :=
(separableClosure F (AlgebraicClosure F)).algebra
∀ (e : SeparableClosure F ≃ₐ[F] SeparableClosure K),
let E := abstractRelativeFixedField K (SeparableClosure K) hJH
letI : FiniteDimensional K F :=
abstractFixedField_finiteDimensional
K (SeparableClosure K) H.field H.finite
letI : NontriviallyNormedField F :=
finiteExtensionSpectralNormedField K F
letI : ValuativeRel F :=
finiteExtensionSpectralValuativeRel K F
letI : IsNonarchimedeanLocalField F :=
finiteExtensionSpectralIsNonarchimedeanLocalField K F
letI : FiniteDimensional F E :=
abstractRelativeFixedField_finiteDimensional
K (SeparableClosure K) H.field J hJH H.finite hJfinite
letI : IsGalois F E :=
abstractRelativeFixedField_isGalois
K (SeparableClosure K) H.field J hJH hJnormal
let i : E →ₐ[F] SeparableClosure F :=
e.symm.toAlgHom.comp E.val
let EI := finiteGaloisAbstractExtensionOfEmbedding F E i
let ψ := intrinsicBaseEquivAmbientFixedField K H e
((localResidueDatum F).extensionInertiaWithin
(intrinsicAbstractBase F) EI.field EI.below).map
ψ.toMonoidHom =
(localResidueDatum K).extensionInertiaWithin
H.field J hJH := by
dsimp only
let F := abstractFixedField K (SeparableClosure K) H.field
let : Algebra F (SeparableClosure F) :=
(separableClosure F (AlgebraicClosure F)).algebra
intro e
let E := abstractRelativeFixedField K (SeparableClosure K) hJH
let : FiniteDimensional K F :=
abstractFixedField_finiteDimensional
K (SeparableClosure K) H.field H.finite
let : NontriviallyNormedField F :=
finiteExtensionSpectralNormedField K F
let : ValuativeRel F :=
finiteExtensionSpectralValuativeRel K F
let : IsNonarchimedeanLocalField F :=
finiteExtensionSpectralIsNonarchimedeanLocalField K F
let : FiniteDimensional F E :=
abstractRelativeFixedField_finiteDimensional
K (SeparableClosure K) H.field J hJH H.finite hJfinite
let : IsGalois F E :=
abstractRelativeFixedField_isGalois
K (SeparableClosure K) H.field J hJH hJnormal
let i : E →ₐ[F] SeparableClosure F :=
e.symm.toAlgHom.comp E.val
let EI := finiteGaloisAbstractExtensionOfEmbedding F E i
let ψ := intrinsicBaseEquivAmbientFixedField K H e
ext σ
constructor
· rintro ⟨τ, hτ, rfl⟩
exact
(intrinsicExtensionInertia_iff_ambientFixedField
K H J hJH e τ).1 hτ
· intro hσ
let τ :
(intrinsicAbstractBase F).toSubgroup :=
ψ.symm σ
refine ⟨τ, ?_, ψ.apply_symm_apply σ⟩
apply
(intrinsicExtensionInertia_iff_ambientFixedField
K H J hJH e τ).2
change
ψ τ ∈
(localResidueDatum K).extensionInertiaWithin
H.field J hJH
have hτImage : ψ τ = σ :=
ψ.apply_symm_apply σ
rw [hτImage]
exact hσ