Source: ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.GroupLike
1import ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Limit
3/-!
4# Fox differential: completed — differential module — map — group like
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraMap_of`
9 The completed prime-power group-algebra map sends the group-like element of `g` to the group-like
10 element of `ψ g`.
11-/
13namespace FoxDifferential
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
20universe u v
22variable (ℓ : ℕ) [Fact (0 < ℓ)]
23variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
26omit [Fact (0 < ℓ)] in
27/--
28The completed prime-power group-algebra map sends the group-like element of `g` to the group-like
29element of `ψ g`.
30-/
31@[simp]
32theorem primePowerCompletedGroupAlgebraMap_of
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))
44 rw [primePowerCompletedGroupAlgebraProjection_map,
45 primePowerCompletedGroupAlgebraProjection_of,
46 primePowerCompletedGroupAlgebraMapStage_of,
47 primePowerCompletedGroupAlgebraProjection_of]
48 rfl
51end
53end FoxDifferential