chore(field_theory|ring_theory|linear_algebra): rename minimal_polyno…

…mial to minpoly (#5771)

This PR renames:

* `minimal_polynomial` -> `minpoly`
* a similar substitution throughout the library for all names containing the substring `minimal_polynomial`
* `fixed_points.minpoly.minimal_polynomial` -> `fixed_points.minpoly_eq_minpoly`

This PR moves a file:

  src/field_theory/minimal_polynomial.lean -> src/field_theory/minpoly.lean





Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

docs/overview.yaml

@@ -153,7 +153,7 @@ Linear algebra:
     determinant: 'matrix.det'
     invertibility: 'matrix.nonsing_inv'
   Endomorphism polynomials:
-    minimal polynomial: 'minimal_polynomial'
+    minimal polynomial: 'minpoly'
     characteristic polynomial: 'char_poly'
     Cayley-Hamilton theorem: 'aeval_self_char_poly'
   Structure theory of endomorphisms:

docs/undergrad.yaml

@@ -52,7 +52,7 @@ Linear algebra:
     row-reduced matrices: ''
   Endomorphism polynomials:
     annihilating polynomials: ''
-    minimal polynomial: 'minimal_polynomial'
+    minimal polynomial: 'minpoly'
     characteristic polynomial: 'char_poly'
     Cayley-Hamilton theorem: 'aeval_self_char_poly'
   Structure theory of endomorphisms:

scripts/style-exceptions.txt

@@ -731,9 +731,6 @@ src/field_theory/fixed.lean : line 27 : ERR_LIN : Line has more than 100 charact
 src/field_theory/fixed.lean : line 77 : ERR_LIN : Line has more than 100 characters
 src/field_theory/intermediate_field.lean : line 150 : ERR_LIN : Line has more than 100 characters
 src/field_theory/intermediate_field.lean : line 155 : ERR_LIN : Line has more than 100 characters
-src/field_theory/minimal_polynomial.lean : line 102 : ERR_LIN : Line has more than 100 characters
-src/field_theory/minimal_polynomial.lean : line 250 : ERR_LIN : Line has more than 100 characters
-src/field_theory/minimal_polynomial.lean : line 319 : ERR_LIN : Line has more than 100 characters
 src/field_theory/mv_polynomial.lean : line 14 : ERR_MOD : Module docstring missing, or too late
 src/field_theory/primitive_element.lean : line 29 : ERR_LIN : Line has more than 100 characters
 src/field_theory/splitting_field.lean : line 16 : ERR_MOD : Module docstring missing, or too late

src/field_theory/adjoin.lean

@@ -300,8 +300,8 @@ begin
   by_cases x = 0,
   { rw [h, inv_zero], exact subalgebra.zero_mem (algebra.adjoin F {α}) },
 
-  let ϕ := alg_equiv.adjoin_singleton_equiv_adjoin_root_minimal_polynomial F α hα,
-  haveI := minimal_polynomial.irreducible hα,
+  let ϕ := alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly F α hα,
+  haveI := minpoly.irreducible hα,
   suffices : ϕ ⟨x, hx⟩ * (ϕ ⟨x, hx⟩)⁻¹ = 1,
   { convert subtype.mem (ϕ.symm (ϕ ⟨x, hx⟩)⁻¹),
     refine (eq_inv_of_mul_right_eq_one _).symm,
@@ -409,69 +409,69 @@ section adjoin_integral_element
 variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] {α : E}
 variables {K : Type*} [field K] [algebra F K]
 
-lemma aeval_gen_minimal_polynomial (h : is_integral F α) :
-  aeval (adjoin_simple.gen F α) (minimal_polynomial h) = 0 :=
+lemma aeval_gen_minpoly (h : is_integral F α) :
+  aeval (adjoin_simple.gen F α) (minpoly h) = 0 :=
 begin
   ext,
-  convert minimal_polynomial.aeval h,
+  convert minpoly.aeval h,
   conv in (aeval α) { rw [← adjoin_simple.algebra_map_gen F α] },
   exact is_scalar_tower.algebra_map_aeval F F⟮α⟯ E _ _
 end
 
 /-- algebra isomorphism between `adjoin_root` and `F⟮α⟯` -/
 noncomputable def adjoin_root_equiv_adjoin (h : is_integral F α) :
-  adjoin_root (minimal_polynomial h) ≃ₐ[F] F⟮α⟯ :=
+  adjoin_root (minpoly h) ≃ₐ[F] F⟮α⟯ :=
 alg_equiv.of_bijective (alg_hom.mk (adjoin_root.lift (algebra_map F F⟮α⟯)
-  (adjoin_simple.gen F α) (aeval_gen_minimal_polynomial F h)) (ring_hom.map_one _)
+  (adjoin_simple.gen F α) (aeval_gen_minpoly F h)) (ring_hom.map_one _)
   (λ x y, ring_hom.map_mul _ x y) (ring_hom.map_zero _) (λ x y, ring_hom.map_add _ x y)
   (by { exact λ _, adjoin_root.lift_of })) (begin
-    set f := adjoin_root.lift _ _ (aeval_gen_minimal_polynomial F h),
-    haveI := minimal_polynomial.irreducible h,
+    set f := adjoin_root.lift _ _ (aeval_gen_minpoly F h),
+    haveI := minpoly.irreducible h,
     split,
     { exact ring_hom.injective f },
     { suffices : F⟮α⟯.to_subfield ≤ ring_hom.field_range ((F⟮α⟯.to_subfield.subtype).comp f),
       { exact λ x, Exists.cases_on (this (subtype.mem x)) (λ y hy, ⟨y, subtype.ext hy.2⟩) },
       exact subfield.closure_le.mpr (set.union_subset (λ x hx, Exists.cases_on hx (λ y hy, ⟨y,
         ⟨subfield.mem_top y, by { rw [ring_hom.comp_apply, adjoin_root.lift_of], exact hy }⟩⟩))
-        (set.singleton_subset_iff.mpr ⟨adjoin_root.root (minimal_polynomial h),
-        ⟨subfield.mem_top (adjoin_root.root (minimal_polynomial h)),
+        (set.singleton_subset_iff.mpr ⟨adjoin_root.root (minpoly h),
+        ⟨subfield.mem_top (adjoin_root.root (minpoly h)),
         by { rw [ring_hom.comp_apply, adjoin_root.lift_root], refl }⟩⟩)) } end)
 
 lemma adjoin_root_equiv_adjoin_apply_root (h : is_integral F α) :
-  adjoin_root_equiv_adjoin F h (adjoin_root.root (minimal_polynomial h)) =
+  adjoin_root_equiv_adjoin F h (adjoin_root.root (minpoly h)) =
     adjoin_simple.gen F α :=
 begin
   refine adjoin_root.lift_root,
-  { exact minimal_polynomial h },
-  { exact aeval_gen_minimal_polynomial F h }
+  { exact minpoly h },
+  { exact aeval_gen_minpoly F h }
 end
 
 /-- Algebra homomorphism `F⟮α⟯ →ₐ[F] K` are in bijection with the set of roots
-of `minimal_polynomial α` in `K`. -/
+of `minpoly α` in `K`. -/
 noncomputable def alg_hom_adjoin_integral_equiv (h : is_integral F α) :
-  (F⟮α⟯ →ₐ[F] K) ≃ {x // x ∈ ((minimal_polynomial h).map (algebra_map F K)).roots} :=
+  (F⟮α⟯ →ₐ[F] K) ≃ {x // x ∈ ((minpoly h).map (algebra_map F K)).roots} :=
 let ϕ := adjoin_root_equiv_adjoin F h,
-  swap1 : (F⟮α⟯ →ₐ[F] K) ≃ (adjoin_root (minimal_polynomial h) →ₐ[F] K) :=
+  swap1 : (F⟮α⟯ →ₐ[F] K) ≃ (adjoin_root (minpoly h) →ₐ[F] K) :=
   { to_fun := λ f, f.comp ϕ.to_alg_hom,
     inv_fun := λ f, f.comp ϕ.symm.to_alg_hom,
     left_inv := λ _, by { ext, simp only [alg_equiv.coe_alg_hom,
       alg_equiv.to_alg_hom_eq_coe, alg_hom.comp_apply, alg_equiv.apply_symm_apply]},
     right_inv := λ _, by { ext, simp only [alg_equiv.symm_apply_apply,
       alg_equiv.coe_alg_hom, alg_equiv.to_alg_hom_eq_coe, alg_hom.comp_apply] } },
-  swap2 := adjoin_root.equiv F K (minimal_polynomial h) (minimal_polynomial.ne_zero h) in
+  swap2 := adjoin_root.equiv F K (minpoly h) (minpoly.ne_zero h) in
 swap1.trans swap2
 
 /-- Fintype of algebra homomorphism `F⟮α⟯ →ₐ[F] K` -/
 noncomputable def fintype_of_alg_hom_adjoin_integral (h : is_integral F α) :
   fintype (F⟮α⟯ →ₐ[F] K) :=
 fintype.of_equiv _ (alg_hom_adjoin_integral_equiv F h).symm
 
-lemma card_alg_hom_adjoin_integral (h : is_integral F α) (h_sep : (minimal_polynomial h).separable)
-  (h_splits : (minimal_polynomial h).splits (algebra_map F K)) :
+lemma card_alg_hom_adjoin_integral (h : is_integral F α) (h_sep : (minpoly h).separable)
+  (h_splits : (minpoly h).splits (algebra_map F K)) :
   @fintype.card (F⟮α⟯ →ₐ[F] K) (fintype_of_alg_hom_adjoin_integral F h) =
-    (minimal_polynomial h).nat_degree :=
+    (minpoly h).nat_degree :=
 begin
-  let s := ((minimal_polynomial h).map (algebra_map F K)).roots.to_finset,
+  let s := ((minpoly h).map (algebra_map F K)).roots.to_finset,
   have H := λ x, multiset.mem_to_finset,
   rw [fintype.card_congr (alg_hom_adjoin_integral_equiv F h), fintype.card_of_subtype s H,
       nat_degree_eq_card_roots h_splits, multiset.to_finset_card_of_nodup],
@@ -539,7 +539,7 @@ section alg_hom_mk_adjoin_splits
 variables {F E K : Type*} [field F] [field E] [field K] [algebra F E] [algebra F K] {S : finset E}
 
 lemma alg_hom_mk_adjoin_splits
-  (hK : ∀ x ∈ S, ∃ H : is_integral F (x : E), (minimal_polynomial H).splits (algebra_map F K)) :
+  (hK : ∀ x ∈ S, ∃ H : is_integral F (x : E), (minpoly H).splits (algebra_map F K)) :
   nonempty ((adjoin F (S : set E)) →ₐ[F] K) :=
 begin
   let P : intermediate_field F E → Prop := λ L, nonempty (L →ₐ[F] K),
@@ -550,22 +550,22 @@ begin
     cases hK x hx with H hH,
     have H' : is_integral L x := is_integral_of_is_scalar_tower x H,
     letI : algebra L K := f.to_ring_hom.to_algebra,
-    have key : (minimal_polynomial H').splits (algebra_map L K),
-    { refine splits_of_splits_of_dvd _ (map_ne_zero (minimal_polynomial.ne_zero H)) _
-        (minimal_polynomial.dvd_map_of_is_scalar_tower L H),
+    have key : (minpoly H').splits (algebra_map L K),
+    { refine splits_of_splits_of_dvd _ (map_ne_zero (minpoly.ne_zero H)) _
+        (minpoly.dvd_map_of_is_scalar_tower L H),
       rwa [splits_map_iff, ←is_scalar_tower.algebra_map_eq F L K] },
     apply nonempty.intro,
     apply alg_hom_equiv_sigma.inv_fun,
     use f,
     apply (alg_hom_adjoin_integral_equiv L H').inv_fun,
-    use root_of_splits (algebra_map L K) key (ne_of_gt (minimal_polynomial.degree_pos H')),
-    simp_rw [mem_roots (map_ne_zero (minimal_polynomial.ne_zero H')), is_root, ←eval₂_eq_eval_map],
-    exact map_root_of_splits (algebra_map L K) key (ne_of_gt (minimal_polynomial.degree_pos H')),
+    use root_of_splits (algebra_map L K) key (ne_of_gt (minpoly.degree_pos H')),
+    simp_rw [mem_roots (map_ne_zero (minpoly.ne_zero H')), is_root, ←eval₂_eq_eval_map],
+    exact map_root_of_splits (algebra_map L K) key (ne_of_gt (minpoly.degree_pos H')),
     exact is_scalar_tower.of_algebra_map_eq (λ x, rfl) },
 end
 
 lemma alg_hom_mk_adjoin_splits' (hS : adjoin F (S : set E) = ⊤)
-  (hK : ∀ x ∈ S, ∃ H : is_integral F (x : E), (minimal_polynomial H).splits (algebra_map F K)) :
+  (hK : ∀ x ∈ S, ∃ H : is_integral F (x : E), (minpoly H).splits (algebra_map F K)) :
   nonempty (E →ₐ[F] K) :=
 begin
   cases alg_hom_mk_adjoin_splits hK with ϕ,

src/field_theory/algebraic_closure.lean

@@ -71,14 +71,14 @@ lemma algebra_map_surjective_of_is_integral {k K : Type*} [field k] [domain K]
   [hk : is_alg_closed k] [algebra k K] (hf : algebra.is_integral k K) :
   function.surjective (algebra_map k K) :=
 begin
-  refine λ x, ⟨-((minimal_polynomial (hf x)).coeff 0), _⟩,
-  have hq : (minimal_polynomial (hf x)).leading_coeff = 1 := minimal_polynomial.monic (hf x),
-  have h : (minimal_polynomial (hf x)).degree = 1 := degree_eq_one_of_irreducible k
-    (minimal_polynomial.ne_zero (hf x)) (minimal_polynomial.irreducible (hf x)),
-  have : (aeval x (minimal_polynomial (hf x))) = 0 := minimal_polynomial.aeval (hf x),
+  refine λ x, ⟨-((minpoly (hf x)).coeff 0), _⟩,
+  have hq : (minpoly (hf x)).leading_coeff = 1 := minpoly.monic (hf x),
+  have h : (minpoly (hf x)).degree = 1 := degree_eq_one_of_irreducible k
+    (minpoly.ne_zero (hf x)) (minpoly.irreducible (hf x)),
+  have : (aeval x (minpoly (hf x))) = 0 := minpoly.aeval (hf x),
   rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul,
     aeval_add, aeval_X, aeval_C, add_eq_zero_iff_eq_neg] at this,
-  exact (ring_hom.map_neg (algebra_map k K) ((minimal_polynomial (hf x)).coeff 0)).symm ▸ this.symm,
+  exact (ring_hom.map_neg (algebra_map k K) ((minpoly (hf x)).coeff 0)).symm ▸ this.symm,
 end
 
 lemma algebra_map_surjective_of_is_algebraic {k K : Type*} [field k] [domain K]

src/field_theory/fixed.lean

@@ -176,20 +176,20 @@ end minpoly
 theorem is_integral : is_integral (fixed_points G F) x :=
 ⟨minpoly G F x, minpoly.monic G F x, minpoly.eval₂ G F x⟩
 
-theorem minpoly.minimal_polynomial :
-  minpoly G F x = minimal_polynomial (is_integral G F x) :=
-minimal_polynomial.unique' _ (minpoly.irreducible G F x)
+theorem minpoly_eq_minpoly :
+  minpoly G F x = _root_.minpoly (is_integral G F x) :=
+minpoly.unique' _ (minpoly.irreducible G F x)
   (minpoly.eval₂ G F x) (minpoly.monic G F x)
 
 instance normal : normal (fixed_points G F) F :=
 λ x, ⟨is_integral G F x, (polynomial.splits_id_iff_splits _).1 $
-by { rw [← minpoly.minimal_polynomial, minpoly,
+by { rw [← minpoly_eq_minpoly, minpoly,
     coe_algebra_map, polynomial.map_to_subring, prod_X_sub_smul],
   exact polynomial.splits_prod _ (λ _ _, polynomial.splits_X_sub_C _) }⟩
 
 instance separable : is_separable (fixed_points G F) F :=
 λ x, ⟨is_integral G F x,
-by { rw [← minpoly.minimal_polynomial,
+by { rw [← minpoly_eq_minpoly,
         ← polynomial.separable_map (is_subring.subtype (fixed_points G F)),
         minpoly, polynomial.map_to_subring],
   exact polynomial.separable_prod_X_sub_C_iff.2 (injective_of_quotient_stabilizer G x) }⟩

src/field_theory/galois.lean

@@ -62,11 +62,11 @@ lemma integral (h : is_galois F E) (x : E) : is_integral F x :=
 Exists.cases_on (h.1 x) (λ H _, H)
 
 lemma separable (h : is_galois F E) (x : E) :
-  (minimal_polynomial (integral h x)).separable :=
+  (minpoly (integral h x)).separable :=
 Exists.cases_on (h.1 x) (λ _ H, H)
 
 lemma normal (h : is_galois F E) (x : E) :
-  (minimal_polynomial (integral h x)).splits (algebra_map F E) :=
+  (minpoly (integral h x)).splits (algebra_map F E) :=
 Exists.cases_on (h.2 x) (λ _ H, H)
 
 variables (F) (E)
@@ -77,8 +77,8 @@ instance of_fixed_field (G : Type*) [group G] [fintype G] [mul_semiring_action G
 
 lemma intermediate_field.adjoin_simple.card_aut_eq_findim
   [finite_dimensional F E] {α : E} (hα : is_integral F α)
-  (h_sep : (minimal_polynomial hα).separable)
-  (h_splits : (minimal_polynomial hα).splits (algebra_map F F⟮α⟯)) :
+  (h_sep : (minpoly hα).separable)
+  (h_splits : (minpoly hα).splits (algebra_map F F⟮α⟯)) :
   fintype.card (F⟮α⟯ ≃ₐ[F] F⟮α⟯) = findim F F⟮α⟯ :=
 begin
   letI : fintype (F⟮α⟯ →ₐ[F] F⟮α⟯) := intermediate_field.fintype_of_alg_hom_adjoin_integral F hα,
@@ -100,9 +100,9 @@ begin
     map_add' := λ _ _, rfl,
     commutes' := λ _, rfl },
   have H : is_integral F α := h.integral α,
-  have h_sep : (minimal_polynomial H).separable := h.separable α,
-  have h_splits : (minimal_polynomial H).splits (algebra_map F E) := h.normal α,
-  replace h_splits : polynomial.splits (algebra_map F F⟮α⟯) (minimal_polynomial H),
+  have h_sep : (minpoly H).separable := h.separable α,
+  have h_splits : (minpoly H).splits (algebra_map F E) := h.normal α,
+  replace h_splits : polynomial.splits (algebra_map F F⟮α⟯) (minpoly H),
   { convert polynomial.splits_comp_of_splits
     (algebra_map F E) iso.symm.to_alg_hom.to_ring_hom h_splits },
   rw ← linear_equiv.findim_eq iso.to_linear_equiv,
@@ -301,17 +301,17 @@ lemma is_separable_splitting_field [finite_dimensional F E] [h : is_galois F E]
 begin
   cases field.exists_primitive_element h.1 with α h1,
   have h2 : is_integral F α := h.integral α,
-  have h3 : (minimal_polynomial h2).separable := h.separable α,
-  have h4 : (minimal_polynomial h2).splits (algebra_map F E) := h.normal α,
-  use [minimal_polynomial h2, h3, h4],
+  have h3 : (minpoly h2).separable := h.separable α,
+  have h4 : (minpoly h2).splits (algebra_map F E) := h.normal α,
+  use [minpoly h2, h3, h4],
   rw [eq_top_iff, ←intermediate_field.top_to_subalgebra, ←h1],
   rw intermediate_field.adjoin_simple_to_subalgebra_of_integral F α h2,
   apply algebra.adjoin_mono,
   rw [set.singleton_subset_iff, finset.mem_coe, multiset.mem_to_finset, polynomial.mem_roots],
   { dsimp only [polynomial.is_root],
     rw [polynomial.eval_map, ←polynomial.aeval_def],
-    exact minimal_polynomial.aeval h2 },
-  { exact polynomial.map_ne_zero (minimal_polynomial.ne_zero h2) }
+    exact minpoly.aeval h2 },
+  { exact polynomial.map_ne_zero (minpoly.ne_zero h2) }
 end
 
 lemma of_fixed_field_eq_bot [finite_dimensional F E]
@@ -342,8 +342,8 @@ lemma of_separable_splitting_field_aux [hFE : finite_dimensional F E]
 begin
   have h : is_integral K x := is_integral_of_is_scalar_tower x (is_integral_of_noetherian hFE x),
   have h1 : p ≠ 0 := λ hp, by rwa [hp, polynomial.map_zero, polynomial.roots_zero] at hx,
-  have h2 : (minimal_polynomial h) ∣ p.map (algebra_map F K),
-  { apply minimal_polynomial.dvd,
+  have h2 : (minpoly h) ∣ p.map (algebra_map F K),
+  { apply minpoly.dvd,
     rw [polynomial.aeval_def, polynomial.eval₂_map, ←polynomial.eval_map],
     exact (polynomial.mem_roots (polynomial.map_ne_zero h1)).mp hx },
   let key_equiv : ((↑K⟮x⟯ : intermediate_field F E) →ₐ[F] E) ≃ Σ (f : K →ₐ[F] E),
@@ -382,7 +382,7 @@ begin
   apply intermediate_field.induction_on_adjoin_finset s P,
   { have key := intermediate_field.card_alg_hom_adjoin_integral F
       (show is_integral F (0 : E), by exact is_integral_zero),
-    rw [minimal_polynomial.zero, polynomial.nat_degree_X] at key,
+    rw [minpoly.zero, polynomial.nat_degree_X] at key,
     specialize key polynomial.separable_X (polynomial.splits_X (algebra_map F E)),
     rw [←@subalgebra.findim_bot F E _ _ _, ←intermediate_field.bot_to_subalgebra] at key,
     refine eq.trans _ key,