English
If a linear map f maps a subspace p into itself, then the generalized eigenspace of the restriction of f to p is the part of the generalized eigenspace of f that lies in p.
Русский
Если линейное отображение f отправляет подпространство p в p, то обобщённое эйгенпространство ограниченного отображения f на p состоит из той части эйгенпространства f, которая лежит в p.
LaTeX
$$$\\mathrm{genEigenspace}(\\mathrm{LinearMap.restrict}\\ f\, hfp)\\,\\mu\\,k = \\mathrm{comap}\; p.\\mathrm{subtype} (f.\\mathrm{genEigenspace}\\ \\mu\\ k)$$$
Lean4
/-- If `f` maps a subspace `p` into itself, then the generalized eigenspace of the restriction
of `f` to `p` is the part of the generalized eigenspace of `f` that lies in `p`. -/
theorem genEigenspace_restrict (f : End R M) (p : Submodule R M) (k : ℕ∞) (μ : R) (hfp : ∀ x : M, x ∈ p → f x ∈ p) :
genEigenspace (LinearMap.restrict f hfp) μ k = Submodule.comap p.subtype (f.genEigenspace μ k) :=
by
ext x
suffices ∀ l : ℕ, genEigenspace (LinearMap.restrict f hfp) μ l = Submodule.comap p.subtype (f.genEigenspace μ l) by
simp_rw [mem_genEigenspace, ← mem_genEigenspace_nat, this, Submodule.mem_comap, mem_genEigenspace (k := k),
mem_genEigenspace_nat]
intro l
simp only [genEigenspace_nat, ← LinearMap.ker_comp]
induction l with
| zero =>
rw [pow_zero, pow_zero, Module.End.one_eq_id]
apply (Submodule.ker_subtype _).symm
| succ l ih =>
erw [pow_succ, pow_succ, LinearMap.ker_comp, LinearMap.ker_comp, ih, ← LinearMap.ker_comp, LinearMap.comp_assoc]
