From 453f2183f268b3c80786a02e2f646cf3c1ba1b4a Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Sun, 26 Sep 2021 10:39:52 +0000
Subject: [PATCH] refactor(linear_algebra/charpoly): move
 linear_algebra/charpoly to linear_algebra/matrix/charpoly (#9368)

We move `linear_algebra/charpoly`to `linear_algebra/matrix/charpoly`, since the results there are for matrices. We also rename some lemmas in `linear_algebra/matrix/charpoly/coeff` to have the namespace `matrix`.
---
 .../83_friendship_graphs.lean                 |  2 +-
 docs/100.yaml                                 |  2 +-
 docs/overview.yaml                            |  2 +-
 docs/undergrad.yaml                           |  2 +-
 src/linear_algebra/charpoly.lean              |  2 +-
 .../{ => matrix}/charpoly/basic.lean          |  2 +-
 .../{ => matrix}/charpoly/coeff.lean          | 39 ++++++++++---------
 src/ring_theory/norm.lean                     |  2 +-
 src/ring_theory/trace.lean                    |  2 +-
 9 files changed, 29 insertions(+), 26 deletions(-)
 rename src/linear_algebra/{ => matrix}/charpoly/basic.lean (98%)
 rename src/linear_algebra/{ => matrix}/charpoly/coeff.lean (88%)

diff --git a/archive/100-theorems-list/83_friendship_graphs.lean b/archive/100-theorems-list/83_friendship_graphs.lean
index e6233ee04bf08..bf2f99f99942f 100644
--- a/archive/100-theorems-list/83_friendship_graphs.lean
+++ b/archive/100-theorems-list/83_friendship_graphs.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jalex Stark, Kyle Miller
 -/
 import combinatorics.simple_graph.adj_matrix
-import linear_algebra.charpoly.coeff
+import linear_algebra.matrix.charpoly.coeff
 import data.int.modeq
 import data.zmod.basic
 import tactic.interval_cases
diff --git a/docs/100.yaml b/docs/100.yaml
index 2a729194d67f0..5a076e62bdefd 100644
--- a/docs/100.yaml
+++ b/docs/100.yaml
@@ -163,7 +163,7 @@
   title  : Dirichlet’s Theorem
 49:
   title  : The Cayley-Hamilton Theorem
-  decl   : aeval_self_charpoly
+  decl   : matrix.aeval_self_charpoly
   author : Scott Morrison
 50:
   title  : The Number of Platonic Solids
diff --git a/docs/overview.yaml b/docs/overview.yaml
index e3f3c0676c2f1..f77b0a77ce65e 100644
--- a/docs/overview.yaml
+++ b/docs/overview.yaml
@@ -165,7 +165,7 @@ Linear algebra:
   Endomorphism polynomials:
     minimal polynomial: 'minpoly'
     characteristic polynomial: 'matrix.charpoly'
-    Cayley-Hamilton theorem: 'aeval_self_charpoly'
+    Cayley-Hamilton theorem: 'matrix.aeval_self_charpoly'
   Structure theory of endomorphisms:
     eigenvalue: 'module.End.has_eigenvalue'
     eigenvector: 'module.End.has_eigenvector'
diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
index ac541cdda2976..1b77d98b09fa9 100644
--- a/docs/undergrad.yaml
+++ b/docs/undergrad.yaml
@@ -54,7 +54,7 @@ Linear algebra:
     annihilating polynomials: ''
     minimal polynomial: 'minpoly'
     characteristic polynomial: 'matrix.charpoly'
-    Cayley-Hamilton theorem: 'aeval_self_charpoly'
+    Cayley-Hamilton theorem: 'matrix.aeval_self_charpoly'
   Structure theory of endomorphisms:
     eigenvalue: 'module.End.has_eigenvalue'
     eigenvector: 'module.End.has_eigenvector'
diff --git a/src/linear_algebra/charpoly.lean b/src/linear_algebra/charpoly.lean
index 204e0746036d1..e34e2b16f4d1f 100644
--- a/src/linear_algebra/charpoly.lean
+++ b/src/linear_algebra/charpoly.lean
@@ -5,7 +5,7 @@ Authors: Riccardo Brasca
 -/
 
 import linear_algebra.free_module
-import linear_algebra.charpoly.coeff
+import linear_algebra.matrix.charpoly.coeff
 import linear_algebra.matrix.basis
 
 /-!
diff --git a/src/linear_algebra/charpoly/basic.lean b/src/linear_algebra/matrix/charpoly/basic.lean
similarity index 98%
rename from src/linear_algebra/charpoly/basic.lean
rename to src/linear_algebra/matrix/charpoly/basic.lean
index 0a0c3f9716776..507bca480ddb1 100644
--- a/src/linear_algebra/charpoly/basic.lean
+++ b/src/linear_algebra/matrix/charpoly/basic.lean
@@ -96,7 +96,7 @@ applied to the matrix itself, is zero.
 This holds over any commutative ring.
 -/
 -- This proof follows http://drorbn.net/AcademicPensieve/2015-12/CayleyHamilton.pdf
-theorem aeval_self_charpoly (M : matrix n n R) :
+theorem matrix.aeval_self_charpoly (M : matrix n n R) :
   aeval M M.charpoly = 0 :=
 begin
   -- We begin with the fact $χ_M(t) I = adjugate (t I - M) * (t I - M)$,
diff --git a/src/linear_algebra/charpoly/coeff.lean b/src/linear_algebra/matrix/charpoly/coeff.lean
similarity index 88%
rename from src/linear_algebra/charpoly/coeff.lean
rename to src/linear_algebra/matrix/charpoly/coeff.lean
index d39ed4b2f9601..f844eaa2a0368 100644
--- a/src/linear_algebra/charpoly/coeff.lean
+++ b/src/linear_algebra/matrix/charpoly/coeff.lean
@@ -8,7 +8,7 @@ import algebra.polynomial.big_operators
 import data.matrix.char_p
 import field_theory.finite.basic
 import group_theory.perm.cycles
-import linear_algebra.charpoly.basic
+import linear_algebra.matrix.charpoly.basic
 import linear_algebra.matrix.trace
 import ring_theory.polynomial.basic
 import ring_theory.power_basis
@@ -20,12 +20,12 @@ We give methods for computing coefficients of the characteristic polynomial.
 
 ## Main definitions
 
-- `charpoly_degree_eq_dim` proves that the degree of the characteristic polynomial
+- `matrix.charpoly_degree_eq_dim` proves that the degree of the characteristic polynomial
   over a nonzero ring is the dimension of the matrix
-- `det_eq_sign_charpoly_coeff` proves that the determinant is the constant term of the
+- `matrix.det_eq_sign_charpoly_coeff` proves that the determinant is the constant term of the
   characteristic polynomial, up to sign.
-- `trace_eq_neg_charpoly_coeff` proves that the trace is the negative of the (d-1)th coefficient of
-  the characteristic polynomial, where d is the dimension of the matrix.
+- `matrix.trace_eq_neg_charpoly_coeff` proves that the trace is the negative of the (d-1)th
+  coefficient of the characteristic polynomial, where d is the dimension of the matrix.
   For a nonzero ring, this is the second-highest coefficient.
 
 -/
@@ -43,7 +43,6 @@ variables {α β : Type v} [decidable_eq α]
 
 
 open finset
-open polynomial
 
 variable {M : matrix n n R}
 
@@ -55,6 +54,8 @@ lemma charmatrix_apply_nat_degree_le (i j : n) :
   (charmatrix M i j).nat_degree ≤ ite (i = j) 1 0 :=
 by split_ifs; simp [h, nat_degree_X_sub_C_le]
 
+namespace matrix
+
 variable (M)
 lemma charpoly_sub_diagonal_degree_lt :
 (M.charpoly - ∏ (i : n), (X - C (M i i))).degree < ↑(fintype.card n - 1) :=
@@ -116,7 +117,7 @@ begin
 end
 
 theorem trace_eq_neg_charpoly_coeff [nonempty n] (M : matrix n n R) :
-  (matrix.trace n R R) M = -M.charpoly.coeff (fintype.card n - 1) :=
+  (trace n R R) M = -M.charpoly.coeff (fintype.card n - 1) :=
 begin
   nontriviality,
   rw charpoly_coeff_eq_prod_coeff_of_le, swap, refl,
@@ -131,8 +132,8 @@ begin
   unfold polynomial.eval, unfold eval₂,
   transitivity polynomial.sum (mat_poly_equiv M) (λ (e : ℕ) (a : matrix n n R),
     (a * (scalar n) r ^ e) i j),
-  { unfold polynomial.sum, rw matrix.sum_apply, dsimp, refl },
-  { simp_rw [←ring_hom.map_pow, ←(matrix.scalar.commute _ _).eq],
+  { unfold polynomial.sum, rw sum_apply, dsimp, refl },
+  { simp_rw [←ring_hom.map_pow, ←(scalar.commute _ _).eq],
     simp only [coe_scalar, matrix.one_mul, ring_hom.id_apply,
       pi.smul_apply, smul_eq_mul, mul_eq_mul, algebra.smul_mul_assoc],
     have h : ∀ x : ℕ, (λ (e : ℕ) (a : R), r ^ e * a) x 0 = 0 := by simp,
@@ -144,7 +145,7 @@ begin
 end
 
 lemma eval_det (M : matrix n n (polynomial R)) (r : R) :
-  polynomial.eval r M.det = (polynomial.eval (matrix.scalar n r) (mat_poly_equiv M)).det :=
+  polynomial.eval r M.det = (polynomial.eval (scalar n r) (mat_poly_equiv M)).det :=
 begin
   rw [polynomial.eval, ← coe_eval₂_ring_hom, ring_hom.map_det],
   apply congr_arg det, ext, symmetry, convert mat_poly_equiv_eval _ _ _ _,
@@ -157,6 +158,8 @@ begin
   simp
 end
 
+end matrix
+
 variables {p : ℕ} [fact p.prime]
 
 lemma mat_poly_equiv_eq_X_pow_sub_C {K : Type*} (k : ℕ) [field K] (M : matrix n n K) :
@@ -178,8 +181,8 @@ begin
       not_false_iff] }
 end
 
-@[simp] lemma finite_field.charpoly_pow_card {K : Type*} [field K] [fintype K] (M : matrix n n K) :
-  (M ^ (fintype.card K)).charpoly = M.charpoly :=
+@[simp] lemma finite_field.matrix.charpoly_pow_card {K : Type*} [field K] [fintype K]
+  (M : matrix n n K) : (M ^ (fintype.card K)).charpoly = M.charpoly :=
 begin
   casesI (is_empty_or_nonempty n).symm,
   { cases char_p.exists K with p hp, letI := hp,
@@ -197,18 +200,18 @@ begin
     { exact (id (mat_poly_equiv_eq_X_pow_sub_C (p ^ k) M) : _) },
     { exact (C M).commute_X } },
   { -- TODO[gh-6025]: remove this `haveI` once `subsingleton_of_empty_right` is a global instance
-    haveI : subsingleton (matrix n n K) := matrix.subsingleton_of_empty_right,
+    haveI : subsingleton (matrix n n K) := subsingleton_of_empty_right,
     exact congr_arg _ (subsingleton.elim _ _), },
 end
 
 @[simp] lemma zmod.charpoly_pow_card (M : matrix n n (zmod p)) :
   (M ^ p).charpoly = M.charpoly :=
-by { have h := finite_field.charpoly_pow_card M, rwa zmod.card at h, }
+by { have h := finite_field.matrix.charpoly_pow_card M, rwa zmod.card at h, }
 
 lemma finite_field.trace_pow_card {K : Type*} [field K] [fintype K] [nonempty n]
   (M : matrix n n K) : trace n K K (M ^ (fintype.card K)) = (trace n K K M) ^ (fintype.card K) :=
-by rw [trace_eq_neg_charpoly_coeff, trace_eq_neg_charpoly_coeff,
-       finite_field.charpoly_pow_card, finite_field.pow_card]
+by rw [matrix.trace_eq_neg_charpoly_coeff, matrix.trace_eq_neg_charpoly_coeff,
+       finite_field.matrix.charpoly_pow_card, finite_field.pow_card]
 
 lemma zmod.trace_pow_card {p:ℕ} [fact p.prime] [nonempty n] (M : matrix n n (zmod p)) :
   trace n (zmod p) (zmod p) (M ^ p) = (trace n (zmod p) (zmod p) M)^p :=
@@ -239,11 +242,11 @@ lemma charpoly_left_mul_matrix {K S : Type*} [field K] [comm_ring S] [algebra K
   (left_mul_matrix h.basis h.gen).charpoly = minpoly K h.gen :=
 begin
   apply minpoly.unique,
-  { apply charpoly_monic },
+  { apply matrix.charpoly_monic },
   { apply (left_mul_matrix _).injective_iff.mp (left_mul_matrix_injective h.basis),
     rw [← polynomial.aeval_alg_hom_apply, aeval_self_charpoly] },
   { intros q q_monic root_q,
-    rw [charpoly_degree_eq_dim, fintype.card_fin, degree_eq_nat_degree q_monic.ne_zero],
+    rw [matrix.charpoly_degree_eq_dim, fintype.card_fin, degree_eq_nat_degree q_monic.ne_zero],
     apply with_bot.some_le_some.mpr,
     exact h.dim_le_nat_degree_of_root q_monic.ne_zero root_q }
 end
diff --git a/src/ring_theory/norm.lean b/src/ring_theory/norm.lean
index b88b547a24ce7..3552686196829 100644
--- a/src/ring_theory/norm.lean
+++ b/src/ring_theory/norm.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 
-import linear_algebra.charpoly.coeff
+import linear_algebra.matrix.charpoly.coeff
 import linear_algebra.determinant
 import ring_theory.power_basis
 
diff --git a/src/ring_theory/trace.lean b/src/ring_theory/trace.lean
index ca5fd3b52c4a8..e3754d741e016 100644
--- a/src/ring_theory/trace.lean
+++ b/src/ring_theory/trace.lean
@@ -5,7 +5,7 @@ Authors: Anne Baanen
 -/
 
 import linear_algebra.bilinear_form
-import linear_algebra.charpoly.coeff
+import linear_algebra.matrix.charpoly.coeff
 import linear_algebra.determinant
 import linear_algebra.vandermonde
 import linear_algebra.trace