FoxDifferential/Completed/DifferentialModule/Map/Surjective.lean
1import FoxDifferential.Completed.DifferentialModule.Map.Limit
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/DifferentialModule/Map/Surjective.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed differential modules
14The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups
21open ProCGroups.ProC
23universe u v
25variable (ℓ : ℕ) [Fact (0 < ℓ)]
26variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
27variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
29/-- If `ψ : G → H` is surjective, then the induced map of prime-power completed group algebras
32inverse-limit projections. -/
34 (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ) :
35 Function.Surjective
36 (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ) := by
37 classical
38 let S := primePowerCompletedGroupAlgebraSystem ℓ H
39 let T := primePowerCompletedGroupAlgebraSystem ℓ G
40 let f : PrimePowerCompletedGroupAlgebra ℓ G → PrimePowerCompletedGroupAlgebra ℓ H :=
41 primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
42 letI : Nonempty (PrimePowerCompletedGroupAlgebraIndex H) :=
43 ⟨(0, _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex H)⟩
44 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, TopologicalSpace (S.X i) :=
45 fun i => S.topologicalSpace i
46 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, DiscreteTopology (S.X i) :=
47 fun _ => ⟨rfl⟩
48 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, CompactSpace (S.X i) :=
49 fun i => by
50 letI : Finite (S.X i) := by
51 dsimp [S, primePowerCompletedGroupAlgebraSystem]
52 infer_instance
53 letI : Fintype (S.X i) := Fintype.ofFinite _
54 infer_instance
55 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, T2Space (S.X i) :=
56 fun _ => inferInstance
57 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, TopologicalSpace (T.X i) :=
58 fun i => T.topologicalSpace i
59 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, DiscreteTopology (T.X i) :=
60 fun _ => ⟨rfl⟩
61 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, CompactSpace (T.X i) :=
62 fun i => by
63 letI : Finite (T.X i) := by
64 dsimp [T, primePowerCompletedGroupAlgebraSystem]
65 infer_instance
66 letI : Fintype (T.X i) := Fintype.ofFinite _
67 infer_instance
68 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, T2Space (T.X i) :=
69 fun _ => inferInstance
70 letI : CompactSpace (PrimePowerCompletedGroupAlgebra ℓ G) :=
71 inferInstance
72 letI : T2Space (PrimePowerCompletedGroupAlgebra ℓ H) :=
73 S.t2Space_inverseLimit
74 have hf_continuous : Continuous f :=
75 continuous_primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
76 have hclosed : IsClosed (Set.range f) :=
77 (isCompact_range hf_continuous).isClosed
78 have hprojection_images :
79 ∀ i : PrimePowerCompletedGroupAlgebraIndex H,
80 S.projection i '' Set.range f =
81 S.projection i '' (Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H)) := by
82 intro i
83 apply Set.Subset.antisymm
84 · rintro z ⟨y, _hy, rfl⟩
85 exact ⟨y, trivial, rfl⟩
86 · rintro z ⟨y, _hy, rfl⟩
88 (ℓ := ℓ) (G := G) (H := H) ψ hψ i (S.projection i y) with
89 ⟨c, hc⟩
90 let sourceIndex : PrimePowerCompletedGroupAlgebraIndex G :=
91 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)
93 (ℓ := ℓ) (G := G) sourceIndex c with
94 ⟨x, hx⟩
95 refine ⟨f x, ⟨x, rfl⟩, ?_⟩
96 change primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := H) i
97 (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ x) =
98 S.projection i y
100 change primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
101 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) sourceIndex x) =
102 S.projection i y
103 rw [hx, hc]
104 have hclosure :
105 closure (Set.range f) =
106 (Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H)) := by
107 have hclosure' :
108 closure (Set.range f) =
109 closure (Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H)) :=
110 S.closure_eq_of_projection_images_eq_of_subsets
111 (directed_primePowerCompletedGroupAlgebraIndex (G := H))
112 (Set.range f)
113 (Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H))
114 hprojection_images
115 simpa using hclosure'
116 intro y
117 have hy_closure : y ∈ closure (Set.range f) := by
118 rw [hclosure]
119 simp only [Set.mem_univ]
120 have hy_range : y ∈ Set.range f := by
121 rwa [hclosed.closure_eq] at hy_closure
122 rcases hy_range with ⟨x, hx⟩
123 exact ⟨x, hx⟩
125/-- A choice of a lift along a surjective completed group-algebra map.
127This is intentionally kept at the completed group-algebra level: it uses the already-proved
128surjectivity of `Λ_G -> Λ_H`, and does not touch the displayed differential premodule topology. -/
130 (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
131 (a : PrimePowerCompletedGroupAlgebra ℓ H) :
133 Classical.choose
135 (ℓ := ℓ) (G := G) (H := H) ψ hψ a)
137/-- The chosen lift maps back to the target coefficient. -/
138@[simp]
140 (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
141 (a : PrimePowerCompletedGroupAlgebra ℓ H) :
142 primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
144 (ℓ := ℓ) (G := G) (H := H) ψ hψ a) = a :=
145 Classical.choose_spec
147 (ℓ := ℓ) (G := G) (H := H) ψ hψ a)
149end
151end FoxDifferential