ClassFieldTheory.finiteAbelianLocalReciprocity_unramified_family_ext
The norm-kernel and arithmetic Frobenius conditions determine the value of two local reciprocity families at an unramified member.
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_unramified_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)
(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])
(E : FiniteAbelianLocalExtension K)
[ValuativeRel E.1] [UniformSpace E.1] [IsUniformAddGroup E.1]
[IsNonarchimedeanLocalField E.1]
[Valuation.HasExtension (ValuativeRel.valuation K)
(ValuativeRel.valuation E.1)]
(hUnram : (𝓂[E.1] : Ideal 𝒪[E.1]).ramificationIdx 𝒪[K] = 1)
(π : 𝒪[K])
(hπ : (ValuativeRel.valuation K).IsUniformizer (π : K)) :
f E = g E