CompletedGroupAlgebra/AllFiniteFunctoriality/Surjectivity.lean
1import CompletedGroupAlgebra.AllFiniteFunctoriality.Map
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/AllFiniteFunctoriality/Surjectivity.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Surjectivity for completed group algebra functorial maps
13-/
15open scoped Topology
17namespace CompletedGroupAlgebra
19noncomputable section
21open ProCGroups
22open ProCGroups.ProC
24universe u v w
26variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
27variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30/-- A surjective continuous homomorphism of profinite groups induces a surjective map on
31completed group algebras. -/
33 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
34 (hH : ProCGroups.IsProfiniteGroup H) (φ : G →* H) (hφ : Continuous φ)
35 (hφsurj : Function.Surjective φ) :
36 Function.Surjective (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ) := by
37 let f := completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
38 letI : CompactSpace (Carrier R G) :=
39 completedGroupAlgebra_compactSpace (R := R) (G := G) hR
40 letI : T2Space (Carrier R H) :=
41 completedGroupAlgebra_t2Space (R := R) (G := H) hR
42 have hfcont : Continuous f :=
43 continuous_completedGroupAlgebraMap (R := R) (G := G) (H := H) hG φ hφ
44 have hclosed : IsClosed (Set.range f) := (isCompact_range hfcont).isClosed
45 have hdense : DenseRange (toCompletedGroupAlgebraRingHom R H) :=
46 denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := H) hH
47 have hcanonical_subset :
48 Set.range (toCompletedGroupAlgebraRingHom R H) ⊆ Set.range f := by
49 intro y hy
50 rcases hy with ⟨a, rfl⟩
51 rcases (show Function.Surjective (MonoidAlgebra.mapDomainRingHom R φ) from by
52 simpa [MonoidAlgebra.mapDomainRingHom_apply] using
53 (Finsupp.mapDomain_surjective (M := R) hφsurj)) a with
54 ⟨b, hb⟩
55 refine ⟨toCompletedGroupAlgebraRingHom R G b, ?_⟩
56 have hcomp := congrFun
57 (congrArg DFunLike.coe
59 (R := R) (G := G) (H := H) hG φ 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