ClassFieldTheory.finiteAbelianLocalReciprocity_family_ext
A coherent family of finite local Artin maps is uniquely determined by its norm kernels and its arithmetic-Frobenius normalization. The chosen uniformizer is only used to express that normalization; the conclusion does not depend on it.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped ValuativeRel
noncomputable section
namespace ClassFieldTheoryLean source · statement
theorem finiteAbelianLocalReciprocity_family_ext
(K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
(f g : (E : FiniteAbelianLocalExtension K) →
Kˣ →ₜ* (E.1 ≃ₐ[K] E.1))
(hfker : ∀ E : FiniteAbelianLocalExtension K,
(f E).toMonoidHom.ker = E.normSubgroup)
(hgker : ∀ E : FiniteAbelianLocalExtension K,
(g E).toMonoidHom.ker = E.normSubgroup)
(hfcoh : ∀ (E F : FiniteAbelianLocalExtension K)
(hEF : E.1 ≤ F.1) (x : Kˣ) (y : E.1),
IntermediateField.inclusion hEF ((f E x) y) =
(f F x) (IntermediateField.inclusion hEF y))
(hgcoh : ∀ (E F : FiniteAbelianLocalExtension K)
(hEF : E.1 ≤ F.1) (x : Kˣ) (y : E.1),
IntermediateField.inclusion hEF ((g E x) y) =
(g F x) (IntermediateField.inclusion hEF y))
(hfrob : ∀ (E : FiniteAbelianLocalExtension K)
[ValuativeRel E.1] [UniformSpace E.1] [IsUniformAddGroup E.1]
[IsNonarchimedeanLocalField E.1]
[Valuation.HasExtension (ValuativeRel.valuation K)
(ValuativeRel.valuation E.1)],
(𝓂[E.1] : Ideal 𝒪[E.1]).ramificationIdx 𝒪[K] = 1 →
∀ (π : 𝒪[K])
(hπ : (ValuativeRel.valuation K).IsUniformizer (π : K))
(x : 𝒪[E.1]),
∃ z : 𝒪[E.1],
(z : E.1) =
(f E ((Units.mk0 (π : K) hπ.ne_zero)⁻¹)) (x : E.1) ∧
IsLocalRing.residue 𝒪[E.1] z =
(IsLocalRing.residue 𝒪[E.1] x) ^ Nat.card 𝓀[K])
(hgrob : ∀ (E : FiniteAbelianLocalExtension K)
[ValuativeRel E.1] [UniformSpace E.1] [IsUniformAddGroup E.1]
[IsNonarchimedeanLocalField E.1]
[Valuation.HasExtension (ValuativeRel.valuation K)
(ValuativeRel.valuation E.1)],
(𝓂[E.1] : Ideal 𝒪[E.1]).ramificationIdx 𝒪[K] = 1 →
∀ (π : 𝒪[K])
(hπ : (ValuativeRel.valuation K).IsUniformizer (π : K))
(x : 𝒪[E.1]),
∃ z : 𝒪[E.1],
(z : E.1) =
(g E ((Units.mk0 (π : K) hπ.ne_zero)⁻¹)) (x : E.1) ∧
IsLocalRing.residue 𝒪[E.1] z =
(IsLocalRing.residue 𝒪[E.1] x) ^ Nat.card 𝓀[K])
: f = g