The completed group algebra of a profinite group

For a topological group Γ and a commutative ring R, the completed group algebra R[[Γ]] is the inverse limit of the group algebras R[Γ ⧸ U] over the open normal subgroups U of Γ: an element is a family of elements of the group algebras R[Γ ⧸ U], compatible along the ring homomorphisms R[Γ ⧸ U] → R[Γ ⧸ V] induced by the quotient maps Γ ⧸ U → Γ ⧸ V for U ≤ V. The index set is the open normal subgroups, because Γ ⧸ U has to be a group for R[Γ ⧸ U] to be a group algebra. For R = ℤ_[p] and Γ a profinite group this is the Iwasawa algebra ℤ_p[[Γ]], the ring over which the relation modules in Labute's classification of Demushkin groups are studied.

It is an R-algebra; each group element γ gives an element of R Γ γ, the family of its classes, and each open normal subgroup U gives the projection proj R Γ U onto R[Γ ⧸ U], which is surjective. Two elements with the same projections are equal, and these two facts are the inverse-limit description of the algebra. Its universal property is lift: a compatible family of R-algebra homomorphisms into the levels R[Γ ⧸ U] assembles into an R-algebra homomorphism into R[[Γ]], unique with the prescribed projections (algHom_ext).

When R is a topological ring, the completed group algebra carries the inverse-limit topology: the coarsest topology making every coefficient of every projection continuous. Scalar multiplication by R is continuous when multiplication in R is. When every open normal quotient Γ ⧸ U is finite, as it is for a compact Γ with separately continuous multiplication, the completed algebra is a topological ring, and it is compact when R is compact Hausdorff. It is totally disconnected when R is, and the map from Γ is continuous. It is commutative when Γ is, stated as the IsMulCommutative mixin and as a CommRing structure extending the ring structure, so that no second multiplication is installed.

For a general topological group Γ the map of R Γ need not be injective and the algebra may be commutative without Γ being so (both happen for an indiscrete Γ, whose only open normal subgroup is Γ itself). When Γ is profinite its open normal subgroups separate the points, so over a nontrivial R the group elements are distinct in R[[Γ]] (of_injective), the map of R Γ is a closed embedding for Hausdorff R (isClosedEmbedding_of), and the algebra is commutative exactly when Γ is (isMulCommutative_iff).

Main definitions

• TauCeti.completedGroupAlgebra R Γ: the completed group algebra R[[Γ]].
• TauCeti.completedGroupAlgebra.proj R Γ U: the projection onto R[Γ ⧸ U].
• TauCeti.completedGroupAlgebra.of R Γ: the group elements inside R[[Γ]].
• TauCeti.completedGroupAlgebra.mk: an element from a compatible family of elements of the group algebras R[Γ ⧸ U].
• TauCeti.completedGroupAlgebra.lift: the R-algebra homomorphism into R[[Γ]] assembled from a compatible family of R-algebra homomorphisms into the group algebras R[Γ ⧸ U].
• TauCeti.completedGroupAlgebra.coeffFamily R Γ: all coefficients of all projections, the map along which the topology is induced.

Main results

• TauCeti.completedGroupAlgebra.ext, TauCeti.completedGroupAlgebra.proj_surjective: the inverse-limit description.
• TauCeti.completedGroupAlgebra.proj_lift, TauCeti.completedGroupAlgebra.algHom_ext: the universal property, an algebra homomorphism into R[[Γ]] is determined by its compositions with the projections and lift has the prescribed ones.
• TauCeti.completedGroupAlgebra.proj_of: a group element projects to the corresponding basis element of the quotient group algebra.
• TauCeti.completedGroupAlgebra.isEmbedding_coeffFamily, TauCeti.completedGroupAlgebra.isClosedEmbedding_coeffFamily: the topology is the inverse-limit topology, and the compatible families form a closed subset of the product.
• TauCeti.completedGroupAlgebra.continuous_of: the group elements depend continuously on the group element.
• TauCeti.completedGroupAlgebra.exists_mem_span_range_of_proj_eq, TauCeti.completedGroupAlgebra.dense_span_range_of: every element agrees at any given level with an R-linear combination of group elements, so the span of the group elements is dense.
• TauCeti.completedGroupAlgebra.isUniformInducing_coeffFamily: over a uniform coefficient ring, the uniformity of the completed group algebra is the one induced along the coefficient map, and the algebra is a uniform additive group when R is.
• TauCeti.completedGroupAlgebra.of_injective, TauCeti.completedGroupAlgebra.isClosedEmbedding_of, TauCeti.completedGroupAlgebra.isMulCommutative_iff: for profinite Γ over a nontrivial R, the group elements are distinct, form a closed copy of Γ when R is Hausdorff, and the algebra is commutative exactly when Γ is.
• The instances IsTopologicalRing, ContinuousSMul R, CompactSpace, TotallyDisconnectedSpace, T2Space, UniformSpace and IsUniformAddGroup, the NoZeroSMulDivisors R instance for R without zero divisors, and the IsMulCommutative and CommRing instances for commutative Γ.

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.

def TauCeti.completedGroupAlgebra (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] : Type (max u v)

The completed group algebra R[[Γ]] of a topological group Γ over a commutative ring R: the inverse limit of the group algebras R[Γ ⧸ U] over the open normal subgroups U of Γ, along the maps induced by the quotient maps. For R = ℤ_[p] and Γ profinite this is the Iwasawa algebra ℤ_p[[Γ]].

Its elements are accessed through the projections completedGroupAlgebra.proj R Γ U onto the levels R[Γ ⧸ U], which determine them (completedGroupAlgebra.ext), and constructed from compatible families of elements of the levels by completedGroupAlgebra.mk. The representation as a subalgebra of the product of the levels is private to this file and is not part of the public interface.

Equations

• TauCeti.completedGroupAlgebra R Γ = ↥(TauCeti.completedGroupAlgebra.subalgebra✝ R Γ)

The ring and algebra structures are transported from the private subalgebra; the instances are @[no_expose], which is what lets their bodies name the private constant.

@[instance_reducible]

noncomputable instance TauCeti.completedGroupAlgebra.instRing (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] : Ring (completedGroupAlgebra R Γ)

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.completedGroupAlgebra.instAlgebra (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] : Algebra R (completedGroupAlgebra R Γ)

Equations

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

noncomputable def TauCeti.completedGroupAlgebra.proj (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] (U : OpenNormalSubgroup Γ) : completedGroupAlgebra R Γ →ₐ[R] MonoidAlgebra R (Γ ⧸ ↑U.toOpenSubgroup)

The projection of the completed group algebra onto the group algebra R[Γ ⧸ U] of the quotient by the open normal subgroup U, as an R-algebra homomorphism. It is surjective (proj_surjective), and the projections jointly determine an element (ext).

Equations

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

@[simp]

theorem TauCeti.completedGroupAlgebra.mapDomain_mapOfLE_proj {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {U V : OpenNormalSubgroup Γ} (hUV : U ≤ V) (x : completedGroupAlgebra R Γ) : MonoidAlgebra.mapDomain (⇑(QuotientGroup.mapOfLE hUV)) ((proj R Γ U) x) = (proj R Γ V) x

The projections at U ≤ V are compatible along the ring homomorphism R[Γ ⧸ U] → R[Γ ⧸ V] induced by the quotient map.

theorem TauCeti.completedGroupAlgebra.ext {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {x y : completedGroupAlgebra R Γ} (h : ∀ (U : OpenNormalSubgroup Γ), (proj R Γ U) x = (proj R Γ U) y) : x = y

Two elements of the completed group algebra with the same projections at every level are equal.

theorem TauCeti.completedGroupAlgebra.ext_iff {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {x y : completedGroupAlgebra R Γ} : x = y ↔ ∀ (U : OpenNormalSubgroup Γ), (proj R Γ U) x = (proj R Γ U) y

noncomputable def TauCeti.completedGroupAlgebra.mk (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] (x : (U : OpenNormalSubgroup Γ) → MonoidAlgebra R (Γ ⧸ ↑U.toOpenSubgroup)) (hx : ∀ ⦃U V : OpenNormalSubgroup Γ⦄ (hUV : U ≤ V), MonoidAlgebra.mapDomain (⇑(QuotientGroup.mapOfLE hUV)) (x U) = x V) : completedGroupAlgebra R Γ

The element of the completed group algebra with a prescribed compatible family of projections onto the levels R[Γ ⧸ U].

Equations

• TauCeti.completedGroupAlgebra.mk R Γ x hx = ⟨x, hx⟩

@[simp]

theorem TauCeti.completedGroupAlgebra.proj_mk (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] (x : (U : OpenNormalSubgroup Γ) → MonoidAlgebra R (Γ ⧸ ↑U.toOpenSubgroup)) (hx : ∀ ⦃U V : OpenNormalSubgroup Γ⦄ (hUV : U ≤ V), MonoidAlgebra.mapDomain (⇑(QuotientGroup.mapOfLE hUV)) (x U) = x V) (U : OpenNormalSubgroup Γ) : (proj R Γ U) (mk R Γ x hx) = x U

The projections of mk x hx are the prescribed family x.

noncomputable def TauCeti.completedGroupAlgebra.lift (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] {A : Type u_1} [Semiring A] [Algebra R A] (f : (U : OpenNormalSubgroup Γ) → A →ₐ[R] MonoidAlgebra R (Γ ⧸ ↑U.toOpenSubgroup)) (hf : ∀ ⦃U V : OpenNormalSubgroup Γ⦄ (hUV : U ≤ V) (a : A), MonoidAlgebra.mapDomain (⇑(QuotientGroup.mapOfLE hUV)) ((f U) a) = (f V) a) : A →ₐ[R] completedGroupAlgebra R Γ

The universal property of the completed group algebra: a family of R-algebra homomorphisms f U : A →ₐ[R] R[Γ ⧸ U], compatible along the maps induced by the quotient maps Γ ⧸ U → Γ ⧸ V for U ≤ V, assembles into an R-algebra homomorphism A →ₐ[R] R[[Γ]] whose projection at U is f U (proj_lift). It is the unique such homomorphism (algHom_ext).

Equations

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

@[simp]

theorem TauCeti.completedGroupAlgebra.proj_lift (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] {A : Type u_1} [Semiring A] [Algebra R A] (f : (U : OpenNormalSubgroup Γ) → A →ₐ[R] MonoidAlgebra R (Γ ⧸ ↑U.toOpenSubgroup)) (hf : ∀ ⦃U V : OpenNormalSubgroup Γ⦄ (hUV : U ≤ V) (a : A), MonoidAlgebra.mapDomain (⇑(QuotientGroup.mapOfLE hUV)) ((f U) a) = (f V) a) (U : OpenNormalSubgroup Γ) (a : A) : (proj R Γ U) ((lift R Γ f hf) a) = (f U) a

The projection of the lift of a compatible family f at U is f U.

@[simp]

theorem TauCeti.completedGroupAlgebra.proj_comp_lift (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] {A : Type u_1} [Semiring A] [Algebra R A] (f : (U : OpenNormalSubgroup Γ) → A →ₐ[R] MonoidAlgebra R (Γ ⧸ ↑U.toOpenSubgroup)) (hf : ∀ ⦃U V : OpenNormalSubgroup Γ⦄ (hUV : U ≤ V) (a : A), MonoidAlgebra.mapDomain (⇑(QuotientGroup.mapOfLE hUV)) ((f U) a) = (f V) a) (U : OpenNormalSubgroup Γ) : (proj R Γ U).comp (lift R Γ f hf) = f U

The lift of a compatible family f composed with the projection at U is f U.

theorem TauCeti.completedGroupAlgebra.algHom_ext {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {A : Type u_1} [Semiring A] [Algebra R A] {g₁ g₂ : A →ₐ[R] completedGroupAlgebra R Γ} (h : ∀ (U : OpenNormalSubgroup Γ), (proj R Γ U).comp g₁ = (proj R Γ U).comp g₂) : g₁ = g₂

Two R-algebra homomorphisms into the completed group algebra with the same compositions with every projection are equal; this is the uniqueness half of the universal property.

noncomputable def TauCeti.completedGroupAlgebra.of (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] : Γ →* completedGroupAlgebra R Γ

The group elements inside the completed group algebra: γ goes to the family of the basis elements at its classes in the quotients Γ ⧸ U. This is the analogue of MonoidAlgebra.of; its values are units, as it is a homomorphism from a group.

Equations

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

@[simp]

theorem TauCeti.completedGroupAlgebra.proj_of (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] (U : OpenNormalSubgroup Γ) (γ : Γ) : (proj R Γ U) ((of R Γ) γ) = MonoidAlgebra.single (↑γ) 1

A group element projects to the basis element of R[Γ ⧸ U] at its class.

theorem TauCeti.completedGroupAlgebra.proj_surjective (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] (U : OpenNormalSubgroup Γ) : Function.Surjective ⇑(proj R Γ U)

Every projection is surjective.

theorem TauCeti.completedGroupAlgebra.exists_mem_span_range_of_proj_eq (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] (x : completedGroupAlgebra R Γ) (V : OpenNormalSubgroup Γ) : ∃ y ∈ Submodule.span R (Set.range ⇑(of R Γ)), (proj R Γ V) y = (proj R Γ V) x

Every element of the completed group algebra agrees at any given level V with a finite R-linear combination of group elements.

instance TauCeti.completedGroupAlgebra.instNontrivial (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [Nontrivial R] : Nontrivial (completedGroupAlgebra R Γ)

instance TauCeti.completedGroupAlgebra.instNoZeroSMulDivisorsOfNoZeroDivisors (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [NoZeroDivisors R] : NoZeroSMulDivisors R (completedGroupAlgebra R Γ)

Over a coefficient ring without zero divisors, the completed group algebra has no scalar torsion: every nonzero scalar acts injectively, as it does on each coefficient of each level.

instance TauCeti.completedGroupAlgebra.instIsMulCommutative (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [IsMulCommutative Γ] : IsMulCommutative (completedGroupAlgebra R Γ)

The completed group algebra of a commutative group is commutative.

@[instance_reducible]

noncomputable instance TauCeti.completedGroupAlgebra.instCommRingOfIsMulCommutative (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [IsMulCommutative Γ] : CommRing (completedGroupAlgebra R Γ)

The completed group algebra of a commutative group, as a commutative ring: the bundled form of the IsMulCommutative instance, obtained from Mathlib's scoped construction. The ring structure is the existing one, so this installs no second multiplication.

Equations

• TauCeti.completedGroupAlgebra.instCommRingOfIsMulCommutative R Γ = inferInstance

theorem TauCeti.completedGroupAlgebra.of_injective (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] [Nontrivial R] : Function.Injective ⇑(of R Γ)

Over a nontrivial coefficient ring, distinct elements of a profinite group are distinct inside its completed group algebra: the open normal subgroups separate the points.

theorem TauCeti.completedGroupAlgebra.isMulCommutative_iff (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] [Nontrivial R] : IsMulCommutative (completedGroupAlgebra R Γ) ↔ IsMulCommutative Γ

Over a nontrivial coefficient ring, the completed group algebra of a profinite group is commutative exactly when the group is.

theorem TauCeti.completedGroupAlgebra.coeff_proj_mul (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] (x y : completedGroupAlgebra R Γ) (U : OpenNormalSubgroup Γ) [Fintype (Γ ⧸ ↑U.toOpenSubgroup)] (g : Γ ⧸ ↑U.toOpenSubgroup) : ((proj R Γ U) (x * y)).coeff g = ∑ h : Γ ⧸ ↑U.toOpenSubgroup, ((proj R Γ U) x).coeff h * ((proj R Γ U) y).coeff (h⁻¹ * g)

The coefficient of a product at a class g of a finite quotient is the sum, over the classes h of that quotient, of the products of the coefficients of the factors at h and h⁻¹ * g.

The inverse-limit topology

noncomputable def TauCeti.completedGroupAlgebra.coeffFamily (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] : completedGroupAlgebra R Γ →+ (U : OpenNormalSubgroup Γ) → Γ ⧸ ↑U.toOpenSubgroup → R

All coefficients of all projections, as one additive map into a product of copies of R. The topology of the completed group algebra is the one induced along this map: the coarsest topology making every coefficient of every projection continuous.

Equations

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

@[simp]

theorem TauCeti.completedGroupAlgebra.coeffFamily_apply (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] (x : completedGroupAlgebra R Γ) (U : OpenNormalSubgroup Γ) : (coeffFamily R Γ) x U = ⇑((proj R Γ U) x).coeff

The coefficients of an element at a quotient are those of its projection.

theorem TauCeti.completedGroupAlgebra.coeffFamily_injective (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] : Function.Injective ⇑(coeffFamily R Γ)

An element is determined by the coefficients of its projections.

@[instance_reducible]

noncomputable instance TauCeti.completedGroupAlgebra.instTopologicalSpace (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] : TopologicalSpace (completedGroupAlgebra R Γ)

The inverse-limit topology on the completed group algebra: the topology induced along the coefficient map coeffFamily R Γ into the product of copies of R.

Equations

• TauCeti.completedGroupAlgebra.instTopologicalSpace R Γ = TopologicalSpace.induced (⇑(TauCeti.completedGroupAlgebra.coeffFamily R Γ)) inferInstance

theorem TauCeti.completedGroupAlgebra.isInducing_coeffFamily (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] : Topology.IsInducing ⇑(coeffFamily R Γ)

The topology of the completed group algebra is induced along the coefficient map.

theorem TauCeti.completedGroupAlgebra.isEmbedding_coeffFamily (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] : Topology.IsEmbedding ⇑(coeffFamily R Γ)

The completed group algebra embeds topologically into the product, over the open normal subgroups U and the elements of Γ ⧸ U, of copies of R.

theorem TauCeti.completedGroupAlgebra.continuous_coeff_proj (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] (U : OpenNormalSubgroup Γ) (g : Γ ⧸ ↑U.toOpenSubgroup) : Continuous fun (x : completedGroupAlgebra R Γ) => ((proj R Γ U) x).coeff g

Every coefficient of every projection is continuous.

theorem TauCeti.completedGroupAlgebra.continuous_iff {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] {X : Type u_1} [TopologicalSpace X] {f : X → completedGroupAlgebra R Γ} : Continuous f ↔ ∀ (U : OpenNormalSubgroup Γ) (g : Γ ⧸ ↑U.toOpenSubgroup), Continuous fun (x : X) => ((proj R Γ U) (f x)).coeff g

A map into the completed group algebra is continuous exactly when every coefficient of every projection of its values is.

instance TauCeti.completedGroupAlgebra.instT2Space (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] [T2Space R] : T2Space (completedGroupAlgebra R Γ)

instance TauCeti.completedGroupAlgebra.instTotallyDisconnectedSpace (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] [TotallyDisconnectedSpace R] : TotallyDisconnectedSpace (completedGroupAlgebra R Γ)

instance TauCeti.completedGroupAlgebra.instIsTopologicalAddGroup (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] [IsTopologicalAddGroup R] : IsTopologicalAddGroup (completedGroupAlgebra R Γ)

instance TauCeti.completedGroupAlgebra.instContinuousSMulOfContinuousMul (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] [ContinuousMul R] : ContinuousSMul R (completedGroupAlgebra R Γ)

Scalar multiplication by the coefficient ring is continuous: it multiplies every coefficient of every projection by the scalar.

theorem TauCeti.completedGroupAlgebra.continuous_of (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] [SeparatelyContinuousMul Γ] : Continuous ⇑(of R Γ)

The group elements of the completed group algebra depend continuously on the group element.

Density of the group elements

theorem TauCeti.completedGroupAlgebra.dense_span_range_of (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] : Dense ↑(Submodule.span R (Set.range ⇑(of R Γ)))

The group elements span a dense subspace. The R-span of the group elements is dense in the completed group algebra.

The results of this section assume that every open normal quotient Γ ⧸ U is finite, so that each coefficient of a product at U is a finite sum of products of coefficients (coeff_proj_mul). For a compact Γ with separately continuous multiplication this hypothesis is Mathlib's instance Finite (Γ ⧸ U.toSubgroup) for open subgroups U, so the instances below apply to compact groups without further assumptions.

instance TauCeti.completedGroupAlgebra.instContinuousMulOfIsTopologicalSemiring (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] [∀ (U : OpenNormalSubgroup Γ), Finite (Γ ⧸ ↑U.toOpenSubgroup)] [IsTopologicalSemiring R] : ContinuousMul (completedGroupAlgebra R Γ)

When every open normal quotient of Γ is finite, multiplication in the completed group algebra is continuous: each coefficient of a product is a finite sum of products of coefficients.

instance TauCeti.completedGroupAlgebra.instIsTopologicalRing (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] [∀ (U : OpenNormalSubgroup Γ), Finite (Γ ⧸ ↑U.toOpenSubgroup)] [IsTopologicalRing R] : IsTopologicalRing (completedGroupAlgebra R Γ)

When every open normal quotient of Γ is finite, the completed group algebra over a topological ring is a topological ring.

theorem TauCeti.completedGroupAlgebra.isClosedEmbedding_coeffFamily (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] [∀ (U : OpenNormalSubgroup Γ), Finite (Γ ⧸ ↑U.toOpenSubgroup)] [T2Space R] [ContinuousAdd R] : Topology.IsClosedEmbedding ⇑(coeffFamily R Γ)

The compatible coefficient families form a closed subset of the product of copies of R, so the completed group algebra is a closed embedding into it.

instance TauCeti.completedGroupAlgebra.instCompactSpaceOfT2SpaceOfContinuousAdd (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] [∀ (U : OpenNormalSubgroup Γ), Finite (Γ ⧸ ↑U.toOpenSubgroup)] [T2Space R] [CompactSpace R] [ContinuousAdd R] : CompactSpace (completedGroupAlgebra R Γ)

When every open normal quotient of Γ is finite, the completed group algebra over a compact Hausdorff ring with continuous addition is compact.

theorem TauCeti.completedGroupAlgebra.isClosedEmbedding_of (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [TopologicalSpace R] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] [Nontrivial R] [T2Space R] : Topology.IsClosedEmbedding ⇑(of R Γ)

Over a nontrivial Hausdorff coefficient ring, the group elements of a profinite group form a closed subset of the completed group algebra homeomorphic to the group.

The inverse-limit uniformity

@[instance_reducible]

noncomputable instance TauCeti.completedGroupAlgebra.instUniformSpace (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [UniformSpace R] : UniformSpace (completedGroupAlgebra R Γ)

The inverse-limit uniformity on the completed group algebra: the uniformity induced along the coefficient map coeffFamily R Γ into the product of copies of R. Its topology is the inverse-limit topology.

Equations

• TauCeti.completedGroupAlgebra.instUniformSpace R Γ = (UniformSpace.comap (⇑(TauCeti.completedGroupAlgebra.coeffFamily R Γ)) inferInstance).replaceTopology ⋯

theorem TauCeti.completedGroupAlgebra.isUniformInducing_coeffFamily (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [UniformSpace R] : IsUniformInducing ⇑(coeffFamily R Γ)

The uniformity of the completed group algebra is induced along the coefficient map.

theorem TauCeti.completedGroupAlgebra.isUniformEmbedding_coeffFamily (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [UniformSpace R] : IsUniformEmbedding ⇑(coeffFamily R Γ)

The coefficient map is a uniform embedding of the completed group algebra into the product, over the open normal subgroups U and the elements of Γ ⧸ U, of copies of R.

instance TauCeti.completedGroupAlgebra.instIsUniformAddGroup (R : Type u) [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] [UniformSpace R] [IsUniformAddGroup R] : IsUniformAddGroup (completedGroupAlgebra R Γ)