chore(LinearAlgebra): prepare library for API refactor (#16738)

This PR adds equation lemmas for several concepts around eigenspaces,
eigenvectors, and eigenvalues, and uses these lemmas in the rest of the
library.

The result is an improved API boundary which allows for a refactor (and
generalization) of the definitions in follow up work.

Author: jcommelin

Mathlib/Algebra/Lie/Sl2.lean

@@ -148,7 +148,7 @@ lemma exists_nat [IsNoetherian R M] [NoZeroSMulDivisors R M] [IsDomain R] [CharZ
     {μ - 2 * n | n : ℕ}
     (fun ⟨s, hs⟩ ↦ ψ Classical.choose hs)
     (fun ⟨r, hr⟩ ↦ by simp [lie_h_pow_toEnd_f P, Classical.choose_spec hr, contra,
-      Module.End.HasEigenvector, Module.End.mem_eigenspace_iff])).finite
+      Module.End.hasEigenvector_iff, Module.End.mem_eigenspace_iff])).finite
 
 lemma pow_toEnd_f_ne_zero_of_eq_nat
     [CharZero R] [NoZeroSMulDivisors R M]

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -165,7 +165,7 @@ theorem mem_genWeightSpaceOf (χ : R) (x : L) (m : M) :
 
 theorem coe_genWeightSpaceOf_zero (x : L) :
     ↑(genWeightSpaceOf M (0 : R) x) = ⨆ k, LinearMap.ker (toEnd R L M x ^ k) := by
-  simp [genWeightSpaceOf, Module.End.maxGenEigenspace]
+  simp [genWeightSpaceOf, Module.End.maxGenEigenspace_def]
 
 /-- If `M` is a representation of a nilpotent Lie algebra `L`
 and `χ : L → R` is a family of scalars,
@@ -272,7 +272,7 @@ lemma genWeightSpaceOf_ne_bot (χ : Weight R L M) (x : L) :
 lemma hasEigenvalueAt (χ : Weight R L M) (x : L) :
     (toEnd R L M x).HasEigenvalue (χ x) := by
   obtain ⟨k : ℕ, hk : (toEnd R L M x).genEigenspace (χ x) k ≠ ⊥⟩ := by
-    simpa [Module.End.maxGenEigenspace, genWeightSpaceOf] using χ.genWeightSpaceOf_ne_bot x
+    simpa [genWeightSpaceOf, Module.End.maxGenEigenspace_def] using χ.genWeightSpaceOf_ne_bot x
   exact Module.End.hasEigenvalue_of_hasGenEigenvalue hk
 
 lemma apply_eq_zero_of_isNilpotent [NoZeroSMulDivisors R M] [IsReduced R]
@@ -313,7 +313,7 @@ theorem exists_genWeightSpace_le_ker_of_isNoetherian [IsNoetherian R M] (χ : L
   intro m hm
   replace hm : m ∈ (toEnd R L M x).maxGenEigenspace (χ x) :=
     genWeightSpace_le_genWeightSpaceOf M x χ hm
-  rwa [Module.End.maxGenEigenspace_eq] at hm
+  rwa [Module.End.maxGenEigenspace_eq, Module.End.genEigenspace_def] at hm
 
 variable (R) in
 theorem exists_genWeightSpace_zero_le_ker_of_isNoetherian
@@ -638,6 +638,8 @@ end fitting_decomposition
 lemma disjoint_genWeightSpaceOf [NoZeroSMulDivisors R M] {x : L} {φ₁ φ₂ : R} (h : φ₁ ≠ φ₂) :
     Disjoint (genWeightSpaceOf M φ₁ x) (genWeightSpaceOf M φ₂ x) := by
   rw [LieSubmodule.disjoint_iff_coe_toSubmodule]
+  dsimp [genWeightSpaceOf]
+  simp_rw [Module.End.maxGenEigenspace_def]
   exact Module.End.disjoint_iSup_genEigenspace _ h
 
 lemma disjoint_genWeightSpace [NoZeroSMulDivisors R M] {χ₁ χ₂ : L → R} (h : χ₁ ≠ χ₂) :
@@ -707,6 +709,8 @@ lemma independent_genWeightSpace' [NoZeroSMulDivisors R M] :
 lemma independent_genWeightSpaceOf [NoZeroSMulDivisors R M] (x : L) :
     CompleteLattice.Independent fun (χ : R) ↦ genWeightSpaceOf M χ x := by
   rw [LieSubmodule.independent_iff_coe_toSubmodule]
+  dsimp [genWeightSpaceOf]
+  simp_rw [Module.End.maxGenEigenspace_def]
   exact (toEnd R L M x).independent_genEigenspace
 
 lemma finite_genWeightSpaceOf_ne_bot [NoZeroSMulDivisors R M] [IsNoetherian R M] (x : L) :
@@ -747,6 +751,8 @@ lemma iSup_genWeightSpaceOf_eq_top [IsTriangularizable R L M] (x : L) :
     ⨆ (φ : R), genWeightSpaceOf M φ x = ⊤ := by
   rw [← LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.iSup_coe_toSubmodule,
     LieSubmodule.top_coeSubmodule]
+  dsimp [genWeightSpaceOf]
+  simp_rw [Module.End.maxGenEigenspace_def]
   exact IsTriangularizable.iSup_eq_top x
 
 open LinearMap FiniteDimensional in

Mathlib/Algebra/Lie/Weights/Linear.lean

@@ -98,13 +98,15 @@ instance instLinearWeightsOfIsLieAbelian [IsLieAbelian L] [NoZeroSMulDivisors R
       rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero]
     intro χ hχ x y
     simp_rw [Ne, ← LieSubmodule.coe_toSubmodule_eq_iff, genWeightSpace, genWeightSpaceOf,
-      LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule] at hχ
+      LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule,
+      Module.End.maxGenEigenspace_def] at hχ
     exact Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute
       (toEnd R L M).toLinearMap χ hχ h x y
   { map_add := aux
     map_smul := fun χ hχ t x ↦ by
       simp_rw [Ne, ← LieSubmodule.coe_toSubmodule_eq_iff, genWeightSpace, genWeightSpaceOf,
-        LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule] at hχ
+        LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule,
+        Module.End.maxGenEigenspace_def] at hχ
       exact Module.End.map_smul_of_iInf_genEigenspace_ne_bot
         (toEnd R L M).toLinearMap χ hχ t x
     map_lie := fun χ hχ t x ↦ by

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

@@ -63,18 +63,26 @@ variable {K R : Type v} {V M : Type w} [CommRing R] [AddCommGroup M] [Module R M
 def eigenspace (f : End R M) (μ : R) : Submodule R M :=
   LinearMap.ker (f - algebraMap R (End R M) μ)
 
+lemma eigenspace_def (f : End R M) (μ : R) :
+    f.eigenspace μ = LinearMap.ker (f - algebraMap R (End R M) μ) := rfl
+
 @[simp]
 theorem eigenspace_zero (f : End R M) : f.eigenspace 0 = LinearMap.ker f := by simp [eigenspace]
 
 /-- A nonzero element of an eigenspace is an eigenvector. (Def 5.7 of [axler2015]) -/
 def HasEigenvector (f : End R M) (μ : R) (x : M) : Prop :=
   x ∈ eigenspace f μ ∧ x ≠ 0
 
+lemma hasEigenvector_iff {f : End R M} {μ : R} {x : M} :
+    f.HasEigenvector μ x ↔ x ∈ eigenspace f μ ∧ x ≠ 0 := Iff.rfl
+
 /-- A scalar `μ` is an eigenvalue for a linear map `f` if there are nonzero vectors `x`
     such that `f x = μ • x`. (Def 5.5 of [axler2015]) -/
 def HasEigenvalue (f : End R M) (a : R) : Prop :=
   eigenspace f a ≠ ⊥
 
+lemma hasEigenvalue_iff (f : End R M) (μ : R) : f.HasEigenvalue μ ↔ eigenspace f μ ≠ ⊥ := Iff.rfl
+
 /-- The eigenvalues of the endomorphism `f`, as a subtype of `R`. -/
 def Eigenvalues (f : End R M) : Type _ :=
   { μ : R // f.HasEigenvalue μ }
@@ -161,6 +169,9 @@ def genEigenspace (f : End R M) (μ : R) : ℕ →o Submodule R M where
       LinearMap.ker_le_ker_comp ((f - algebraMap R (End R M) μ) ^ k)
         ((f - algebraMap R (End R M) μ) ^ (m - k))
 
+lemma genEigenspace_def (f : End R M) (μ : R) (k : ℕ) :
+    f.genEigenspace μ k = LinearMap.ker ((f - algebraMap R (End R M) μ) ^ k) := rfl
+
 @[simp]
 theorem mem_genEigenspace (f : End R M) (μ : R) (k : ℕ) (m : M) :
     m ∈ f.genEigenspace μ k ↔ ((f - μ • (1 : End R M)) ^ k) m = 0 := Iff.rfl
@@ -175,16 +186,25 @@ theorem genEigenspace_zero (f : End R M) (k : ℕ) :
 def HasGenEigenvector (f : End R M) (μ : R) (k : ℕ) (x : M) : Prop :=
   x ≠ 0 ∧ x ∈ genEigenspace f μ k
 
+lemma hasGenEigenvector_iff {f : End R M} {μ : R} {k : ℕ} {x : M} :
+    f.HasGenEigenvector μ k x ↔ x ≠ 0 ∧ x ∈ f.genEigenspace μ k := Iff.rfl
+
 /-- 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 HasGenEigenvalue (f : End R M) (μ : R) (k : ℕ) : Prop :=
   genEigenspace f μ k ≠ ⊥
 
+lemma hasGenEigenvalue_iff (f : End R M) (μ : R) (k : ℕ) :
+    f.HasGenEigenvalue μ k ↔ genEigenspace f μ k ≠ ⊥ := Iff.rfl
+
 /-- The generalized eigenrange for a linear map `f`, a scalar `μ`, and an exponent `k ∈ ℕ` is the
     range of `(f - μ • id) ^ k`. -/
 def genEigenrange (f : End R M) (μ : R) (k : ℕ) : Submodule R M :=
   LinearMap.range ((f - algebraMap R (End R M) μ) ^ k)
 
+lemma genEigenrange_def (f : End R M) (μ : R) (k : ℕ) :
+    f.genEigenrange μ k = LinearMap.range ((f - algebraMap R (End R M) μ) ^ k) := rfl
+
 /-- The exponent of a generalized eigenvalue is never 0. -/
 theorem exp_ne_zero_of_hasGenEigenvalue {f : End R M} {μ : R} {k : ℕ}
     (h : f.HasGenEigenvalue μ k) : k ≠ 0 := by
@@ -195,6 +215,9 @@ theorem exp_ne_zero_of_hasGenEigenvalue {f : End R M} {μ : R} {k : ℕ}
 def maxGenEigenspace (f : End R M) (μ : R) : Submodule R M :=
   ⨆ k, f.genEigenspace μ k
 
+lemma maxGenEigenspace_def (f : End R M) (μ : R) :
+    f.maxGenEigenspace μ = ⨆ k, f.genEigenspace μ k := rfl
+
 theorem genEigenspace_le_maximal (f : End R M) (μ : R) (k : ℕ) :
     f.genEigenspace μ k ≤ f.maxGenEigenspace μ :=
   le_iSup _ _

Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

@@ -68,7 +68,7 @@ variable {f} {μ : K}
 
 theorem hasEigenvalue_of_isRoot (h : (minpoly K f).IsRoot μ) : f.HasEigenvalue μ := by
   cases' dvd_iff_isRoot.2 h with p hp
-  rw [HasEigenvalue, eigenspace]
+  rw [hasEigenvalue_iff, eigenspace_def]
   intro con
   cases' (LinearMap.isUnit_iff_ker_eq_bot _).2 con with u hu
   have p_ne_0 : p ≠ 0 := by

Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean

@@ -55,7 +55,7 @@ lemma IsSemisimple.genEigenspace_eq_eigenspace
 lemma IsSemisimple.maxGenEigenspace_eq_eigenspace
     (hf : f.IsSemisimple) (μ : R) :
     f.maxGenEigenspace μ = f.eigenspace μ := by
-  simp_rw [maxGenEigenspace, ← (f.genEigenspace μ).monotone.iSup_nat_add 1,
+  simp_rw [maxGenEigenspace_def, ← (f.genEigenspace μ).monotone.iSup_nat_add 1,
     hf.genEigenspace_eq_eigenspace μ (Nat.zero_lt_succ _), ciSup_const]
 
 end Module.End

Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

@@ -53,7 +53,7 @@ theorem exists_hasEigenvalue_of_iSup_genEigenspace_eq_top [Nontrivial M] {f : En
   intro μ
   replace contra : ∀ k, f.genEigenspace μ k = ⊥ := fun k ↦ by
     have hk : ¬ f.HasGenEigenvalue μ k := fun hk ↦ contra μ (f.hasEigenvalue_of_hasGenEigenvalue hk)
-    rwa [HasGenEigenvalue, not_not] at hk
+    rwa [hasGenEigenvalue_iff, not_not] at hk
   simp [contra]
 
 -- This is Lemma 5.21 of [axler2015], although we are no longer following that proof.
@@ -99,6 +99,8 @@ theorem iSup_genEigenspace_eq_top [IsAlgClosed K] [FiniteDimensional K V] (f : E
       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_def, Module.End.genEigenrange_def]
       apply LinearMap.finrank_range_add_finrank_ker
     -- Therefore the dimension `ER` mus be smaller than `finrank K V`.
     have h_dim_ER : finrank K ER < n.succ := by linarith
@@ -168,7 +170,8 @@ theorem inf_iSup_genEigenspace [FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈
     · rw [hμμ']
     replace hm₂ : ((f - algebraMap K (End K V) μ') ^ finrank K V) (m μ') = 0 := by
       obtain ⟨k, hk⟩ := (mem_iSup_of_chain _ _).mp (hm₂ μ')
-      exact Module.End.genEigenspace_le_genEigenspace_finrank _ _ k hk
+      simpa only [End.mem_genEigenspace] using
+        Module.End.genEigenspace_le_genEigenspace_finrank _ _ k hk
     have : _ = g := (m.support.erase μ).noncommProd_erase_mul (Finset.mem_erase.mpr ⟨hμμ', hμ'⟩)
       (fun μ ↦ (f - algebraMap K (End K V) μ) ^ finrank K V) (fun μ₁ _ μ₂ _ _ ↦ h_comm μ₁ μ₂)
     rw [← this, LinearMap.mul_apply, hm₂, _root_.map_zero]
@@ -185,9 +188,10 @@ theorem inf_iSup_genEigenspace [FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈
     apply LinearMap.injOn_of_disjoint_ker (subset_refl _)
     have this := f.independent_genEigenspace
     simp_rw [f.iSup_genEigenspace_eq_genEigenspace_finrank] at this ⊢
-    rw [LinearMap.ker_noncommProd_eq_of_supIndep_ker _ _ <| this.supIndep' (m.support.erase μ),
-      ← Finset.sup_eq_iSup]
-    exact Finset.supIndep_iff_disjoint_erase.mp (this.supIndep' m.support) μ hμ
+    rw [LinearMap.ker_noncommProd_eq_of_supIndep_ker, ← Finset.sup_eq_iSup]
+    · simpa only [End.genEigenspace_def] using
+        Finset.supIndep_iff_disjoint_erase.mp (this.supIndep' m.support) μ hμ
+    · simpa only [End.genEigenspace_def] using this.supIndep' (m.support.erase μ)
   have hg₄ : SurjOn g
       ↑(p ⊓ ⨆ k, f.genEigenspace μ k) ↑(p ⊓ ⨆ k, f.genEigenspace μ k) := by
     have : MapsTo g

Mathlib/LinearAlgebra/Eigenspace/Zero.lean

@@ -135,7 +135,7 @@ lemma finrank_maxGenEigenspace (φ : Module.End K M) :
     finrank K (φ.maxGenEigenspace 0) = natTrailingDegree (φ.charpoly) := by
   set V := φ.maxGenEigenspace 0
   have hV : V = ⨆ (n : ℕ), ker (φ ^ n) := by
-    simp [V, Module.End.maxGenEigenspace, Module.End.genEigenspace]
+    simp [V, Module.End.maxGenEigenspace_def, Module.End.genEigenspace_def]
   let W := ⨅ (n : ℕ), LinearMap.range (φ ^ n)
   have hVW : IsCompl V W := by
     rw [hV]

Mathlib/LinearAlgebra/Matrix/Gershgorin.lean

@@ -62,7 +62,7 @@ theorem det_ne_zero_of_sum_row_lt_diag (h : ∀ k, ∑ j ∈ Finset.univ.erase k
   suffices ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖) by
     exact this.imp (fun a h ↦ by rwa [mem_closedBall_iff_norm', sub_zero] at h)
   refine eigenvalue_mem_ball ?_
-  rw [Module.End.HasEigenvalue,  Module.End.eigenspace_zero, ne_comm]
+  rw [Module.End.hasEigenvalue_iff, Module.End.eigenspace_zero, ne_comm]
   exact ne_of_lt (LinearMap.bot_lt_ker_of_det_eq_zero (by rwa [LinearMap.det_toLin']))
 
 /-- If `A` is a column strictly dominant diagonal matrix, then it's determinant is nonzero. -/