The cokernel of the completed norm

Let L/K be a finite Galois extension of nonarchimedean local fields, let p be a prime with p ≠ 0 in K, and let A(K) = lim_m Kˣ/(Kˣ)^(p^m) be the p-adic completion of Kˣ. The field norm induces the completed norm N : A(L) → A(K) (TauCeti.padicCompletionUnitsNorm). Its cokernel is the maximal p-quotient of Gal(L/K)^ab, read off from the norm residue isomorphism Kˣ / N_{L/K}(Lˣ) ≃ Gal(L/K)^ab (TauCeti.ClassFieldTheory.normResidue).

Concretely, for every m the class of x ∈ A(K) at level m followed by the norm residue symbol modulo p ^ m-th powers is a surjective homomorphism

padicCompletionUnitsNormResidue p K L m : A(K) → Gal(L/K)^ab / (Gal(L/K)^ab)^(p^m),

and once p ^ m contains the full power of p dividing #Gal(L/K)^ab its kernel is exactly the image of N. For such m the target is the maximal p-quotient of Gal(L/K)^ab, of order the full power of p dividing #Gal(L/K)^ab = [Kˣ : N_{L/K}(Lˣ)], so A(K) / N(A(L)) is the p-completion of Kˣ / N_{L/K}(Lˣ).

The proof is algebraic. Every element of A(K) is the class of a unit up to a p ^ m-multiple (TauCeti.exists_eq_padicCompletionUnitsOf_add_pow_smul), and n-th powers of units being norms forces n • A(K) ⊆ N(A(L)) (TauCeti.nsmul_mem_range_padicCompletionUnitsNorm), which for n = #Gal(L/K)^ab absorbs the p ^ m-multiples.

Main definitions

• TauCeti.padicCompletionUnitsNormResidue p K L m: the completed norm residue map A(K) → Gal(L/K)^ab / (Gal(L/K)^ab)^(p^m).
• TauCeti.padicCompletionUnitsNormCokernelEquiv: the resulting isomorphism A(K) / N(A(L)) ≃ Gal(L/K)^ab / (Gal(L/K)^ab)^(p^m).

Main results

• TauCeti.nsmul_mem_range_padicCompletionUnitsNorm: if every n-th power in Kˣ is a norm from L, then n kills the cokernel of the completed norm.
• TauCeti.padicCompletionUnitsNormResidue_of: on the class of a unit, the completed norm residue map is its norm residue symbol.
• TauCeti.padicCompletionUnitsNormResidue_surjective: the completed norm residue map is surjective.
• TauCeti.padicCompletionUnitsNormResidue_padicCompletionUnitsNorm: it kills completed norms.
• TauCeti.ker_padicCompletionUnitsNormResidue: its kernel is the image of the completed norm.
• TauCeti.natCard_quotient_range_padicCompletionUnitsNorm: the cokernel of the completed norm has order the full power of p dividing #Gal(L/K)^ab.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., VII §4, especially the proof of (7.4.4).
• J.-P. Serre, Local Fields, Chapter XI, §3.

theorem TauCeti.nsmul_mem_range_padicCompletionUnitsNorm (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [(powMonoidHom p).range.FiniteIndex] {n : ℕ} (hn : ∀ (u : Kˣ), u ^ n ∈ normGroup K L) (x : Additive ↥(padicCompletionUnits p K)) : n • x ∈ (padicCompletionUnitsNorm p K L).range

A bound on the cokernel of the completed norm. If (Kˣ)^p has finite index in Kˣ and every n-th power in Kˣ is a norm from L, then n • x lies in the image of the completed norm A(L) → A(K) for every x ∈ A(K). For instance n = [L : K] always works (TauCeti.pow_finrank_mem_normGroup).

noncomputable def TauCeti.padicCompletionUnitsNormResidue (p : ℕ) (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (m : ℕ) : Additive ↥(padicCompletionUnits p K) →+ Additive (powerClassQuotient (Abelianization Gal(L/K)) (p ^ m))

The completed norm residue map at level m: the class of an element of A(K) in Kˣ / (Kˣ)^(p^m), followed by the norm residue isomorphism Kˣ / N_{L/K}(Lˣ) ≃ Gal(L/K)^ab modulo p ^ m-th powers.

theorem TauCeti.padicCompletionUnitsNormResidue_eq (p : ℕ) (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {m : ℕ} {x : Additive ↥(padicCompletionUnits p K)} {u : Kˣ} (hu : ↑(Additive.toMul x) m = ↑u) : (padicCompletionUnitsNormResidue p K L m) x = Additive.ofMul ↑((ClassFieldTheory.normResidue K L) ↑u)

The completed norm residue map at level m only depends on the level-m coordinate: if that coordinate is the class of u ∈ Kˣ, the value is the norm residue symbol of u.

@[simp]

theorem TauCeti.padicCompletionUnitsNormResidue_of (p : ℕ) (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (m : ℕ) (u : Kˣ) : (padicCompletionUnitsNormResidue p K L m) (Additive.ofMul ((padicCompletionUnitsOf p K) u)) = Additive.ofMul ↑((ClassFieldTheory.normResidue K L) ↑u)

On the class of a unit u ∈ Kˣ, the completed norm residue map is the norm residue symbol of u, modulo p ^ m-th powers.

theorem TauCeti.padicCompletionUnitsNormResidue_surjective (p : ℕ) (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (m : ℕ) : Function.Surjective ⇑(padicCompletionUnitsNormResidue p K L m)

The completed norm residue map is surjective, since the norm residue isomorphism is.

@[simp]

theorem TauCeti.padicCompletionUnitsNormResidue_pow_smul (p : ℕ) (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [Fact (Nat.Prime p)] (m : ℕ) (y : Additive ↥(padicCompletionUnits p K)) : (padicCompletionUnitsNormResidue p K L m) (↑p ^ m • y) = 0

The completed norm residue map at level m kills p ^ m-multiples, since its target has exponent dividing p ^ m.

@[simp]

theorem TauCeti.padicCompletionUnitsNormResidue_padicCompletionUnitsNorm (p : ℕ) (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [Fact (Nat.Prime p)] (m : ℕ) (y : Additive ↥(padicCompletionUnits p L)) : (padicCompletionUnitsNormResidue p K L m) ((padicCompletionUnitsNorm p K L) y) = 0

The completed norm residue map kills completed norms: the level-m coordinate of a completed norm is the class of a norm, whose norm residue symbol is trivial.

theorem TauCeti.ker_padicCompletionUnitsNormResidue (p : ℕ) (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [Fact (Nat.Prime p)] (hpK : ↑p ≠ 0) {m : ℕ} (hm : (Nat.card (Abelianization Gal(L/K))).factorization p ≤ m) : (padicCompletionUnitsNormResidue p K L m).ker = (padicCompletionUnitsNorm p K L).range.toAddSubgroup

The kernel of the completed norm residue map is the image of the completed norm, once p ^ m contains the full power of p dividing #Gal(L/K)^ab. Together with TauCeti.padicCompletionUnitsNormResidue_surjective, this identifies the cokernel of A(L) → A(K) with the maximal p-quotient of Gal(L/K)^ab.

noncomputable def TauCeti.padicCompletionUnitsNormCokernelEquiv (p : ℕ) (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [Fact (Nat.Prime p)] (hpK : ↑p ≠ 0) {m : ℕ} (hm : (Nat.card (Abelianization Gal(L/K))).factorization p ≤ m) : Additive ↥(padicCompletionUnits p K) ⧸ (padicCompletionUnitsNorm p K L).range.toAddSubgroup ≃+ Additive (powerClassQuotient (Abelianization Gal(L/K)) (p ^ m))

The cokernel of the completed norm A(L) → A(K) is Gal(L/K)^ab / (Gal(L/K)^ab)^(p^m), the maximal p-quotient of Gal(L/K)^ab, once p ^ m contains the full power of p dividing #Gal(L/K)^ab. The isomorphism is induced by the completed norm residue map (TauCeti.padicCompletionUnitsNormCokernelEquiv_mk).

@[simp]

theorem TauCeti.padicCompletionUnitsNormCokernelEquiv_mk (p : ℕ) (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [Fact (Nat.Prime p)] (hpK : ↑p ≠ 0) {m : ℕ} (hm : (Nat.card (Abelianization Gal(L/K))).factorization p ≤ m) (x : Additive ↥(padicCompletionUnits p K)) : (padicCompletionUnitsNormCokernelEquiv p K L hpK hm) ↑x = (padicCompletionUnitsNormResidue p K L m) x

The isomorphism padicCompletionUnitsNormCokernelEquiv sends the class of x ∈ A(K) to its completed norm residue.

theorem TauCeti.natCard_quotient_range_padicCompletionUnitsNorm (p : ℕ) (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [Fact (Nat.Prime p)] (hpK : ↑p ≠ 0) : Nat.card (Additive ↥(padicCompletionUnits p K) ⧸ (padicCompletionUnitsNorm p K L).range.toAddSubgroup) = p ^ (Nat.card (Abelianization Gal(L/K))).factorization p

The order of the cokernel of the completed norm A(L) → A(K) is the full power of p dividing #Gal(L/K)^ab = [Kˣ : N_{L/K}(Lˣ)].