Local reciprocity for the multiplicative p-adic completion

Let L/K be a finite extension, L a nonarchimedean local field of characteristic zero, and let V ≤ G_K be the open subgroup fixing the copy ι(L) of L in a separable closure of K. Local reciprocity identifies the multiplicative p-adic completion A(L) = lim_m Lˣ/(Lˣ)^(p^m) with V^ab(p), the maximal pro-p quotient of the topological abelianization of V ≃ G_L. The construction identifies A(L) with the maximal pro-p quotient of the profinite completion of Lˣ, applies the profinite-completion form of local reciprocity ClassFieldTheory.profiniteCompletionArtinEquiv, and transports the result along G_L ≃ V.

When L/K is normal, G_K ⧸ V ≃ Gal(L/K) acts on both sides, and the identification is equivariant. This is what lets statements about the class module V^ab(p) of the pair V ◁ G_K be read as statements about the Gal(L/K)-module A(L). Equivariance reduces, by density of Lˣ in A(L), to the naturality of the Artin map under the field automorphisms of L (ClassFieldTheory.artinMap_congr).

Second cohomology with this conjugation action is identified with second cohomology of the completed-units representation by explicitH2EquivPadicCompletionUnits; its cocycle formula retains the reciprocity coordinates when comparing coefficient maps.

Main declarations

• TauCeti.padicCompletionUnitsEquivAbsoluteGaloisGroupAbelianizationProP: the isomorphism A(L) ≃ₜ* G_L^ab(p), for Mathlib's absolute Galois group of L.
• TauCeti.padicCompletionUnitsEquivAbelianizationProP: the isomorphism A(L) ≃ₜ* V^ab(p).
• TauCeti.padicCompletionUnitsEquivAbelianizationProP_smul: for normal L/K, it is equivariant for Gal(L/K) ≃ G_K ⧸ V.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.4.1).

Conjugating by an element of G_K

The reciprocity isomorphism

noncomputable def TauCeti.padicCompletionUnitsEquivAbsoluteGaloisGroupAbelianizationProP (p : ℕ) [Fact (Nat.Prime p)] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] : ↥(padicCompletionUnits p L) ≃ₜ* maximalProPQuotient p (Field.absoluteGaloisGroupAbelianization L)

Local reciprocity for A(L), absolute form. The multiplicative p-adic completion A(L) is the maximal pro-p quotient of the abelianized absolute Galois group G_L^ab of L: it is the maximal pro-p quotient of the profinite completion of Lˣ, which local reciprocity identifies with G_L^ab (ClassFieldTheory.profiniteCompletionArtinEquiv).

@[simp]

theorem TauCeti.padicCompletionUnitsEquivAbsoluteGaloisGroupAbelianizationProP_of (p : ℕ) [Fact (Nat.Prime p)] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] (x : Lˣ) : (padicCompletionUnitsEquivAbsoluteGaloisGroupAbelianizationProP p L) ((padicCompletionUnitsOf p L) x) = ↑((ClassFieldTheory.artinMap L) x)

The absolute form of local reciprocity for A(L) sends the class of a unit to the class of its absolute Artin symbol.

noncomputable def TauCeti.padicCompletionUnitsEquivAbelianizationProP (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] (ι : L →ₐ[K] SeparableClosure K) : ↥(padicCompletionUnits p L) ≃ₜ* abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L ι)

Local reciprocity for A(L). If V ≤ G_K is the subgroup fixing the image of a finite extension L/K under ι : L →ₐ[K] Kˢ, then the multiplicative p-adic completion A(L) of Lˣ is canonically isomorphic to V^ab(p), the maximal pro-p quotient of the topological abelianization of V.

theorem TauCeti.padicCompletionUnitsEquivAbelianizationProP_of (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] (ι : L →ₐ[K] SeparableClosure K) (x : Lˣ) (σ : Field.absoluteGaloisGroup L) (hσ : ↑σ = (ClassFieldTheory.artinMap L) x) : (padicCompletionUnitsEquivAbelianizationProP p K L ι) ((padicCompletionUnitsOf p L) x) = (abelianizationProPMk p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L ι)) ((galoisSubgroupEquiv K L ι) ((absoluteGaloisGroupRestrictEquiv L) σ))

On the dense image of Lˣ, local reciprocity for A(L) sends the class of a unit x to the class of σ_V, where σ ∈ G_L represents the absolute Artin symbol of x and σ_V ∈ V is its image under G_L ≃ V.

Equivariance

theorem TauCeti.padicCompletionUnitsEquivAbelianizationProP_smul (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Normal K L] (ι : L →ₐ[K] SeparableClosure K) (g : AbsoluteGaloisGroup K) (z : ↥(padicCompletionUnits p L)) [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] : (padicCompletionUnitsEquivAbelianizationProP p K L ι) (((padicCompletionUnitsAut p L K) (ι.restrictNormalHom g)) z) = ↑g • (padicCompletionUnitsEquivAbelianizationProP p K L ι) z

Equivariance of local reciprocity for A(L). Let L/K be a finite normal extension of p-adic fields and V ≤ G_K the subgroup fixing ι(L). For g ∈ G_K, the action of its restriction ι.restrictNormalHom g ∈ Gal(L/K) on A(L) corresponds to the conjugation action of the class of g in G_K ⧸ V on V^ab(p). As quotientFixingSubgroupFieldRangeEquiv K L ι sends the class of g to ι.restrictNormalHom g, this is equivariance for Gal(L/K) ≃ G_K ⧸ V.

theorem TauCeti.padicCompletionUnitsEquivAbelianizationProP_galois_smul (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Normal K L] (j : L →ₐ[K] SeparableClosure K) (t : Gal(L/K)) (z : ↥(padicCompletionUnits p L)) [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] : have this := galoisClassModuleAction p K L j; (padicCompletionUnitsEquivAbelianizationProP p K L j) (((padicCompletionUnitsAut p L K) t) z) = t • (padicCompletionUnitsEquivAbelianizationProP p K L j) z

Reciprocity intertwines the finite Galois group's action on the completed units with its transported conjugation action on the arithmetic pro-p class module.

theorem TauCeti.padicCompletionUnitsEquivAbelianizationProP_symm_galois_smul (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Normal K L] (j : L →ₐ[K] SeparableClosure K) (t : Gal(L/K)) (x : abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j)) [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] : have this := galoisClassModuleAction p K L j; (padicCompletionUnitsEquivAbelianizationProP p K L j).symm (t • x) = ((padicCompletionUnitsAut p L K) t) ((padicCompletionUnitsEquivAbelianizationProP p K L j).symm x)

Inverse reciprocity carries the arithmetic class-module action to the action on units.

theorem TauCeti.ofMul_padicCompletionUnitsEquivAbelianizationProP_symm_galois_smul (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Normal K L] (j : L →ₐ[K] SeparableClosure K) (t : Gal(L/K)) (x : Additive (abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j))) [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] : Additive.ofMul ((padicCompletionUnitsEquivAbelianizationProP p K L j).symm (t • Additive.toMul x)) = MonoidAlgebra.single t 1 • Additive.ofMul ((padicCompletionUnitsEquivAbelianizationProP p K L j).symm (Additive.toMul x))

Inverse reciprocity intertwines the Galois action on the pro-p class module with the group-algebra action on the completed units, after reading the latter additively.

noncomputable def TauCeti.explicitH2EquivPadicCompletionUnits (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Normal K L] (j : L →ₐ[K] SeparableClosure K) [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] : ContCohomology.H2 Gal(L/K) (Additive (abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j))) ≃+ ↑(groupCohomology (Rep.ofModuleMonoidAlgebra.obj ↧(Additive ↥(padicCompletionUnits p L))) 2)

Explicit second cohomology of the arithmetic pro-p class module, with the finite Galois group's conjugation action, is second cohomology of the completed-units representation. The comparison reads coefficient values through the inverse of local reciprocity.

theorem TauCeti.explicitH2EquivPadicCompletionUnits_eq_explicitH2AddEquivGroupCohomology (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] (j : L →ₐ[K] SeparableClosure K) : let C := Rep.ofModuleMonoidAlgebra.obj ↧(Additive ↥(padicCompletionUnits p L)); ∀ (χ : Additive (abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j)) ≃+ ↑C) (hχ : ∀ (t : Gal(L/K)) (x : Additive (abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j))), χ (t • x) = (C.ρ t) (χ x)), χ = (MulEquiv.toAdditive (padicCompletionUnitsEquivAbelianizationProP p K L j).symm.toMulEquiv).trans (RestrictScalars.addEquiv ℤ_[p] (MonoidAlgebra ℤ_[p] Gal(L/K)) (Additive ↥(padicCompletionUnits p L))).symm → explicitH2EquivPadicCompletionUnits p K L j = ContCohomology.explicitH2AddEquivGroupCohomology (MulEquiv.refl Gal(L/K)) χ hχ

The arithmetic comparison is the generic comparison in any equal inverse-reciprocity coordinates. This characterization keeps its construction opaque to consumers.

theorem TauCeti.explicitH2EquivPadicCompletionUnits_mk (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Normal K L] (j : L →ₐ[K] SeparableClosure K) [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] (z : ↥(ContCohomology.Z2 Gal(L/K) (Additive (abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j))))) (c : ↥(groupCohomology.cocycles₂ (Rep.ofModuleMonoidAlgebra.obj ↧(Additive ↥(padicCompletionUnits p L))))) : (∀ (t : Gal(L/K) × Gal(L/K)), c t = Additive.ofMul ((padicCompletionUnitsEquivAbelianizationProP p K L j).symm (Additive.toMul (↑z t)))) → (explicitH2EquivPadicCompletionUnits p K L j) ↑z = (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.ofModuleMonoidAlgebra.obj ↧(Additive ↥(padicCompletionUnits p L))))) c

The arithmetic second-cohomology comparison sends a cocycle class to the cocycle obtained by reading its values through inverse local reciprocity.