English
Let p be a submodule and f an endomorphism with p invariant under f. Then the infimum of p with the supremum of generalized eigenspaces equals the supremum of the infima: p ∩ (⊔μ f.genEigenspace μ k) = ⊔μ (p ∩ f.genEigenspace μ k).
Русский
Пусть p — подпомодуль и f — эндоморфизм, сохраняющий p. Тогда пересечение p с объединением обобщённых эйгенпространств равно объединению пересечений: p ∩ (⊔μ f.genEigenspace μ k) = ⊔μ (p ∩ f.genEigenspace μ k).
LaTeX
$$$p \\cap \\big(\\bigvee_{\\mu} f.genEigenspace(\\mu, k)\\big) = \\bigvee_{\\mu} (p \\cap f.genEigenspace(\\mu, k)).$$$
Lean4
/-- In finite dimensions, over an algebraically closed field, the generalized eigenspaces of any
linear endomorphism span the whole space. -/
theorem iSup_maxGenEigenspace_eq_top [IsAlgClosed K] [FiniteDimensional K V] (f : End K V) :
⨆ (μ : K), f.maxGenEigenspace μ = ⊤ := by
-- We prove the claim by strong induction on the dimension of the vector space.
suffices ∀ n, finrank K V = n → ⨆ (μ : K), f.maxGenEigenspace μ = ⊤ by exact this _ rfl
intro n h_dim
induction n using Nat.strong_induction_on generalizing V with
| h n ih =>
rcases n with - | n
· rw [← top_le_iff]
simp only [Submodule.finrank_eq_zero.1 (Eq.trans (finrank_top _ _) h_dim), bot_le]
-- Otherwise the vector space is nontrivial.
· haveI : Nontrivial V :=
finrank_pos_iff.1
(by rw [h_dim]; apply Nat.zero_lt_succ)
-- Hence, `f` has an eigenvalue `μ₀`.
obtain ⟨μ₀, hμ₀⟩ : ∃ μ₀, f.HasEigenvalue μ₀ := exists_eigenvalue f
let ES :=
f.genEigenspace μ₀
(finrank K V)
-- and `ER` to be the generalized eigenrange.
let ER :=
f.genEigenrange μ₀
(finrank K V)
-- `f` maps `ER` into itself.
have h_f_ER : ∀ x : V, x ∈ ER → f x ∈ ER := fun x hx =>
map_genEigenrange_le
(Submodule.mem_map_of_mem hx)
-- Therefore, we can define the restriction `f'` of `f` to `ER`.
let f' : End K ER := f.restrict h_f_ER
have h_dim_ES_pos : 0 < finrank K ES := by
dsimp only [ES]
rw [h_dim]
apply
pos_finrank_genEigenspace_of_hasEigenvalue hμ₀
(Nat.zero_lt_succ n)
-- and the dimensions of `ES` and `ER` add up to `finrank K V`.
have h_dim_add : finrank K ER + finrank K ES = finrank K V :=
by
dsimp only [ER, ES]
rw [Module.End.genEigenspace_nat, Module.End.genEigenrange_nat]
apply LinearMap.finrank_range_add_finrank_ker
have h_dim_ER : finrank K ER < n.succ := by
omega
-- This allows us to apply the induction hypothesis on `ER`:
have ih_ER : ⨆ (μ : K), f'.maxGenEigenspace μ = ⊤ := ih (finrank K ER) h_dim_ER f' rfl
have ih_ER' : ⨆ (μ : K), (f'.maxGenEigenspace μ).map ER.subtype = ER := by
simp only [(Submodule.map_iSup _ _).symm, ih_ER, Submodule.map_subtype_top ER]
-- Moreover, every generalized eigenspace of `f'` is contained in the corresponding generalized
-- eigenspace of `f`.
have hff' : ∀ μ, (f'.maxGenEigenspace μ).map ER.subtype ≤ f.maxGenEigenspace μ :=
by
intros
rw [maxGenEigenspace, genEigenspace_restrict]
apply Submodule.map_comap_le
have hER : ER ≤ ⨆ (μ : K), f.maxGenEigenspace μ :=
by
rw [← ih_ER']
exact iSup_mono hff'
have hES : ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ :=
((f.genEigenspace μ₀).mono le_top).trans
(le_iSup f.maxGenEigenspace μ₀)
-- Moreover, we know that `ER` and `ES` are disjoint.
have h_disjoint : Disjoint ER ES := generalized_eigenvec_disjoint_range_ker f μ₀
change ⨆ (μ : K), f.maxGenEigenspace μ = ⊤
rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add.ge h_disjoint]
apply sup_le hER hES
