English
Let f: M →ₛₗ[σ] M₂ and g: M₂ →ₛₗ[τ] M₃ be semilinear maps with suitable surjectivity. Then the image of p under the composed map equals the image under g of the image under f, i.e., map (g ∘ f) p = map g (map f p).
Русский
Пусть f: M →ₛₗ[σ] M₂ и g: M₂ →ₛₗ[τ] M₃ — полуприводимые отображения с подходящей сурьективностью. Тогда образ p под композиции равен образу под g от образа под f: map (g ∘ f) p = map g (map f p).
LaTeX
$$$\\operatorname{map}(g\\circ f)\,p = \\operatorname{map} g (\\operatorname{map} f\\,p)$$$
Lean4
theorem map_comp [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃)
(p : Submodule R M) : map (g.comp f : M →ₛₗ[σ₁₃] M₃) p = map g (map f p) :=
SetLike.coe_injective <| by simp only [← image_comp, map_coe, LinearMap.coe_comp, comp_apply]
