English
Let f: G → N and g: G' → N' be homomorphisms, and S ≤ N, S' ≤ N'. Then the preimage of S × S' under the product map equals the product of the preimages.
Русский
Пусть f: G → N и g: G' → N' — гомоморфизмы, S ⊆ N и S' ⊆ N'. Тогда предобраз S × S' по отображению prodMap равен произведению их предобразов.
LaTeX
$$$ (S \\times S') \\\\mathrm{comap} (\\\\mathrm{prodMap}(f,g)) = (S \\\\mathrm{comap} f) \\\\mathrm{prod} (S' \\\\mathrm{comap} g) $$$
Lean4
@[to_additive prodMap_comap_prod]
theorem prodMap_comap_prod {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') (S : Subgroup N)
(S' : Subgroup N') : (S.prod S').comap (prodMap f g) = (S.comap f).prod (S'.comap g) :=
SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _
