English
Equality of iInf of restricted maxGenEigenspace spaces with the mapped subtype version.
Русский
Равенство iInf ограниченного пространства maxGenEigenspace и его отображения через подтип.
LaTeX
$$$$ (\inf_j (f_j).maxGenEigenspace(\mu_j)).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
distinguished index `i` whose maximal generalised `μ i`-eigenspace is invariant w.r.t. every `f j`,
taking simultaneous maximal generalised eigenspaces is unaffected by first restricting to the
distinguished generalised `μ i`-eigenspace. -/
theorem iInf_maxGenEigenspace_restrict_map_subtype_eq {μ : ι → R} (i : ι)
(h : ∀ j, MapsTo (f j) ((f i).maxGenEigenspace (μ i)) ((f i).maxGenEigenspace (μ i))) :
letI p := (f i).maxGenEigenspace (μ i)
letI q (j : ι) := maxGenEigenspace ((f j).restrict (h j)) (μ j)
(⨅ j, q j).map p.subtype = ⨅ j, (f j).maxGenEigenspace (μ j) :=
by
have : Nonempty ι := ⟨i⟩
set p := (f i).maxGenEigenspace (μ i)
have : ⨅ j, (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ j, (f j).maxGenEigenspace (μ j) :=
by
refine le_antisymm ?_ inf_le_right
simpa only [le_inf_iff, le_refl, and_true] using iInf_le _ _
rw [Submodule.map_iInf _ p.injective_subtype, this, Submodule.inf_iInf]
conv_rhs =>
enter [1]
ext
rw [p.inf_genEigenspace (f _) (h _)]
