English
If p is invariant under f and g, and a map h sends maxGenEigenspace of g to maxGenEigenspace of g, then the restriction of f to p preserves the corresponding maxGenEigenspace structure.
Русский
Если p инвариантно по отношению к f и g, и отображение h переводит maxGenEigenspace g μ1 в maxGenEigenspace g μ2, то ограничение f на p сохраняет соответствующую структуру maxGenEigenspace.
LaTeX
$$$\\text{MapsTo} (f|_p)\\big(\\text{maxGenEigenspace}(g|_p)\\mu_1\\big) = \\text{maxGenEigenspace}(g|_p)\\mu_2$$$
Lean4
theorem mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo {p : Submodule R M} (f g : End R M) (hf : MapsTo f p p)
(hg : MapsTo g p p) {μ₁ μ₂ : R} (h : MapsTo f (g.maxGenEigenspace μ₁) (g.maxGenEigenspace μ₂)) :
MapsTo (f.restrict hf) (maxGenEigenspace (g.restrict hg) μ₁) (maxGenEigenspace (g.restrict hg) μ₂) :=
by
intro x hx
simp_rw [SetLike.mem_coe, mem_maxGenEigenspace, ← LinearMap.restrict_smul_one _, LinearMap.restrict_sub _,
Module.End.pow_restrict _, LinearMap.restrict_apply, Submodule.mk_eq_zero, ← mem_maxGenEigenspace] at hx ⊢
exact h hx
