Theorems · Theorem · linear algebra

Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo

∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : ι → Module.End R M) {μ : ι → R} (p : Submodule R M) (hfp : ∀ (i : ι), Set.MapsTo ⇑(f i) ↑p ↑p),
  p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ i, Module.End.maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

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.

Defined in

Mathlib.LinearAlgebra.Eigenspace.Pi

Cited by

1 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule