ClassFieldTheory.finiteAbelianLocalReciprocity_quotientEquiv_of_artin
Any specified continuous surjective homomorphism with the field-norm kernel induces one and only one continuous equivalence of the norm quotient. The equivalence evaluates to the specified map on every quotient class.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe u vLean source · statement
theorem finiteAbelianLocalReciprocity_quotientEquiv_of_artin
(K : Type u) (L : Type v)
[Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsAbelianGalois K L]
[ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
(artin : Kˣ →ₜ* (L ≃ₐ[K] L))
(hsurj : Function.Surjective artin)
(hker : artin.ker = fieldNormSubgroup K L) :
∃! e : FieldNormQuotient K L ≃ₜ* (L ≃ₐ[K] L),
∀ x : Kˣ, e (QuotientGroup.mk' (fieldNormSubgroup K L) x) = artin x