Multiplicative p-adic completion as a maximal pro-p quotient

For a mixed-characteristic nonarchimedean local field L, the inverse limit A(L) = lim_m Lˣ/(Lˣ)^(p^m) is canonically the maximal pro-p quotient of the profinite completion (Lˣ)^ of the abstract group Lˣ. The comparison is characterized by sending the class of a unit to its compatible family of power classes.

Local reciprocity identifies (Lˣ)^ with the abelianized absolute Galois group of L, so this comparison is the bridge from A(L) to the maximal abelian pro-p quotient of that Galois group.

Main declarations

• TauCeti.maximalProPQuotientProfiniteCompletionEquivPadicCompletionUnits: the canonical isomorphism of topological groups from the maximal pro-p quotient of (Lˣ)^ to A(L).

noncomputable def TauCeti.maximalProPQuotientProfiniteCompletionEquivPadicCompletionUnits (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] : maximalProPQuotient p ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧Lˣ).toProfinite.toTop ≃ₜ* ↥(padicCompletionUnits p L)

The maximal pro-p quotient of the profinite completion of Lˣ is canonically the inverse-limit completion A(L) = lim_m Lˣ/(Lˣ)^(p^m).

@[simp]

theorem TauCeti.maximalProPQuotientProfiniteCompletionEquivPadicCompletionUnits_mk (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] (x : Lˣ) : (maximalProPQuotientProfiniteCompletionEquivPadicCompletionUnits p L) ↑(ProfiniteGrp.ProfiniteCompletion.etaFn (↧Lˣ) x) = (padicCompletionUnitsOf p L) x

The canonical comparison sends the class of a unit to its compatible family of power classes.

@[simp]

theorem TauCeti.maximalProPQuotientProfiniteCompletionEquivPadicCompletionUnits_symm_apply (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] (x : Lˣ) : (maximalProPQuotientProfiniteCompletionEquivPadicCompletionUnits p L).symm ((padicCompletionUnitsOf p L) x) = ↑(ProfiniteGrp.ProfiniteCompletion.etaFn (↧Lˣ) x)

The inverse comparison sends the compatible family of power classes of a unit to the class of that unit.