ClassFieldTheory.finiteAbelianLocalReciprocity_unramified_hom_ext
For an unramified extension, two norm-kernel homomorphisms that agree on one inverse uniformizer agree on all field units.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped ValuativeRel
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace ClassFieldTheoryLean source · statement
theorem finiteAbelianLocalReciprocity_unramified_hom_ext
(K L : Type)
[Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
[Field L] [ValuativeRel L] [TopologicalSpace L]
[IsNonarchimedeanLocalField L]
[Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
[Valuation.HasExtension (ValuativeRel.valuation K)
(ValuativeRel.valuation L)]
(hUnram : (𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K] = 1)
(π : 𝒪[K])
(hπ : (ValuativeRel.valuation K).IsUniformizer (π : K))
(f g : Kˣ →ₜ* (L ≃ₐ[K] L))
(hfker : f.toMonoidHom.ker = fieldNormSubgroup K L)
(hgker : g.toMonoidHom.ker = fieldNormSubgroup K L)
(hϖ : f ((Units.mk0 (π : K) hπ.ne_zero)⁻¹) =
g ((Units.mk0 (π : K) hπ.ne_zero)⁻¹)) :
f = g