The p-adic completion of a multiplicative group

For a prime p and a commutative monoid L, this file constructs the inverse limit

A(L) = lim_m Lˣ / (Lˣ)^(p^m).

The carrier is the subgroup of the product of the power-class groups consisting of compatible families. Its ℤ_p-module structure is intrinsic: at level m, a p-adic integer acts through its residue modulo p^m. For a commutative semiring algebra, algebra automorphisms preserve power subgroups and therefore act on the whole inverse limit.

For a finite extension L of ℚ_p, this completed multiplicative module is the one used in local reciprocity and in the Galois-module theory of local units, where it is finitely generated over ℤ_p. This file imposes no such hypothesis and proves no finiteness statement: it supplies only the carrier, its ℤ_p-module structure, and its Galois action. Finite generation is proved in TauCeti.NumberTheory.Padics.MultiplicativeCompletion.Finite.

Main declarations

• padicCompletionUnits: the inverse-limit carrier A(L).
• padicCompletionUnitsPadicModule: its intrinsic ℤ_p-module structure.
• padicCompletionUnitsAut: the coordinatewise Galois action.
• padicCompletionUnitsRepresentation: the ℤ_p-linear Galois representation on A(L).
• padicCompletionUnitsCongr: the isomorphism A(L) ≃* A(L') induced by L ≃* L'.
• padicCompletionUnitsModule: the integral ℤ_p[Gal(L/K)]-module structure on A(L), namely Mathlib's Representation.asModule structure of padicCompletionUnitsRepresentation.
• MonoidAlgebra.smul_padicCompletionUnitsOf: a group-algebra element acts on the class of a unit through the classes of its conjugates.
• MonoidAlgebra.smul_padicCompletionUnitsOf_of_forall_eq: on the class of a unit fixed by every automorphism, the group algebra acts through the augmentation.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, §VII.4.

def TauCeti.padicCompletionTransition (p : ℕ) (L : Type u_1) [CommMonoid L] (m : ℕ) : Lˣ ⧸ (powMonoidHom (p ^ (m + 1))).range →* Lˣ ⧸ (powMonoidHom (p ^ m)).range

The transition map from p^(m+1)-power classes to p^m-power classes.

@[simp]

theorem TauCeti.padicCompletionTransition_mk (p : ℕ) (L : Type u_1) [CommMonoid L] (m : ℕ) (x : Lˣ) : (padicCompletionTransition p L m) ↑x = ↑x

The transition map sends the class of a unit to its class at the previous level.

def TauCeti.padicCompletionUnits (p : ℕ) (L : Type u_1) [CommMonoid L] : Subgroup ((m : ℕ) → Lˣ ⧸ (powMonoidHom (p ^ m)).range)

A(L) = lim_m Lˣ/(Lˣ)^(p^m), realized as the subgroup of compatible families in the product of the power-class groups.

@[instance_reducible]

instance TauCeti.instCommGroupSubtypeForallQuotientUnitsSubgroupRangePowMonoidHomHPowNatMemPadicCompletionUnits (p : ℕ) (L : Type u_1) [CommMonoid L] : CommGroup ↥(padicCompletionUnits p L)

A(L) is a commutative group, with the pointwise group structure of compatible families of power classes inherited from the product ∏ₘ Lˣ/(Lˣ)^(p^m).

@[simp]

theorem TauCeti.mem_padicCompletionUnits_iff (p : ℕ) (L : Type u_1) [CommMonoid L] (x : (m : ℕ) → Lˣ ⧸ (powMonoidHom (p ^ m)).range) : x ∈ padicCompletionUnits p L ↔ ∀ (m : ℕ), (padicCompletionTransition p L m) (x (m + 1)) = x m

A compatible family is characterized by the transition equation at every level.

def TauCeti.padicCompletionUnitsOf (p : ℕ) (L : Type u_1) [CommMonoid L] : Lˣ →* ↥(padicCompletionUnits p L)

The canonical homomorphism from Lˣ to its p-adic completion.

@[simp]

theorem TauCeti.padicCompletionUnitsOf_apply (p : ℕ) (L : Type u_1) [CommMonoid L] (x : Lˣ) (m : ℕ) : ↑((padicCompletionUnitsOf p L) x) m = (QuotientGroup.mk' (powMonoidHom (p ^ m)).range) x

The m-th coordinate of the canonical map is the power-class quotient map.

def TauCeti.padicCompletionUnitsLift (p : ℕ) (L : Type u_1) [CommMonoid L] (K : Type u_2) [CommMonoid K] (f : (m : ℕ) → Lˣ ⧸ (powMonoidHom (p ^ m)).range →* Kˣ ⧸ (powMonoidHom (p ^ m)).range) (hf : ∀ (m : ℕ) (x : Lˣ ⧸ (powMonoidHom (p ^ (m + 1))).range), (padicCompletionTransition p K m) ((f (m + 1)) x) = (f m) ((padicCompletionTransition p L m) x)) : ↥(padicCompletionUnits p L) →* ↥(padicCompletionUnits p K)

Compatible homomorphisms on the power-class coordinates induce a homomorphism between the completed multiplicative groups.

@[simp]

theorem TauCeti.padicCompletionUnitsLift_apply (p : ℕ) (L : Type u_1) [CommMonoid L] (K : Type u_2) [CommMonoid K] (f : (m : ℕ) → Lˣ ⧸ (powMonoidHom (p ^ m)).range →* Kˣ ⧸ (powMonoidHom (p ^ m)).range) (hf : ∀ (m : ℕ) (x : Lˣ ⧸ (powMonoidHom (p ^ (m + 1))).range), (padicCompletionTransition p K m) ((f (m + 1)) x) = (f m) ((padicCompletionTransition p L m) x)) (x : ↥(padicCompletionUnits p L)) (m : ℕ) : ↑((padicCompletionUnitsLift p L K f hf) x) m = (f m) (↑x m)

The induced homomorphism is computed by the given homomorphism at every coordinate.

@[instance_reducible]

noncomputable instance TauCeti.padicCompletionUnitsSMul (p : ℕ) (L : Type u_1) [CommMonoid L] [Fact (Nat.Prime p)] : SMul ℤ_[p] (Additive ↥(padicCompletionUnits p L))

A p-adic integer acts on A(L) by truncated exponentiation: at level m it acts through its residue modulo p^m.

@[simp]

theorem TauCeti.padicCompletionUnits_smul_apply (p : ℕ) (L : Type u_1) [CommMonoid L] [Fact (Nat.Prime p)] (a : ℤ_[p]) (x : Additive ↥(padicCompletionUnits p L)) (m : ℕ) : ↑(Additive.toMul (a • x)) m = ↑(Additive.toMul x) m ^ a.appr m

Scalar multiplication in the completion is truncated exponentiation in every coordinate.

@[instance_reducible]

noncomputable instance TauCeti.padicCompletionUnitsPadicModule (p : ℕ) (L : Type u_1) [CommMonoid L] [Fact (Nat.Prime p)] : Module ℤ_[p] (Additive ↥(padicCompletionUnits p L))

The intrinsic ℤ_p-module structure on the completed multiplicative group.

@[simp]

theorem TauCeti.padicCompletionUnits_natCast_smul (p : ℕ) (L : Type u_1) [CommMonoid L] [Fact (Nat.Prime p)] (n : ℕ) (x : Additive ↥(padicCompletionUnits p L)) : ↑n • x = n • x

The ℤ_p-action extends the intrinsic natural-number action on the completion.

theorem TauCeti.padicCompletionUnits_add_pow_smul_apply (p : ℕ) (L : Type u_1) [CommMonoid L] [Fact (Nat.Prime p)] (m : ℕ) (y z : Additive ↥(padicCompletionUnits p L)) : ↑(Additive.toMul (y + ↑p ^ m • z)) m = ↑(Additive.toMul y) m

Adding a p ^ m-multiple in A(L) does not change the level-m coordinate.

def TauCeti.padicCompletionPowerClassMap (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] (σ : L ≃ₐ[K] L) (m : ℕ) : Lˣ ⧸ (powMonoidHom (p ^ m)).range ≃* Lˣ ⧸ (powMonoidHom (p ^ m)).range

The automorphism of a power-class group induced by an algebra automorphism.

@[simp]

theorem TauCeti.padicCompletionPowerClassMap_mk (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] (σ : L ≃ₐ[K] L) (m : ℕ) (x : Lˣ) : (padicCompletionPowerClassMap p L K σ m) ↑x = ↑((Units.map σ.toRingEquiv.toMonoidHom) x)

An automorphism acts on a power class through its action on a representative.

def TauCeti.padicCompletionUnitsAut (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] : (L ≃ₐ[K] L) →* MulAut ↥(padicCompletionUnits p L)

The Galois action on the completed multiplicative group.

@[simp]

theorem TauCeti.padicCompletionUnitsAut_apply (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] (σ : L ≃ₐ[K] L) (x : ↥(padicCompletionUnits p L)) (m : ℕ) : ↑(((padicCompletionUnitsAut p L K) σ) x) m = (padicCompletionPowerClassMap p L K σ m) (↑x m)

The Galois action on A(L) is induced coordinatewise from the action on Lˣ.

@[simp]

theorem TauCeti.padicCompletionUnitsAut_of (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] (σ : L ≃ₐ[K] L) (x : Lˣ) : ((padicCompletionUnitsAut p L K) σ) ((padicCompletionUnitsOf p L) x) = (padicCompletionUnitsOf p L) ((Units.map σ.toRingEquiv.toMonoidHom) x)

The Galois action sends the canonical class of a unit to the class of its conjugate.

def TauCeti.padicCompletionUnitsLinearMap (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] [Fact (Nat.Prime p)] (σ : L ≃ₐ[K] L) : Additive ↥(padicCompletionUnits p L) →ₗ[ℤ_[p]] Additive ↥(padicCompletionUnits p L)

The Galois action regarded as a ℤ_p-linear endomorphism.

@[simp]

theorem TauCeti.padicCompletionUnitsLinearMap_apply (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] [Fact (Nat.Prime p)] (σ : L ≃ₐ[K] L) (x : Additive ↥(padicCompletionUnits p L)) : (padicCompletionUnitsLinearMap p L K σ) x = Additive.ofMul (((padicCompletionUnitsAut p L K) σ) (Additive.toMul x))

The ℤ_p-linear Galois action is the multiplicative Galois action.

def TauCeti.padicCompletionUnitsRepresentation (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] [Fact (Nat.Prime p)] : Representation ℤ_[p] (L ≃ₐ[K] L) (Additive ↥(padicCompletionUnits p L))

The linear representation underlying the integral Galois module A(L).

@[simp]

theorem TauCeti.padicCompletionUnitsRepresentation_apply (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] [Fact (Nat.Prime p)] (σ : L ≃ₐ[K] L) : (padicCompletionUnitsRepresentation p L K) σ = padicCompletionUnitsLinearMap p L K σ

The representation acts on A(L) through the ℤ_p-linear Galois action.

@[instance_reducible]

noncomputable instance TauCeti.padicCompletionUnitsModule (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] [Fact (Nat.Prime p)] : Module (MonoidAlgebra ℤ_[p] (L ≃ₐ[K] L)) (Additive ↥(padicCompletionUnits p L))

The integral ℤ_p[Gal(L/K)]-module structure on A(L): the Representation.asModule structure of the Galois representation, placed on A(L) itself.

@[simp]

theorem TauCeti.padicCompletionUnits_single_smul (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] [Fact (Nat.Prime p)] (σ : L ≃ₐ[K] L) (a : ℤ_[p]) (x : ↥(padicCompletionUnits p L)) : MonoidAlgebra.single σ a • Additive.ofMul x = a • Additive.ofMul (((padicCompletionUnitsAut p L K) σ) x)

A group-algebra monomial acts through the corresponding algebra automorphism, scaled by its coefficient.

instance TauCeti.padicCompletionUnits_isScalarTower (p : ℕ) (L : Type u_1) [CommSemiring L] (K : Type u_2) [CommSemiring K] [Algebra K L] [Fact (Nat.Prime p)] : IsScalarTower ℤ_[p] (MonoidAlgebra ℤ_[p] (L ≃ₐ[K] L)) (Additive ↥(padicCompletionUnits p L))

Restriction of the group-algebra action recovers the intrinsic ℤ_p-action on A(L).

theorem MonoidAlgebra.smul_padicCompletionUnitsOf (p : ℕ) {L : Type u_1} [CommSemiring L] {K : Type u_2} [CommSemiring K] [Algebra K L] [Fact (Nat.Prime p)] [Fintype (L ≃ₐ[K] L)] (x : MonoidAlgebra ℤ_[p] (L ≃ₐ[K] L)) (u : Lˣ) : x • Additive.ofMul ((TauCeti.padicCompletionUnitsOf p L) u) = ∑ σ : L ≃ₐ[K] L, x.coeff σ • Additive.ofMul ((TauCeti.padicCompletionUnitsOf p L) ((Units.map σ.toRingEquiv.toMonoidHom) u))

For a finite automorphism group, an element x = ∑ σ, x_σ σ of the group algebra acts on the class of a unit u as the combination ∑ σ, x_σ [σ u] of the classes of its conjugates.

theorem MonoidAlgebra.smul_padicCompletionUnitsOf_of_forall_eq (p : ℕ) {L : Type u_1} [CommSemiring L] {K : Type u_2} [CommSemiring K] [Algebra K L] [Fact (Nat.Prime p)] (x : MonoidAlgebra ℤ_[p] (L ≃ₐ[K] L)) {u : Lˣ} (hu : ∀ (σ : L ≃ₐ[K] L), (Units.map σ.toRingEquiv.toMonoidHom) u = u) : x • Additive.ofMul ((TauCeti.padicCompletionUnitsOf p L) u) = (TauCeti.MonoidAlgebra.augmentation ℤ_[p] (L ≃ₐ[K] L)) x • Additive.ofMul ((TauCeti.padicCompletionUnitsOf p L) u)

The group algebra acts on the class of a unit fixed by every automorphism through the augmentation.

Transport along a multiplicative equivalence

def TauCeti.padicCompletionUnitsCongr (p : ℕ) {L : Type u_1} [CommMonoid L] {L' : Type u_2} [CommMonoid L'] (e : L ≃* L') : ↥(padicCompletionUnits p L) ≃* ↥(padicCompletionUnits p L')

A multiplicative equivalence L ≃* L' induces A(L) ≃* A(L'), coordinatewise on the power-class groups.

@[simp]

theorem TauCeti.padicCompletionUnitsCongr_apply (p : ℕ) {L : Type u_1} [CommMonoid L] {L' : Type u_2} [CommMonoid L'] (e : L ≃* L') (x : ↥(padicCompletionUnits p L)) (m : ℕ) : ↑((padicCompletionUnitsCongr p e) x) m = (QuotientGroup.congrRangePowMonoidHom (Units.mapEquiv e) (p ^ m)) (↑x m)

padicCompletionUnitsCongr is computed coordinatewise.

theorem TauCeti.padicCompletionUnitsCongr_smul (p : ℕ) {L : Type u_1} [CommMonoid L] {L' : Type u_2} [CommMonoid L'] [Fact (Nat.Prime p)] (e : L ≃* L') (a : ℤ_[p]) (x : Additive ↥(padicCompletionUnits p L)) : Additive.ofMul ((padicCompletionUnitsCongr p e) (Additive.toMul (a • x))) = a • Additive.ofMul ((padicCompletionUnitsCongr p e) (Additive.toMul x))

padicCompletionUnitsCongr is ℤ_p-linear.

theorem TauCeti.padicCompletionUnitsCongr_aut (p : ℕ) {L : Type u_1} [CommSemiring L] {L' : Type u_2} [CommSemiring L'] (K : Type u_3) [CommSemiring K] [Algebra K L] {K' : Type u_4} [CommSemiring K'] [Algebra K' L'] (e : L ≃* L') (σ : L ≃ₐ[K] L) (σ' : L' ≃ₐ[K'] L') (hσ : ∀ (y : L), σ' (e y) = e (σ y)) (x : ↥(padicCompletionUnits p L)) : (padicCompletionUnitsCongr p e) (((padicCompletionUnitsAut p L K) σ) x) = ((padicCompletionUnitsAut p L' K') σ') ((padicCompletionUnitsCongr p e) x)

padicCompletionUnitsCongr intertwines the actions of automorphisms σ of L and σ' of L' that correspond under the isomorphism.