English
If μ1 ≠ μ2 and k,l are ENat, the generalized eigenspaces genEigenspace(f, μ1, k) and genEigenspace(f, μ2, l) are disjoint provided NoZeroSMulDivisors holds.
Русский
Если μ1 ≠ μ2, то обобщённые эйгенпространства г(f, μ1, k) и г(f, μ2, l) взаимно непересекаются при условии NoZeroSMulDivisors.
LaTeX
$$$\\mathrm{Disjoint}\\bigl( \\mathrm{genEigenspace}(f, μ_1, k), \\mathrm{genEigenspace}(f, μ_2, l) \\bigr) \\quad \\text{если } μ_1 \\neq μ_2.$$$
Lean4
theorem disjoint_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) {μ₁ μ₂ : R} (hμ : μ₁ ≠ μ₂) (k l : ℕ∞) :
Disjoint (f.genEigenspace μ₁ k) (f.genEigenspace μ₂ l) :=
by
rw [genEigenspace_eq_iSup_genEigenspace_nat, genEigenspace_eq_iSup_genEigenspace_nat]
simp_rw [genEigenspace_directed.disjoint_iSup_left, genEigenspace_directed.disjoint_iSup_right]
rintro ⟨k, -⟩ ⟨l, -⟩
nontriviality M
have := NoZeroSMulDivisors.isReduced R M
rw [disjoint_iff]
set p := f.genEigenspace μ₁ k ⊓ f.genEigenspace μ₂ l
by_contra hp
replace hp : Nontrivial p := Submodule.nontrivial_iff_ne_bot.mpr hp
let f₁ : End R p :=
(f - algebraMap R (End R M) μ₁).restrict <|
MapsTo.inter_inter (mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₁) μ₁ k)
(mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₁) μ₂ l)
let f₂ : End R p :=
(f - algebraMap R (End R M) μ₂).restrict <|
MapsTo.inter_inter (mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₂) μ₁ k)
(mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₂) μ₂ l)
have : IsNilpotent (f₂ - f₁) :=
by
apply
Commute.isNilpotent_sub (x := f₂) (y := f₁) _ (isNilpotent_restrict_of_le inf_le_right _)
(isNilpotent_restrict_of_le inf_le_left _)
· ext; simp [f₁, f₂, smul_sub, sub_sub, smul_comm μ₁, add_sub_left_comm]
apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)
apply isNilpotent_restrict_genEigenspace_nat
apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)
apply isNilpotent_restrict_genEigenspace_nat
have hf₁₂ : f₂ - f₁ = algebraMap R (End R p) (μ₁ - μ₂) := by ext; simp [f₁, f₂]
rw [hf₁₂, IsNilpotent.map_iff (FaithfulSMul.algebraMap_injective R (End R p)), isNilpotent_iff_eq_zero,
sub_eq_zero] at this
contradiction
