ClassFieldTheory.finiteAbelianLocalReciprocity_quotientEquiv_mk
The continuous norm-quotient equivalence is uniquely determined by the canonical finite local Artin map, with the expected value on every class.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheoryLean source · statement
theorem finiteAbelianLocalReciprocity_quotientEquiv_mk
(K L : Type)
[Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsAbelianGalois K L]
[ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K] :
∃ artin : Kˣ →ₜ* (L ≃ₐ[K] L),
Function.Surjective artin ∧
artin.ker = fieldNormSubgroup K L ∧
∃! e : FieldNormQuotient K L ≃ₜ* (L ≃ₐ[K] L),
∀ x : Kˣ, e (QuotientGroup.mk' (fieldNormSubgroup K L) x) = artin x