English
For commuting endomorphisms f1,f2, the infimum of their generalized eigenspaces embeds into the generalized eigenspace of their sum with eigenvalues μ1+μ2 and exponent k1+k2.
Русский
При коммьютировании концевые отображения f1,f2: пересечение их обобщённых эйгенпространств вложено в эйгенпространство суммы с суммой собственных значений μ1+μ2 и показателем k1+k2.
LaTeX
$$$\\text{Commute } f_1,f_2 \\;\\Rightarrow\\; (f_1.\\mathrm{genEigenspace}(μ_1,k_1) \\cap f_2.\\mathrm{genEigenspace}(μ_2,k_2)) \\le (f_1+f_2).\\mathrm{genEigenspace}(μ_1+μ_2,k_1+k_2)$$$
Lean4
theorem genEigenspace_inf_le_add (f₁ f₂ : End R M) (μ₁ μ₂ : R) (k₁ k₂ : ℕ∞) (h : Commute f₁ f₂) :
(f₁.genEigenspace μ₁ k₁) ⊓ (f₂.genEigenspace μ₂ k₂) ≤ (f₁ + f₂).genEigenspace (μ₁ + μ₂) (k₁ + k₂) :=
by
intro m hm
simp only [Submodule.mem_inf, mem_genEigenspace, LinearMap.mem_ker] at hm ⊢
obtain ⟨⟨l₁, hlk₁, hl₁⟩, ⟨l₂, hlk₂, hl₂⟩⟩ := hm
use l₁ + l₂
have : f₁ + f₂ - (μ₁ + μ₂) • 1 = (f₁ - μ₁ • 1) + (f₂ - μ₂ • 1) := by rw [add_smul];
exact add_sub_add_comm f₁ f₂ (μ₁ • 1) (μ₂ • 1)
replace h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1) :=
(h.sub_right <| Algebra.commute_algebraMap_right μ₂ f₁).sub_left (Algebra.commute_algebraMap_left μ₁ _)
rw [this, h.add_pow', LinearMap.coeFn_sum, Finset.sum_apply]
constructor
· simpa only [Nat.cast_add] using add_le_add hlk₁ hlk₂
refine Finset.sum_eq_zero fun ⟨i, j⟩ hij ↦ ?_
suffices (((f₁ - μ₁ • 1) ^ i) * ((f₂ - μ₂ • 1) ^ j)) m = 0 by rw [LinearMap.smul_apply, this, smul_zero]
rw [Finset.mem_antidiagonal] at hij
obtain hi | hj : l₁ ≤ i ∨ l₂ ≤ j := by cutsat
· rw [(h.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hl₁, LinearMap.map_zero]
· rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hl₂, LinearMap.map_zero]
