FoxDifferential/Completed/DifferentialModule/Map/GroupLike.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/GroupLike.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]
29omit [Fact (0 < ℓ)] in
30/-- Evaluation formula for primePowerCompletedGroupAlgebraMap_of. -/
31@[simp]
33 (ψ : ContinuousMonoidHom G H) (g : G) :
34 primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
35 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := G) g) =
36 primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := H) (ψ g) := by
37 apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
38 intro i
39 change primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := H) i
40 (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
41 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := G) g)) =
42 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := H) i
43 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := H) (ψ g))
48 rfl
51end
53end FoxDifferential