English
Let S ⊆ M and S' ⊆ M2 be submodules. The preimage under the product map f.prodMap g of the product S × S' equals the product of the preimages: (S × S') comap (f × g) = (S comap f) × (S' comap g).
Русский
Пусть S ⊆ M и S' ⊆ M₂ — подмодули. Предобразие по произведению отображений f.prodMap g от S × S' равно произведению предобразований: (S × S') comap (f × g) = (S comap f) × (S' comap g).
LaTeX
$$$ (S \\text{ prod } S').comap (f \\text{ prodMap } g) = (S\\.comap f) \\text{.prod} (S'\\.comap g). $$$
Lean4
theorem prodMap_comap_prod (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) (S : Submodule R M₂) (S' : Submodule R M₄) :
(Submodule.prod S S').comap (LinearMap.prodMap f g) = (S.comap f).prod (S'.comap g) :=
SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _
