CompletedGroupAlgebra.Separation
This module proves separation lemmas for completed group algebras using finite quotients.
theorem exists_completedGroupAlgebraIndex_avoids_finset
(hG : ProCGroups.IsProfiniteGroup G) (s : Finset G)
(hs : ∀ x ∈ s, x ≠ 1) :
∃ U : CompletedGroupAlgebraIndex G,
∀ x ∈ s, x ∉ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)Show proof
by
classical
let hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
(isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
revert hs
refine Finset.induction_on s ?_ ?_
· intro _hs
letI : Nonempty (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) :=
IsProCGroup.openNormalSubgroupInClass_nonempty hProC
letI : Nonempty (CompletedGroupAlgebraIndex G) := inferInstance
exact ⟨Classical.choice inferInstance, by simp only [Finset.notMem_empty, OpenSubgroup.mem_toSubgroup, IsEmpty.forall_iff, implies_true]⟩
· intro a s has ih hs
have ha : a ≠ 1 := hs a (by simp only [Finset.mem_insert, true_or])
rcases hProC.exists_openNormalSubgroupInClass_not_mem ha with ⟨A, hA⟩
have hs' : ∀ x ∈ s, x ≠ 1 := by
intro x hx
exact hs x (by simp only [Finset.mem_insert, hx, or_true])
rcases ih hs' with ⟨U, hU⟩
let Aidx : CompletedGroupAlgebraIndex G := OrderDual.toDual A
rcases directed_openNormalSubgroupInClass
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) ProCGroups.FiniteGroupClass.allFinite_formation
Aidx U with
⟨W, hAW, hUW⟩
refine ⟨W, ?_⟩
intro x hx hxW
rw [Finset.mem_insert] at hx
rcases hx with rfl | hx
· exact hA (hAW hxW)
· exact hU x hx (hUW hxW)Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem exists_completedGroupAlgebraIndex_separating_support
(hG : ProCGroups.IsProfiniteGroup G) (x : MonoidAlgebra R G) (g : G) :
∃ U : CompletedGroupAlgebraIndex G,
∀ h ∈ x.support, h ≠ g →
openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U h ≠
openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U gShow proof
by
classical
let bad : Finset G := (x.support.erase g).image fun h => h⁻¹ * g
have hbad : ∀ y ∈ bad, y ≠ 1 := by
intro y hy
rcases Finset.mem_image.mp hy with ⟨h, hh, rfl⟩
intro h1
have hg : h = g := by
have hmul := congrArg (fun t : G => h * t) h1
have hg' : g = h := by
simpa [mul_assoc] using hmul
exact hg'.symm
exact (Finset.mem_erase.mp hh).1 hg
rcases exists_completedGroupAlgebraIndex_avoids_finset (G := G) hG bad hbad with
⟨U, hU⟩
refine ⟨U, ?_⟩
intro h hh hne heq
have hbadmem : h⁻¹ * g ∈ bad := by
exact Finset.mem_image.mpr ⟨h, Finset.mem_erase.mpr ⟨hne, hh⟩, rfl⟩
have hmem :
h⁻¹ * g ∈ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) := by
exact QuotientGroup.eq.1 heq
exact hU (h⁻¹ * g) hbadmem hmemProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem completedGroupAlgebraStageMap_coeff_of_support_separated
(U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) (g : G)
(hsep : ∀ h ∈ x.support, h ≠ g →
openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U h ≠
openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) :
completedGroupAlgebraStageMap R G U x
(openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) =
x gIf a finite quotient separates \(g\) from the other support points of \(x\), then the coefficient of the image of \(g\) in the quotient group algebra is exactly the original coefficient of \(g\).
Show proof
by
classical
rw [completedGroupAlgebraStageMap]
change (Finsupp.mapDomain
(openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U) x)
(openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) =
x g
rw [Finsupp.mapDomain, Finsupp.sum_apply]
rw [Finsupp.sum_eq_single g]
· simp only [Finsupp.single_eq_same]
· intro h hh hne
exact Finsupp.single_eq_of_ne fun heq =>
hsep h (Finsupp.mem_support_iff.mpr hh) hne heq.symm
· intro _hg
simp only [Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem exists_completedGroupAlgebraIndexInClass_avoids_finset
(C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
(hG : IsProCGroup C G) (s : Finset G) (hs : ∀ x ∈ s, x ≠ 1) :
∃ U : CompletedGroupAlgebraIndexInClass G C,
∀ x ∈ s, x ∉ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)Show proof
by
classical
revert hs
refine Finset.induction_on s ?_ ?_
· intro _hs
letI : Nonempty (OpenNormalSubgroupInClass C G) :=
IsProCGroup.openNormalSubgroupInClass_nonempty hG
letI : Nonempty (CompletedGroupAlgebraIndexInClass G C) := inferInstance
exact ⟨Classical.choice inferInstance, by simp only [Finset.notMem_empty, OpenSubgroup.mem_toSubgroup, IsEmpty.forall_iff, implies_true]⟩
· intro a s has ih hs
have ha : a ≠ 1 := hs a (by simp only [Finset.mem_insert, true_or])
rcases hG.exists_openNormalSubgroupInClass_not_mem ha with ⟨A, hA⟩
have hs' : ∀ x ∈ s, x ≠ 1 := by
intro x hx
exact hs x (by simp only [Finset.mem_insert, hx, or_true])
rcases ih hs' with ⟨U, hU⟩
let Aidx : CompletedGroupAlgebraIndexInClass G C := OrderDual.toDual A
rcases directed_openNormalSubgroupInClass (C := C) (G := G) hForm Aidx U with
⟨W, hAW, hUW⟩
refine ⟨W, ?_⟩
intro x hx hxW
rw [Finset.mem_insert] at hx
rcases hx with rfl | hx
· exact hA (hAW hxW)
· exact hU x hx (hUW hxW)Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem exists_completedGroupAlgebraIndexInClass_separating_finsupp_support
{M : Type w} [Zero M]
(C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
(hG : IsProCGroup C G) (x : G →₀ M) (g : G) :
∃ U : CompletedGroupAlgebraIndexInClass G C,
∀ h ∈ x.support, h ≠ g →
openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
openNormalSubgroupInClassProj (C := C) (G := G) U gFor any finitely supported family on a pro-\(C\) group and a chosen basis point \(g\), one \(C\)-quotient separates the image of \(g\) from all other support points.
Show proof
by
classical
let bad : Finset G := (x.support.erase g).image fun h => h⁻¹ * g
have hbad : ∀ y ∈ bad, y ≠ 1 := by
intro y hy
rcases Finset.mem_image.mp hy with ⟨h, hh, rfl⟩
intro h1
have hg : h = g := by
have hmul := congrArg (fun t : G => h * t) h1
have hg' : g = h := by
simpa [mul_assoc] using hmul
exact hg'.symm
exact (Finset.mem_erase.mp hh).1 hg
rcases exists_completedGroupAlgebraIndexInClass_avoids_finset
(G := G) C hForm hG bad hbad with
⟨U, hU⟩
refine ⟨U, ?_⟩
intro h hh hne heq
have hbadmem : h⁻¹ * g ∈ bad := by
exact Finset.mem_image.mpr ⟨h, Finset.mem_erase.mpr ⟨hne, hh⟩, rfl⟩
have hmem :
h⁻¹ * g ∈ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) := by
exact QuotientGroup.eq.1 heq
exact hU (h⁻¹ * g) hbadmem hmemProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem exists_completedGroupAlgebraIndexInClass_separating_support
(C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
(hG : IsProCGroup C G) (x : MonoidAlgebra R G) (g : G) :
∃ U : CompletedGroupAlgebraIndexInClass G C,
∀ h ∈ x.support, h ≠ g →
openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
openNormalSubgroupInClassProj (C := C) (G := G) U gShow proof
exists_completedGroupAlgebraIndexInClass_separating_finsupp_support
(G := G) C hForm hG x gProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem completedGroupAlgebraStageMapInClass_coeff_of_support_separated
(C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
(x : MonoidAlgebra R G) (g : G)
(hsep : ∀ h ∈ x.support, h ≠ g →
openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
openNormalSubgroupInClassProj (C := C) (G := G) U g) :
completedGroupAlgebraStageMapInClass C R G U x
(openNormalSubgroupInClassProj (C := C) (G := G) U g) =
x gIf a \(C\)-quotient separates \(g\) from the other support points of \(x\), then the coefficient of the image of \(g\) in the quotient group algebra is exactly the original coefficient of \(g\).
Show proof
by
classical
rw [completedGroupAlgebraStageMapInClass]
change (Finsupp.mapDomain
(openNormalSubgroupInClassProj (C := C) (G := G) U) x)
(openNormalSubgroupInClassProj (C := C) (G := G) U g) =
x g
rw [Finsupp.mapDomain, Finsupp.sum_apply]
rw [Finsupp.sum_eq_single g]
· simp only [Finsupp.single_eq_same]
· intro h hh hne
exact Finsupp.single_eq_of_ne fun heq =>
hsep h (Finsupp.mem_support_iff.mpr hh) hne heq.symm
· intro _hg
simp only [Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem injective_toCompletedGroupAlgebraRingHom
(hG : ProCGroups.IsProfiniteGroup G) :
Function.Injective (toCompletedGroupAlgebraRingHom R G)In Lemma 5.3.5(a), fixed-coefficient form, the canonical map from the abstract group algebra to the completed group algebra is injective for profinite G. Equivalently, the kernels of the finite group-quotient maps have trivial intersection.
Show proof
by
intro x y hxy
apply Finsupp.ext
intro g
have hcoeff : (x - y) g = 0 := by
rcases exists_completedGroupAlgebraIndex_separating_support (R := R) (G := G)
hG (x - y) g with
⟨U, hsep⟩
have hstage_eq : completedGroupAlgebraStageMap R G U x =
completedGroupAlgebraStageMap R G U y := by
have hp := congrArg (fun z : Carrier R G =>
completedGroupAlgebraProjection R G U z) hxy
change completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G x) =
completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G y) at hp
simpa [completedGroupAlgebraProjection_toCompletedGroupAlgebra] using hp
have hstage : completedGroupAlgebraStageMap R G U (x - y) = 0 := by
rw [map_sub, hstage_eq, sub_self]
have hstage_coeff :
completedGroupAlgebraStageMap R G U (x - y)
(openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) = 0 := by
simpa using congrArg
(fun z : CompletedGroupAlgebraStage R G U =>
z (openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g))
hstage
rw [completedGroupAlgebraStageMap_coeff_of_support_separated
(R := R) (G := G) U (x - y) g hsep] at hstage_coeff
simpa using hstage_coeff
exact sub_eq_zero.mp hcoeffProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Injectivity follows because two elements with identical finite-stage coordinates are equal in the inverse limit, and subtype inclusions are injective on their underlying elements. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. For the all-finite and \(C\)-indexed comparisons, both composites have the same finite-stage coordinates; hence inverse-limit extensionality proves the ring, algebra, or topological equivalence. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. For injectivity, suppose two source elements have the same image. After projecting to every finite quotient stage the corresponding finite-stage map is injective, or the equality is simply equality of subtype carriers; hence all source coordinates agree, and the inverse-limit extensionality principle identifies the original elements.
□theorem toCompletedGroupAlgebraRingHom_ker_eq_bot
(hG : ProCGroups.IsProfiniteGroup G) :
RingHom.ker (toCompletedGroupAlgebraRingHom R G) = ⊥The dense map from the ordinary group algebra into the completed group algebra has trivial kernel after separation by all finite quotient stages.
Show proof
(RingHom.injective_iff_ker_eq_bot (toCompletedGroupAlgebraRingHom R G)).mp
(injective_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG)Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem toCompletedGroupAlgebraRingHom_ker_eq_iInf_stageMap_ker :
RingHom.ker (toCompletedGroupAlgebraRingHom R G) =
⨅ U : CompletedGroupAlgebraIndex G, RingHom.ker (completedGroupAlgebraStageMap R G U)The kernel of the map to \(\widehat{R[G]}\) is the intersection of the finite-stage kernels.
Show proof
by
ext x
constructor
· intro hx
rw [RingHom.mem_ker] at hx
rw [Submodule.mem_iInf]
intro U
rw [RingHom.mem_ker]
have hU := congrArg (fun y : Carrier R G =>
completedGroupAlgebraProjection R G U y) hx
change completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G x) =
completedGroupAlgebraProjection R G U (0 : Carrier R G) at hU
simpa [completedGroupAlgebraProjection_toCompletedGroupAlgebra] using hU
· intro hx
rw [RingHom.mem_ker]
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraStageMap R G U x = 0
exact (Submodule.mem_iInf
(p := fun U : CompletedGroupAlgebraIndex G =>
RingHom.ker (completedGroupAlgebraStageMap R G U))).1 hx UProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem iInf_completedGroupAlgebraStageMap_ker_eq_bot
(hG : ProCGroups.IsProfiniteGroup G) :
(⨅ U : CompletedGroupAlgebraIndex G,
RingHom.ker (completedGroupAlgebraStageMap R G U)) = ⊥Fixed-coefficient finite-stage kernel-family form of Lemma 5.3.5(a).
Show proof
by
rw [← toCompletedGroupAlgebraRingHom_ker_eq_iInf_stageMap_ker (R := R) (G := G),
toCompletedGroupAlgebraRingHom_ker_eq_bot (R := R) (G := G) hG]Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem injective_toCompletedGroupAlgebraInClassRingHom
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
Function.Injective (toCompletedGroupAlgebraInClassRingHom C hC R G)\(C\)-indexed form of Lemma 5.3.5(a): for a pro-\(C\) group, the canonical map from the abstract group algebra to \(\widehat{R[G]}_{C}\) is injective.
Show proof
by
intro x y hxy
apply injective_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG.1
have h := congrArg
(completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG) hxy
simpa [RingHom.congr_fun
(completedGroupAlgebraFromInClassRingHom_comp_toCompletedGroupAlgebraInClass
(R := R) (G := G) C hC hForm hG)] using hProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Injectivity follows because two elements with identical finite-stage coordinates are equal in the inverse limit, and subtype inclusions are injective on their underlying elements. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. For injectivity, suppose two source elements have the same image. After projecting to every finite quotient stage the corresponding finite-stage map is injective, or the equality is simply equality of subtype carriers; hence all source coordinates agree, and the inverse-limit extensionality principle identifies the original elements.
□theorem toCompletedGroupAlgebraInClassRingHom_ker_eq_bot
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
RingHom.ker (toCompletedGroupAlgebraInClassRingHom C hC R G) = ⊥Kernel form of the \(C\)-indexed injectivity statement.
Show proof
(RingHom.injective_iff_ker_eq_bot (toCompletedGroupAlgebraInClassRingHom C hC R G)).mp
(injective_toCompletedGroupAlgebraInClassRingHom (R := R) (G := G) C hC hForm hG)Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Injectivity follows because two elements with identical finite-stage coordinates are equal in the inverse limit, and subtype inclusions are injective on their underlying elements. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. For injectivity, suppose two source elements have the same image. After projecting to every finite quotient stage the corresponding finite-stage map is injective, or the equality is simply equality of subtype carriers; hence all source coordinates agree, and the inverse-limit extensionality principle identifies the original elements. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem toCompletedGroupAlgebraInClassRingHom_ker_eq_iInf_stageMapInClass_ker
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
RingHom.ker (toCompletedGroupAlgebraInClassRingHom C hC R G) =
⨅ U : CompletedGroupAlgebraIndexInClass G C,
RingHom.ker (completedGroupAlgebraStageMapInClass C R G U)The kernel of the map to \(\widehat{R[G]}_{C}\) is the intersection of the \(C\)-indexed finite-stage kernels.
Show proof
by
ext x
constructor
· intro hx
rw [RingHom.mem_ker] at hx
rw [Submodule.mem_iInf]
intro U
rw [RingHom.mem_ker]
have hU := congrArg (fun y : CompletedGroupAlgebraInClass C hC R G =>
completedGroupAlgebraProjectionInClass C hC R G U y) hx
change completedGroupAlgebraProjectionInClass C hC R G U
(toCompletedGroupAlgebraInClass C hC R G x) =
completedGroupAlgebraProjectionInClass C hC R G U
(0 : CompletedGroupAlgebraInClass C hC R G) at hU
simpa [completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass] using hU
· intro hx
rw [RingHom.mem_ker]
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
change completedGroupAlgebraStageMapInClass C R G U x = 0
exact (Submodule.mem_iInf
(p := fun U : CompletedGroupAlgebraIndexInClass G C =>
RingHom.ker (completedGroupAlgebraStageMapInClass C R G U))).1 hx UProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem iInf_completedGroupAlgebraStageMapInClass_ker_eq_bot
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
(⨅ U : CompletedGroupAlgebraIndexInClass G C,
RingHom.ker (completedGroupAlgebraStageMapInClass C R G U)) = ⊥\(C\)-indexed finite-stage kernel-family form of Lemma 5.3.5(a).
Show proof
by
rw [← toCompletedGroupAlgebraInClassRingHom_ker_eq_iInf_stageMapInClass_ker
(R := R) (G := G) C hC,
toCompletedGroupAlgebraInClassRingHom_ker_eq_bot (R := R) (G := G) C hC hForm hG]Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem iInf_groupAlgebraOpenFiniteQuotientKernel_eq_bot
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
(⨅ K : CompletedGroupAlgebraOpenQuotientIndex R G,
groupAlgebraOpenFiniteQuotientKernel R G K) = ⊥In Lemma 5.3.5(a), book kernel-family form, the intersection of the kernels of \(R[G] \to (R/I)[G/U]\), over open coefficient ideals and finite group quotients, is zero.
Show proof
by
apply le_antisymm
· intro x hx
rw [Ideal.mem_bot]
have hxall :
∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
x ∈ groupAlgebraOpenFiniteQuotientKernel R G K := by
simpa using (Submodule.mem_iInf
(p := fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
groupAlgebraOpenFiniteQuotientKernel R G K)).1 hx
have hxlimit :
toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G x = 0 := by
apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
intro K
change groupAlgebraOpenFiniteQuotientMap R G K x = 0
exact (mem_groupAlgebraOpenFiniteQuotientKernel_iff R G K x).1 (hxall K)
have hcompleted :
toCompletedGroupAlgebraRingHom R G x = 0 := by
apply injective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G) hR
change completedGroupAlgebraToOpenFiniteQuotientLimit R G
(toCompletedGroupAlgebra R G x) =
completedGroupAlgebraToOpenFiniteQuotientLimit R G
(0 : Carrier R G)
simpa [toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom] using hxlimit
exact (injective_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG) (by
simpa using hcompleted)
· exact bot_leProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem completedGroupAlgebra_kernelTopology_isHausdorffProfiniteCompletion
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
letI : TopologicalSpace (MonoidAlgebra R G)In Lemma 5.3.5(b/c), concrete completion form, with the book kernel-neighborhood topology on \(R[G]\), the canonical map into \(\widehat{R[G]}\) is an injective dense continuous map into a profinite ring, and that topology is precisely the one induced from \(\widehat{R[G]}\).
Show proof
groupAlgebraOpenFiniteQuotientKernelTopology R G
IsProfiniteRing (Carrier R G) ∧
Function.Injective (toCompletedGroupAlgebraRingHom R G) ∧
DenseRange (toCompletedGroupAlgebraRingHom R G) ∧
Continuous (toCompletedGroupAlgebraRingHom R G) ∧
groupAlgebraOpenFiniteQuotientKernelTopology R G =
TopologicalSpace.induced (toCompletedGroupAlgebra R G) inferInstance := by
have hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
(isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
letI : Nonempty (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) :=
IsProCGroup.openNormalSubgroupInClass_nonempty hProC
letI : Nonempty (CompletedGroupAlgebraIndex G) := inferInstance
letI : Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G) := inferInstance
refine ⟨completedGroupAlgebra_isProfiniteRing (R := R) (G := G) hR,
injective_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG,
denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG,
continuous_toCompletedGroupAlgebraRingHom_kernelTopology (R := R) (G := G) hR, ?_⟩
have hτ :=
completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology
(R := R) (G := G) hR
simpa [completedGroupAlgebraNaturalTopology] using hτ.symmProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Injectivity follows because two elements with identical finite-stage coordinates are equal in the inverse limit, and subtype inclusions are injective on their underlying elements. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. For injectivity, suppose two source elements have the same image. After projecting to every finite quotient stage the corresponding finite-stage map is injective, or the equality is simply equality of subtype carriers; hence all source coordinates agree, and the inverse-limit extensionality principle identifies the original elements.
□theorem completedGroupAlgebraRingHom_ext_of_comp_toCompleted
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
{f g : Carrier R G →+* Carrier R H}
(hf : Continuous f) (hg : Continuous g)
(hfg : f.comp (toCompletedGroupAlgebraRingHom R G) =
g.comp (toCompletedGroupAlgebraRingHom R G)) :
f = gContinuous ring homomorphisms out of \(\widehat{R[G]}\) into another completed group algebra are determined by their values on the dense abstract group algebra.
Show proof
by
letI : T2Space (Carrier R H) :=
completedGroupAlgebra_t2Space (R := R) (G := H) hR
have hdense : DenseRange (toCompletedGroupAlgebraRingHom R G) :=
denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG
have hcomp : (f : Carrier R G → Carrier R H) ∘
(toCompletedGroupAlgebraRingHom R G) =
(g : Carrier R G → Carrier R H) ∘
(toCompletedGroupAlgebraRingHom R G) := by
funext x
exact congrFun (congrArg DFunLike.coe hfg) x
have hfun : (f : Carrier R G → Carrier R H) = g :=
DenseRange.equalizer hdense hf hg hcomp
exact RingHom.ext fun x => congrFun hfun xProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraMap_id
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
completedGroupAlgebraMap (G := G) (H := G) R hG (MonoidHom.id G) continuous_id =
RingHom.id (Carrier R G)Lemma 5.3.5(e), identity law for the completed-group-algebra functor.
Show proof
by
apply completedGroupAlgebraRingHom_ext_of_comp_toCompleted (R := R) (G := G) (H := G)
hR hG
· exact continuous_completedGroupAlgebraMap (R := R) (G := G) (H := G)
hG (MonoidHom.id G) continuous_id
· exact continuous_id
· rw [completedGroupAlgebraMap_comp_toCompletedGroupAlgebra,
finiteGroupAlgebra_mapDomainRingHom_id]
rflProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem completedGroupAlgebraMapAlgHom_id
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
completedGroupAlgebraMapAlgHom (G := G) (H := G) R hG (MonoidHom.id G) continuous_id =
AlgHom.id R (Carrier R G)Lemma 5.3.5(e), identity law for the completed-group-algebra functor, as an \(R\)-algebra homomorphism.
Show proof
by
apply AlgHom.ext
intro x
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMap_id (R := R) (G := G) hR hG))
x
simpa using hProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□