feat(linear_algebra): eigenspaces of linear maps (#3927)

Add eigenspaces and eigenvalues of linear maps. Add lemma that in a
finite-dimensional vector space over an algebraically closed field,
eigenvalues exist. Add lemma that eigenvectors belonging to distinct
eigenvalues are linearly independent.

This is a rework of #3864, following Cyril's suggestion. Generalized
eigenspaces will come in a subsequent PR.

Author: abentkamp

src/data/finsupp/basic.lean

@@ -241,6 +241,21 @@ rfl
   (on_finset s f hf).support ⊆ s :=
 filter_subset _
 
+lemma mem_support_on_finset
+  {s : finset α} {f : α → β} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) {a : α} :
+  a ∈ (finsupp.on_finset s f hf).support ↔ f a ≠ 0 :=
+by simp [finsupp.mem_support_iff, finsupp.on_finset_apply]
+
+lemma support_on_finset
+  {s : finset α} {f : α → β} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) :
+  (finsupp.on_finset s f hf).support = s.filter (λ a, f a ≠ 0) :=
+begin
+  ext a,
+  rw [mem_support_on_finset, finset.mem_filter],
+  specialize hf a,
+  finish
+end
+
 end on_finset
 
 /-! ### Declarations about `map_range` -/

src/data/multiset/basic.lean

@@ -247,6 +247,23 @@ theorem subset_zero {s : multiset α} : s ⊆ 0 ↔ s = 0 :=
 
 end subset
 
+section to_list
+
+/-- Produces a list of the elements in the multiset using choice. -/
+@[reducible] noncomputable def to_list {α : Type*} (s : multiset α) :=
+classical.some (quotient.exists_rep s)
+
+@[simp] lemma to_list_zero {α : Type*} : (multiset.to_list 0 : list α) = [] :=
+(multiset.coe_eq_zero _).1 (classical.some_spec (quotient.exists_rep multiset.zero))
+
+lemma coe_to_list {α : Type*} (s : multiset α) : (s.to_list : multiset α) = s :=
+classical.some_spec (quotient.exists_rep _)
+
+lemma mem_to_list {α : Type*} (a : α) (s : multiset α) : a ∈ s.to_list ↔ a ∈ s :=
+by rw [←multiset.mem_coe, multiset.coe_to_list]
+
+end to_list
+
 /- multiset order -/
 
 /-- `s ≤ t` means that `s` is a sublist of `t` (up to permutation).
@@ -797,6 +814,13 @@ theorem prod_ne_zero {R : Type*} [integral_domain R] {m : multiset R} :
 multiset.induction_on m (λ _, one_ne_zero) $ λ hd tl ih H,
   by { rw forall_mem_cons at H, rw prod_cons, exact mul_ne_zero H.1 (ih H.2) }
 
+lemma prod_eq_zero {α : Type*} [comm_semiring α] {s : multiset α} (h : (0 : α) ∈ s) :
+  multiset.prod s = 0 :=
+begin
+  rcases multiset.exists_cons_of_mem h with ⟨s', hs'⟩,
+  simp [hs', multiset.prod_cons]
+end
+
 @[to_additive]
 lemma prod_hom [comm_monoid α] [comm_monoid β] (s : multiset α) (f : α → β) [is_monoid_hom f] :
   (s.map f).prod = f s.prod :=

src/field_theory/algebraic_closure.lean

@@ -62,6 +62,10 @@ theorem of_exists_root (H : ∀ p : polynomial k, p.monic → irreducible p →
  let ⟨x, hx⟩ := H (q * C (leading_coeff q)⁻¹) (monic_mul_leading_coeff_inv hq.ne_zero) this in
  degree_mul_leading_coeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root this hx⟩
 
+lemma degree_eq_one_of_irreducible [is_alg_closed k] {p : polynomial k} (h_nz : p ≠ 0) (hp : irreducible p) :
+  p.degree = 1 :=
+degree_eq_one_of_irreducible_of_splits h_nz hp (polynomial.splits' _)
+
 end is_alg_closed
 
 instance complex.is_alg_closed : is_alg_closed ℂ :=

src/field_theory/splitting_field.lean

@@ -117,6 +117,15 @@ begin
   rw [finset.prod_insert hat, splits_mul_iff i ht.1 (finset.prod_ne_zero_iff.2 ht.2), ih ht.2]
 end
 
+lemma degree_eq_one_of_irreducible_of_splits {p : polynomial β}
+  (h_nz : p ≠ 0) (hp : irreducible p) (hp_splits : splits (ring_hom.id β) p) :
+  p.degree = 1 :=
+begin
+  rcases hp_splits,
+  { contradiction },
+  { apply hp_splits hp, simp }
+end
+
 lemma exists_root_of_splits {f : polynomial α} (hs : splits i f) (hf0 : degree f ≠ 0) :
   ∃ x, eval₂ i x f = 0 :=
 if hf0 : f = 0 then ⟨37, by simp [hf0]⟩

src/group_theory/submonoid/basic.lean

@@ -339,6 +339,23 @@ lemma closure_Union {ι} (s : ι → set M) : closure (⋃ i, s i) = ⨆ i, clos
 
 end submonoid
 
+section is_unit
+
+/-- The submonoid consisting of the units of a monoid -/
+def is_unit.submonoid (M : Type*) [monoid M] : submonoid M :=
+{ carrier := set_of is_unit,
+  one_mem' := by simp only [is_unit_one, set.mem_set_of_eq],
+  mul_mem' := by { intros a b ha hb, rw set.mem_set_of_eq at *, exact is_unit.mul ha hb } }
+
+lemma is_unit.mem_submonoid_iff {M : Type*} [monoid M] (a : M) :
+  a ∈ is_unit.submonoid M ↔ is_unit a :=
+begin
+  change a ∈ set_of is_unit ↔ is_unit a,
+  rw set.mem_set_of_eq
+end
+
+end is_unit
+
 namespace monoid_hom
 
 variables {N : Type*} {P : Type*} [monoid N] [monoid P] (S : submonoid M)

src/linear_algebra/eigenspace.lean

@@ -0,0 +1,246 @@
+/-
+Copyright (c) 2020 Alexander Bentkamp. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Alexander Bentkamp.
+-/
+
+import field_theory.algebraic_closure
+import linear_algebra.finsupp
+
+/-!
+# Eigenvectors and eigenvalues
+
+This file defines eigenspaces and eigenvalues.
+
+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
+there are eigenvectors for a scalar `μ`, the scalar `μ` is called an eigenvalue.
+
+There is no consensus in the literature whether `0` is an eigenvector. Our definition of
+`eigenvector` permits only nonzero vectors. For an eigenvector `x` that may also be `0`, we write
+`x ∈ eigenspace f μ`.
+
+## 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]
+* https://en.wikipedia.org/wiki/Eigenvalues_and_eigenvectors
+
+## Tags
+
+eigenspace, eigenvector, eigenvalue, eigen
+-/
+
+universes u v w
+
+namespace module
+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)
+
+/-- 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
+
+/-- 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 :=
+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 :=
+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 :=
+by rw [eigenspace, linear_map.mem_ker, linear_map.sub_apply, algebra_map_End_apply,
+   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 :=
+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]
+
+lemma eigenspace_eval₂_polynomial_degree_1 [field K] [vector_space K V]
+  (f : End K V) (q : polynomial K) (hq : degree q = 1) :
+  eigenspace f (- q.coeff 0 / q.leading_coeff) = (eval₂ am f q).ker :=
+calc
+  eigenspace f (- q.coeff 0 / q.leading_coeff) = (q.leading_coeff • f - am (- 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 }
+  ... = (eval₂ am f (C q.leading_coeff * X + C (q.coeff 0))).ker
+    : by { rw C_mul', simpa [algebra_map, algebra.to_ring_hom] }
+  ... = (eval₂ am f q).ker
+     : by { congr, apply (eq_X_add_C_of_degree_eq_one hq).symm }
+
+lemma ker_eval₂_ring_hom_noncomm_unit_polynomial [field K] [vector_space K V]
+  (f : End K V) (c : units (polynomial K)) :
+  ((eval₂_ring_hom_noncomm am (λ x y, (algebra.commutes x y).symm) f) ↑c).ker = ⊥ :=
+begin
+  rw polynomial.eq_C_of_degree_eq_zero (degree_coe_units c),
+  simp only [eval₂_ring_hom_noncomm, ring_hom.of, ring_hom.coe_mk, eval₂_C],
+  apply ker_algebra_map_End,
+  apply coeff_coe_units_zero_ne_zero c
+end
+
+/-- 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) :
+  ∃ (c : K), f.has_eigenvalue c :=
+begin
+  classical,
+  -- Choose a nonzero vector `v`.
+  obtain ⟨v, hv⟩ : ∃ v : V, v ≠ 0 := exists_ne (0 : V),
+  -- The infinitely many vectors v, f v, f (f v), ... cannot be linearly independent
+  -- because the vector space is finite dimensional.
+  have h_lin_dep : ¬ linear_independent K (λ n : ℕ, (f ^ n) v),
+  { apply not_linear_independent_of_infinite, },
+  -- Therefore, there must be a nonzero polynomial `p` such that `p(f) v = 0`.
+  obtain ⟨p, h_eval_p, h_p_ne_0⟩ : ∃ p, eval₂ am f p v = 0 ∧ p ≠ 0,
+  { simp only [not_imp.symm],
+    exact not_forall.1 (λ h, h_lin_dep ((linear_independent_powers_iff_eval₂ f v).2 h)) },
+  -- Then `p(f)` is not invertible.
+  have h_eval_p_not_unit : eval₂_ring_hom_noncomm am _ f p ∉ is_unit.submonoid (End K V),
+  { rw [is_unit.mem_submonoid_iff, linear_map.is_unit_iff, linear_map.ker_eq_bot'],
+    intro h,
+    exact hv (h v h_eval_p) },
+  -- Hence, there must be a factor `q` of `p` such that `q(f)` is not invertible.
+  obtain ⟨q, hq_factor, hq_nonunit⟩ : ∃ q, q ∈ factors p ∧ ¬ is_unit (eval₂ am f q),
+  { 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_noncomm am (λ x y, (algebra.commutes x y).symm) f)
+      (is_unit.submonoid (End K V)) p h_p_ne_0 h _)),
+    simp only [is_unit.mem_submonoid_iff, linear_map.is_unit_iff],
+    apply ker_eval₂_ring_hom_noncomm_unit_polynomial },
+  -- Since the field is algebraically closed, `q` has degree 1.
+  have h_deg_q : q.degree = 1 := is_alg_closed.degree_eq_one_of_irreducible _
+    (ne_zero_of_mem_factors h_p_ne_0 hq_factor)
+    ((factors_spec p h_p_ne_0).1 q hq_factor),
+  -- Then the kernel of `q(f)` is an eigenspace.
+  have h_eigenspace: eigenspace f (-q.coeff 0 / q.leading_coeff) = (eval₂ am f q).ker,
+    from eigenspace_eval₂_polynomial_degree_1 f q h_deg_q,
+  -- Since `q(f)` is not invertible, the kernel is not `⊥`, and thus there exists an eigenvalue.
+  show ∃ (c : K), f.has_eigenvalue c,
+  { use -q.coeff 0 / q.leading_coeff,
+    rw [has_eigenvalue, h_eigenspace],
+    intro h_eval_ker,
+    exact hq_nonunit ((linear_map.is_unit_iff (eval₂ am f q)).2 h_eval_ker) }
+end
+
+/-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly
+    independent. (Axler's Proposition 2.2)
+
+    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)
+  (h_eigenvec : ∀ μ : μs, f.has_eigenvector μ (xs μ)) :
+  linear_independent K xs :=
+begin
+  classical,
+  -- We need to show that if a linear combination `l` of the eigenvectors `xs` is `0`, then all
+  -- its coefficients are zero.
+  suffices : ∀ l, finsupp.total μs V K xs l = 0 → l = 0,
+  { rw linear_independent_iff,
+    apply this },
+  intros l hl,
+  -- We apply induction on the finite set of eigenvalues whose eigenvectors have nonzero
+  -- coefficients, i.e. on the support of `l`.
+  induction h_l_support : l.support using finset.induction with μ₀ l_support' hμ₀ ih generalizing l,
+  -- If the support is empty, all coefficients are zero and we are done.
+  { exact finsupp.support_eq_empty.1 h_l_support },
+  -- Now assume that the support of `l` contains at least one eigenvalue `μ₀`. We define a new
+  -- linear combination `l'` to apply the induction hypothesis on later. The linear combination `l'`
+  -- is derived from `l` by multiplying the coefficient of the eigenvector with eigenvalue `μ`
+  -- by `μ - μ₀`.
+  -- To get started, we define `l'` as a function `l'_f : μs → K` with potentially infinite support.
+  { let l'_f : μs → K := (λ μ : μs, (↑μ - ↑μ₀) * l μ),
+    -- The support of `l'_f` is the support of `l` without `μ₀`.
+    have h_l_support' : ∀ (μ : μs), μ ∈ l_support' ↔ l'_f μ ≠ 0 ,
+    { intro μ,
+      suffices : μ ∈ l_support' → μ ≠ μ₀,
+      { simp [l'_f, ← finsupp.not_mem_support_iff, h_l_support, sub_eq_zero, ←subtype.ext_iff],
+        tauto },
+      rintro hμ rfl,
+      contradiction },
+    -- Now we can define `l'_f` as an actual linear combination `l'` because we know that the
+    -- support is finite.
+    let l' : μs →₀ K :=
+      { 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 μ₀,
+      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],
+      have h_useless_filter : finset.filter (λ (a : μs), l'_f a ≠ 0) l_support' = l_support',
+      { rw finset.filter_congr _,
+        { apply finset.filter_true },
+        { apply_instance },
+        exact λ μ hμ, (iff_true _).mpr ((h_l_support' μ).1 hμ) },
+      have bodies_eq : ∀ (μ : μs), l'_f μ • xs μ = g (l μ • xs μ),
+      { intro μ,
+        dsimp only [g, l'_f],
+        rw [linear_map.map_smul, linear_map.sub_apply, mem_eigenspace_iff.1 (h_eigenvec _).2,
+          algebra_map_End_apply, ←sub_smul, smul_smul, mul_comm] },
+      rw [←linear_map.map_zero g, ←hl, finsupp.total_apply, finsupp.total_apply,
+          finsupp.sum, finsupp.sum, linear_map.map_sum, h_l_support,
+          finset.sum_insert hμ₀, h_gμ₀, zero_add],
+      refine finset.sum_congr rfl (λ μ _, _),
+      apply bodies_eq },
+    -- Therefore, by the induction hypothesis, all coefficients in `l'` are zero.
+    have l'_eq_0 : l' = 0 := ih l' total_l' rfl,
+    -- By the defintion of `l'`, this means that `(μ - μ₀) * l μ = 0` for all `μ`.
+    have h_mul_eq_0 : ∀ μ : μs, (↑μ - ↑μ₀) * l μ = 0,
+    { intro μ,
+      calc (↑μ - ↑μ₀) * l μ = l' μ : rfl
+      ... = 0 : by { rw [l'_eq_0], refl } },
+    -- Thus, the coefficients in `l` for all `μ ≠ μ₀` are `0`.
+    have h_lμ_eq_0 : ∀ μ : μs, μ ≠ μ₀ → l μ = 0,
+    { intros μ hμ,
+      apply or_iff_not_imp_left.1 (mul_eq_zero.1 (h_mul_eq_0 μ)),
+      rwa [sub_eq_zero, ←subtype.ext_iff] },
+    -- So if we sum over all these coefficients, we obtain `0`.
+    have h_sum_l_support'_eq_0 : finset.sum l_support' (λ (μ : ↥μs), l μ • xs μ) = 0,
+    { rw ←finset.sum_const_zero,
+      apply finset.sum_congr rfl,
+      intros μ hμ,
+      rw h_lμ_eq_0,
+      apply zero_smul,
+      intro h,
+      rw h at hμ,
+      contradiction },
+    -- The only potentially nonzero coefficient in `l` is the one corresponding to `μ₀`. But since
+    -- the overall sum is `0` by assumption, this coefficient must also be `0`.
+    have : l μ₀ = 0,
+    { rw [finsupp.total_apply, finsupp.sum, h_l_support,
+          finset.sum_insert hμ₀, h_sum_l_support'_eq_0, add_zero] at hl,
+      by_contra h,
+      exact (h_eigenvec μ₀).1 ((smul_eq_zero.1 hl).resolve_left h) },
+    -- Thus, all coefficients in `l` are `0`.
+    show l = 0,
+    { ext μ,
+      by_cases h_cases : μ = μ₀,
+      { rw h_cases,
+        assumption },
+      exact h_lμ_eq_0 μ h_cases } }
+end
+
+end End
+end module

src/linear_algebra/finite_dimensional.lean

@@ -255,6 +255,15 @@ begin
   apply cardinal.nat_lt_omega,
 end
 
+lemma not_linear_independent_of_infinite {ι : Type w} [inf : infinite ι] [finite_dimensional K V]
+  (v : ι → V) : ¬ linear_independent K v :=
+begin
+  intro h_lin_indep,
+  have : ¬ omega ≤ mk ι := not_le.mpr (lt_omega_of_linear_independent h_lin_indep),
+  have : omega ≤ mk ι := infinite_iff.mp inf,
+  contradiction
+end
+
 /-- A finite dimensional space has positive `findim` iff it has a nonzero element. -/
 lemma findim_pos_iff_exists_ne_zero [finite_dimensional K V] : 0 < findim K V ↔ ∃ x : V, x ≠ 0 :=
 iff.trans (by { rw ← findim_eq_dim, norm_cast }) (@dim_pos_iff_exists_ne_zero K V _ _ _)

src/linear_algebra/finsupp.lean

@@ -395,6 +395,18 @@ lemma total_comap_domain
    (l.support.preimage f hf).sum (λ i, (l (f i)) • (v i)) :=
 by rw finsupp.total_apply; refl
 
+lemma total_on_finset
+  {s : finset α} {f : α → R} (g : α → M) (hf : ∀ a, f a ≠ 0 → a ∈ s):
+  finsupp.total α M R g (finsupp.on_finset s f hf) =
+    finset.sum s (λ (x : α), f x • g x) :=
+begin
+  simp only [finsupp.total_apply, finsupp.sum, finsupp.on_finset_apply, finsupp.support_on_finset],
+  rw finset.sum_filter_of_ne,
+  intros x hx h,
+  contrapose! h,
+  simp [h],
+end
+
 end total
 
 /-- An equivalence of domains induces a linear equivalence of finitely supported functions. -/