From ef18740b7b57fbd1d017ef9276d0cc05af57dfbd Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 24 Sep 2020 03:33:52 +0000 Subject: [PATCH] feat(linear_algebra/eigenspace): generalized eigenvectors span the entire space (#4111) --- docs/references.bib | 13 ++ src/linear_algebra/basic.lean | 4 + src/linear_algebra/eigenspace.lean | 227 ++++++++++++++++++++--------- src/ring_theory/algebra.lean | 18 +++ 4 files changed, 196 insertions(+), 66 deletions(-) diff --git a/docs/references.bib b/docs/references.bib index f65e404e0921b..85ddf94d8cd04 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -4,6 +4,19 @@ % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +@book{axler2015, + Author = {Sheldon Axler}, + Title = {Linear algebra done right. 3rd ed.}, + FJournal = {Undergraduate Texts in Mathematics}, + Journal = {Undergraduate Texts Math.}, + ISSN = {0172-6056; 2197-5604/e}, + Edition = {3rd ed.}, + ISBN = {978-3-319-11079-0/hbk; 978-3-319-11080-6/ebook}, + Pages = {xvii + 340}, + Year = {2015}, + Publisher = {Springer}, +} + @article {MR1167694, AUTHOR = {Blass, Andreas}, TITLE = {A game semantics for linear logic}, diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean index 7c944f9d62a47..15218e52a0b57 100644 --- a/src/linear_algebra/basic.lean +++ b/src/linear_algebra/basic.lean @@ -1221,6 +1221,10 @@ lemma range_cod_restrict (p : submodule R M) (f : M₂ →ₗ[R] M) (hf) : range (cod_restrict p f hf) = comap p.subtype f.range := map_cod_restrict _ _ _ _ +lemma ker_restrict {p : submodule R M} {f : M →ₗ[R] M} (hf : ∀ x : M, x ∈ p → f x ∈ p) : + ker (f.restrict hf) = (f.dom_restrict p).ker := +by rw [restrict_eq_cod_restrict_dom_restrict, ker_cod_restrict] + lemma map_comap_eq (f : M →ₗ[R] M₂) (q : submodule R M₂) : map f (comap f q) = range f ⊓ q := le_antisymm (le_inf (map_mono le_top) (map_comap_le _ _)) $ diff --git a/src/linear_algebra/eigenspace.lean b/src/linear_algebra/eigenspace.lean index 67420ac786409..fc117cb26b704 100644 --- a/src/linear_algebra/eigenspace.lean +++ b/src/linear_algebra/eigenspace.lean @@ -12,7 +12,8 @@ import linear_algebra.matrix # Eigenvectors and eigenvalues This file defines eigenspaces, eigenvalues, and eigenvalues, as well as their generalized -counterparts. +counterparts. We follow Axler's approach [axler2015] because it allows us to derive many properties +without choosing a basis and without using matrices. An eigenspace of a linear map `f` for a scalar `μ` is the kernel of the map `(f - μ • id)`. The nonzero elements of an eigenspace are eigenvectors `x`. They have the property `f x = μ • x`. If @@ -27,15 +28,9 @@ of the map `(f - μ • id) ^ k`. The nonzero elements of a generalized eigenspa eigenvectors `x`. If there are generalized eigenvectors for a natural number `k` and a scalar `μ`, the scalar `μ` is called a generalized eigenvalue. -## Notations - -The expression `algebra_map K (End K V)` appears very often, which is why we use `am` as a local -notation for it. - ## References -* [Sheldon Axler, *Down with determinants!*, - https://www.maa.org/sites/default/files/pdf/awards/Axler-Ford-1996.pdf][axler1996] +* [Sheldon Axler, *Linear Algebra Done Right*][axler2015] * https://en.wikipedia.org/wiki/Eigenvalues_and_eigenvectors ## Tags @@ -50,51 +45,50 @@ namespace End open vector_space principal_ideal_ring polynomial finite_dimensional -variables {K : Type v} {V : Type w} [add_comm_group V] - -local notation `am` := algebra_map K (End K V) +variables {K R : Type v} {V M : Type w} + [comm_ring R] [add_comm_group M] [module R M] [field K] [add_comm_group V] [vector_space K V] /-- The submodule `eigenspace f μ` for a linear map `f` and a scalar `μ` consists of all vectors `x` - such that `f x = μ • x`. -/ -def eigenspace [comm_ring K] [module K V] (f : End K V) (μ : K) : submodule K V := -(f - am μ).ker + such that `f x = μ • x`. (Def 5.36 of [axler2015])-/ +def eigenspace (f : End R M) (μ : R) : submodule R M := +(f - algebra_map R (End R M) μ).ker -/-- A nonzero element of an eigenspace is an eigenvector. -/ -def has_eigenvector [comm_ring K] [module K V] (f : End K V) (μ : K) (x : V) : Prop := +/-- A nonzero element of an eigenspace is an eigenvector. (Def 5.7 of [axler2015]) -/ +def has_eigenvector (f : End R M) (μ : R) (x : M) : Prop := x ≠ 0 ∧ x ∈ eigenspace f μ /-- A scalar `μ` is an eigenvalue for a linear map `f` if there are nonzero vectors `x` - such that `f x = μ • x`. -/ -def has_eigenvalue [comm_ring K] [module K V] (f : End K V) (a : K) : Prop := + such that `f x = μ • x`. (Def 5.5 of [axler2015]) -/ +def has_eigenvalue (f : End R M) (a : R) : Prop := eigenspace f a ≠ ⊥ -lemma mem_eigenspace_iff [comm_ring K] [module K V] - {f : End K V} {μ : K} {x : V} : x ∈ eigenspace f μ ↔ f x = μ • x := +lemma mem_eigenspace_iff {f : End R M} {μ : R} {x : M} : x ∈ eigenspace f μ ↔ f x = μ • x := by rw [eigenspace, linear_map.mem_ker, linear_map.sub_apply, algebra_map_End_apply, - sub_eq_zero] + sub_eq_zero] -lemma eigenspace_div [field K] [vector_space K V] (f : End K V) (a b : K) (hb : b ≠ 0) : - eigenspace f (a / b) = (b • f - am a).ker := +lemma eigenspace_div (f : End K V) (a b : K) (hb : b ≠ 0) : + eigenspace f (a / b) = (b • f - algebra_map K (End K V) a).ker := calc eigenspace f (a / b) = eigenspace f (b⁻¹ * a) : by { dsimp [(/)], rw mul_comm } ... = (f - (b⁻¹ * a) • linear_map.id).ker : rfl ... = (f - b⁻¹ • a • linear_map.id).ker : by rw smul_smul - ... = (f - b⁻¹ • am a).ker : rfl - ... = (b • (f - b⁻¹ • am a)).ker : by rw linear_map.ker_smul _ b hb - ... = (b • f - am a).ker : by rw [smul_sub, smul_inv_smul' hb] + ... = (f - b⁻¹ • algebra_map K (End K V) a).ker : rfl + ... = (b • (f - b⁻¹ • algebra_map K (End K V) a)).ker : by rw linear_map.ker_smul _ b hb + ... = (b • f - algebra_map K (End K V) a).ker : by rw [smul_sub, smul_inv_smul' hb] -lemma eigenspace_aeval_polynomial_degree_1 [field K] [vector_space K V] +lemma eigenspace_aeval_polynomial_degree_1 (f : End K V) (q : polynomial K) (hq : degree q = 1) : eigenspace f (- q.coeff 0 / q.leading_coeff) = (aeval f q).ker := calc - eigenspace f (- q.coeff 0 / q.leading_coeff) = (q.leading_coeff • f - am (- q.coeff 0)).ker + eigenspace f (- q.coeff 0 / q.leading_coeff) + = (q.leading_coeff • f - algebra_map K (End K V) (- q.coeff 0)).ker : by { rw eigenspace_div, intro h, rw leading_coeff_eq_zero_iff_deg_eq_bot.1 h at hq, cases hq } ... = (aeval f (C q.leading_coeff * X + C (q.coeff 0))).ker : by { rw [C_mul', aeval_def], simpa [algebra_map, algebra.to_ring_hom], } ... = (aeval f q).ker : by { congr, apply (eq_X_add_C_of_degree_eq_one hq).symm } -lemma ker_aeval_ring_hom'_unit_polynomial [field K] [vector_space K V] +lemma ker_aeval_ring_hom'_unit_polynomial (f : End K V) (c : units (polynomial K)) : (aeval f (c : polynomial K)).ker = ⊥ := begin @@ -104,7 +98,7 @@ begin apply coeff_coe_units_zero_ne_zero c end -theorem aeval_apply_of_has_eigenvector [field K] [vector_space K V] {f : End K V} +theorem aeval_apply_of_has_eigenvector {f : End K V} {p : polynomial K} {μ : K} {x : V} (h : f.has_eigenvector μ x) : aeval f p x = (p.eval μ) • x := begin @@ -118,7 +112,7 @@ end section minimal_polynomial -variables [field K] [vector_space K V] [finite_dimensional K V] (f : End K V) +variables [finite_dimensional K V] (f : End K V) protected theorem is_integral : is_integral K f := is_integral_of_noetherian (by apply_instance) f @@ -160,10 +154,8 @@ theorem has_eigenvalue_iff_is_root : end minimal_polynomial /-- Every linear operator on a vector space over an algebraically closed field has - an eigenvalue. (Axler's Theorem 2.1.) -/ -lemma exists_eigenvalue - [field K] [is_alg_closed K] [vector_space K V] [finite_dimensional K V] [nontrivial V] - (f : End K V) : + an eigenvalue. (Lemma 5.21 of [axler2015]) -/ +lemma exists_eigenvalue [is_alg_closed K] [finite_dimensional K V] [nontrivial V] (f : End K V) : ∃ (c : K), f.has_eigenvalue c := begin classical, @@ -185,7 +177,7 @@ begin { simp only [←not_imp, (is_unit.mem_submonoid_iff _).symm], apply not_forall.1 (λ h, h_eval_p_not_unit (ring_hom_mem_submonoid_of_factors_subset_of_units_subset - (eval₂_ring_hom' am algebra.commutes f) + (eval₂_ring_hom' (algebra_map _ _) algebra.commutes f) (is_unit.submonoid (End K V)) p h_mon.ne_zero h _)), simp only [is_unit.mem_submonoid_iff, linear_map.is_unit_iff], apply ker_aeval_ring_hom'_unit_polynomial }, @@ -205,12 +197,11 @@ begin end /-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly - independent. (Axler's Proposition 2.2) + independent. (Lemma 5.10 of [axler2015]) We use the eigenvalues as indexing set to ensure that there is only one eigenvector for each eigenvalue in the image of `xs`. -/ -lemma eigenvectors_linear_independent [field K] [vector_space K V] - (f : End K V) (μs : set K) (xs : μs → V) +lemma eigenvectors_linear_independent (f : End K V) (μs : set K) (xs : μs → V) (h_eigenvec : ∀ μ : μs, f.has_eigenvector μ (xs μ)) : linear_independent K xs := begin @@ -246,7 +237,7 @@ begin { to_fun := l'_f, support := l_support', mem_support_to_fun := h_l_support' }, -- The linear combination `l'` over `xs` adds up to `0`. have total_l' : finsupp.total μs V K xs l' = 0, - { let g := f - am μ₀, + { let g := f - algebra_map K (End K V) μ₀, have h_gμ₀: g (l μ₀ • xs μ₀) = 0, by rw [linear_map.map_smul, linear_map.sub_apply, mem_eigenspace_iff.1 (h_eigenvec _).2, algebra_map_End_apply, sub_self, smul_zero], @@ -304,26 +295,28 @@ begin end /-- The generalized eigenspace for a linear map `f`, a scalar `μ`, and an exponent `k ∈ ℕ` is the - kernel of `(f - μ • id) ^ k`. -/ -def generalized_eigenspace [comm_ring K] [module K V] - (f : End K V) (μ : K) (k : ℕ) : submodule K V := -((f - am μ) ^ k).ker - -/-- A nonzero element of a generalized eigenspace is a generalized eigenvector. -/ -def has_generalized_eigenvector [comm_ring K] [module K V] - (f : End K V) (μ : K) (k : ℕ) (x : V) : Prop := + kernel of `(f - μ • id) ^ k`. (Def 8.10 of [axler2015])-/ +def generalized_eigenspace (f : End R M) (μ : R) (k : ℕ) : submodule R M := +((f - algebra_map R (End R M) μ) ^ k).ker + +/-- A nonzero element of a generalized eigenspace is a generalized eigenvector. + (Def 8.9 of [axler2015])-/ +def has_generalized_eigenvector (f : End R M) (μ : R) (k : ℕ) (x : M) : Prop := x ≠ 0 ∧ x ∈ generalized_eigenspace f μ k /-- A scalar `μ` is a generalized eigenvalue for a linear map `f` and an exponent `k ∈ ℕ` if there are generalized eigenvectors for `f`, `k`, and `μ`. -/ -def has_generalized_eigenvalue [comm_ring K] [module K V] - (f : End K V) (μ : K) (k : ℕ) : Prop := +def has_generalized_eigenvalue (f : End R M) (μ : R) (k : ℕ) : Prop := generalized_eigenspace f μ k ≠ ⊥ +/-- The generalized eigenrange for a linear map `f`, a scalar `μ`, and an exponent `k ∈ ℕ` is the + range of `(f - μ • id) ^ k`. -/ +def generalized_eigenrange (f : End R M) (μ : R) (k : ℕ) : submodule R M := +((f - algebra_map R (End R M) μ) ^ k).range + /-- The exponent of a generalized eigenvalue is never 0. -/ -lemma exp_ne_zero_of_has_generalized_eigenvalue [comm_ring K] [module K V] - {f : End K V} {μ : K} {k : ℕ} (h : f.has_generalized_eigenvalue μ k) : - k ≠ 0 := +lemma exp_ne_zero_of_has_generalized_eigenvalue {f : End R M} {μ : R} {k : ℕ} + (h : f.has_generalized_eigenvalue μ k) : k ≠ 0 := begin rintro rfl, exact h linear_map.ker_id @@ -331,17 +324,17 @@ end /-- A generalized eigenspace for some exponent `k` is contained in the generalized eigenspace for exponents larger than `k`. -/ -lemma generalized_eigenspace_mono [field K] [vector_space K V] - {f : End K V} {μ : K} {k : ℕ} {m : ℕ} (hm : k ≤ m) : +lemma generalized_eigenspace_mono {f : End K V} {μ : K} {k : ℕ} {m : ℕ} (hm : k ≤ m) : f.generalized_eigenspace μ k ≤ f.generalized_eigenspace μ m := begin simp only [generalized_eigenspace, ←pow_sub_mul_pow _ hm], - exact linear_map.ker_le_ker_comp ((f - am μ) ^ k) ((f - am μ) ^ (m - k)) + exact linear_map.ker_le_ker_comp + ((f - algebra_map K (End K V) μ) ^ k) ((f - algebra_map K (End K V) μ) ^ (m - k)) end /-- A generalized eigenvalue for some exponent `k` is also a generalized eigenvalue for exponents larger than `k`. -/ -lemma has_generalized_eigenvalue_of_has_generalized_eigenvalue_of_le [field K] [vector_space K V] +lemma has_generalized_eigenvalue_of_has_generalized_eigenvalue_of_le {f : End K V} {μ : K} {k : ℕ} {m : ℕ} (hm : k ≤ m) (hk : f.has_generalized_eigenvalue μ k) : f.has_generalized_eigenvalue μ m := begin @@ -352,13 +345,12 @@ begin end /-- The eigenspace is a subspace of the generalized eigenspace. -/ -lemma eigenspace_le_generalized_eigenspace [field K] [vector_space K V] - {f : End K V} {μ : K} {k : ℕ} (hk : 0 < k) : +lemma eigenspace_le_generalized_eigenspace {f : End K V} {μ : K} {k : ℕ} (hk : 0 < k) : f.eigenspace μ ≤ f.generalized_eigenspace μ k := generalized_eigenspace_mono (nat.succ_le_of_lt hk) /-- All eigenvalues are generalized eigenvalues. -/ -lemma has_generalized_eigenvalue_of_has_eigenvalue [field K] [vector_space K V] +lemma has_generalized_eigenvalue_of_has_eigenvalue {f : End K V} {μ : K} {k : ℕ} (hk : 0 < k) (hμ : f.has_eigenvalue μ) : f.has_generalized_eigenvalue μ k := begin @@ -366,23 +358,22 @@ begin rwa [has_generalized_eigenvalue, generalized_eigenspace, pow_one] end -/-- Every generalized eigenvector is a generalized eigenvector for exponent `findim K V`. -/ +/-- Every generalized eigenvector is a generalized eigenvector for exponent `findim K V`. + (Lemma 8.11 of [axler2015]) -/ lemma generalized_eigenspace_le_generalized_eigenspace_findim - [field K] [vector_space K V] [finite_dimensional K V] - (f : End K V) (μ : K) (k : ℕ) : + [finite_dimensional K V] (f : End K V) (μ : K) (k : ℕ) : f.generalized_eigenspace μ k ≤ f.generalized_eigenspace μ (findim K V) := ker_pow_le_ker_pow_findim _ _ /-- Generalized eigenspaces for exponents at least `findim K V` are equal to each other. -/ -lemma generalized_eigenspace_eq_generalized_eigenspace_findim_of_le - [field K] [vector_space K V] [finite_dimensional K V] +lemma generalized_eigenspace_eq_generalized_eigenspace_findim_of_le [finite_dimensional K V] (f : End K V) (μ : K) {k : ℕ} (hk : findim K V ≤ k) : f.generalized_eigenspace μ k = f.generalized_eigenspace μ (findim K V) := ker_pow_eq_ker_pow_findim_of_le hk /-- If `f` maps a subspace `p` into itself, then the generalized eigenspace of the restriction of `f` to `p` is the part of the generalized eigenspace of `f` that lies in `p`. -/ -lemma generalized_eigenspace_restrict [field K] [vector_space K V] +lemma generalized_eigenspace_restrict (f : End K V) (p : submodule K V) (k : ℕ) (μ : K) (hfp : ∀ (x : V), x ∈ p → f x ∈ p) : generalized_eigenspace (linear_map.restrict f hfp) μ k = submodule.comap p.subtype (f.generalized_eigenspace μ k) := @@ -396,5 +387,109 @@ begin ih, ←linear_map.ker_comp, linear_map.comp_assoc], } end +/-- Generalized eigenrange and generalized eigenspace for exponent `findim K V` are disjoint. -/ +lemma generalized_eigenvec_disjoint_range_ker [finite_dimensional K V] (f : End K V) (μ : K) : + disjoint (f.generalized_eigenrange μ (findim K V)) (f.generalized_eigenspace μ (findim K V)) := +begin + have h := calc + submodule.comap ((f - algebra_map _ _ μ) ^ findim K V) (f.generalized_eigenspace μ (findim K V)) + = ((f - algebra_map _ _ μ) ^ findim K V * (f - algebra_map K (End K V) μ) ^ findim K V).ker : + by { rw [generalized_eigenspace, ←linear_map.ker_comp], refl } + ... = f.generalized_eigenspace μ (findim K V + findim K V) : + by { rw ←pow_add, refl } + ... = f.generalized_eigenspace μ (findim K V) : + by { rw generalized_eigenspace_eq_generalized_eigenspace_findim_of_le, linarith }, + rw [disjoint, generalized_eigenrange, linear_map.range, submodule.map_inf_eq_map_inf_comap, + top_inf_eq, h], + apply submodule.map_comap_le +end + +/-- The generalized eigenspace of an eigenvalue has positive dimension for positive exponents. -/ +lemma pos_findim_generalized_eigenspace_of_has_eigenvalue [finite_dimensional K V] + {f : End K V} {k : ℕ} {μ : K} (hx : f.has_eigenvalue μ) (hk : 0 < k): + 0 < findim K (f.generalized_eigenspace μ k) := +calc + 0 = findim K (⊥ : submodule K V) : by rw findim_bot + ... < findim K (f.eigenspace μ) : submodule.findim_lt_findim_of_lt (bot_lt_iff_ne_bot.2 hx) + ... ≤ findim K (f.generalized_eigenspace μ k) : + submodule.findim_mono (generalized_eigenspace_mono (nat.succ_le_of_lt hk)) + +/-- A linear map maps a generalized eigenrange into itself. -/ +lemma map_generalized_eigenrange_le {f : End K V} {μ : K} {n : ℕ} : + submodule.map f (f.generalized_eigenrange μ n) ≤ f.generalized_eigenrange μ n := +calc submodule.map f (f.generalized_eigenrange μ n) + = (f * ((f - algebra_map _ _ μ) ^ n)).range : (linear_map.range_comp _ _).symm + ... = (((f - algebra_map _ _ μ) ^ n) * f).range : by rw algebra.mul_sub_algebra_map_pow_commutes + ... = submodule.map ((f - algebra_map _ _ μ) ^ n) f.range : linear_map.range_comp _ _ + ... ≤ f.generalized_eigenrange μ n : linear_map.map_le_range + +/-- The generalized eigenvectors span the entire vector space (Lemma 8.21 of [axler2015]). -/ +lemma supr_generalized_eigenspace_eq_top [is_alg_closed K] [finite_dimensional K V] (f : End K V) : + (⨆ (μ : K) (k : ℕ), f.generalized_eigenspace μ k) = ⊤ := +begin + tactic.unfreeze_local_instances, + -- We prove the claim by strong induction on the dimension of the vector space. + induction h_dim : findim K V using nat.strong_induction_on with n ih generalizing V, + cases n, + -- If the vector space is 0-dimensional, the result is trivial. + { rw ←top_le_iff, + simp only [findim_eq_zero.1 (eq.trans findim_top h_dim), bot_le] }, + -- Otherwise the vector space is nontrivial. + { haveI : nontrivial V := findim_pos_iff.1 (by { rw h_dim, apply nat.zero_lt_succ }), + -- Hence, `f` has an eigenvalue `μ₀`. + obtain ⟨μ₀, hμ₀⟩ : ∃ μ₀, f.has_eigenvalue μ₀ := exists_eigenvalue f, + -- We define `ES` to be the generalized eigenspace + let ES := f.generalized_eigenspace μ₀ (findim K V), + -- and `ER` to be the generalized eigenrange. + let ER := f.generalized_eigenrange μ₀ (findim K V), + -- `f` maps `ER` into itself. + have h_f_ER : ∀ (x : V), x ∈ ER → f x ∈ ER, + from λ x hx, map_generalized_eigenrange_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, + -- The dimension of `ES` is positive + have h_dim_ES_pos : 0 < findim K ES, + { dsimp only [ES], + rw h_dim, + apply pos_findim_generalized_eigenspace_of_has_eigenvalue hμ₀ (nat.zero_lt_succ n) }, + -- and the dimensions of `ES` and `ER` add up to `findim K V`. + have h_dim_add : findim K ER + findim K ES = findim K V, + { apply linear_map.findim_range_add_findim_ker }, + -- Therefore the dimension `ER` mus be smaller than `findim K V`. + have h_dim_ER : findim K ER < n.succ, by omega, + -- This allows us to apply the induction hypothesis on `ER`: + have ih_ER : (⨆ (μ : K) (k : ℕ), f'.generalized_eigenspace μ k) = ⊤, + from ih (findim K ER) h_dim_ER f' rfl, + -- The induction hypothesis gives us a statement about subspaces of `ER`. We can transfer this + -- to a statement about subspaces of `V` via `submodule.subtype`: + have ih_ER' : (⨆ (μ : K) (k : ℕ), (f'.generalized_eigenspace μ k).map ER.subtype) = ER, + by simp only [(submodule.map_supr _ _).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' : ∀ μ k, + (f'.generalized_eigenspace μ k).map ER.subtype ≤ f.generalized_eigenspace μ k, + { intros, + rw generalized_eigenspace_restrict, + apply submodule.map_comap_le }, + -- It follows that `ER` is contained in the span of all generalized eigenvectors. + have hER : ER ≤ ⨆ (μ : K) (k : ℕ), f.generalized_eigenspace μ k, + { rw ← ih_ER', + apply supr_le_supr _, + exact λ μ, supr_le_supr (λ k, hff' μ k), }, + -- `ES` is contained in this span by definition. + have hES : ES ≤ ⨆ (μ : K) (k : ℕ), f.generalized_eigenspace μ k, + from le_trans + (le_supr (λ k, f.generalized_eigenspace μ₀ k) (findim K V)) + (le_supr (λ (μ : K), ⨆ (k : ℕ), f.generalized_eigenspace μ k) μ₀), + -- Moreover, we know that `ER` and `ES` are disjoint. + have h_disjoint : disjoint ER ES, + from generalized_eigenvec_disjoint_range_ker f μ₀, + -- Since the dimensions of `ER` and `ES` add up to the dimension of `V`, it follows that the + -- span of all generalized eigenvectors is all of `V`. + show (⨆ (μ : K) (k : ℕ), f.generalized_eigenspace μ k) = ⊤, + { rw [←top_le_iff, ←submodule.eq_top_of_disjoint ER ES h_dim_add h_disjoint], + apply sup_le hER hES } } +end + end End end module diff --git a/src/ring_theory/algebra.lean b/src/ring_theory/algebra.lean index 1392cc09b4947..06017030cb802 100644 --- a/src/ring_theory/algebra.lean +++ b/src/ring_theory/algebra.lean @@ -285,6 +285,24 @@ instance linear_map.semimodule' (R : Type u) [comm_semiring R] end semiring +section ring +variables [comm_ring R] [comm_ring S] [ring A] [algebra R A] + +lemma mul_sub_algebra_map_commutes (x : A) (r : R) : + x * (x - algebra_map R A r) = (x - algebra_map R A r) * x := +by rw [mul_sub, ←commutes, sub_mul] + +lemma mul_sub_algebra_map_pow_commutes (x : A) (r : R) (n : ℕ) : + x * (x - algebra_map R A r) ^ n = (x - algebra_map R A r) ^ n * x := +begin + induction n with n ih, + { simp }, + { rw [pow_succ, ←mul_assoc, mul_sub_algebra_map_commutes, + mul_assoc, ih, ←mul_assoc], } +end + +end ring + end algebra namespace module