CompletedGroupAlgebra.InClassFunctoriality.Maps
Completed Group Algebra / Functoriality Within a Class / Maps.
def completedGroupAlgebraMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
(φ : G →* H) (hφ : Continuous φ) :
CompletedGroupAlgebraInClass C hC R G →+* CompletedGroupAlgebraInClass C hC R H where
toFun x := ⟨fun V =>
completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x), by
intro V W hVW
change completedGroupAlgebraTransitionInClass C R H hVW
(completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ W
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W) x)) =
completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
have hcomp := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraFunctorialStageMapInClass_transition
(R := R) (G := G) (H := H) C hHer φ hφ hVW))
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W) x)
rw [RingHom.comp_apply, RingHom.comp_apply] at hcomp
rw [← completedGroupAlgebraProjectionInClass_compatible
(R := R) (G := G) C hC
(completedGroupAlgebraComapIndexInClass_mono
(G := G) (H := H) C hHer φ hφ hVW) x]
exact hcomp⟩
map_zero' := by
apply (completedGroupAlgebraSystemInClass C hC R H).ext
intro V
exact map_zero (completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V)
map_one' := by
apply (completedGroupAlgebraSystemInClass C hC R H).ext
intro V
exact map_one (completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V)
map_add' x y := by
apply (completedGroupAlgebraSystemInClass C hC R H).ext
intro V
exact map_add (completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V)
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) y)
map_mul' x y := by
apply (completedGroupAlgebraSystemInClass C hC R H).ext
intro V
exact map_mul (completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V)
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) y)A continuous homomorphism of groups induces a ring homomorphism on \(C\)-indexed completed group algebras, when \(C\) is hereditary.
theorem completedGroupAlgebraProjectionInClass_map
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ)
(V : CompletedGroupAlgebraIndexInClass H C) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraProjectionInClass C hC R H V
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x) =
completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)The in-class completed group-algebra map is characterized by its finite-stage projections.
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. 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. 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.
□def completedGroupAlgebraMapAlgHomInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
(φ : G →* H) (hφ : Continuous φ) :
CompletedGroupAlgebraInClass C hC R G →ₐ[R] CompletedGroupAlgebraInClass C hC R H where
toRingHom := completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
commutes' := by
intro r
apply (completedGroupAlgebraSystemInClass C hC R H).ext
intro V
change completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V
(algebraMap R
(CompletedGroupAlgebraStageInClass C R G
(completedGroupAlgebraComapIndexInClass
(G := G) (H := H) C hHer φ hφ V)) r) =
algebraMap R (CompletedGroupAlgebraStageInClass C R H V) r
exact completedGroupAlgebraFunctorialStageMapInClass_algebraMap
(R := R) (G := G) (H := H) C hHer φ hφ V rCoefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.
theorem completedGroupAlgebraMapAlgHomInClass_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ x =
completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ xThe bundled algebra homomorphism has the same underlying function as the coordinatewise construction.
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, 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. 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 continuous_completedGroupAlgebraMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) :
Continuous (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ)The induced \(C\)-indexed completed-group-algebra map is continuous.
Show proof
by
let A := CompletedGroupAlgebraInClass C hC R G
let S := completedGroupAlgebraSystemInClass C hC R H
letI : ∀ V : CompletedGroupAlgebraIndexInClass H C,
TopologicalSpace (CompletedGroupAlgebraStageInClass C R H V) :=
fun V => S.topologicalSpace V
have hval : Continuous fun x : A =>
((completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x) :
(V : CompletedGroupAlgebraIndexInClass H C) → S.X V) := by
change Continuous fun x : A =>
fun V : CompletedGroupAlgebraIndexInClass H C =>
completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
apply continuous_pi
intro V
letI : TopologicalSpace
(CompletedGroupAlgebraStageInClass C R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) :=
(completedGroupAlgebraSystemInClass C hC R G).topologicalSpace
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
exact (continuous_completedGroupAlgebraFunctorialStageMapInClass
(R := R) (G := G) (H := H) C hC hHer φ hφ V).comp
((completedGroupAlgebraSystemInClass C hC R G).continuous_projection
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
exact Continuous.subtype_mk hval fun x =>
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x).2Proof. 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 completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) :
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ).comp
(toCompletedGroupAlgebraInClassRingHom C hC R G) =
(toCompletedGroupAlgebraInClassRingHom C hC R H).comp
(MonoidAlgebra.mapDomainRingHom R φ)The in-class completed group-algebra map composes with the dense abstract map as expected.
Show proof
by
apply RingHom.ext
intro x
apply (completedGroupAlgebraSystemInClass C hC R H).ext
intro V
have hstage := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraFunctorialStageMapInClass_comp_stageMap
(R := R) (G := G) (H := H) C hHer φ hφ V))
x
change completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V
(completedGroupAlgebraStageMapInClass C R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x) =
completedGroupAlgebraStageMapInClass C R H V (MonoidAlgebra.mapDomainRingHom R φ x)
exact hstageProof. 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. 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. 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.
□theorem completedGroupAlgebraMapInClass_surjective_of_surjective
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hR : IsProfiniteRing R) (hH : IsProCGroup C H)
(φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ) :
Function.Surjective
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ)A surjective continuous homomorphism onto a pro-\(C\) group induces a surjective map on \(C\)-indexed completed group algebras.
Show proof
by
let f := completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
letI : CompactSpace (CompletedGroupAlgebraInClass C hC R G) :=
completedGroupAlgebraInClass_compactSpace (R := R) (G := G) C hC hR
letI : T2Space (CompletedGroupAlgebraInClass C hC R H) :=
completedGroupAlgebraInClass_t2Space (R := R) (G := H) C hC hR
have hfcont : Continuous f :=
continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := H)
C hC hHer φ hφ
have hclosed : IsClosed (Set.range f) := (isCompact_range hfcont).isClosed
have hdense : DenseRange (toCompletedGroupAlgebraInClassRingHom C hC R H) := by
change DenseRange (toCompletedGroupAlgebraInClass C hC R H)
exact denseRange_toCompletedGroupAlgebraInClass (R := R) (G := H) C hC hForm hH
have hcanonical_subset :
Set.range (toCompletedGroupAlgebraInClassRingHom C hC R H) ⊆ Set.range f := by
intro y hy
rcases hy with ⟨a, rfl⟩
rcases (show Function.Surjective (MonoidAlgebra.mapDomainRingHom R φ) from by
simpa [MonoidAlgebra.mapDomainRingHom_apply] using
(Finsupp.mapDomain_surjective (M := R) hφsurj)) a with
⟨b, hb⟩
refine ⟨toCompletedGroupAlgebraInClassRingHom C hC R G b, ?_⟩
have hcomp := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
(R := R) (G := G) (H := H) C hC hHer φ hφ))
b
simpa [f, RingHom.comp_apply, hb] using hcomp
intro y
have hycanonical :
y ∈ closure (Set.range (toCompletedGroupAlgebraInClassRingHom C hC R H)) := by
rw [hdense.closure_range]
exact Set.mem_univ y
have hyf : y ∈ closure (Set.range f) :=
closure_mono hcanonical_subset hycanonical
exact hclosed.closure_subset_iff.2 (fun z hz => hz) hyfProof. 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. 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. 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. 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 completedGroupAlgebraInClassRingHom_ext_of_comp_toCompleted
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hR : IsProfiniteRing R) (hG : IsProCGroup C G)
{f g : CompletedGroupAlgebraInClass C hC R G →+*
CompletedGroupAlgebraInClass C hC R H}
(hf : Continuous f) (hg : Continuous g)
(hfg : f.comp (toCompletedGroupAlgebraInClassRingHom C hC R G) =
g.comp (toCompletedGroupAlgebraInClassRingHom C hC R G)) :
f = gContinuous ring homomorphisms out of \(\widehat{R[G]}_C\) are determined by their values on the dense abstract group algebra.
Show proof
by
letI : T2Space (CompletedGroupAlgebraInClass C hC R H) :=
completedGroupAlgebraInClass_t2Space (R := R) (G := H) C hC hR
have hdense : DenseRange (toCompletedGroupAlgebraInClassRingHom C hC R G) := by
change DenseRange (toCompletedGroupAlgebraInClass C hC R G)
exact denseRange_toCompletedGroupAlgebraInClass (R := R) (G := G) C hC hForm hG
have hcomp : (f : CompletedGroupAlgebraInClass C hC R G →
CompletedGroupAlgebraInClass C hC R H) ∘
(toCompletedGroupAlgebraInClassRingHom C hC R G) =
(g : CompletedGroupAlgebraInClass C hC R G →
CompletedGroupAlgebraInClass C hC R H) ∘
(toCompletedGroupAlgebraInClassRingHom C hC R G) := by
funext x
exact congrFun (congrArg DFunLike.coe hfg) x
have hfun : (f : CompletedGroupAlgebraInClass C hC R G →
CompletedGroupAlgebraInClass C hC 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 completedGroupAlgebraMapInClass_id
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hR : IsProfiniteRing R) (hG : IsProCGroup C G) :
completedGroupAlgebraMapInClass (G := G) (H := G) C hC hHer R
(MonoidHom.id G) continuous_id =
RingHom.id (CompletedGroupAlgebraInClass C hC R G)Identity law for the \(C\)-indexed completed-group-algebra functor.
Show proof
by
apply completedGroupAlgebraInClassRingHom_ext_of_comp_toCompleted
(R := R) (G := G) (H := G) C hC hForm hR hG
· exact continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := G)
C hC hHer (MonoidHom.id G) continuous_id
· exact continuous_id
· rw [completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass,
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. 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. 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.
□theorem completedGroupAlgebraMapAlgHomInClass_id
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hR : IsProfiniteRing R) (hG : IsProCGroup C G) :
completedGroupAlgebraMapAlgHomInClass (G := G) (H := G) C hC hHer R
(MonoidHom.id G) continuous_id =
AlgHom.id R (CompletedGroupAlgebraInClass C hC R G)Identity law for the \(C\)-indexed completed-group-algebra functor, as an \(R\)-algebra homomorphism.
Show proof
by
apply AlgHom.ext
intro x
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMapInClass_id (R := R) (G := G) C hC hForm hHer 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. 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. 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.
□theorem completedGroupAlgebraMapInClass_comp
{K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hR : IsProfiniteRing R) (hG : IsProCGroup C G)
(φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
(completedGroupAlgebraMapInClass (G := H) (H := K) C hC hHer R ψ hψ).comp
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ) =
completedGroupAlgebraMapInClass (G := G) (H := K) C hC hHer R
(ψ.comp φ) (hψ.comp hφ)Composition law for the \(C\)-indexed completed-group-algebra functor.
Show proof
by
apply completedGroupAlgebraInClassRingHom_ext_of_comp_toCompleted
(R := R) (G := G) (H := K) C hC hForm hR hG
· exact (continuous_completedGroupAlgebraMapInClass (R := R) (G := H) (H := K)
C hC hHer ψ hψ).comp
(continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := H)
C hC hHer φ hφ)
· exact continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := K)
C hC hHer (ψ.comp φ) (hψ.comp hφ)
· apply RingHom.ext
intro x
have hφdense := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
(R := R) (G := G) (H := H) C hC hHer φ hφ))
x
have hψdense := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
(R := R) (G := H) (H := K) C hC hHer ψ hψ))
(MonoidAlgebra.mapDomainRingHom R φ x)
have hdomain := congrFun
(congrArg DFunLike.coe
(finiteGroupAlgebra_mapDomainRingHom_comp R G H K φ ψ))
x
have hcompdense := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
(R := R) (G := G) (H := K) C hC hHer (ψ.comp φ) (hψ.comp hφ)))
x
calc
(((completedGroupAlgebraMapInClass (G := H) (H := K) C hC hHer R ψ hψ).comp
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ)).comp
(toCompletedGroupAlgebraInClassRingHom C hC R G)) x
=
completedGroupAlgebraMapInClass (G := H) (H := K) C hC hHer R ψ hψ
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
(toCompletedGroupAlgebraInClassRingHom C hC R G x)) := rfl
_ =
completedGroupAlgebraMapInClass (G := H) (H := K) C hC hHer R ψ hψ
(toCompletedGroupAlgebraInClassRingHom C hC R H
(MonoidAlgebra.mapDomainRingHom R φ x)) := by
have hφdense' :
completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
(toCompletedGroupAlgebraInClassRingHom C hC R G x) =
toCompletedGroupAlgebraInClassRingHom C hC R H
(MonoidAlgebra.mapDomainRingHom R φ x) := by
simpa [RingHom.comp_apply] using hφdense
exact congrArg (completedGroupAlgebraMapInClass (G := H) (H := K)
C hC hHer R ψ hψ) hφdense'
_ =
toCompletedGroupAlgebraInClassRingHom C hC R K
(MonoidAlgebra.mapDomainRingHom R ψ (MonoidAlgebra.mapDomainRingHom R φ x)) := by
simpa [RingHom.comp_apply] using hψdense
_ =
toCompletedGroupAlgebraInClassRingHom C hC R K
(MonoidAlgebra.mapDomainRingHom R (ψ.comp φ) x) := by
exact congrArg (toCompletedGroupAlgebraInClassRingHom C hC R K) (by
change (MonoidAlgebra.mapDomainRingHom R ψ)
((MonoidAlgebra.mapDomainRingHom R φ) x) =
(MonoidAlgebra.mapDomainRingHom R (ψ.comp φ)) x at hdomain
exact hdomain)
_ =
((completedGroupAlgebraMapInClass (G := G) (H := K) C hC hHer R
(ψ.comp φ) (hψ.comp hφ)).comp
(toCompletedGroupAlgebraInClassRingHom C hC R G)) x := by
simpa [RingHom.comp_apply] using hcompdense.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. 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 completedGroupAlgebraMapAlgHomInClass_comp
{K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hR : IsProfiniteRing R) (hG : IsProCGroup C G)
(φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
(completedGroupAlgebraMapAlgHomInClass (G := H) (H := K) C hC hHer R ψ hψ).comp
(completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ) =
completedGroupAlgebraMapAlgHomInClass (G := G) (H := K) C hC hHer R
(ψ.comp φ) (hψ.comp hφ)Composition law for the \(C\)-indexed completed-group-algebra functor, as an \(R\)-algebra homomorphism.
Show proof
by
apply AlgHom.ext
intro x
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMapInClass_comp (R := R) (G := G) (H := H) (K := K)
C hC hForm hHer hR hG φ hφ ψ hψ))
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.
□theorem completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_of
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (g : G) :
completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
(toCompletedGroupAlgebraInClass C hC R G (MonoidAlgebra.of R G g)) =
toCompletedGroupAlgebraInClass C hC R H (MonoidAlgebra.of R H (φ g))The in-class completed group-algebra map sends group-like elements to group-like elements.
Show proof
by
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
(R := R) (G := G) (H := H) C hC hHer φ hφ))
(MonoidAlgebra.of R G g)
simpa [RingHom.comp_apply, finiteGroupAlgebra_mapDomainRingHom_of] 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. 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 completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_sub_one_of
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (g : G) :
completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
(toCompletedGroupAlgebraInClass C hC R G (MonoidAlgebra.of R G g) - 1) =
toCompletedGroupAlgebraInClass C hC R H (MonoidAlgebra.of R H (φ g)) - 1The in-class completed group-algebra map sends group-like augmentation generators to their images.
Show proof
by
rw [map_sub, completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_of, 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, 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. 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\). 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. 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.
□