chore(field_theory/minpoly): meaningful variable names (#5773)

src/field_theory/minpoly.lean

@@ -10,41 +10,39 @@ import ring_theory.polynomial.gauss_lemma
 /-!
 # Minimal polynomials
 
-This file defines the minimal polynomial of an element x of an A-algebra B,
-under the assumption that x is integral over A.
+This file defines the minimal polynomial of an element `x` of an `A`-algebra `B`,
+under the assumption that x is integral over `A`.
 
 After stating the defining property we specialize to the setting of field extensions
 and derive some well-known properties, amongst which the fact that minimal polynomials
 are irreducible, and uniquely determined by their defining property.
 
 -/
 
-universes u v w
-
 open_locale classical
 open polynomial set function
 
-variables {α : Type u} {β : Type v}
+variables {A B : Type*}
 
 section min_poly_def
-variables [comm_ring α] [ring β] [algebra α β]
+variables [comm_ring A] [ring B] [algebra A B]
 
 /-- Let `B` be an `A`-algebra, and `x` an element of `B` that is integral over `A`
 so we have some term `hx : is_integral A x`.
 The minimal polynomial `minpoly hx` of `x` is a monic polynomial of smallest degree
 that has `x` as its root.
 For instance, if `V` is a `K`-vector space for some field `K`, and `f : V →ₗ[K] V` then
 the minimal polynomial of `f` is `minpoly f.is_integral`. -/
-noncomputable def minpoly {x : β} (hx : is_integral α x) : polynomial α :=
+noncomputable def minpoly {x : B} (hx : is_integral A x) : polynomial A :=
 well_founded.min degree_lt_wf _ hx
 
 end min_poly_def
 
 namespace minpoly
 
 section ring
-variables [comm_ring α] [ring β] [algebra α β]
-variables {x : β} (hx : is_integral α x)
+variables [comm_ring A] [ring B] [algebra A B]
+variables {x : B} (hx : is_integral A x)
 
 /--A minimal polynomial is monic.-/
 lemma monic : monic (minpoly hx) :=
@@ -56,34 +54,34 @@ lemma monic : monic (minpoly hx) :=
 
 /--The defining property of the minimal polynomial of an element x:
 it is the monic polynomial with smallest degree that has x as its root.-/
-lemma min {p : polynomial α} (pmonic : p.monic) (hp : polynomial.aeval x p = 0) :
+lemma min {p : polynomial A} (pmonic : p.monic) (hp : polynomial.aeval x p = 0) :
   degree (minpoly hx) ≤ degree p :=
 le_of_not_lt $ well_founded.not_lt_min degree_lt_wf _ hx ⟨pmonic, hp⟩
 
 /-- A minimal polynomial is nonzero. -/
-lemma ne_zero [nontrivial α] : (minpoly hx) ≠ 0 :=
+lemma ne_zero [nontrivial A] : (minpoly hx) ≠ 0 :=
 ne_zero_of_monic (monic hx)
 
 /-- If an element `x` is a root of a nonzero monic polynomial `p`,
 then the degree of `p` is at least the degree of the minimal polynomial of `x`. -/
 lemma degree_le_of_monic
-  {p : polynomial α} (hmonic : p.monic) (hp : polynomial.aeval x p = 0) :
+  {p : polynomial A} (hmonic : p.monic) (hp : polynomial.aeval x p = 0) :
   degree (minpoly hx) ≤ degree p :=
 min _ hmonic (by simp [hp])
 
 end ring
 
 section integral_domain
 
-variables [integral_domain α]
+variables [integral_domain A]
 
 section ring
 
-variables [ring β] [algebra α β] [nontrivial β]
-variables {x : β} (hx : is_integral α x)
+variables [ring B] [algebra A B] [nontrivial B]
+variables {x : B} (hx : is_integral A x)
 
-/--The degree of a minimal polynomial is positive. -/
-lemma degree_pos [nontrivial α] : 0 < degree (minpoly hx) :=
+/-- The degree of a minimal polynomial is positive. -/
+lemma degree_pos [nontrivial A] : 0 < degree (minpoly hx) :=
 begin
   apply lt_of_le_of_ne,
   { simpa only [zero_le_degree_iff] using ne_zero hx },
@@ -99,25 +97,25 @@ end
 
 /-- If `L/K` is a ring extension, and `x` is an element of `L` in the image of `K`,
 then the minimal polynomial of `x` is `X - C x`. -/
-lemma eq_X_sub_C_of_algebra_map_inj [nontrivial α] (a : α)
-  (hf : function.injective (algebra_map α β)) :
-  minpoly (@is_integral_algebra_map α β _ _ _ a) = X - C a :=
+lemma eq_X_sub_C_of_algebra_map_inj [nontrivial A] (a : A)
+  (hf : function.injective (algebra_map A B)) :
+  minpoly (@is_integral_algebra_map A B _ _ _ a) = X - C a :=
 begin
-  have hdegle : (minpoly (@is_integral_algebra_map α β _ _ _ a)).nat_degree ≤ 1,
+  have hdegle : (minpoly (@is_integral_algebra_map A B _ _ _ a)).nat_degree ≤ 1,
   { apply with_bot.coe_le_coe.1,
-    rw [←degree_eq_nat_degree (ne_zero (@is_integral_algebra_map α β _ _ _ a)),
+    rw [←degree_eq_nat_degree (ne_zero (@is_integral_algebra_map A B _ _ _ a)),
       with_top.coe_one, ←degree_X_sub_C a],
-    refine degree_le_of_monic (@is_integral_algebra_map α β _ _ _ a) (monic_X_sub_C a) _,
+    refine degree_le_of_monic (@is_integral_algebra_map A B _ _ _ a) (monic_X_sub_C a) _,
     simp only [aeval_C, aeval_X, alg_hom.map_sub, sub_self] },
-  have hdeg : (minpoly (@is_integral_algebra_map α β _ _ _ a)).degree = 1,
-  { apply (degree_eq_iff_nat_degree_eq (ne_zero (@is_integral_algebra_map α β _ _ _ a))).2,
+  have hdeg : (minpoly (@is_integral_algebra_map A B _ _ _ a)).degree = 1,
+  { apply (degree_eq_iff_nat_degree_eq (ne_zero (@is_integral_algebra_map A B _ _ _ a))).2,
     exact (has_le.le.antisymm hdegle (nat.succ_le_of_lt (with_bot.coe_lt_coe.1
-    (lt_of_lt_of_le (degree_pos (@is_integral_algebra_map α β _ _ _ a)) degree_le_nat_degree)))) },
+    (lt_of_lt_of_le (degree_pos (@is_integral_algebra_map A B _ _ _ a)) degree_le_nat_degree)))) },
   have hrw := eq_X_add_C_of_degree_eq_one hdeg,
-  simp only [monic (@is_integral_algebra_map α β _ _ _ a), one_mul,
+  simp only [monic (@is_integral_algebra_map A B _ _ _ a), one_mul,
     monic.leading_coeff, ring_hom.map_one] at hrw,
-  have h0 : (minpoly (@is_integral_algebra_map α β _ _ _ a)).coeff 0 = -a,
-  { have hroot := aeval (@is_integral_algebra_map α β _ _ _ a),
+  have h0 : (minpoly (@is_integral_algebra_map A B _ _ _ a)).coeff 0 = -a,
+  { have hroot := aeval (@is_integral_algebra_map A B _ _ _ a),
     rw [hrw, add_comm] at hroot,
     simp only [aeval_C, aeval_X, aeval_add] at hroot,
     replace hroot := eq_neg_of_add_eq_zero hroot,
@@ -135,11 +133,11 @@ end ring
 
 section domain
 
-variables [domain β] [algebra α β]
-variables {x : β} (hx : is_integral α x)
+variables [domain B] [algebra A B]
+variables {x : B} (hx : is_integral A x)
 
 /-- If `a` strictly divides the minimal polynomial of `x`, then `x` cannot be a root for `a`. -/
-lemma aeval_ne_zero_of_dvd_not_unit_minpoly {a : polynomial α}
+lemma aeval_ne_zero_of_dvd_not_unit_minpoly {a : polynomial A}
   (hamonic : a.monic) (hdvd : dvd_not_unit a (minpoly hx)) :
   polynomial.aeval x a ≠ 0 :=
 begin
@@ -201,26 +199,26 @@ end domain
 end integral_domain
 
 section field
-variables [field α]
+variables [field A]
 
 section ring
-variables [ring β] [algebra α β]
-variables {x : β} (hx : is_integral α x)
+variables [ring B] [algebra A B]
+variables {x : B} (hx : is_integral A x)
 
-/--If an element x is a root of a nonzero polynomial p,
-then the degree of p is at least the degree of the minimal polynomial of x.-/
+/-- If an element `x` is a root of a nonzero polynomial `p`,
+then the degree of `p` is at least the degree of the minimal polynomial of `x`. -/
 lemma degree_le_of_ne_zero
-  {p : polynomial α} (pnz : p ≠ 0) (hp : polynomial.aeval x p = 0) :
+  {p : polynomial A} (pnz : p ≠ 0) (hp : polynomial.aeval x p = 0) :
   degree (minpoly hx) ≤ degree p :=
 calc degree (minpoly hx) ≤ degree (p * C (leading_coeff p)⁻¹) :
     min _ (monic_mul_leading_coeff_inv pnz) (by simp [hp])
   ... = degree p : degree_mul_leading_coeff_inv p pnz
 
-/--The minimal polynomial of an element x is uniquely characterized by its defining property:
-if there is another monic polynomial of minimal degree that has x as a root,
-then this polynomial is equal to the minimal polynomial of x.-/
-lemma unique {p : polynomial α} (pmonic : p.monic) (hp : polynomial.aeval x p = 0)
-  (pmin : ∀ q : polynomial α, q.monic → polynomial.aeval x q = 0 → degree p ≤ degree q) :
+/-- The minimal polynomial of an element `x` is uniquely characterized by its defining property:
+if there is another monic polynomial of minimal degree that has `x` as a root,
+then this polynomial is equal to the minimal polynomial of `x`. -/
+lemma unique {p : polynomial A} (pmonic : p.monic) (hp : polynomial.aeval x p = 0)
+  (pmin : ∀ q : polynomial A, q.monic → polynomial.aeval x q = 0 → degree p ≤ degree q) :
   p = minpoly hx :=
 begin
   symmetry, apply eq_of_sub_eq_zero,
@@ -233,8 +231,9 @@ begin
       (pmin (minpoly hx) (monic hx) (aeval hx)) },
 end
 
-/--If an element x is a root of a polynomial p, then the minimal polynomial of x divides p.-/
-lemma dvd {p : polynomial α} (hp : polynomial.aeval x p = 0) :
+/-- If an element `x` is a root of a polynomial `p`, then the minimal polynomial of `x` divides `p`.
+-/
+lemma dvd {p : polynomial A} (hp : polynomial.aeval x p = 0) :
   minpoly hx ∣ p :=
 begin
   rw ← dvd_iff_mod_by_monic_eq_zero (monic hx),
@@ -246,14 +245,14 @@ begin
     simpa using hp }
 end
 
-lemma dvd_map_of_is_scalar_tower {α γ : Type*} (β : Type*) [comm_ring α] [field β] [comm_ring γ]
-  [algebra α β] [algebra α γ] [algebra β γ] [is_scalar_tower α β γ] {x : γ} (hx : is_integral α x) :
-  minpoly (is_integral_of_is_scalar_tower x hx) ∣ (minpoly hx).map (algebra_map α β) :=
+lemma dvd_map_of_is_scalar_tower {A γ : Type*} (B : Type*) [comm_ring A] [field B] [comm_ring γ]
+  [algebra A B] [algebra A γ] [algebra B γ] [is_scalar_tower A B γ] {x : γ} (hx : is_integral A x) :
+  minpoly (is_integral_of_is_scalar_tower x hx) ∣ (minpoly hx).map (algebra_map A B) :=
 by { apply minpoly.dvd, rw [← is_scalar_tower.aeval_apply, minpoly.aeval] }
 
-variables [nontrivial β]
+variables [nontrivial B]
 
-theorem unique' {p : polynomial α} (hp1 : _root_.irreducible p) (hp2 : polynomial.aeval x p = 0)
+theorem unique' {p : polynomial A} (hp1 : _root_.irreducible p) (hp2 : polynomial.aeval x p = 0)
   (hp3 : p.monic) : p = minpoly hx :=
 let ⟨q, hq⟩ := dvd hx hp2 in
 eq_of_monic_of_associated hp3 (monic hx) $
@@ -264,16 +263,16 @@ section gcd_domain
 
 /-- For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
 over the fraction field. -/
-lemma gcd_domain_eq_field_fractions {α : Type u} {β : Type v} {γ : Type w} [integral_domain α]
-  [gcd_monoid α] [field β] [integral_domain γ] (f : fraction_map α β) [algebra f.codomain γ]
-  [algebra α γ] [is_scalar_tower α f.codomain γ] {x : γ} (hx : is_integral α x) :
-  minpoly (@is_integral_of_is_scalar_tower α f.codomain γ _ _ _ _ _ _ _ x hx) =
+lemma gcd_domain_eq_field_fractions {A K R : Type*} [integral_domain A]
+  [gcd_monoid A] [field K] [integral_domain R] (f : fraction_map A K) [algebra f.codomain R]
+  [algebra A R] [is_scalar_tower A f.codomain R] {x : R} (hx : is_integral A x) :
+  minpoly (@is_integral_of_is_scalar_tower A f.codomain R _ _ _ _ _ _ _ x hx) =
     ((minpoly hx).map (localization_map.to_ring_hom f)) :=
 begin
-  refine (unique' (@is_integral_of_is_scalar_tower α f.codomain γ _ _ _ _ _ _ _ x hx) _ _ _).symm,
+  refine (unique' (@is_integral_of_is_scalar_tower A f.codomain R _ _ _ _ _ _ _ x hx) _ _ _).symm,
   { exact (polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map f
   (polynomial.monic.is_primitive (monic hx))).1 (irreducible hx) },
-  { have htower := is_scalar_tower.aeval_apply α f.codomain γ x (minpoly hx),
+  { have htower := is_scalar_tower.aeval_apply A f.codomain R x (minpoly hx),
     simp only [localization_map.algebra_map_eq, aeval] at htower,
     exact htower.symm },
   { exact monic_map _ (monic hx) }
@@ -282,27 +281,27 @@ end
 /-- The minimal polynomial over `ℤ` is the same as the minimal polynomial over `ℚ`. -/
 --TODO use `gcd_domain_eq_field_fractions` directly when localizations are defined
 -- in terms of algebras instead of `ring_hom`s
-lemma over_int_eq_over_rat {α : Type u} [integral_domain α] {x : α} [algebra ℚ α]
+lemma over_int_eq_over_rat {A : Type*} [integral_domain A] {x : A} [algebra ℚ A]
   (hx : is_integral ℤ x) :
-  minpoly (@is_integral_of_is_scalar_tower ℤ ℚ α _ _ _ _ _ _ _ x hx) =
+  minpoly (@is_integral_of_is_scalar_tower ℤ ℚ A _ _ _ _ _ _ _ x hx) =
     map (int.cast_ring_hom ℚ) (minpoly hx) :=
 begin
-  refine (unique' (@is_integral_of_is_scalar_tower ℤ ℚ α _ _ _ _ _ _ _ x hx) _ _ _).symm,
+  refine (unique' (@is_integral_of_is_scalar_tower ℤ ℚ A _ _ _ _ _ _ _ x hx) _ _ _).symm,
   { exact (is_primitive.int.irreducible_iff_irreducible_map_cast
   (polynomial.monic.is_primitive (monic hx))).1 (irreducible hx) },
-  { have htower := is_scalar_tower.aeval_apply ℤ ℚ α x (minpoly hx),
+  { have htower := is_scalar_tower.aeval_apply ℤ ℚ A x (minpoly hx),
     simp only [localization_map.algebra_map_eq, aeval] at htower,
     exact htower.symm },
   { exact monic_map _ (monic hx) }
 end
 
 /-- For GCD domains, the minimal polynomial divides any primitive polynomial that has the integral
 element as root. -/
-lemma gcd_domain_dvd {α : Type u} {β : Type v} {γ : Type w}
-  [integral_domain α] [gcd_monoid α] [field β] [integral_domain γ]
-  (f : fraction_map α β) [algebra f.codomain γ] [algebra α γ] [is_scalar_tower α f.codomain γ]
-  {x : γ} (hx : is_integral α x)
-  {P : polynomial α} (hprim : is_primitive P) (hroot : polynomial.aeval x P = 0) :
+lemma gcd_domain_dvd {A K R : Type*}
+  [integral_domain A] [gcd_monoid A] [field K] [integral_domain R]
+  (f : fraction_map A K) [algebra f.codomain R] [algebra A R] [is_scalar_tower A f.codomain R]
+  {x : R} (hx : is_integral A x)
+  {P : polynomial A} (hprim : is_primitive P) (hroot : polynomial.aeval x P = 0) :
   minpoly hx ∣ P :=
 begin
   apply (is_primitive.dvd_iff_fraction_map_dvd_fraction_map f
@@ -316,7 +315,7 @@ end
 as root. -/
 -- TODO use `gcd_domain_dvd` directly when localizations are defined in terms of algebras
 -- instead of `ring_hom`s
-lemma integer_dvd {α : Type u} [integral_domain α] [algebra ℚ α] {x : α} (hx : is_integral ℤ x)
+lemma integer_dvd {A : Type*} [integral_domain A] [algebra ℚ A] {x : A} (hx : is_integral ℤ x)
   {P : polynomial ℤ} (hprim : is_primitive P) (hroot : polynomial.aeval x P = 0) :
   minpoly hx ∣ P :=
 begin
@@ -329,35 +328,35 @@ end
 
 end gcd_domain
 
-variable (β)
-/--If L/K is a field extension, and x is an element of L in the image of K,
-then the minimal polynomial of x is X - C x.-/
-lemma eq_X_sub_C (a : α) :
-  minpoly (@is_integral_algebra_map α β _ _ _ a) =
+variable (B)
+/-- If `L/K` is a field extension, and `x` is an element of `L` in the image of `K`,
+then the minimal polynomial of `x` is `X - C x`. -/
+lemma eq_X_sub_C (a : A) :
+  minpoly (@is_integral_algebra_map A B _ _ _ a) =
   X - C a :=
-eq.symm $ unique' (@is_integral_algebra_map α β _ _ _ a) (irreducible_X_sub_C a)
+eq.symm $ unique' (@is_integral_algebra_map A B _ _ _ a) (irreducible_X_sub_C a)
   (by rw [alg_hom.map_sub, aeval_X, aeval_C, sub_self]) (monic_X_sub_C a)
-variable {β}
+variable {B}
 
-/--The minimal polynomial of 0 is X.-/
-@[simp] lemma zero {h₀ : is_integral α (0:β)} :
+/-- The minimal polynomial of `0` is `X`. -/
+@[simp] lemma zero {h₀ : is_integral A (0:B)} :
   minpoly h₀ = X :=
 by simpa only [add_zero, C_0, sub_eq_add_neg, neg_zero, ring_hom.map_zero]
-  using eq_X_sub_C β (0:α)
+  using eq_X_sub_C B (0:A)
 
-/--The minimal polynomial of 1 is X - 1.-/
-@[simp] lemma one {h₁ : is_integral α (1:β)} :
+/-- The minimal polynomial of `1` is `X - 1`. -/
+@[simp] lemma one {h₁ : is_integral A (1:B)} :
   minpoly h₁ = X - 1 :=
 by simpa only [ring_hom.map_one, C_1, sub_eq_add_neg]
-  using eq_X_sub_C β (1:α)
+  using eq_X_sub_C B (1:A)
 
 end ring
 
 section domain
-variables [domain β] [algebra α β]
-variables {x : β} (hx : is_integral α x)
+variables [domain B] [algebra A B]
+variables {x : B} (hx : is_integral A x)
 
-/--A minimal polynomial is prime.-/
+/-- A minimal polynomial is prime. -/
 lemma prime : prime (minpoly hx) :=
 begin
   refine ⟨ne_zero hx, not_is_unit hx, _⟩,
@@ -367,10 +366,10 @@ begin
   exact or.imp (dvd hx) (dvd hx) this
 end
 
-/--If L/K is a field extension and an element y of K is a root of the minimal polynomial
-of an element x ∈ L, then y maps to x under the field embedding.-/
-lemma root {x : β} (hx : is_integral α x) {y : α}
-  (h : is_root (minpoly hx) y) : algebra_map α β y = x :=
+/-- If `L/K` is a field extension and an element `y` of `K` is a root of the minimal polynomial
+of an element `x ∈ L`, then `y` maps to `x` under the field embedding. -/
+lemma root {x : B} (hx : is_integral A x) {y : A} (h : is_root (minpoly hx) y) :
+  algebra_map A B y = x :=
 have key : minpoly hx = X - C y :=
 eq_of_monic_of_associated (monic hx) (monic_X_sub_C y) (associated_of_dvd_dvd
   (dvd_symm_of_irreducible (irreducible_X_sub_C y) (irreducible hx) (dvd_iff_is_root.2 h))