refactor(data/{mv_,}polynomial): lemmas about adjoin (#10670)

Prove `adjoin {X} = ⊤` and `adjoin (range X) = ⊤` for `polynomial`s
and `mv_polynomial`s much earlier and use these equalities to golf
some proofs.

Also drop some `comm_` in typeclass assumptions.

src/algebra/algebra/subalgebra.lean

@@ -348,6 +348,10 @@ lemma mem_map {S : subalgebra R A} {f : A →ₐ[R] B} {y : B} :
   y ∈ map S f ↔ ∃ x ∈ S, f x = y :=
 subsemiring.mem_map
 
+@[simp] lemma coe_map (S : subalgebra R A) (f : A →ₐ[R] B) :
+  (S.map f : set B) = f '' S :=
+rfl
+
 /-- Preimage of a subalgebra under an algebra homomorphism. -/
 def comap' (S : subalgebra R B) (f : A →ₐ[R] B) : subalgebra R A :=
 { algebra_map_mem' := λ r, show f (algebra_map R A r) ∈ S,
@@ -423,19 +427,12 @@ f.cod_restrict f.range f.mem_range_self
 /-- The equalizer of two R-algebra homomorphisms -/
 def equalizer (ϕ ψ : A →ₐ[R] B) : subalgebra R A :=
 { carrier := {a | ϕ a = ψ a},
-  add_mem' := λ x y hx hy, by
-  { change ϕ x = ψ x at hx,
-    change ϕ y = ψ y at hy,
-    change ϕ (x + y) = ψ (x + y),
-    rw [alg_hom.map_add, alg_hom.map_add, hx, hy] },
-  mul_mem' := λ x y hx hy, by
-  { change ϕ x = ψ x at hx,
-    change ϕ y = ψ y at hy,
-    change ϕ (x * y) = ψ (x * y),
-    rw [alg_hom.map_mul, alg_hom.map_mul, hx, hy] },
-  algebra_map_mem' := λ x, by
-  { change ϕ (algebra_map R A x) = ψ (algebra_map R A x),
-    rw [alg_hom.commutes, alg_hom.commutes] } }
+  add_mem' := λ x y (hx : ϕ x = ψ x) (hy : ϕ y = ψ y),
+    by rw [set.mem_set_of_eq, ϕ.map_add, ψ.map_add, hx, hy],
+  mul_mem' := λ x y (hx : ϕ x = ψ x) (hy : ϕ y = ψ y),
+    by rw [set.mem_set_of_eq, ϕ.map_mul, ψ.map_mul, hx, hy],
+  algebra_map_mem' := λ x,
+    by rw [set.mem_set_of_eq, alg_hom.commutes, alg_hom.commutes] }
 
 @[simp] lemma mem_equalizer (ϕ ψ : A →ₐ[R] B) (x : A) :
   x ∈ ϕ.equalizer ψ ↔ ϕ x = ψ x := iff.rfl
@@ -581,12 +578,11 @@ theorem eq_top_iff {S : subalgebra R A} :
 ⟨λ h x, by rw h; exact mem_top, λ h, by ext x; exact ⟨λ _, mem_top, λ _, h x⟩⟩
 
 @[simp] theorem map_top (f : A →ₐ[R] B) : subalgebra.map (⊤ : subalgebra R A) f = f.range :=
-subalgebra.ext $ λ x,
-  ⟨λ ⟨y, _, hy⟩, ⟨y, hy⟩, λ ⟨y, hy⟩, ⟨y, algebra.mem_top, hy⟩⟩
+set_like.coe_injective set.image_univ
 
 @[simp] theorem map_bot (f : A →ₐ[R] B) : subalgebra.map (⊥ : subalgebra R A) f = ⊥ :=
-eq_bot_iff.2 $ λ x ⟨y, hy, hfy⟩, let ⟨r, hr⟩ := mem_bot.1 hy in subalgebra.range_le _
-⟨r, by rwa [← f.commutes, hr]⟩
+set_like.coe_injective $
+  by simp only [← set.range_comp, (∘), algebra.coe_bot, subalgebra.coe_map, f.commutes]
 
 @[simp] theorem comap_top (f : A →ₐ[R] B) : subalgebra.comap' (⊤ : subalgebra R B) f = ⊤ :=
 eq_top_iff.2 $ λ x, mem_top

src/data/mv_polynomial/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 -/
 
-import algebra.algebra.tower
+import ring_theory.adjoin.basic
 import data.finsupp.antidiagonal
 import algebra.monoid_algebra.basic
 import order.symm_diff
@@ -345,7 +345,7 @@ hom_eq_hom f (ring_hom.id _) hC hX p
 alg_hom.coe_ring_hom_injective (mv_polynomial.ring_hom_ext'
   (congr_arg alg_hom.to_ring_hom h₁) h₂)
 
-@[ext] lemma alg_hom_ext {A : Type*} [comm_semiring A] [algebra R A]
+@[ext] lemma alg_hom_ext {A : Type*} [semiring A] [algebra R A]
   {f g : mv_polynomial σ R →ₐ[R] A} (hf : ∀ i : σ, f (X i) = g (X i)) :
   f = g :=
 add_monoid_algebra.alg_hom_ext' (mul_hom_ext' (λ (x : σ), monoid_hom.ext_mnat (hf x)))
@@ -354,6 +354,15 @@ add_monoid_algebra.alg_hom_ext' (mul_hom_ext' (λ (x : σ), monoid_hom.ext_mnat
   f (C r) = C r :=
 f.commutes r
 
+@[simp] lemma adjoin_range_X : algebra.adjoin R (range (X : σ → mv_polynomial σ R)) = ⊤ :=
+begin
+  set S := algebra.adjoin R (range (X : σ → mv_polynomial σ R)),
+  refine top_unique (λ p hp, _), clear hp,
+  induction p using mv_polynomial.induction_on,
+  case h_C : { exact S.algebra_map_mem _ },
+  case h_add : p q hp hq { exact S.add_mem hp hq },
+  case h_X : p i hp { exact S.mul_mem hp (algebra.subset_adjoin $ mem_range_self _) }
+end
 
 section support
 
@@ -1127,6 +1136,17 @@ lemma aeval_prod {ι : Type*} (s : finset ι) (φ : ι → mv_polynomial σ R) :
   aeval f (∏ i in s, φ i) = ∏ i in s, aeval f (φ i) :=
 (mv_polynomial.aeval f).map_prod _ _
 
+variable (R)
+
+lemma _root_.algebra.adjoin_range_eq_range_aeval :
+  algebra.adjoin R (set.range f) = (mv_polynomial.aeval f).range :=
+by simp only [← algebra.map_top, ← mv_polynomial.adjoin_range_X, alg_hom.map_adjoin,
+  ← set.range_comp, (∘), mv_polynomial.aeval_X]
+
+theorem _root_.algebra.adjoin_eq_range (s : set S₁) :
+  algebra.adjoin R s = (mv_polynomial.aeval (coe : s → S₁)).range :=
+by rw [← algebra.adjoin_range_eq_range_aeval, subtype.range_coe]
+
 end aeval
 
 section aeval_tower

src/data/mv_polynomial/supported.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import ring_theory.adjoin.polynomial
 import data.mv_polynomial.variables
 
 /-!

src/data/polynomial/algebra_map.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
-import algebra.algebra.tower
+import ring_theory.adjoin.basic
 import data.polynomial.eval
 
 /-!
@@ -150,13 +150,17 @@ def aeval : polynomial R →ₐ[R] A :=
 
 variables {R A}
 
-@[ext] lemma alg_hom_ext {f g : polynomial R →ₐ[R] A} (h : f X = g X) : f = g :=
+@[simp] lemma adjoin_X : algebra.adjoin R ({X} : set (polynomial R)) = ⊤ :=
 begin
-  ext p,
-  rw [← sum_monomial_eq p],
-  simp [sum, f.map_sum, g.map_sum, monomial_eq_smul_X, h],
+  refine top_unique (λ p hp, _),
+  set S := algebra.adjoin R ({X} : set (polynomial R)),
+  rw [← sum_monomial_eq p], simp only [monomial_eq_smul_X, sum],
+  exact S.sum_mem (λ n hn, S.smul_mem (S.pow_mem (algebra.subset_adjoin rfl) _) _)
 end
 
+@[ext] lemma alg_hom_ext {f g : polynomial R →ₐ[R] A} (h : f X = g X) : f = g :=
+alg_hom.ext_of_adjoin_eq_top adjoin_X $ λ p hp, (set.mem_singleton_iff.1 hp).symm ▸ h
+
 theorem aeval_def (p : polynomial R) : aeval x p = eval₂ (algebra_map R A) x p := rfl
 
 @[simp] lemma aeval_zero : aeval x (0 : polynomial R) = 0 :=
@@ -199,20 +203,15 @@ eval₂_comp (algebra_map R A)
   aeval b (p.map (algebra_map R A)) = aeval b p :=
 by rw [aeval_def, eval₂_map, ←is_scalar_tower.algebra_map_eq, ←aeval_def]
 
+theorem aeval_alg_hom (f : A →ₐ[R] B) (x : A) : aeval (f x) = f.comp (aeval x) :=
+alg_hom_ext $ by simp only [aeval_X, alg_hom.comp_apply]
+
+@[simp] theorem aeval_X_left : aeval (X : polynomial R) = alg_hom.id R (polynomial R) :=
+alg_hom_ext $ aeval_X X
+
 theorem eval_unique (φ : polynomial R →ₐ[R] A) (p) :
   φ p = eval₂ (algebra_map R A) (φ X) p :=
-begin
-  apply polynomial.induction_on p,
-  { intro r, rw eval₂_C, exact φ.commutes r },
-  { intros f g ih1 ih2,
-    rw [φ.map_add, ih1, ih2, eval₂_add] },
-  { intros n r ih,
-    rw [pow_succ', ← mul_assoc, φ.map_mul,
-        eval₂_mul_noncomm (algebra_map R A) _ (λ k, algebra.commutes _ _), eval₂_X, ih] }
-end
-
-theorem aeval_alg_hom (f : A →ₐ[R] B) (x : A) : aeval (f x) = f.comp (aeval x) :=
-alg_hom.ext $ λ p, by rw [eval_unique (f.comp (aeval x)), alg_hom.comp_apply, aeval_X, aeval_def]
+by rw [← aeval_def, aeval_alg_hom, aeval_X_left, alg_hom.comp_id]
 
 theorem aeval_alg_hom_apply (f : A →ₐ[R] B) (x : A) (p : polynomial R) :
   aeval (f x) p = f (aeval x p) :=
@@ -248,6 +247,14 @@ lemma coeff_zero_eq_aeval_zero' (p : polynomial R) :
   algebra_map R A (p.coeff 0) = aeval (0 : A) p :=
 by simp [aeval_def]
 
+variable (R)
+
+theorem _root_.algebra.adjoin_singleton_eq_range_aeval (x : A) :
+  algebra.adjoin R {x} = (polynomial.aeval x).range :=
+by rw [← algebra.map_top, ← adjoin_X, alg_hom.map_adjoin, set.image_singleton, aeval_X]
+
+variable {R}
+
 section comm_semiring
 
 variables [comm_semiring S] {f : R →+* S}

src/ring_theory/adjoin/basic.lean

@@ -10,17 +10,11 @@ import linear_algebra.prod
 # Adjoining elements to form subalgebras
 
 This file develops the basic theory of subalgebras of an R-algebra generated
-by a set of elements. A basic interface for `adjoin` is set up, and various
-results about finitely-generated subalgebras and submodules are proved.
-
-## Definitions
-
-* `fg (S : subalgebra R A)` : A predicate saying that the subalgebra is finitely-generated
-as an A-algebra
+by a set of elements. A basic interface for `adjoin` is set up.
 
 ## Tags
 
-adjoin, algebra, finitely-generated algebra
+adjoin, algebra
 
 -/
 
@@ -251,4 +245,12 @@ lemma map_adjoin (φ : A →ₐ[R] B) (s : set A) :
   (adjoin R s).map φ = adjoin R (φ '' s) :=
 (adjoin_image _ _ _).symm
 
+lemma adjoin_le_equalizer (φ₁ φ₂ : A →ₐ[R] B) {s : set A} (h : s.eq_on φ₁ φ₂) :
+  adjoin R s ≤ φ₁.equalizer φ₂ :=
+adjoin_le h
+
+lemma ext_of_adjoin_eq_top {s : set A} (h : adjoin R s = ⊤) ⦃φ₁ φ₂ : A →ₐ[R] B⦄
+  (hs : s.eq_on φ₁ φ₂) : φ₁ = φ₂ :=
+ext $ λ x, adjoin_le_equalizer φ₁ φ₂ hs $ h.symm ▸ trivial
+
 end alg_hom

src/ring_theory/adjoin/fg.lean

@@ -5,7 +5,7 @@ Authors: Kenny Lau
 -/
 import ring_theory.polynomial.basic
 import ring_theory.principal_ideal_domain
-import ring_theory.adjoin.polynomial
+import data.mv_polynomial.basic
 
 /-!
 # Adjoining elements to form subalgebras