feat(ring_theory/power_basis): matrix of multiplication by generator (#…

…18177)

+ `power_basis.left_mul_matrix` computes the matrix of left multiplication by the generator with respect to the power basis: the last column is the negation of the coefficients of the minimal polynomial, while in other columns there are 1's below the diagonal and 0 elsewhere.

+ Also generalizes `comm_ring` or `field` in other files to `ring` where possible.

src/algebraic_topology/dold_kan/normalized.lean

@@ -120,11 +120,18 @@ def N₁_iso_normalized_Moore_complex_comp_to_karoubi :
 { hom :=
   { app := λ X,
     { f := P_infty_to_normalized_Moore_complex X,
-      comm := by tidy, }, },
+      comm := by erw [comp_id, P_infty_comp_P_infty_to_normalized_Moore_complex] },
+    naturality' := λ X Y f, by simp only [functor.comp_map, normalized_Moore_complex_map,
+      P_infty_to_normalized_Moore_complex_naturality, karoubi.hom_ext, karoubi.comp_f, N₁_map_f,
+      P_infty_comp_P_infty_to_normalized_Moore_complex_assoc, to_karoubi_map_f, assoc] },
   inv :=
   { app := λ X,
     { f := inclusion_of_Moore_complex_map X,
-      comm := by tidy, }, },
+      comm := by erw [inclusion_of_Moore_complex_map_comp_P_infty, id_comp] },
+    naturality' := λ X Y f, by { ext, simp only [functor.comp_map, normalized_Moore_complex_map,
+      karoubi.comp_f, to_karoubi_map_f, homological_complex.comp_f, normalized_Moore_complex.map_f,
+      inclusion_of_Moore_complex_map_f, factor_thru_arrow, N₁_map_f,
+      inclusion_of_Moore_complex_map_comp_P_infty_assoc, alternating_face_map_complex.map_f] } },
   hom_inv_id' := begin
     ext X : 3,
     simp only [P_infty_to_normalized_Moore_complex_comp_inclusion_of_Moore_complex_map,

src/linear_algebra/matrix/charpoly/minpoly.lean

@@ -45,18 +45,16 @@ In combination with `det_eq_sign_charpoly_coeff` or `trace_eq_neg_charpoly_coeff
 and a bit of rewriting, this will allow us to conclude the
 field norm resp. trace of `x` is the product resp. sum of `x`'s conjugates.
 -/
-lemma charpoly_left_mul_matrix {K S : Type*} [field K] [comm_ring S] [algebra K S]
-  (h : power_basis K S) :
-  (left_mul_matrix h.basis h.gen).charpoly = minpoly K h.gen :=
+lemma charpoly_left_mul_matrix {S : Type*} [ring S] [algebra R S] (h : power_basis R S) :
+  (left_mul_matrix h.basis h.gen).charpoly = minpoly R h.gen :=
 begin
-  apply minpoly.unique,
-  { apply matrix.charpoly_monic },
+  casesI subsingleton_or_nontrivial R, { apply subsingleton.elim },
+  apply minpoly.unique' R h.gen (charpoly_monic _),
   { apply (injective_iff_map_eq_zero (left_mul_matrix _)).mp (left_mul_matrix_injective h.basis),
     rw [← polynomial.aeval_alg_hom_apply, aeval_self_charpoly] },
-  { intros q q_monic root_q,
-    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 }
+  refine λ q hq, or_iff_not_imp_left.2 (λ h0, _),
+  rw [matrix.charpoly_degree_eq_dim, fintype.card_fin] at hq,
+  contrapose! hq, exact h.dim_le_degree_of_root h0 hq,
 end
 
 end power_basis

src/linear_algebra/matrix/to_lin.lean

@@ -637,12 +637,8 @@ namespace algebra
 
 section lmul
 
-variables {R S T : Type*} [comm_ring R] [comm_ring S] [comm_ring T]
-variables [algebra R S] [algebra S T] [algebra R T] [is_scalar_tower R S T]
-variables {m n : Type*} [fintype m] [decidable_eq m] [decidable_eq n]
-variables (b : basis m R S) (c : basis n S T)
-
-open algebra
+variables {R S : Type*} [comm_ring R] [ring S] [algebra R S]
+variables {m : Type*} [fintype m] [decidable_eq m] (b : basis m R S)
 
 lemma to_matrix_lmul' (x : S) (i j) :
   linear_map.to_matrix b b (lmul R S x) i j = b.repr (x * b j) i :=
@@ -690,7 +686,14 @@ lemma left_mul_matrix_injective : function.injective (left_mul_matrix b) :=
              ... = algebra.lmul R S x' 1 : by rw (linear_map.to_matrix b b).injective h
              ... = x' : mul_one x'
 
-variable [fintype n]
+end lmul
+
+section lmul_tower
+
+variables {R S T : Type*} [comm_ring R] [comm_ring S] [ring T]
+variables [algebra R S] [algebra S T] [algebra R T] [is_scalar_tower R S T]
+variables {m n : Type*} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n]
+variables (b : basis m R S) (c : basis n S T)
 
 lemma smul_left_mul_matrix (x) (ik jk) :
   left_mul_matrix (b.smul c) x ik jk =
@@ -715,7 +718,7 @@ lemma smul_left_mul_matrix_algebra_map_ne (x : S) (i j) {k k'}
   (h : k ≠ k') : left_mul_matrix (b.smul c) (algebra_map _ _ x) (i, k) (j, k') = 0 :=
 by rw [smul_left_mul_matrix_algebra_map, block_diagonal_apply_ne _ _ _ h]
 
-end lmul
+end lmul_tower
 
 end algebra
 

src/ring_theory/adjoin_root.lean

@@ -455,7 +455,7 @@ end
 
 end minpoly
 
-section is_domain
+section equiv'
 
 variables [comm_ring R] [comm_ring S] [algebra R S]
 variables (g : R[X]) (pb : _root_.power_basis R S)
@@ -489,7 +489,7 @@ rfl
   (equiv' g pb h₁ h₂).symm.to_alg_hom = pb.lift (root g) h₁ :=
 rfl
 
-end is_domain
+end equiv'
 
 section field
 

src/ring_theory/norm.lean

@@ -41,7 +41,7 @@ See also `algebra.trace`, which is defined similarly as the trace of
 
 universes u v w
 
-variables {R S T : Type*} [comm_ring R] [comm_ring S]
+variables {R S T : Type*} [comm_ring R] [ring S]
 variables [algebra R S]
 variables {K L F : Type*} [field K] [field L] [field F]
 variables [algebra K L] [algebra K F]
@@ -75,7 +75,7 @@ lemma norm_eq_matrix_det [fintype ι] [decidable_eq ι] (b : basis ι R S) (s :
   norm R s = matrix.det (algebra.left_mul_matrix b s) :=
 by { rwa [norm_apply, ← linear_map.det_to_matrix b, ← to_matrix_lmul_eq], refl }
 
-/-- If `x` is in the base field `K`, then the norm is `x ^ [L : K]`. -/
+/-- If `x` is in the base ring `K`, then the norm is `x ^ [L : K]`. -/
 lemma norm_algebra_map_of_basis [fintype ι] (b : basis ι R S) (x : R) :
   norm R (algebra_map R S x) = x ^ fintype.card ι :=
 begin
@@ -91,7 +91,7 @@ end
 (If `L` is not finite-dimensional over `K`, then `norm = 1 = x ^ 0 = x ^ (finrank L K)`.)
 -/
 @[simp]
-protected lemma norm_algebra_map {K L : Type*} [field K] [comm_ring L] [algebra K L] (x : K) :
+protected lemma norm_algebra_map {L : Type*} [ring L] [algebra K L] (x : K) :
   norm K (algebra_map K L x) = x ^ finrank K L :=
 begin
   by_cases H : ∃ (s : finset L), nonempty (basis s K L),
@@ -105,25 +105,24 @@ section eq_prod_roots
 
 /-- Given `pb : power_basis K S`, then the norm of `pb.gen` is
 `(-1) ^ pb.dim * coeff (minpoly K pb.gen) 0`. -/
-lemma power_basis.norm_gen_eq_coeff_zero_minpoly [algebra K S] (pb : power_basis K S) :
-  norm K pb.gen = (-1) ^ pb.dim * coeff (minpoly K pb.gen) 0 :=
-begin
-  rw [norm_eq_matrix_det pb.basis, det_eq_sign_charpoly_coeff, charpoly_left_mul_matrix,
-    fintype.card_fin]
-end
-
-/-- Given `pb : power_basis K S`, then the norm of `pb.gen` is
-`((minpoly K pb.gen).map (algebra_map K F)).roots.prod`. -/
-lemma power_basis.norm_gen_eq_prod_roots [algebra K S] (pb : power_basis K S)
-  (hf : (minpoly K pb.gen).splits (algebra_map K F)) :
-  algebra_map K F (norm K pb.gen) =
-    ((minpoly K pb.gen).map (algebra_map K F)).roots.prod :=
+lemma power_basis.norm_gen_eq_coeff_zero_minpoly (pb : power_basis R S) :
+  norm R pb.gen = (-1) ^ pb.dim * coeff (minpoly R pb.gen) 0 :=
+by rw [norm_eq_matrix_det pb.basis, det_eq_sign_charpoly_coeff,
+       charpoly_left_mul_matrix, fintype.card_fin]
+
+/-- Given `pb : power_basis R S`, then the norm of `pb.gen` is
+`((minpoly R pb.gen).map (algebra_map R F)).roots.prod`. -/
+lemma power_basis.norm_gen_eq_prod_roots [algebra R F] (pb : power_basis R S)
+  (hf : (minpoly R pb.gen).splits (algebra_map R F)) :
+  algebra_map R F (norm R pb.gen) =
+    ((minpoly R pb.gen).map (algebra_map R F)).roots.prod :=
 begin
+  haveI := module.nontrivial R F,
+  have := minpoly.monic pb.is_integral_gen,
   rw [power_basis.norm_gen_eq_coeff_zero_minpoly, ← pb.nat_degree_minpoly, ring_hom.map_mul,
-    ← coeff_map, prod_roots_eq_coeff_zero_of_monic_of_split
-      ((minpoly.monic (power_basis.is_integral_gen _)).map _)
-      ((splits_id_iff_splits _).2 hf), nat_degree_map, map_pow, ← mul_assoc, ← mul_pow],
-  simp
+    ← coeff_map, prod_roots_eq_coeff_zero_of_monic_of_split (this.map _)
+      ((splits_id_iff_splits _).2 hf), this.nat_degree_map, map_pow, ← mul_assoc, ← mul_pow],
+  { simp only [map_neg, _root_.map_one, neg_mul, neg_neg, one_pow, one_mul] }, apply_instance,
 end
 
 end eq_prod_roots
@@ -225,20 +224,19 @@ section eq_prod_embeddings
 
 open intermediate_field intermediate_field.adjoin_simple polynomial
 
-lemma norm_eq_prod_embeddings_gen {K L : Type*} [field K] [comm_ring L] [algebra K L]
-  (E : Type*) [field E] [algebra K E]
-  (pb : power_basis K L)
-  (hE : (minpoly K pb.gen).splits (algebra_map K E)) (hfx : (minpoly K pb.gen).separable) :
-  algebra_map K E (norm K pb.gen) =
-    (@@finset.univ (power_basis.alg_hom.fintype pb)).prod (λ σ, σ pb.gen) :=
+variables (F) (E : Type*) [field E] [algebra K E]
+
+lemma norm_eq_prod_embeddings_gen [algebra R F] (pb : power_basis R S)
+  (hE : (minpoly R pb.gen).splits (algebra_map R F)) (hfx : (minpoly R pb.gen).separable) :
+  algebra_map R F (norm R pb.gen) = (@@finset.univ pb^.alg_hom.fintype).prod (λ σ, σ pb.gen) :=
 begin
-  letI := classical.dec_eq E,
-  rw [power_basis.norm_gen_eq_prod_roots pb hE, fintype.prod_equiv pb.lift_equiv',
+  letI := classical.dec_eq F,
+  rw [pb.norm_gen_eq_prod_roots hE, fintype.prod_equiv pb.lift_equiv',
     finset.prod_mem_multiset, finset.prod_eq_multiset_prod, multiset.to_finset_val,
     multiset.dedup_eq_self.mpr, multiset.map_id],
-  { exact nodup_roots ((separable_map _).mpr hfx) },
+  { exact nodup_roots hfx.map },
   { intro x, refl },
-  { intro σ, rw [power_basis.lift_equiv'_apply_coe, id.def] }
+  { intro σ, rw [pb.lift_equiv'_apply_coe, id.def] }
 end
 
 lemma norm_eq_prod_roots [is_separable K L] [finite_dimensional K L]
@@ -247,13 +245,10 @@ lemma norm_eq_prod_roots [is_separable K L] [finite_dimensional K L]
 by rw [norm_eq_norm_adjoin K x, map_pow,
   intermediate_field.adjoin_simple.norm_gen_eq_prod_roots _ hF]
 
-variables (F) (E : Type*) [field E] [algebra K E]
-
 lemma prod_embeddings_eq_finrank_pow [algebra L F] [is_scalar_tower K L F] [is_alg_closed E]
   [is_separable K F] [finite_dimensional K F] (pb : power_basis K L) :
   ∏ σ : F →ₐ[K] E, σ (algebra_map L F pb.gen) =
-  ((@@finset.univ (power_basis.alg_hom.fintype pb)).prod
-    (λ σ : L →ₐ[K] E, σ pb.gen)) ^ finrank L F :=
+  ((@@finset.univ pb^.alg_hom.fintype).prod (λ σ : L →ₐ[K] E, σ pb.gen)) ^ finrank L F :=
 begin
   haveI : finite_dimensional L F := finite_dimensional.right K L F,
   haveI : is_separable L F := is_separable_tower_top_of_is_separable K L F,
@@ -301,18 +296,18 @@ begin
                ring_hom.id_apply] },
 end
 
-lemma is_integral_norm [algebra S L] [algebra S K] [is_scalar_tower S K L]
-  [is_separable K L] [finite_dimensional K L] {x : L} (hx : _root_.is_integral S x) :
-  _root_.is_integral S (norm K x) :=
+lemma is_integral_norm [algebra R L] [algebra R K] [is_scalar_tower R K L]
+  [is_separable K L] [finite_dimensional K L] {x : L} (hx : _root_.is_integral R x) :
+  _root_.is_integral R (norm K x) :=
 begin
   have hx' : _root_.is_integral K x := is_integral_of_is_scalar_tower hx,
   rw [← is_integral_algebra_map_iff (algebra_map K (algebraic_closure L)).injective,
       norm_eq_prod_roots],
   { refine (is_integral.multiset_prod (λ y hy, _)).pow _,
     rw mem_roots_map (minpoly.ne_zero hx') at hy,
-    use [minpoly S x, minpoly.monic hx],
+    use [minpoly R x, minpoly.monic hx],
     rw ← aeval_def at ⊢ hy,
-    exact minpoly.aeval_of_is_scalar_tower S x y hy },
+    exact minpoly.aeval_of_is_scalar_tower R x y hy },
   { apply is_alg_closed.splits_codomain },
   { apply_instance }
 end

src/ring_theory/power_basis.lean

@@ -214,6 +214,24 @@ lemma nat_degree_minpoly [nontrivial A] (pb : power_basis A S) :
   (minpoly A pb.gen).nat_degree = pb.dim :=
 by rw [← minpoly_gen_eq, nat_degree_minpoly_gen]
 
+protected lemma left_mul_matrix (pb : power_basis A S) :
+  algebra.left_mul_matrix pb.basis pb.gen = matrix.of
+    (λ i j, if ↑j + 1 = pb.dim then -pb.minpoly_gen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0) :=
+begin
+  casesI subsingleton_or_nontrivial A, { apply subsingleton.elim },
+  rw [algebra.left_mul_matrix_apply, ← linear_equiv.eq_symm_apply, linear_map.to_matrix_symm],
+  refine pb.basis.ext (λ k, _),
+  simp_rw [matrix.to_lin_self, matrix.of_apply, pb.basis_eq_pow],
+  apply (pow_succ _ _).symm.trans,
+  split_ifs with h h,
+  { simp_rw [h, neg_smul, finset.sum_neg_distrib, eq_neg_iff_add_eq_zero],
+    convert pb.aeval_minpoly_gen,
+    rw [add_comm, aeval_eq_sum_range, finset.sum_range_succ, ← leading_coeff,
+        pb.minpoly_gen_monic.leading_coeff, one_smul, nat_degree_minpoly_gen, finset.sum_range] },
+  { rw [fintype.sum_eq_single (⟨↑k + 1, lt_of_le_of_ne k.2 h⟩ : fin pb.dim), if_pos, one_smul],
+    { refl }, { refl }, intros x hx, rw [if_neg, zero_smul], apply mt fin.ext hx },
+end
+
 end minpoly
 
 section equiv