CompletedGroupAlgebra.AllFiniteFunctoriality.Surjectivity
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 completedGroupAlgebraMap_surjective_of_surjective
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
(hH : ProCGroups.IsProfiniteGroup H) (φ : G →* H) (hφ : Continuous φ)
(hφsurj : Function.Surjective φ) :
Function.Surjective (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)A surjective continuous homomorphism of profinite groups induces a surjective map on completed group algebras.
Show proof
by
let f := completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
letI : CompactSpace (Carrier R G) :=
completedGroupAlgebra_compactSpace (R := R) (G := G) hR
letI : T2Space (Carrier R H) :=
completedGroupAlgebra_t2Space (R := R) (G := H) hR
have hfcont : Continuous f :=
continuous_completedGroupAlgebraMap (R := R) (G := G) (H := H) hG φ hφ
have hclosed : IsClosed (Set.range f) := (isCompact_range hfcont).isClosed
have hdense : DenseRange (toCompletedGroupAlgebraRingHom R H) :=
denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := H) hH
have hcanonical_subset :
Set.range (toCompletedGroupAlgebraRingHom 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 ⟨toCompletedGroupAlgebraRingHom R G b, ?_⟩
have hcomp := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMap_comp_toCompletedGroupAlgebra
(R := R) (G := G) (H := H) hG φ hφ))
b
simpa [f, RingHom.comp_apply, hb] using hcomp
intro y
have hycanonical : y ∈ closure (Set.range (toCompletedGroupAlgebraRingHom 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.
□