English
The iInf of maxGenEigenspace spaces maps via subspaces equivalently.
Русский
iInf от пространств maxGenEigenspace отображается эквивалентно через подпространство.
LaTeX
$$$$ (\inf_j (f_j).maxGenEigenspace(\mu_j)).map p.subtype = \inf_j (f_j).maxGenEigenspace(\mu_j). $$$$
Lean4
/-- Given a family of endomorphisms `i ↦ f i`, a family of candidate eigenvalues `i ↦ μ i`, and a
submodule `p` which is invariant w.r.t. every `f i`, the intersection of `p` with the simultaneous
maximal generalised eigenspace (taken over all `i`), is the same as the simultaneous maximal
generalised eigenspace of the `f i` restricted to `p`. -/
theorem _root_.Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo {μ : ι → R} (p : Submodule R M)
(hfp : ∀ i, MapsTo (f i) p p) :
p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) = (⨅ i, maxGenEigenspace ((f i).restrict (hfp i)) (μ i)).map p.subtype :=
by
cases isEmpty_or_nonempty ι
· simp [iInf_of_isEmpty]
· simp_rw [inf_iInf, p.inf_genEigenspace _ (hfp _), Submodule.map_iInf _ p.injective_subtype]
