CompletedGroupAlgebra.OpenFiniteQuotientTopology.FiniteQuotients
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
theorem continuous_idealQuotient_mk_openIdeal_discrete
(I : Ideal R) (hI : IsOpen (I : Set R)) :
letI : TopologicalSpace (R ⧸ I)An open coefficient ideal gives a continuous quotient map when the quotient is equipped with the discrete topology. This is the coefficient-side continuity used in Ribes--Zalesskii Section \(5.3\).
Show proof
⊥
Continuous (Ideal.Quotient.mk I) := by
letI : TopologicalSpace (R ⧸ I) := ⊥
haveI : DiscreteTopology (R ⧸ I) := ⟨rfl⟩
rw [continuous_discrete_rng]
intro b
rcases Ideal.Quotient.mk_surjective (I := I) b with ⟨a, rfl⟩
have hpre :
(Ideal.Quotient.mk I) ⁻¹' ({Ideal.Quotient.mk I a} : Set (R ⧸ I)) =
(fun x : R => x - a) ⁻¹' (I : Set R) := by
ext x
simp only [Set.mem_preimage, Set.mem_singleton_iff, Ideal.Quotient.eq, SetLike.mem_coe]
rw [hpre]
exact hI.preimage (continuous_id.sub continuous_const)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. 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. 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 finiteGroupAlgebra_mapRangeRingHom_continuous
(S : Type u) [CommRing S] [TopologicalSpace S]
(Q : Type v) [Group Q] [Finite Q]
(f : R →+* S) (hf : Continuous f) :
letI : TopologicalSpace (MonoidAlgebra R Q)Finite-stage group algebras are functorial in the coefficient ring by continuous maps.
Show proof
finiteGroupAlgebraTopology R Q
letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
Continuous (MonoidAlgebra.mapRangeRingHom Q f :
MonoidAlgebra R Q → MonoidAlgebra S Q) := by
classical
letI : Fintype Q := Fintype.ofFinite Q
letI : TopologicalSpace (MonoidAlgebra R Q) := finiteGroupAlgebraTopology R Q
letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
let eR : MonoidAlgebra R Q ≃ (Q → R) := Finsupp.equivFunOnFinite
let eS : MonoidAlgebra S Q ≃ (Q → S) := Finsupp.equivFunOnFinite
have heS : Topology.IsInducing (eS : MonoidAlgebra S Q → Q → S) :=
Topology.IsInducing.induced eS
have hcoordR : ∀ q : Q, Continuous fun x : MonoidAlgebra R Q => x q := by
intro q
simpa [eR] using
(continuous_apply q).comp
(continuous_induced_dom : Continuous (eR : MonoidAlgebra R Q → Q → R))
rw [heS.continuous_iff]
apply continuous_pi
intro q
change Continuous fun x : MonoidAlgebra R Q =>
(MonoidAlgebra.mapRangeRingHom Q f x : MonoidAlgebra S Q) q
simpa [MonoidAlgebra.mapRangeRingHom_apply] using hf.comp (hcoordR q)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. 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. 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 finiteGroupAlgebraTopology_discrete_of_discrete_coeff
(S : Type u) [CommRing S] [TopologicalSpace S] [DiscreteTopology S]
(Q : Type v) [Group Q] [Finite Q] :
letI : TopologicalSpace (MonoidAlgebra S Q)Show proof
finiteGroupAlgebraTopology S Q
DiscreteTopology (MonoidAlgebra S Q) := by
classical
letI : Fintype Q := Fintype.ofFinite Q
letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
let e : MonoidAlgebra S Q ≃ (Q → S) := Finsupp.equivFunOnFinite
haveI : DiscreteTopology (Q → S) := inferInstance
exact DiscreteTopology.of_continuous_injective
(continuous_induced_dom : Continuous (e : MonoidAlgebra S Q → Q → S)) e.injectiveProof. 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. 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. 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. 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.
□abbrev CompletedGroupAlgebraCoeffQuotientStage
(R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
Type (max u v) :=
MonoidAlgebra (R ⧸ I) (CompletedGroupAlgebraQuotient G U)The Ribes--Zalesskii Section \(5.3\) finite quotient \((R/I)[G/U]\) applies both the coefficient quotient and the group quotient and is used in the kernel-neighborhood topology.
def completedGroupAlgebraStageCoeffQuotientMap
(R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G]
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
CompletedGroupAlgebraStage R G U →+*
CompletedGroupAlgebraCoeffQuotientStage R G I U :=
MonoidAlgebra.mapRangeRingHom (CompletedGroupAlgebraQuotient G U)
(Ideal.Quotient.mk I)The coefficient quotient map \(R[G/U]\) \(\to\) \((R/I)[G/U]\).
theorem completedGroupAlgebraStageCoeffQuotientMap_single
(I : Ideal R) (U : CompletedGroupAlgebraIndex G)
(q : CompletedGroupAlgebraQuotient G U) (r : R) :
completedGroupAlgebraStageCoeffQuotientMap R G I U (MonoidAlgebra.single q r) =
MonoidAlgebra.single q (Ideal.Quotient.mk I r)The coefficient-quotient map sends a singleton supported at a finite quotient class to the corresponding singleton with transformed coefficient and unchanged quotient support.
Show proof
by
exact MonoidAlgebra.mapRangeRingHom_single (Ideal.Quotient.mk I) q rProof. 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. 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 completedGroupAlgebraStageCoeffQuotientMap_surjective
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
Function.Surjective (completedGroupAlgebraStageCoeffQuotientMap R G I U)The finite-stage coefficient-quotient map is surjective; every target singleton is lifted by keeping the quotient support and lifting the coefficient.
Show proof
by
classical
intro x
induction x using Finsupp.induction with
| zero =>
exact ⟨0, map_zero (completedGroupAlgebraStageCoeffQuotientMap R G I U)⟩
| single_add q r x _ _ ih =>
rcases Ideal.Quotient.mk_surjective (I := I) r with ⟨a, ha⟩
rcases ih with ⟨y, hy⟩
refine ⟨(MonoidAlgebra.single q a : CompletedGroupAlgebraStage R G U) + y, ?_⟩
rw [map_add, completedGroupAlgebraStageCoeffQuotientMap_single, hy, ha]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. Surjectivity is obtained by lifting a representative through the underlying surjective quotient or group homomorphism and then checking the defining finite-stage formula. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□def groupAlgebraFiniteQuotientMap
(R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G]
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
MonoidAlgebra R G →+* CompletedGroupAlgebraCoeffQuotientStage R G I U :=
(completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
(completedGroupAlgebraStageMap R G U)The finite-quotient map \(R[G]\to (R/I)[G/U]\) used in Ribes--Zalesskii Section \(5.3\).
theorem groupAlgebraFiniteQuotientMap_single
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) (g : G) (r : R) :
groupAlgebraFiniteQuotientMap R G I U (MonoidAlgebra.single g r) =
MonoidAlgebra.single
(openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)
(Ideal.Quotient.mk I r)The finite quotient map on a group algebra sends a singleton \(r[g]\) to the singleton \(\bar r[\bar g]\) in \((R/I)[G/U]\).
Show proof
by
rw [groupAlgebraFiniteQuotientMap, RingHom.comp_apply,
completedGroupAlgebraStageMap_single, completedGroupAlgebraStageCoeffQuotientMap_single]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. 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. 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 groupAlgebraFiniteQuotientMap_of
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) (g : G) :
groupAlgebraFiniteQuotientMap R G I U (MonoidAlgebra.of R G g) =
MonoidAlgebra.of (R ⧸ I) (CompletedGroupAlgebraQuotient G U)
(openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)The finite quotient group-algebra map is computed by choosing representatives and applying the quotient map to supports.
Show proof
by
simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk,
groupAlgebraFiniteQuotientMap_single (R := R) (G := G) I U g (1 : R), map_one]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. 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. 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 groupAlgebraFiniteQuotientMap_eq_mapDomain_comp_mapRange
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
groupAlgebraFiniteQuotientMap R G I U =
(MonoidAlgebra.mapDomainRingHom (R ⧸ I)
(openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U)).comp
(MonoidAlgebra.mapRangeRingHom G (Ideal.Quotient.mk I))The quotient map \(R[G] \to (R/I)[G/U]\) factors equally as coefficient quotient followed by group quotient, or group quotient followed by coefficient quotient.
Show proof
by
simpa [groupAlgebraFiniteQuotientMap, completedGroupAlgebraStageCoeffQuotientMap,
completedGroupAlgebraStageMap] using
(MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom
(f := Ideal.Quotient.mk I)
(g := openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U))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. 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 groupAlgebraFiniteQuotientMap_surjective
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
Function.Surjective (groupAlgebraFiniteQuotientMap R G I U)Show proof
by
classical
intro x
induction x using Finsupp.induction with
| zero =>
exact ⟨0, map_zero (groupAlgebraFiniteQuotientMap R G I U)⟩
| single_add q r x _ _ ih =>
rcases openNormalSubgroupInClassProj_surjective
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U q with
⟨g, hg⟩
rcases Ideal.Quotient.mk_surjective (I := I) r with ⟨a, ha⟩
rcases ih with ⟨y, hy⟩
refine ⟨(MonoidAlgebra.single g a : MonoidAlgebra R G) + y, ?_⟩
rw [map_add, groupAlgebraFiniteQuotientMap_single, hy, hg, ha]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. Surjectivity is obtained by lifting a representative through the underlying surjective quotient or group homomorphism and then checking the defining finite-stage formula. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□def groupAlgebraFiniteQuotientKernel
(R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G]
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
Ideal (MonoidAlgebra R G) :=
RingHom.ker (groupAlgebraFiniteQuotientMap R G I U)The kernels used in Ribes--Zalesskii's natural topology on \(R[G]\); for the kernel-neighborhood topology this family is restricted to open ideals \(I\) and open normal subgroups \(U\).
theorem mem_groupAlgebraFiniteQuotientKernel_iff
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) :
x ∈ groupAlgebraFiniteQuotientKernel R G I U ↔
groupAlgebraFiniteQuotientMap R G I U x = 0Membership in the named kernel is equivalent to vanishing under its defining quotient or augmentation map.
Show proof
Iff.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. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). 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. 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 the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□theorem groupAlgebraFiniteQuotientKernel_eq_comap
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
groupAlgebraFiniteQuotientKernel R G I U =
Ideal.comap (completedGroupAlgebraStageMap R G U)
(RingHom.ker (completedGroupAlgebraStageCoeffQuotientMap R G I U))The kernel of the finite quotient group-algebra map is the comap of the corresponding quotient-kernel data.
Show proof
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. 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. 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.
□def completedGroupAlgebraCoeffQuotientTransition
(R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] {I J : Ideal R} (hIJ : I ≤ J)
(U : CompletedGroupAlgebraIndex G) :
CompletedGroupAlgebraCoeffQuotientStage R G I U →+*
CompletedGroupAlgebraCoeffQuotientStage R G J U :=
MonoidAlgebra.mapRangeRingHom (CompletedGroupAlgebraQuotient G U)
(Ideal.Quotient.factor hIJ)Coefficient transition \((R/I)[G/U]\) \(\to\) \((R/J)[G/U]\) induced by an inclusion \(I\le J\).
theorem completedGroupAlgebraCoeffQuotientTransition_single
{I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G)
(q : CompletedGroupAlgebraQuotient G U) (r : R ⧸ I) :
completedGroupAlgebraCoeffQuotientTransition R G hIJ U (MonoidAlgebra.single q r) =
MonoidAlgebra.single q (Ideal.Quotient.factor hIJ r)The finite-stage transition sends a singleton basis function to the singleton supported at its image in the coarser quotient.
Show proof
by
exact MonoidAlgebra.mapRangeRingHom_single (Ideal.Quotient.factor hIJ) q rProof. 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. 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 completedGroupAlgebraCoeffQuotientTransition_comp_stageCoeffQuotientMap
{I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G) :
(completedGroupAlgebraCoeffQuotientTransition R G hIJ U).comp
(completedGroupAlgebraStageCoeffQuotientMap R G I U) =
completedGroupAlgebraStageCoeffQuotientMap R G J UThe finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
rw [completedGroupAlgebraCoeffQuotientTransition,
completedGroupAlgebraStageCoeffQuotientMap, completedGroupAlgebraStageCoeffQuotientMap,
← MonoidAlgebra.mapRangeRingHom_comp]
simp only [Ideal.Quotient.factor_comp_mk]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. 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 completedGroupAlgebraCoeffQuotientTransition_surjective
{I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G) :
Function.Surjective (completedGroupAlgebraCoeffQuotientTransition R G hIJ U)The finite-stage transition map is surjective, with preimages obtained by lifting quotient representatives.
Show proof
by
classical
intro x
induction x using Finsupp.induction with
| zero =>
exact ⟨0, map_zero (completedGroupAlgebraCoeffQuotientTransition R G hIJ U)⟩
| single_add q r x _ _ ih =>
rcases Ideal.Quotient.factor_surjective hIJ r with ⟨a, ha⟩
rcases ih with ⟨y, hy⟩
refine ⟨(MonoidAlgebra.single q a :
CompletedGroupAlgebraCoeffQuotientStage R G I U) + y, ?_⟩
rw [map_add, completedGroupAlgebraCoeffQuotientTransition_single, hy, ha]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. Surjectivity is obtained by lifting a representative through the underlying surjective quotient or group homomorphism and then checking the defining finite-stage formula. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□def completedGroupAlgebraCoeffQuotientGroupTransition
(R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] (I : Ideal R) {U V : CompletedGroupAlgebraIndex G}
(hUV : U ≤ V) :
CompletedGroupAlgebraCoeffQuotientStage R G I V →+*
CompletedGroupAlgebraCoeffQuotientStage R G I U :=
MonoidAlgebra.mapDomainRingHom (R ⧸ I)
(OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)Group-quotient transition \((R/I)[G/V]\) \(\to\) \((R/I)[G/U]\) induced by \(U\le V\).
theorem completedGroupAlgebraCoeffQuotientGroupTransition_single
(I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
(q : CompletedGroupAlgebraQuotient G V) (r : R ⧸ I) :
completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV
(MonoidAlgebra.single q r) =
MonoidAlgebra.single
((OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) rThe finite-stage transition sends a singleton basis function to the singleton supported at its image in the coarser quotient.
Show proof
by
classical
simp only [completedGroupAlgebraCoeffQuotientGroupTransition, MonoidAlgebra.single,
MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
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. 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. 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 completedGroupAlgebraCoeffQuotientGroupTransition_comp_stageCoeffQuotientMap
(I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
(completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV).comp
(completedGroupAlgebraStageCoeffQuotientMap R G I V) =
(completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
(completedGroupAlgebraTransition R G hUV)The finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
rw [completedGroupAlgebraCoeffQuotientGroupTransition,
completedGroupAlgebraStageCoeffQuotientMap, completedGroupAlgebraStageCoeffQuotientMap,
completedGroupAlgebraTransition]
exact (MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom
(f := Ideal.Quotient.mk I)
(g := OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)).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, 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. 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 completedGroupAlgebraQuotientTransition_surjective
{U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
Function.Surjective
(OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)The finite-stage transition map is surjective, with preimages obtained by lifting quotient representatives.
Show proof
by
intro q
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)) q with
⟨g, rfl⟩
refine ⟨QuotientGroup.mk'
((((OrderDual.ofDual V).1 : OpenNormalSubgroup G) : Subgroup G)) g, rfl⟩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. Surjectivity is obtained by lifting a representative through the underlying surjective quotient or group homomorphism and then checking the defining finite-stage formula. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□theorem completedGroupAlgebraCoeffQuotientGroupTransition_surjective
(I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
Function.Surjective (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV)The finite-stage transition map is surjective, with preimages obtained by lifting quotient representatives.
Show proof
by
classical
intro x
induction x using Finsupp.induction with
| zero =>
exact ⟨0, map_zero (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV)⟩
| single_add q r x _ _ ih =>
rcases completedGroupAlgebraQuotientTransition_surjective
(G := G) hUV q with
⟨p, hp⟩
rcases ih with ⟨y, hy⟩
refine ⟨(MonoidAlgebra.single p r :
CompletedGroupAlgebraCoeffQuotientStage R G I V) + y, ?_⟩
rw [map_add, completedGroupAlgebraCoeffQuotientGroupTransition_single, hy, hp]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. Surjectivity is obtained by lifting a representative through the underlying surjective quotient or group homomorphism and then checking the defining finite-stage formula. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□def completedGroupAlgebraFiniteQuotientTransition
(R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] {I J : Ideal R} (hIJ : I ≤ J)
{U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
CompletedGroupAlgebraCoeffQuotientStage R G I V →+*
CompletedGroupAlgebraCoeffQuotientStage R G J U :=
(completedGroupAlgebraCoeffQuotientTransition R G hIJ U).comp
(completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV)The combined transition (R/I)[G/V] -> (R/J)[G/U].
theorem completedGroupAlgebraFiniteQuotientTransition_single
{I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
(hUV : U ≤ V) (q : CompletedGroupAlgebraQuotient G V) (r : R ⧸ I) :
completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV
(MonoidAlgebra.single q r) =
MonoidAlgebra.single
((OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q)
(Ideal.Quotient.factor hIJ r)The finite-stage transition sends a singleton basis function to the singleton supported at its image in the coarser quotient.
Show proof
by
rw [completedGroupAlgebraFiniteQuotientTransition, RingHom.comp_apply,
completedGroupAlgebraCoeffQuotientGroupTransition_single,
completedGroupAlgebraCoeffQuotientTransition_single]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. 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. 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 completedGroupAlgebraCoeffQuotientGroupTransition_comp_finiteQuotientMap
(I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
(completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV).comp
(groupAlgebraFiniteQuotientMap R G I V) =
groupAlgebraFiniteQuotientMap R G I UThe finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
rw [groupAlgebraFiniteQuotientMap_eq_mapDomain_comp_mapRange,
groupAlgebraFiniteQuotientMap_eq_mapDomain_comp_mapRange]
rw [completedGroupAlgebraCoeffQuotientGroupTransition, ← RingHom.comp_assoc,
← MonoidAlgebra.mapDomainRingHom_comp]
congr 1Proof. 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. 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 completedGroupAlgebraFiniteQuotientTransition_comp_finiteQuotientMap
{I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
(hUV : U ≤ V) :
(completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV).comp
(groupAlgebraFiniteQuotientMap R G I V) =
groupAlgebraFiniteQuotientMap R G J UThe finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
rw [completedGroupAlgebraFiniteQuotientTransition, RingHom.comp_assoc,
completedGroupAlgebraCoeffQuotientGroupTransition_comp_finiteQuotientMap]
rw [groupAlgebraFiniteQuotientMap, groupAlgebraFiniteQuotientMap]
rw [← RingHom.comp_assoc,
completedGroupAlgebraCoeffQuotientTransition_comp_stageCoeffQuotientMap]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. 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. 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 completedGroupAlgebraFiniteQuotientTransition_surjective
{I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
(hUV : U ≤ V) :
Function.Surjective (completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV)The finite-stage transition map is surjective, with preimages obtained by lifting quotient representatives.
Show proof
by
intro x
rcases completedGroupAlgebraCoeffQuotientTransition_surjective
(R := R) (G := G) hIJ U x with
⟨y, hy⟩
rcases completedGroupAlgebraCoeffQuotientGroupTransition_surjective
(R := R) (G := G) I hUV y with
⟨z, hz⟩
exact ⟨z, by rw [completedGroupAlgebraFiniteQuotientTransition, RingHom.comp_apply, hz, hy]⟩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. Surjectivity is obtained by lifting a representative through the underlying surjective quotient or group homomorphism and then checking the defining finite-stage formula. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□def completedGroupAlgebraFiniteQuotientProjection
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
[IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
Carrier R G →+*
CompletedGroupAlgebraCoeffQuotientStage R G I U :=
(completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
(completedGroupAlgebraProjectionRingHom R G U)
@[simp]The corresponding projection from the completed group algebra to \((R/I)[G/U]\).
theorem completedGroupAlgebraFiniteQuotientProjection_toCompletedGroupAlgebra
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
(completedGroupAlgebraFiniteQuotientProjection R G I U).comp
(toCompletedGroupAlgebraRingHom R G) =
groupAlgebraFiniteQuotientMap R G I UProjecting the canonical dense map to a finite quotient stage gives the corresponding stage map.
Show proof
by
apply RingHom.ext
intro x
rfl
@[simp]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. 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 completedGroupAlgebraFiniteQuotientProjection_apply_toCompletedGroupAlgebra
(I : Ideal R) (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) :
completedGroupAlgebraFiniteQuotientProjection R G I U
(toCompletedGroupAlgebra R G x) =
groupAlgebraFiniteQuotientMap R G I U xThe finite-quotient projection of the canonical dense element is computed by the associated quotient-stage map.
Show proof
rfl
@[simp 900]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. 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 completedGroupAlgebraFiniteQuotientTransition_comp_projection
{I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
(hUV : U ≤ V) :
(completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV).comp
(completedGroupAlgebraFiniteQuotientProjection R G I V) =
completedGroupAlgebraFiniteQuotientProjection R G J UThe finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
apply RingHom.ext
intro x
calc
completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV
(completedGroupAlgebraFiniteQuotientProjection R G I V x)
=
completedGroupAlgebraCoeffQuotientTransition R G hIJ U
(completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV
(completedGroupAlgebraStageCoeffQuotientMap R G I V
(completedGroupAlgebraProjection R G V x))) := rfl
_ =
completedGroupAlgebraCoeffQuotientTransition R G hIJ U
(completedGroupAlgebraStageCoeffQuotientMap R G I U
(completedGroupAlgebraTransition R G hUV
(completedGroupAlgebraProjection R G V x))) := by
have hstage := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraCoeffQuotientGroupTransition_comp_stageCoeffQuotientMap
(R := R) (G := G) I (U := U) (V := V) hUV))
(completedGroupAlgebraProjection R G V x)
exact congrArg (completedGroupAlgebraCoeffQuotientTransition R G hIJ U) hstage
_ =
completedGroupAlgebraCoeffQuotientTransition R G hIJ U
(completedGroupAlgebraStageCoeffQuotientMap R G I U
(completedGroupAlgebraProjection R G U x)) := by
rw [completedGroupAlgebraProjection_compatible (R := R) (G := G) x hUV]
_ =
completedGroupAlgebraStageCoeffQuotientMap R G J U
(completedGroupAlgebraProjection R G U x) := by
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraCoeffQuotientTransition_comp_stageCoeffQuotientMap
(R := R) (G := G) (I := I) (J := J) hIJ U))
(completedGroupAlgebraProjection R G U x)
_ = completedGroupAlgebraFiniteQuotientProjection R G J U x := 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. 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. 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. 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.
□