English
Let f,g be linear endomaps on a module M over a semiring, and suppose they commute (fg = gf). If p is a submodule of M and f and g preserve p (i.e., f(p) ⊆ p and g(p) ⊆ p), then the restrictions of f and g to p also commute on p.
Русский
Пусть f и g — линейные отображения M → M над полем, которые коммутируют (fg = gf). Пусть p — подпространство M, причём f(p) ⊆ p и g(p) ⊆ p. Тогда ограничения f|_p и g|_p на p также коммутаторы на p.
LaTeX
$$$(fg = gf) \\wedge (f(p) \\subseteq p) \\wedge (g(p) \\subseteq p) \\\\Rightarrow (f|_p) \\circ (g|_p) = (g|_p) \\circ (f|_p) \\text{ as maps } p \\to p.$$$
Lean4
theorem restrict_commute {f g : M →ₗ[R] M} (h : Commute f g) {p : Submodule R M} (hf : MapsTo f p p)
(hg : MapsTo g p p) : Commute (f.restrict hf) (g.restrict hg) :=
by
change (f ∘ₗ g).restrict (hf.comp hg) = (g ∘ₗ f).restrict (hg.comp hf)
congr 1
