English
If H is p-group and φ: K → G, and ker φ is p-group, then H.comap φ is p-group.
Русский
Если H — p-группа и φ: K → G, и ker φ — p-группа, то H.comap φ — p-группа.
LaTeX
$$$\IsPGroup(p,H) \rightarrow (\varphi : K \to^* G) \rightarrow IsPGroup(p) (H.comap \varphi)$$$
Lean4
theorem comap_of_ker_isPGroup {H : Subgroup G} (hH : IsPGroup p H) {K : Type*} [Group K] (ϕ : K →* G)
(hϕ : IsPGroup p ϕ.ker) : IsPGroup p (H.comap ϕ) := by
intro g
obtain ⟨j, hj⟩ := hH ⟨ϕ g.1, g.2⟩
rw [Subtype.ext_iff, H.coe_pow, Subtype.coe_mk, ← ϕ.map_pow] at hj
obtain ⟨k, hk⟩ := hϕ ⟨g.1 ^ p ^ j, hj⟩
rw [Subtype.ext_iff, ϕ.ker.coe_pow, Subtype.coe_mk, ← pow_mul, ← pow_add] at hk
exact ⟨j + k, by rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]⟩
