English
For submodules S ⊆ M and S' ⊆ M₂, the image of S × S' under coprod f g equals the join of the images of S under f and S' under g.
Русский
Для подмодулей S ⊆ M и S' ⊆ M₂ образ coprod f g на S × S' равен объединению изображений S под f и S' под g.
LaTeX
$$$ (Submodule.prod S S').map (coprod f g) = S.map f \\sqcup S'.map g $$$
Lean4
@[simp]
theorem coprod_map_prod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : Submodule R M) (S' : Submodule R M₂) :
(Submodule.prod S S').map (LinearMap.coprod f g) = S.map f ⊔ S'.map g :=
SetLike.coe_injective <|
by
simp only [LinearMap.coprod_apply, Submodule.coe_sup, Submodule.map_coe]
rw [← Set.image2_add, Set.image2_image_left, Set.image2_image_right]
exact Set.image_prod fun m m₂ => f m + g m₂
