LocalFieldTheory.shrinkIntermediateField_normSubgroup_map
The norm subgroup attached to an intermediate field is carried to the norm subgroup of the same field viewed over Shrink K.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory
universe u
variable (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]Lean source · full declaration
theorem shrinkIntermediateField_normSubgroup_map
(E : ClassFieldTheory.FiniteAbelianLocalExtension K) :
letI : Small.{0} K := nonarchimedeanLocalField_small K
letI : Algebra (Shrink.{0} K) (SeparableClosure K) :=
shrinkSeparableClosureAlgebra K
letI : FiniteDimensional (Shrink.{0} K) (shrinkIntermediateField K E.1) :=
shrinkIntermediateField_finiteDimensional K E
(E.normSubgroup).map
(Units.mapEquiv (Shrink.ringEquiv K).symm.toMulEquiv).toMonoidHom =
ClassFieldTheory.fieldNormSubgroup (Shrink.{0} K)
(shrinkIntermediateField K E.1) := by
let : Small.{0} K := nonarchimedeanLocalField_small K
let : Algebra (Shrink.{0} K) (SeparableClosure K) :=
shrinkSeparableClosureAlgebra K
let : FiniteDimensional (Shrink.{0} K) (shrinkIntermediateField K E.1) :=
shrinkIntermediateField_finiteDimensional K E
change (ClassFieldTheory.fieldNormSubgroup K E.1).map
(Units.mapEquiv (Shrink.ringEquiv K).symm.toMulEquiv).toMonoidHom =
ClassFieldTheory.fieldNormSubgroup (Shrink.{0} K)
(shrinkIntermediateField K E.1)
exact ClassFieldTheory.fieldNormSubgroup_map_ringEquiv
(Shrink.ringEquiv K).symm
(shrinkIntermediateFieldRingEquiv K E.1)
(shrinkIntermediateFieldRingEquiv_commutes K E.1)