Functoriality of the completed group algebra

A continuous group homomorphism f : Γ →* Δ induces an R-algebra homomorphism completedGroupAlgebra.map R f hf : R[[Γ]] →ₐ[R] R[[Δ]] between the completed group algebras. At the level V of R[[Δ]] it is the map R[Γ ⧸ f⁻¹(V)] → R[Δ ⧸ V] induced by f on the quotients, applied to the level f⁻¹(V) of R[[Γ]] (proj_map); the same description holds at every level U ≤ f⁻¹(V) of R[[Γ]] (proj_map_of_le), which is how the levels of a composite are compared. The map sends group elements to group elements (map_of) and satisfies the two functor laws map_id and map_comp. A topological isomorphism e : Γ ≃ₜ* Δ therefore induces an isomorphism of R-algebras completedGroupAlgebra.domCongr R e : R[[Γ]] ≃ₐ[R] R[[Δ]].

When the open normal quotients of Γ are finite, map is continuous for the inverse-limit topologies (continuous_map). When moreover the coefficient ring is compact Hausdorff and f is surjective, map is surjective (map_surjective); the compactness is what lets the levelwise preimages be assembled into one element. For R = ℤ_[p] and profinite Γ, Δ these hypotheses are all instances, so a continuous surjection of profinite groups induces a surjection of Iwasawa algebras.

Main definitions

• TauCeti.completedGroupAlgebra.map R f hf: the R-algebra homomorphism R[[Γ]] →ₐ[R] R[[Δ]] induced by a continuous homomorphism f : Γ →* Δ.
• TauCeti.completedGroupAlgebra.domCongr R e: the R-algebra isomorphism R[[Γ]] ≃ₐ[R] R[[Δ]] induced by a topological isomorphism e : Γ ≃ₜ* Δ.

Main results

• TauCeti.completedGroupAlgebra.proj_map, TauCeti.completedGroupAlgebra.proj_map_of_le: the levelwise description of map; TauCeti.completedGroupAlgebra.mapDomain_map_proj_of_le is the compatibility between the levels of R[[Γ]] behind it.
• TauCeti.completedGroupAlgebra.proj_map_eq_zero_iff: the level V of map R f hf x vanishes exactly when the level f⁻¹(V) of x does.
• TauCeti.completedGroupAlgebra.map_of: map sends the group element γ to the group element f γ.
• TauCeti.completedGroupAlgebra.map_id, TauCeti.completedGroupAlgebra.map_comp: the functor laws.
• TauCeti.completedGroupAlgebra.continuous_map: map is continuous when the open normal quotients of Γ are finite.
• TauCeti.completedGroupAlgebra.map_surjective: map is surjective when f is, for a compact Hausdorff coefficient ring.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 5.3.
• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), Section 1.5.

theorem TauCeti.completedGroupAlgebra.mapDomain_map_proj_of_le (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] (f : Γ →* Δ) {U U' : OpenNormalSubgroup Γ} (hUU' : U ≤ U') (V : Subgroup Δ) [V.Normal] (h : ↑U'.toOpenSubgroup ≤ Subgroup.comap f V) (x : completedGroupAlgebra R Γ) : MonoidAlgebra.mapDomain (⇑(QuotientGroup.map (↑U'.toOpenSubgroup) V f h)) ((proj R Γ U') x) = MonoidAlgebra.mapDomain (⇑(QuotientGroup.map (↑U.toOpenSubgroup) V f ⋯)) ((proj R Γ U) x)

The image of the projection of x at the level U' of R[[Γ]] under the map R[Γ ⧸ U'] → R[Δ ⧸ V] induced by f can be read from any level U ≤ U': it is the image of the projection of x at U under the map R[Γ ⧸ U] → R[Δ ⧸ V] induced by f. This is the compatibility between the levels of R[[Γ]] that the levelwise description of map rests on.

noncomputable def TauCeti.completedGroupAlgebra.map (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (f : Γ →* Δ) (hf : Continuous ⇑f) : completedGroupAlgebra R Γ →ₐ[R] completedGroupAlgebra R Δ

The R-algebra homomorphism R[[Γ]] →ₐ[R] R[[Δ]] induced by a continuous group homomorphism f : Γ →* Δ: at the level V of R[[Δ]] it applies the map R[Γ ⧸ f⁻¹(V)] → R[Δ ⧸ V] induced by f to the level f⁻¹(V) of R[[Γ]] (proj_map). It sends group elements to group elements (map_of) and satisfies the functor laws map_id and map_comp.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.completedGroupAlgebra.proj_map (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (f : Γ →* Δ) (hf : Continuous ⇑f) (V : OpenNormalSubgroup Δ) (x : completedGroupAlgebra R Γ) : (proj R Δ V) ((map R f hf) x) = MonoidAlgebra.mapDomain (⇑(QuotientGroup.map (↑(V.comap f hf).toOpenSubgroup) (↑V.toOpenSubgroup) f ⋯)) ((proj R Γ (V.comap f hf)) x)

The projection of map R f hf x at the level V of R[[Δ]] is the image of the projection of x at the level f⁻¹(V) of R[[Γ]] under the map induced by f on the quotients.

@[simp]

theorem TauCeti.completedGroupAlgebra.proj_comp_map (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (f : Γ →* Δ) (hf : Continuous ⇑f) (V : OpenNormalSubgroup Δ) : (proj R Δ V).comp (map R f hf) = (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑(V.comap f hf).toOpenSubgroup) (↑V.toOpenSubgroup) f ⋯)).comp (proj R Γ (V.comap f hf))

The composite of map R f hf with the projection at the level V of R[[Δ]] is the projection at the level f⁻¹(V) of R[[Γ]] followed by the map induced by f on the quotients.

theorem TauCeti.completedGroupAlgebra.proj_map_of_le (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (f : Γ →* Δ) (hf : Continuous ⇑f) (U : OpenNormalSubgroup Γ) (V : OpenNormalSubgroup Δ) (h : ↑U.toOpenSubgroup ≤ Subgroup.comap f ↑V.toOpenSubgroup) (x : completedGroupAlgebra R Γ) : (proj R Δ V) ((map R f hf) x) = MonoidAlgebra.mapDomain (⇑(QuotientGroup.map (↑U.toOpenSubgroup) (↑V.toOpenSubgroup) f h)) ((proj R Γ U) x)

The projection of map R f hf x at the level V of R[[Δ]] can be read from any level U of R[[Γ]] that f maps into V: it is the image of the projection of x at U under the map R[Γ ⧸ U] → R[Δ ⧸ V] induced by f.

theorem TauCeti.completedGroupAlgebra.proj_map_eq_zero_iff (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (f : Γ →* Δ) (hf : Continuous ⇑f) (V : OpenNormalSubgroup Δ) (x : completedGroupAlgebra R Γ) : (proj R Δ V) ((map R f hf) x) = 0 ↔ (proj R Γ (V.comap f hf)) x = 0

The projection of map R f hf x at the level V of R[[Δ]] vanishes exactly when the projection of x at the level f⁻¹(V) of R[[Γ]] does: the map R[Γ ⧸ f⁻¹(V)] → R[Δ ⧸ V] induced by f is injective.

@[simp]

theorem TauCeti.completedGroupAlgebra.map_of (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (f : Γ →* Δ) (hf : Continuous ⇑f) (γ : Γ) : (map R f hf) ((of R Γ) γ) = (of R Δ) (f γ)

The induced map sends the group element γ to the group element f γ.

@[simp]

theorem TauCeti.completedGroupAlgebra.map_id (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] : map R (MonoidHom.id Γ) ⋯ = AlgHom.id R (completedGroupAlgebra R Γ)

The map induced by the identity is the identity.

@[simp]

theorem TauCeti.completedGroupAlgebra.map_comp (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (f : Γ →* Δ) (hf : Continuous ⇑f) {E : Type u_1} [Group E] [TopologicalSpace E] (g : Δ →* E) (hg : Continuous ⇑g) : map R (g.comp f) ⋯ = (map R g hg).comp (map R f hf)

The map induced by a composite is the composite of the induced maps.

noncomputable def TauCeti.completedGroupAlgebra.domCongr (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (e : Γ ≃ₜ* Δ) : completedGroupAlgebra R Γ ≃ₐ[R] completedGroupAlgebra R Δ

The R-algebra isomorphism R[[Γ]] ≃ₐ[R] R[[Δ]] induced by a topological isomorphism e : Γ ≃ₜ* Δ; its underlying map is map R e (map_continuous e), and its inverse is induced by e.symm.

Equations

• TauCeti.completedGroupAlgebra.domCongr R e = AlgEquiv.ofAlgHom (TauCeti.completedGroupAlgebra.map R ↑e ⋯) (TauCeti.completedGroupAlgebra.map R ↑e.symm ⋯) ⋯ ⋯

@[simp]

theorem TauCeti.completedGroupAlgebra.coe_domCongr (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (e : Γ ≃ₜ* Δ) : ⇑(domCongr R e) = ⇑(map R ↑e ⋯)

@[simp]

theorem TauCeti.completedGroupAlgebra.domCongr_symm (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (e : Γ ≃ₜ* Δ) : (domCongr R e).symm = domCongr R e.symm

@[simp]

theorem TauCeti.completedGroupAlgebra.domCongr_of (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (e : Γ ≃ₜ* Δ) (γ : Γ) : (domCongr R e) ((of R Γ) γ) = (of R Δ) (e γ)

The isomorphism induced by e sends the group element γ to the group element e γ.

theorem TauCeti.completedGroupAlgebra.continuous_map (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (f : Γ →* Δ) (hf : Continuous ⇑f) [TopologicalSpace R] [ContinuousAdd R] [∀ (U : OpenNormalSubgroup Γ), Finite (Γ ⧸ ↑U.toOpenSubgroup)] : Continuous ⇑(map R f hf)

When the open normal quotients of Γ are finite, the induced map between the completed group algebras is continuous for the inverse-limit topologies.

theorem TauCeti.completedGroupAlgebra.map_surjective (R : Type u) [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {Δ : Type w} [Group Δ] [TopologicalSpace Δ] (f : Γ →* Δ) (hf : Continuous ⇑f) [TopologicalSpace R] [ContinuousAdd R] [∀ (U : OpenNormalSubgroup Γ), Finite (Γ ⧸ ↑U.toOpenSubgroup)] [T2Space R] [CompactSpace R] (hs : Function.Surjective ⇑f) : Function.Surjective ⇑(map R f hf)

When the open normal quotients of Γ are finite and the coefficient ring is compact Hausdorff, the map induced by a continuous surjection f : Γ →* Δ between the completed group algebras is surjective. For R = ℤ_[p] and profinite Γ all the hypotheses on R and Γ are instances.