chore(algebra/associated): make irreducible not a class (#14713)

This functionality was rarely used and doesn't align with how `irreducible` is used in practice.

In a future PR, we can remove some `unfreezingI`s caused by this.



Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

src/algebra/associated.lean

@@ -133,21 +133,18 @@ end
 We explicitly avoid stating that `p` is non-zero, this would require a semiring. Assuming only a
 monoid allows us to reuse irreducible for associated elements.
 -/
-class irreducible [monoid α] (p : α) : Prop :=
-(not_unit' : ¬ is_unit p)
+structure irreducible [monoid α] (p : α) : Prop :=
+(not_unit : ¬ is_unit p)
 (is_unit_or_is_unit' : ∀a b, p = a * b → is_unit a ∨ is_unit b)
 
 namespace irreducible
 
-lemma not_unit [monoid α] {p : α} (hp : irreducible p) : ¬ is_unit p :=
-hp.1
-
 lemma not_dvd_one [comm_monoid α] {p : α} (hp : irreducible p) : ¬ p ∣ 1 :=
 mt (is_unit_of_dvd_one _) hp.not_unit
 
 lemma is_unit_or_is_unit [monoid α] {p : α} (hp : irreducible p) {a b : α} (h : p = a * b) :
   is_unit a ∨ is_unit b :=
-irreducible.is_unit_or_is_unit' a b h
+hp.is_unit_or_is_unit' a b h
 
 end irreducible
 

src/algebra/module/pid.lean

@@ -60,7 +60,7 @@ open submodule
 `p i ^ e i`-torsion submodules for some primes `p i` and numbers `e i`.-/
 theorem submodule.is_internal_prime_power_torsion_of_pid
   [module.finite R M] (hM : module.is_torsion R M) :
-  ∃ (ι : Type u) [fintype ι] [decidable_eq ι] (p : ι → R) [∀ i, irreducible $ p i] (e : ι → ℕ),
+  ∃ (ι : Type u) [fintype ι] [decidable_eq ι] (p : ι → R) (h : ∀ i, irreducible $ p i) (e : ι → ℕ),
   by exactI direct_sum.is_internal (λ i, torsion_by R M $ p i ^ e i) :=
 begin
   obtain ⟨P, dec, hP, e, this⟩ := is_internal_prime_power_torsion hM,
@@ -202,7 +202,7 @@ end p_torsion
 /--A finitely generated torsion module over a PID is isomorphic to a direct sum of some
   `R ⧸ R ∙ (p i ^ e i)` where the `p i ^ e i` are prime powers.-/
 theorem equiv_direct_sum_of_is_torsion [h' : module.finite R N] (hN : module.is_torsion R N) :
-  ∃ (ι : Type u) [fintype ι] (p : ι → R) [∀ i, irreducible $ p i] (e : ι → ℕ),
+  ∃ (ι : Type u) [fintype ι] (p : ι → R) (h : ∀ i, irreducible $ p i) (e : ι → ℕ),
   nonempty $ N ≃ₗ[R] ⨁ (i : ι), R ⧸ R ∙ (p i ^ e i) :=
 begin
   obtain ⟨I, fI, _, p, hp, e, h⟩ := submodule.is_internal_prime_power_torsion_of_pid hN,
@@ -226,7 +226,7 @@ end
   module over a PID is isomorphic to the product of a free module and a direct sum of some
   `R ⧸ R ∙ (p i ^ e i)` where the `p i ^ e i` are prime powers.-/
 theorem equiv_free_prod_direct_sum [h' : module.finite R N] :
-  ∃ (n : ℕ) (ι : Type u) [fintype ι] (p : ι → R) [∀ i, irreducible $ p i] (e : ι → ℕ),
+  ∃ (n : ℕ) (ι : Type u) [fintype ι] (p : ι → R) (h : ∀ i, irreducible $ p i) (e : ι → ℕ),
   nonempty $ N ≃ₗ[R] (fin n →₀ R) × ⨁ (i : ι), R ⧸ R ∙ (p i ^ e i) :=
 begin
   haveI := is_noetherian_of_fg_of_noetherian' (module.finite_def.mp h'),

src/field_theory/adjoin.lean

@@ -372,7 +372,7 @@ begin
   { rw [h, inv_zero], exact subalgebra.zero_mem (algebra.adjoin F {α}) },
 
   let ϕ := alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly F α,
-  haveI := minpoly.irreducible hα,
+  haveI := fact.mk (minpoly.irreducible hα),
   suffices : ϕ ⟨x, hx⟩ * (ϕ ⟨x, hx⟩)⁻¹ = 1,
   { convert subtype.mem (ϕ.symm (ϕ ⟨x, hx⟩)⁻¹),
     refine inv_eq_of_mul_eq_one_right _,
@@ -512,7 +512,7 @@ alg_equiv.of_bijective
   (adjoin_root.lift_hom (minpoly F α) (adjoin_simple.gen F α) (aeval_gen_minpoly F α))
   (begin
     set f := adjoin_root.lift _ _ (aeval_gen_minpoly F α : _),
-    haveI := minpoly.irreducible h,
+    haveI := fact.mk (minpoly.irreducible h),
     split,
     { exact ring_hom.injective f },
     { suffices : F⟮α⟯.to_subfield ≤ ring_hom.field_range ((F⟮α⟯.to_subfield.subtype).comp f),

src/field_theory/normal.lean

@@ -137,6 +137,7 @@ begin
   refine ⟨Hx, or.inr _⟩,
   rintros q q_irred ⟨r, hr⟩,
   let D := adjoin_root q,
+  haveI := fact.mk q_irred,
   let pbED := adjoin_root.power_basis q_irred.ne_zero,
   haveI : finite_dimensional E D := power_basis.finite_dimensional pbED,
   have finrankED : finite_dimensional.finrank E D = q.nat_degree := power_basis.finrank pbED,
@@ -152,7 +153,7 @@ begin
       (linear_map.finrank_le_finrank_of_injective (show function.injective ϕ.to_linear_map,
         from ϕ.to_ring_hom.injective)) finite_dimensional.finrank_pos, },
   let C := adjoin_root (minpoly F x),
-  have Hx_irred := minpoly.irreducible Hx,
+  haveI Hx_irred := fact.mk (minpoly.irreducible Hx),
   letI : algebra C D := ring_hom.to_algebra (adjoin_root.lift
     (algebra_map F D) (adjoin_root.root q) (by rw [algebra_map_eq F E D, ←eval₂_map, hr,
       adjoin_root.algebra_map_eq, eval₂_mul, adjoin_root.eval₂_root, zero_mul])),

src/field_theory/separable_degree.lean

@@ -15,11 +15,12 @@ This file contains basics about the separable degree of a polynomial.
 
 ## Main results
 
-- `is_separable_contraction`: is the condition that `g(x^(q^m)) = f(x)` for some `m : ℕ`
+- `is_separable_contraction`: is the condition that, for `g` a separable polynomial, we have that
+   `g(x^(q^m)) = f(x)` for some `m : ℕ`.
 - `has_separable_contraction`: the condition of having a separable contraction
 - `has_separable_contraction.degree`: the separable degree, defined as the degree of some
   separable contraction
-- `irreducible_has_separable_contraction`: any irreducible polynomial can be contracted
+- `irreducible.has_separable_contraction`: any irreducible polynomial can be contracted
   to a separable polynomial
 - `has_separable_contraction.dvd_degree'`: the degree of a separable contraction divides the degree,
   in function of the exponential characteristic of the field
@@ -90,8 +91,8 @@ variables (q : ℕ) {f : F[X]} (hf : has_separable_contraction q f)
 
 /-- Every irreducible polynomial can be contracted to a separable polynomial.
 https://stacks.math.columbia.edu/tag/09H0 -/
-lemma irreducible_has_separable_contraction (q : ℕ) [hF : exp_char F q]
-  (f : F[X]) [irred : irreducible f] : has_separable_contraction q f :=
+lemma _root_.irreducible.has_separable_contraction (q : ℕ) [hF : exp_char F q]
+  (f : F[X]) (irred : irreducible f) : has_separable_contraction q f :=
 begin
   casesI hF,
   { exact ⟨f, irred.separable, ⟨0, by rw [pow_zero, expand_one]⟩⟩ },

src/field_theory/splitting_field.lean

@@ -435,11 +435,17 @@ section splitting_field
 def factor (f : K[X]) : K[X] :=
 if H : ∃ g, irreducible g ∧ g ∣ f then classical.some H else X
 
-instance irreducible_factor (f : K[X]) : irreducible (factor f) :=
+lemma irreducible_factor (f : K[X]) : irreducible (factor f) :=
 begin
   rw factor, split_ifs with H, { exact (classical.some_spec H).1 }, { exact irreducible_X }
 end
 
+/-- See note [fact non-instances]. -/
+lemma fact_irreducible_factor (f : K[X]) : fact (irreducible (factor f)) :=
+⟨irreducible_factor f⟩
+
+local attribute [instance] fact_irreducible_factor
+
 theorem factor_dvd_of_not_is_unit {f : K[X]} (hf1 : ¬is_unit f) : factor f ∣ f :=
 begin
   by_cases hf2 : f = 0, { rw hf2, exact dvd_zero _ },

src/number_theory/number_field.lean

@@ -152,17 +152,13 @@ section
 open_locale polynomial
 
 local attribute [-instance] algebra_rat
+local attribute [instance] algebra_rat_subsingleton
 
 /-- The quotient of `ℚ[X]` by the ideal generated by an irreducible polynomial of `ℚ[X]`
 is a number field. -/
-instance {f : ℚ[X]} [hf : irreducible f] : number_field (adjoin_root f) :=
+instance {f : ℚ[X]} [hf : fact (irreducible f)] : number_field (adjoin_root f) :=
 { to_char_zero := char_zero_of_injective_algebra_map (algebra_map ℚ _).injective,
-  to_finite_dimensional := begin
-   let := (adjoin_root.power_basis (irreducible.ne_zero hf : f ≠ 0)),
-   convert power_basis.finite_dimensional this,
-   haveI : subsingleton (algebra ℚ (adjoin_root f)) := algebra_rat_subsingleton,
-   exact subsingleton.elim _ _,
-  end }
+  to_finite_dimensional := by convert (adjoin_root.power_basis hf.out.ne_zero).finite_dimensional }
 
 end
 
@@ -204,13 +200,11 @@ begin
     exact minpoly.ne_zero hx, },
   { intro ha,
     let Qx := adjoin_root (minpoly ℚ x),
-    haveI : irreducible (minpoly ℚ x) := minpoly.irreducible hx,
-    have hK : (aeval x) (minpoly ℚ x) = 0, { exact minpoly.aeval _ _, },
+    haveI : fact (irreducible $ minpoly ℚ x) := ⟨minpoly.irreducible hx⟩,
+    have hK : (aeval x) (minpoly ℚ x) = 0 := minpoly.aeval _ _,
     have hA : (aeval a) (minpoly ℚ x) = 0,
-    { rw [aeval_def, ←eval_map, ←mem_root_set_iff'],
-      exact ha,
-      refine polynomial.monic.ne_zero _,
-      exact polynomial.monic.map (algebra_map ℚ A) (minpoly.monic hx), },
+    { rwa [aeval_def, ←eval_map, ←mem_root_set_iff'],
+      exact ((minpoly.monic hx).map $ algebra_map ℚ A).ne_zero, },
     let ψ : Qx →+* A := adjoin_root.lift (algebra_map ℚ A) a hA,
     letI : algebra Qx A := ring_hom.to_algebra ψ,
     letI : algebra Qx K := ring_hom.to_algebra (adjoin_root.lift (algebra_map ℚ K) x hK),

src/ring_theory/adjoin_root.lean

@@ -62,6 +62,14 @@ instance : inhabited (adjoin_root f) := ⟨0⟩
 
 instance : decidable_eq (adjoin_root f) := classical.dec_eq _
 
+protected lemma nontrivial [is_domain R] (h : degree f ≠ 0) : nontrivial (adjoin_root f) :=
+ideal.quotient.nontrivial
+begin
+  simp_rw [ne.def, span_singleton_eq_top, polynomial.is_unit_iff, not_exists, not_and],
+  rintro x hx rfl,
+  exact h (degree_C hx.ne_zero),
+end
+
 /-- Ring homomorphism from `R[x]` to `adjoin_root f` sending `X` to the `root`. -/
 def mk : R[X] →+* adjoin_root f := ideal.quotient.mk _
 
@@ -196,23 +204,25 @@ end comm_ring
 
 section irreducible
 
-variables [field K] {f : K[X]} [irreducible f]
+variables [field K] {f : K[X]}
 
-instance is_maximal_span : is_maximal (span {f} : ideal K[X]) :=
-principal_ideal_ring.is_maximal_of_irreducible ‹irreducible f›
+instance span_maximal_of_irreducible [fact (irreducible f)] : (span {f}).is_maximal :=
+principal_ideal_ring.is_maximal_of_irreducible $ fact.out _
 
-noncomputable instance field : field (adjoin_root f) :=
+noncomputable instance field [fact (irreducible f)] : field (adjoin_root f) :=
 { ..adjoin_root.comm_ring f,
   ..ideal.quotient.field (span {f} : ideal K[X]) }
 
-lemma coe_injective : function.injective (coe : K → adjoin_root f) :=
+lemma coe_injective (h : degree f ≠ 0) : function.injective (coe : K → adjoin_root f) :=
+have _ := adjoin_root.nontrivial f h, by exactI (of f).injective
+
+lemma coe_injective' [fact (irreducible f)] : function.injective (coe : K → adjoin_root f) :=
 (of f).injective
 
 variable (f)
 
-lemma mul_div_root_cancel :
-  ((X - C (root f)) * (f.map (of f) / (X - C (root f))) : polynomial (adjoin_root f)) =
-    f.map (of f) :=
+lemma mul_div_root_cancel [fact (irreducible f)] :
+  ((X - C (root f)) * (f.map (of f) / (X - C (root f)))) = f.map (of f) :=
 mul_div_eq_iff_is_root.2 $ is_root_root _
 
 end irreducible