feat(ring_theory/adjoin): adjoin_range_eq_range_aeval (#9179)

Co-authored-by: Chris Hughes <chrishughes24@gmail.com>

Author: ChrisHughes24

src/field_theory/splitting_field.lean

@@ -454,12 +454,14 @@ alg_equiv.symm $ alg_equiv.of_bijective
   (alg_hom.cod_restrict
     (adjoin_root.lift_hom _ x $ minpoly.aeval F x) _
     (λ p, adjoin_root.induction_on _ p $ λ p,
-      (algebra.adjoin_singleton_eq_range F x).symm ▸ (polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩))
+      (algebra.adjoin_singleton_eq_range_aeval F x).symm ▸
+        (polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩))
   ⟨(alg_hom.injective_cod_restrict _ _ _).2 $ (alg_hom.injective_iff _).2 $ λ p,
     adjoin_root.induction_on _ p $ λ p hp, ideal.quotient.eq_zero_iff_mem.2 $
     ideal.mem_span_singleton.2 $ minpoly.dvd F x hp,
   λ y,
-    let ⟨p, hp⟩ := (set_like.ext_iff.1 (algebra.adjoin_singleton_eq_range F x) (y : R)).1 y.2 in
+    let ⟨p, hp⟩ := (set_like.ext_iff.1
+      (algebra.adjoin_singleton_eq_range_aeval F x) (y : R)).1 y.2 in
     ⟨adjoin_root.mk _ p, subtype.eq hp⟩⟩
 
 open finset

src/ring_theory/adjoin/basic.lean

@@ -206,7 +206,29 @@ le_antisymm
     (λ p ⟨n, hn⟩ hp, by rw [alg_hom.map_mul, mv_polynomial.aeval_def _ (mv_polynomial.X _),
       mv_polynomial.eval₂_X]; exact subalgebra.mul_mem _ hp (subset_adjoin hn)))
 
-theorem adjoin_singleton_eq_range (x : A) : adjoin R {x} = (polynomial.aeval x).range :=
+lemma adjoin_range_eq_range_aeval {σ : Type*} (f : σ → A) :
+  adjoin R (set.range f) = (mv_polynomial.aeval f).range :=
+begin
+  ext x,
+  simp only [adjoin_eq_range, alg_hom.mem_range],
+  split,
+  { rintros ⟨p, rfl⟩,
+    use mv_polynomial.rename (function.surj_inv (@@set.surjective_onto_range f)) p,
+    rw [← alg_hom.comp_apply],
+    refine congr_fun (congr_arg _ _) _,
+    ext,
+    simp only [mv_polynomial.rename_X, function.comp_app, mv_polynomial.aeval_X, alg_hom.coe_comp],
+    simpa [subtype.ext_iff] using function.surj_inv_eq (@@set.surjective_onto_range f) i },
+  { rintros ⟨p, rfl⟩,
+    use mv_polynomial.rename (set.range_factorization f) p,
+    rw [← alg_hom.comp_apply],
+    refine congr_fun (congr_arg _ _) _,
+    ext,
+    simp only [mv_polynomial.rename_X, function.comp_app, mv_polynomial.aeval_X, alg_hom.coe_comp,
+      set.range_factorization_coe] }
+end
+
+theorem adjoin_singleton_eq_range_aeval (x : A) : adjoin R {x} = (polynomial.aeval x).range :=
 le_antisymm
   (adjoin_le $ set.singleton_subset_iff.2 ⟨polynomial.X, polynomial.eval₂_X _ _⟩)
   (λ y ⟨p, (hp : polynomial.aeval x p = y)⟩, hp ▸ polynomial.induction_on p

src/ring_theory/adjoin/power_basis.lean

@@ -45,7 +45,7 @@ begin
     have := hx'.mem_span_pow,
     rw minpoly_eq at this,
     apply this,
-    { rw [adjoin_singleton_eq_range] at hy,
+    { rw [adjoin_singleton_eq_range_aeval] at hy,
       obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy,
       use f,
       ext,

src/ring_theory/adjoin_root.lean

@@ -101,7 +101,7 @@ polynomial.induction_on p (λ x, by { rw aeval_C, refl })
 
 theorem adjoin_root_eq_top : algebra.adjoin R ({root f} : set (adjoin_root f)) = ⊤ :=
 algebra.eq_top_iff.2 $ λ x, induction_on f x $ λ p,
-(algebra.adjoin_singleton_eq_range R (root f)).symm ▸ ⟨p, aeval_eq p⟩
+(algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩
 
 @[simp] lemma eval₂_root (f : polynomial R) : f.eval₂ (of f) (root f) = 0 :=
 by rw [← algebra_map_eq, ← aeval_def, aeval_eq, mk_self]

src/ring_theory/integral_closure.lean

@@ -168,7 +168,7 @@ begin
     rcases finset.mem_image.1 hs with ⟨k, hk, rfl⟩, clear hk,
     exact (algebra.adjoin R {x}).pow_mem (algebra.subset_adjoin (set.mem_singleton _)) k },
   intros r hr, change r ∈ algebra.adjoin R ({x} : set A) at hr,
-  rw algebra.adjoin_singleton_eq_range at hr,
+  rw algebra.adjoin_singleton_eq_range_aeval at hr,
   rcases (aeval x).mem_range.mp hr with ⟨p, rfl⟩,
   rw ← mod_by_monic_add_div p hfm,
   rw ← aeval_def at hfx,