feat(ring_theory/polynomial): mv_polynomial.integral_domain (#2021)

* feat(ring_theory/polynomial): mv_polynomial.integral_domain

* Add docstrings

* Add docstrings

* Fix import

* Fix build

* Please linter, please

* Update src/algebra/ring.lean

* Clean up code, process comments

* Update src/data/equiv/fin.lean

* Update src/data/equiv/fin.lean

* Update src/data/equiv/fin.lean

* Update src/ring_theory/polynomial.lean

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebra/ring.lean

@@ -627,3 +627,24 @@ variables [domain α]
 end domain
 
 end units
+
+/-- A predicate to express that a ring is an integral domain.
+
+This is mainly useful because such a predicate does not contain data,
+and can therefore be easily transported along ring isomorphisms. -/
+structure is_integral_domain (R : Type u) [ring R] : Prop :=
+(mul_comm : ∀ (x y : R), x * y = y * x)
+(eq_zero_or_eq_zero_of_mul_eq_zero : ∀ x y : R, x * y = 0 → x = 0 ∨ y = 0)
+(zero_ne_one : (0 : R) ≠ 1)
+
+/-- Every integral domain satisfies the predicate for integral domains. -/
+lemma integral_domain.to_is_integral_domain (R : Type u) [integral_domain R] :
+  is_integral_domain R :=
+{ .. (‹_› : integral_domain R) }
+
+/-- If a ring satisfies the predicate for integral domains,
+then it can be endowed with an `integral_domain` instance
+whose data is definitionally equal to the existing data. -/
+def is_integral_domain.to_integral_domain (R : Type u) [ring R] (h : is_integral_domain R) :
+  integral_domain R :=
+{ .. (‹_› : ring R), .. (‹_› : is_integral_domain R) }

src/data/equiv/algebra.lean

@@ -609,6 +609,21 @@ begin
   { exact congr_arg equiv.inv_fun h₁ }
 end
 
+/-- If two rings are isomorphic, and the second is an integral domain, then so is the first. -/
+protected lemma is_integral_domain {A : Type u} (B : Type v) [ring A] [ring B]
+  (hB : is_integral_domain B) (e : A ≃+* B) : is_integral_domain A :=
+{ mul_comm := λ x y, have e.symm (e x * e y) = e.symm (e y * e x), by rw hB.mul_comm, by simpa,
+  eq_zero_or_eq_zero_of_mul_eq_zero := λ x y hxy,
+    have e x * e y = 0, by rw [← e.map_mul, hxy, e.map_zero],
+    (hB.eq_zero_or_eq_zero_of_mul_eq_zero _ _ this).imp (λ hx, by simpa using congr_arg e.symm hx)
+      (λ hy, by simpa using congr_arg e.symm hy),
+  zero_ne_one := λ H, hB.zero_ne_one $ by rw [← e.map_zero, ← e.map_one, H] }
+
+/-- If two rings are isomorphic, and the second is an integral domain, then so is the first. -/
+protected def integral_domain {A : Type u} (B : Type v) [ring A] [integral_domain B]
+  (e : A ≃+* B) : integral_domain A :=
+{ .. (‹_› : ring A), .. e.is_integral_domain B (integral_domain.to_is_integral_domain B) }
+
 end ring_equiv
 
 /-- The group of ring automorphisms. -/

src/data/equiv/fin.lean

@@ -2,19 +2,31 @@
 Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kenny Lau
-
-Equivalences between finite numbers.
 -/
+
 import data.fin data.equiv.basic
 
+/-!
+# Equivalences for `fin n`
+-/
+
+universe variables u
+
 variables {m n : ℕ}
 
+/-- Equivalence between `fin 0` and `empty`. -/
 def fin_zero_equiv : fin 0 ≃ empty :=
 ⟨fin_zero_elim, empty.elim, assume a, fin_zero_elim a, assume a, empty.elim a⟩
 
+/-- Equivalence between `fin 0` and `pempty`. -/
+def fin_zero_equiv' : fin 0 ≃ pempty.{u} :=
+equiv.equiv_pempty fin.elim0
+
+/-- Equivalence between `fin 1` and `punit`. -/
 def fin_one_equiv : fin 1 ≃ punit :=
 ⟨λ_, (), λ_, 0, fin.cases rfl (λa, fin_zero_elim a), assume ⟨⟩, rfl⟩
 
+/-- Equivalence between `fin 2` and `bool`. -/
 def fin_two_equiv : fin 2 ≃ bool :=
 ⟨@fin.cases 1 (λ_, bool) ff (λ_, tt),
   λb, cond b 1 0,
@@ -25,6 +37,14 @@ def fin_two_equiv : fin 2 ≃ bool :=
   end,
   assume b, match b with tt := rfl | ff := rfl end⟩
 
+/-- Equivalence between `fin n.succ` and `option (fin n)` -/
+def fin_succ_equiv (n : ℕ) : fin n.succ ≃ option (fin n) :=
+⟨λ x, fin.cases none some x, λ x, option.rec_on x 0 fin.succ,
+  λ x, fin.cases rfl (λ i, show (option.rec_on (fin.cases none some (fin.succ i) : option (fin n))
+    0 fin.succ : fin n.succ) = _, by rw fin.cases_succ) x,
+  by rintro ⟨none | x⟩; [refl, exact fin.cases_succ _]⟩
+
+/-- Equivalence between `fin m ⊕ fin n` and `fin (m + n)` -/
 def sum_fin_sum_equiv : fin m ⊕ fin n ≃ fin (m + n) :=
 { to_fun := λ x, sum.rec_on x
     (λ y, ⟨y.1, nat.lt_of_lt_of_le y.2 $ nat.le_add_right m n⟩)
@@ -46,6 +66,7 @@ def sum_fin_sum_equiv : fin m ⊕ fin n ≃ fin (m + n) :=
     { dsimp, rw [dif_neg H], simp [fin.ext_iff, nat.add_sub_of_le (le_of_not_gt H)] }
   end }
 
+/-- Equivalence between `fin m × fin n` and `fin (m * n)` -/
 def fin_prod_fin_equiv : fin m × fin n ≃ fin (m * n) :=
 { to_fun := λ x, ⟨x.2.1 + n * x.1.1,
     calc x.2.1 + n * x.1.1 + 1
@@ -71,8 +92,10 @@ def fin_prod_fin_equiv : fin m × fin n ≃ fin (m * n) :=
         ... = y.1 : nat.mod_eq_of_lt y.2),
   right_inv := λ x, fin.eq_of_veq $ nat.mod_add_div _ _ }
 
+/-- `fin 0` is a subsingleton. -/
 instance subsingleton_fin_zero : subsingleton (fin 0) :=
 fin_zero_equiv.subsingleton
 
+/-- `fin 1` is a subsingleton. -/
 instance subsingleton_fin_one : subsingleton (fin 1) :=
 fin_one_equiv.subsingleton

src/data/mv_polynomial.lean

@@ -1044,6 +1044,34 @@ eval₂_rename_prodmk id _ _ _
 
 end
 
+/-- Every polynomial is a polynomial in finitely many variables. -/
+theorem exists_finset_rename (p : mv_polynomial γ α) :
+  ∃ (s : finset γ) (q : mv_polynomial {x // x ∈ s} α), p = q.rename coe :=
+begin
+  apply induction_on p,
+  { intro r, exact ⟨∅, C r, by rw rename_C⟩ },
+  { rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩,
+    refine ⟨s ∪ t, ⟨_, _⟩⟩,
+    { exact rename (subtype.map id (finset.subset_union_left s t)) p +
+            rename (subtype.map id (finset.subset_union_right s t)) q },
+    { rw [rename_add, rename_rename, rename_rename], refl } },
+  { rintro p n ⟨s, p, rfl⟩,
+    refine ⟨insert n s, ⟨_, _⟩⟩,
+  { exact rename (subtype.map id (finset.subset_insert n s)) p * X ⟨n, s.mem_insert_self n⟩ },
+    { rw [rename_mul, rename_X, rename_rename], refl } }
+end
+
+/-- Every polynomial is a polynomial in finitely many variables. -/
+theorem exists_fin_rename (p : mv_polynomial γ α) :
+  ∃ (n : ℕ) (f : fin n → γ) (hf : injective f) (q : mv_polynomial (fin n) α), p = q.rename f :=
+begin
+  obtain ⟨s, q, rfl⟩ := exists_finset_rename p,
+  obtain ⟨n, ⟨e⟩⟩ := fintype.exists_equiv_fin {x // x ∈ s},
+  refine ⟨n, coe ∘ e.symm, injective_comp subtype.val_injective e.symm.injective, q.rename e, _⟩,
+  rw [← rename_rename, rename_rename e],
+  simp only [function.comp, equiv.symm_apply_apply, rename_rename]
+end
+
 end rename
 
 lemma eval₂_cast_comp {β : Type u} {γ : Type v} (f : γ → β)

src/ring_theory/adjoin.lean

@@ -178,7 +178,7 @@ theorem is_noetherian_ring_of_fg {S : subalgebra R A} (HS : S.fg)
   [is_noetherian_ring R] : is_noetherian_ring S :=
 let ⟨t, ht⟩ := HS in ht ▸ (algebra.adjoin_eq_range R (↑t : set A)).symm ▸
 by haveI : is_noetherian_ring (mv_polynomial (↑t : set A) R) :=
-is_noetherian_ring_mv_polynomial_of_fintype;
+mv_polynomial.is_noetherian_ring;
 convert alg_hom.is_noetherian_ring_range _; apply_instance
 
 theorem is_noetherian_ring_closure (s : set R) (hs : s.finite) :

src/ring_theory/polynomial.lean

@@ -8,7 +8,7 @@ Ring-theoretic supplement of data.polynomial.
 Main result: Hilbert basis theorem, that if a ring is noetherian then so is its polynomial ring.
 -/
 
-import data.polynomial data.mv_polynomial
+import data.equiv.fin data.polynomial data.mv_polynomial
 import ring_theory.subring
 import ring_theory.ideals ring_theory.noetherian
 
@@ -131,7 +131,7 @@ def of_subring (p : polynomial T) : polynomial R :=
 
 end polynomial
 
-variables {R : Type u} [comm_ring R]
+variables {R : Type u} {σ : Type v} [comm_ring R]
 
 namespace ideal
 open polynomial
@@ -225,8 +225,8 @@ is_noetherian_submodule_left.1 (is_noetherian_of_fg_of_noetherian _
 
 end ideal
 
-/-- Hilbert basis theorem. -/
-theorem is_noetherian_ring_polynomial [is_noetherian_ring R] : is_noetherian_ring (polynomial R) :=
+/-- Hilbert basis theorem: a polynomial ring over a noetherian ring is a noetherian ring. -/
+protected theorem polynomial.is_noetherian_ring [is_noetherian_ring R] : is_noetherian_ring (polynomial R) :=
 ⟨assume I : ideal (polynomial R),
 let L := I.leading_coeff in
 let M := well_founded.min (is_noetherian_iff_well_founded.1 (by apply_instance))
@@ -284,25 +284,101 @@ from hs ▸ λ x hx, submodule.span_induction hx (λ _ hx, ideal.subset_span hx)
     exact hs2 ⟨polynomial.mem_degree_le.2 hdq, hq⟩ }
 end⟩⟩
 
-theorem is_noetherian_ring_mv_polynomial_fin {n : ℕ} [is_noetherian_ring R] :
+attribute [instance] polynomial.is_noetherian_ring
+
+namespace mv_polynomial
+
+theorem is_noetherian_ring_fin {n : ℕ} [is_noetherian_ring R] :
   is_noetherian_ring (mv_polynomial (fin n) R) :=
 begin
   induction n with n ih,
-  { exact is_noetherian_ring_of_ring_equiv R
-      ((mv_polynomial.pempty_ring_equiv R).symm.trans $ mv_polynomial.ring_equiv_of_equiv _
-        ⟨pempty.elim, fin.elim0, λ x, pempty.elim x, λ x, fin.elim0 x⟩) },
+  { apply is_noetherian_ring_of_ring_equiv R,
+    refine (mv_polynomial.pempty_ring_equiv R).symm.trans _,
+    refine mv_polynomial.ring_equiv_of_equiv _ _,
+    exact ⟨pempty.elim, fin.elim0, λ x, pempty.elim x, λ x, fin.elim0 x⟩ },
+  resetI,
   exact @is_noetherian_ring_of_ring_equiv (polynomial (mv_polynomial (fin n) R)) _
     (mv_polynomial (fin (n+1)) R) _
     ((mv_polynomial.option_equiv_left _ _).symm.trans (mv_polynomial.ring_equiv_of_equiv _
       ⟨λ x, option.rec_on x 0 fin.succ, λ x, fin.cases none some x,
       by rintro ⟨none | x⟩; [refl, exact fin.cases_succ _],
       λ x, fin.cases rfl (λ i, show (option.rec_on (fin.cases none some (fin.succ i) : option (fin n))
         0 fin.succ : fin n.succ) = _, by rw fin.cases_succ) x⟩))
-    (@@is_noetherian_ring_polynomial _ ih)
+    (by apply_instance)
 end
 
-theorem is_noetherian_ring_mv_polynomial_of_fintype {σ : Type v} [fintype σ]
-  [is_noetherian_ring R] : is_noetherian_ring (mv_polynomial σ R) :=
+/-- The multivariate polynomial ring in finitely many variables over a noetherian ring
+is itself a noetherian ring. -/
+instance is_noetherian_ring [fintype σ] [is_noetherian_ring R] :
+  is_noetherian_ring (mv_polynomial σ R) :=
 trunc.induction_on (fintype.equiv_fin σ) $ λ e,
 @is_noetherian_ring_of_ring_equiv (mv_polynomial (fin (fintype.card σ)) R) _ _ _
-  (mv_polynomial.ring_equiv_of_equiv _ e.symm) is_noetherian_ring_mv_polynomial_fin
+  (mv_polynomial.ring_equiv_of_equiv _ e.symm) is_noetherian_ring_fin
+
+/-- Auxilliary lemma:
+Multivariate polynomials over an integral domain
+with variables indexed by `fin n` form an integral domain.
+This fact is proven inductively,
+and then used to prove the general case without any finiteness hypotheses.
+See `mv_polynomial.integral_domain` for the general case. -/
+lemma is_integral_domain_fin (R : Type u) [comm_ring R] (hR : is_integral_domain R) (n : ℕ) :
+  is_integral_domain (mv_polynomial (fin n) R) :=
+begin
+  induction n with n ih,
+  { let e : mv_polynomial (fin 0) R ≃+* R :=
+      (ring_equiv_of_equiv R fin_zero_equiv').trans (mv_polynomial.pempty_ring_equiv R),
+    exact ring_equiv.is_integral_domain R hR e },
+  let e : mv_polynomial (fin (n.succ)) R ≃+* polynomial (mv_polynomial (fin n) R) :=
+    (ring_equiv_of_equiv R $ fin_succ_equiv n).trans (option_equiv_left R (fin n)),
+  refine ring_equiv.is_integral_domain (polynomial (mv_polynomial (fin n) R)) _ e,
+  letI _ih := @is_integral_domain.to_integral_domain (mv_polynomial (fin n) R) _ ih,
+  letI _id := @polynomial.integral_domain _ _ih,
+  exact @integral_domain.to_is_integral_domain _ _id,
+end
+
+lemma is_integral_domain_fintype (R : Type u) (σ : Type v) [comm_ring R] [fintype σ]
+  (hR : is_integral_domain R) : is_integral_domain (mv_polynomial σ R) :=
+trunc.induction_on (fintype.equiv_fin σ) $ λ e,
+@ring_equiv.is_integral_domain _ (mv_polynomial (fin $ fintype.card σ) R) _ _
+  (mv_polynomial.is_integral_domain_fin _ hR _)
+  (ring_equiv_of_equiv R e)
+
+/-- Auxilliary definition:
+Multivariate polynomials in finitely many variables over an integral domain form an integral domain.
+This fact is proven by transport of structure from the `mv_polynomial.integral_domain_fin`,
+and then used to prove the general case without finiteness hypotheses.
+See `mv_polynomial.integral_domain` for the general case. -/
+def integral_domain_fintype (R : Type u) (σ : Type v) [integral_domain R] [fintype σ] :
+  integral_domain (mv_polynomial σ R) :=
+@is_integral_domain.to_integral_domain _ _ $ mv_polynomial.is_integral_domain_fintype R σ $
+integral_domain.to_is_integral_domain R
+
+protected theorem eq_zero_or_eq_zero_of_mul_eq_zero {R : Type u} [integral_domain R] {σ : Type v}
+  (p q : mv_polynomial σ R) (h : p * q = 0) : p = 0 ∨ q = 0 :=
+begin
+  obtain ⟨s, p, rfl⟩ := exists_finset_rename p,
+  obtain ⟨t, q, rfl⟩ := exists_finset_rename q,
+  have : p.rename (subtype.map id (finset.subset_union_left s t) : {x // x ∈ s} → {x // x ∈ s ∪ t}) *
+    q.rename (subtype.map id (finset.subset_union_right s t)) = 0,
+  { apply injective_rename _ subtype.val_injective, simpa using h },
+  letI := mv_polynomial.integral_domain_fintype R {x // x ∈ (s ∪ t)},
+  rw mul_eq_zero at this,
+  cases this; [left, right],
+  all_goals { simpa using congr_arg (rename subtype.val) this }
+end
+
+/-- The multivariate polynomial ring over an integral domain is an integral domain. -/
+instance {R : Type u} {σ : Type v} [integral_domain R] :
+  integral_domain (mv_polynomial σ R) :=
+{ eq_zero_or_eq_zero_of_mul_eq_zero := mv_polynomial.eq_zero_or_eq_zero_of_mul_eq_zero,
+  zero_ne_one :=
+  begin
+    intro H,
+    have : eval₂ id (λ s, (0:R)) (0 : mv_polynomial σ R) =
+      eval₂ id (λ s, (0:R)) (1 : mv_polynomial σ R),
+    { congr, exact H },
+    simpa,
+  end,
+  .. (by apply_instance : comm_ring (mv_polynomial σ R)) }
+
+end mv_polynomial