mapsTo_genEigenspace_of_comm — Mathlib

English

If f and g commute, then g maps f.genEigenspace μ k into itself.

Русский

Если f и g commute, то g сохраняет подпространство f.genEigenspace μ k.

LaTeX

$$If f and g commute, then g[ f. genEigenspace(μ,k) ] ⊆ f. genEigenspace(μ,k).$$

Lean4

theorem mapsTo_genEigenspace_of_comm {f g : End R M} (h : Commute f g) (μ : R) (k : ℕ∞) :
    MapsTo g (f.genEigenspace μ k) (f.genEigenspace μ k) :=
  by
  intro x hx
  simp only [SetLike.mem_coe, mem_genEigenspace, LinearMap.mem_ker] at hx ⊢
  rcases hx with ⟨l, hl, hx⟩
  replace h : Commute ((f - μ • (1 : End R M)) ^ l) g := (h.sub_left <| Algebra.commute_algebraMap_left μ g).pow_left l
  use l, hl
  rw [← LinearMap.comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp, LinearMap.comp_apply, hx,
    map_zero]

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