inf_genEigenspace — Mathlib

English

The infimum (intersection) of a subspace with a generalized eigenspace has a description via the restricted generalized eigenspace map.

Русский

Пересечение подпространства с обобщённым эйгенпространством описывается через отображение ограниченного обобщённого эйгенпространства.

LaTeX

$$$p\\;\\cap\\; f.genEigenspace(\\mu,k) = (genEigenspace(\\mathrm{LinearMap.restrict}\\ f hfp)\\; \\mu\\ k).map\\ p.subtype$$$

Lean4

theorem _root_.Submodule.inf_genEigenspace (f : End R M) (p : Submodule R M) {k : ℕ∞} {μ : R}
    (hfp : ∀ x : M, x ∈ p → f x ∈ p) :
    p ⊓ f.genEigenspace μ k = (genEigenspace (LinearMap.restrict f hfp) μ k).map p.subtype := by
  rw [f.genEigenspace_restrict _ _ _ hfp, Submodule.map_comap_eq, Submodule.range_subtype]

Похожие утверждения