map_add_of_iInf_genEigenspace_ne_bot_of_commute

English

If all endomorphisms commute and the iInf of genEigenspace is non-bottom, then μ(x+y) = μ(x) + μ(y).

Русский

Если все отображения коммутируют и iInf эгенпространств не равно ⊥, то μ сохраняет сложение аргументов.

LaTeX

$$$\\forall x,y:\\;\\text{Commute }(f x, f y) \\Rightarrow μ(x+y)=μ(x)+μ(y)$$$

Lean4

theorem map_add_of_iInf_genEigenspace_ne_bot_of_commute [NoZeroSMulDivisors R M] {L F : Type*} [Add L]
    [FunLike F L (End R M)] [AddHomClass F L (End R M)] (f : F) (μ : L → R) (k : ℕ∞)
    (h_ne : ⨅ x, (f x).genEigenspace (μ x) k ≠ ⊥) (h : ∀ x y, Commute (f x) (f y)) (x y : L) : μ (x + y) = μ x + μ y :=
  by
  by_contra contra
  let g : L → Submodule R M := fun x ↦ (f x).genEigenspace (μ x) k
  have : ⨅ x, g x ≤ (g x ⊓ g y) ⊓ g (x + y) :=
    le_inf_iff.mpr ⟨le_inf_iff.mpr ⟨iInf_le g x, iInf_le g y⟩, iInf_le g (x + y)⟩
  refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
  apply Disjoint.mono_left (genEigenspace_inf_le_add (f x) (f y) (μ x) (μ y) k k (h x y))
  simp only [g, map_add]
  exact disjoint_genEigenspace (f x + f y) (Ne.symm contra) _ k

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