Source: ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Surjectivity
1import ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Map
2import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison
4/-!
5# Surjectivity of completed group-algebra maps
7A surjective continuous group homomorphism induces a surjective map of all-finite completed group
8algebras. The proof combines finite-stage surjectivity with the inverse-limit lifting argument.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
20universe u v w
22variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
23variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
26/--
27A surjective continuous homomorphism of profinite groups induces a surjective map on completed
28group algebras.
29-/
30theorem completedGroupAlgebraMap_surjective_of_surjective
31 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
32 (φ : G →* H) (hφ : Continuous φ)
33 (hφsurj : Function.Surjective φ) :
34 Function.Surjective (completedGroupAlgebraMap (G := G) (H := H) R φ hφ) := by
35 let f := completedGroupAlgebraMap (G := G) (H := H) R φ hφ
36 letI : CompactSpace (CompletedGroupAlgebraCarrier R G) :=
37 completedGroupAlgebra_compactSpace (R := R) (G := G)
38 letI : T2Space (CompletedGroupAlgebraCarrier R H) :=
39 completedGroupAlgebra_t2Space (R := R) (G := H)
40 have hfcont : Continuous f :=
41 continuous_completedGroupAlgebraMap (R := R) (G := G) (H := H) φ hφ
42 have hclosed : IsClosed (Set.range f) := (isCompact_range hfcont).isClosed
43 have hdense : DenseRange (toCompletedGroupAlgebraRingHom R H) :=
44 denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := H)
45 have hcanonical_subset :
46 Set.range (toCompletedGroupAlgebraRingHom R H) ⊆ Set.range f := by
47 intro y hy
48 rcases hy with ⟨a, rfl⟩
49 obtain ⟨bCoeff, hbCoeff⟩ :=
50 Finsupp.mapDomain_surjective (M := R) hφsurj a.coeff
51 let b : MonoidAlgebra R G := MonoidAlgebra.ofCoeff bCoeff
52 have hb : MonoidAlgebra.mapDomainRingHom R φ b = a := by
53 apply MonoidAlgebra.coeff_injective
54 exact hbCoeff
55 refine ⟨toCompletedGroupAlgebraRingHom R G b, ?_⟩
56 have hcomp := congrFun
57 (congrArg DFunLike.coe
58 (completedGroupAlgebraMap_comp_toCompletedGroupAlgebra
59 (R := R) (G := G) (H := H) φ hφ))
60 b
61 simpa [f, RingHom.comp_apply, hb] using hcomp
62 intro y
63 have hycanonical : y ∈ closure (Set.range (toCompletedGroupAlgebraRingHom R H)) := by
64 rw [hdense.closure_range]
65 exact Set.mem_univ y
66 have hyf : y ∈ closure (Set.range f) :=
67 closure_mono hcanonical_subset hycanonical
68 exact hclosed.closure_subset_iff.2 (fun z hz => hz) hyf
70end
72end CompletedGroupAlgebra