refactor(field_theory,ring_theory): generalize adjoin_root.equiv to …

…`power_basis` (#8726)

We had two proofs that `A`-preserving maps from `A[x]` or `A(x)` to `B` are in bijection with the set of conjugate roots to `x` in `B`, so by stating the result for `power_basis` we can avoid reproving it twice, and get some generalizations (to a `comm_ring` instead of an `integral_domain`) for free.

There's probably a bit more to generalize in `adjoin_root` or `intermediate_field.adjoin`, which I will do in follow-up PRs.

src/field_theory/adjoin.lean

@@ -429,9 +429,19 @@ end adjoin_intermediate_field_lattice
 
 section adjoin_integral_element
 
-variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] {α : E}
+variables {F : Type*} [field F] {E : Type*} [field E] [algebra F E] {α : E}
 variables {K : Type*} [field K] [algebra F K]
 
+lemma minpoly_gen {α : E} (h : is_integral F α) :
+  minpoly F (adjoin_simple.gen F α) = minpoly F α :=
+begin
+  rw ← adjoin_simple.algebra_map_gen F α at h,
+  have inj := (algebra_map F⟮α⟯ E).injective,
+  exact minpoly.eq_of_algebra_map_eq inj ((is_integral_algebra_map_iff inj).mp h)
+    (adjoin_simple.algebra_map_gen _ _).symm
+end
+
+variables (F)
 lemma aeval_gen_minpoly (α : E) :
   aeval (adjoin_simple.gen F α) (minpoly F α) = 0 :=
 begin
@@ -468,37 +478,59 @@ begin
   { exact aeval_gen_minpoly F α }
 end
 
+section power_basis
+
+variables {L : Type*} [field L] [algebra K L]
+
+/-- The elements `1, x, ..., x ^ (d - 1)` form a basis for `K⟮x⟯`,
+where `d` is the degree of the minimal polynomial of `x`. -/
+noncomputable def power_basis_aux {x : L} (hx : is_integral K x) :
+  basis (fin (minpoly K x).nat_degree) K K⟮x⟯ :=
+(adjoin_root.power_basis (minpoly.ne_zero hx)).basis.map
+  (adjoin_root_equiv_adjoin K hx).to_linear_equiv
+
+/-- The power basis `1, x, ..., x ^ (d - 1)` for `K⟮x⟯`,
+where `d` is the degree of the minimal polynomial of `x`. -/
+@[simps]
+noncomputable def adjoin.power_basis {x : L} (hx : is_integral K x) :
+  power_basis K K⟮x⟯ :=
+{ gen := adjoin_simple.gen K x,
+  dim := (minpoly K x).nat_degree,
+  basis := power_basis_aux hx,
+  basis_eq_pow := λ i,
+    by rw [power_basis_aux, basis.map_apply, power_basis.basis_eq_pow,
+           alg_equiv.to_linear_equiv_apply, alg_equiv.map_pow, adjoin_root.power_basis_gen,
+           adjoin_root_equiv_adjoin_apply_root] }
+
+lemma adjoin.finite_dimensional {x : L} (hx : is_integral K x) : finite_dimensional K K⟮x⟯ :=
+power_basis.finite_dimensional (adjoin.power_basis hx)
+
+lemma adjoin.finrank {x : L} (hx : is_integral K x) :
+  finite_dimensional.finrank K K⟮x⟯ = (minpoly K x).nat_degree :=
+begin
+  rw power_basis.finrank (adjoin.power_basis hx : _),
+  refl
+end
+
+end power_basis
+
 /-- Algebra homomorphism `F⟮α⟯ →ₐ[F] K` are in bijection with the set of roots
 of `minpoly α` in `K`. -/
 noncomputable def alg_hom_adjoin_integral_equiv (h : is_integral F α) :
   (F⟮α⟯ →ₐ[F] K) ≃ {x // x ∈ ((minpoly F α).map (algebra_map F K)).roots} :=
-let ϕ := adjoin_root_equiv_adjoin F h,
-  swap1 : (F⟮α⟯ →ₐ[F] K) ≃ (adjoin_root (minpoly F α) →ₐ[F] K) :=
-  { to_fun := λ f, f.comp ϕ.to_alg_hom,
-    inv_fun := λ f, f.comp ϕ.symm.to_alg_hom,
-    left_inv := λ _, by { ext, simp only [alg_equiv.coe_alg_hom,
-      alg_equiv.to_alg_hom_eq_coe, alg_hom.comp_apply, alg_equiv.apply_symm_apply] },
-    right_inv := λ _, by { ext, simp only [alg_equiv.symm_apply_apply,
-      alg_equiv.coe_alg_hom, alg_equiv.to_alg_hom_eq_coe, alg_hom.comp_apply] } },
-  swap2 := adjoin_root.equiv F K (minpoly F α) (minpoly.ne_zero h) in
-swap1.trans swap2
+(adjoin.power_basis h).lift_equiv'.trans ((equiv.refl _).subtype_equiv (λ x,
+  by rw [adjoin.power_basis_gen, minpoly_gen h, equiv.refl_apply]))
 
 /-- Fintype of algebra homomorphism `F⟮α⟯ →ₐ[F] K` -/
 noncomputable def fintype_of_alg_hom_adjoin_integral (h : is_integral F α) :
   fintype (F⟮α⟯ →ₐ[F] K) :=
-fintype.of_equiv _ (alg_hom_adjoin_integral_equiv F h).symm
+power_basis.alg_hom.fintype (adjoin.power_basis h)
 
 lemma card_alg_hom_adjoin_integral (h : is_integral F α) (h_sep : (minpoly F α).separable)
   (h_splits : (minpoly F α).splits (algebra_map F K)) :
   @fintype.card (F⟮α⟯ →ₐ[F] K) (fintype_of_alg_hom_adjoin_integral F h) =
     (minpoly F α).nat_degree :=
-begin
-  let s := ((minpoly F α).map (algebra_map F K)).roots.to_finset,
-  have H := λ x, multiset.mem_to_finset,
-  rw [fintype.card_congr (alg_hom_adjoin_integral_equiv F h), fintype.card_of_subtype s H,
-      nat_degree_eq_card_roots h_splits, multiset.to_finset_card_of_nodup],
-  exact nodup_roots ((separable_map (algebra_map F K)).mpr h_sep),
-end
+by { rw alg_hom.card_of_power_basis, all_goals { rwa [adjoin.power_basis_gen, minpoly_gen h] } }
 
 end adjoin_integral_element
 
@@ -728,42 +760,6 @@ section power_basis
 
 variables {K L : Type*} [field K] [field L] [algebra K L]
 
-namespace intermediate_field
-
-/-- The elements `1, x, ..., x ^ (d - 1)` form a basis for `K⟮x⟯`,
-where `d` is the degree of the minimal polynomial of `x`. -/
-noncomputable def power_basis_aux {x : L} (hx : is_integral K x) :
-  basis (fin (minpoly K x).nat_degree) K K⟮x⟯ :=
-(adjoin_root.power_basis (minpoly.ne_zero hx)).basis.map
-  (adjoin_root_equiv_adjoin K hx).to_linear_equiv
-
-/-- The power basis `1, x, ..., x ^ (d - 1)` for `K⟮x⟯`,
-where `d` is the degree of the minimal polynomial of `x`. -/
-noncomputable def adjoin.power_basis {x : L} (hx : is_integral K x) :
-  power_basis K K⟮x⟯ :=
-{ gen := adjoin_simple.gen K x,
-  dim := (minpoly K x).nat_degree,
-  basis := power_basis_aux hx,
-  basis_eq_pow := λ i,
-    by rw [power_basis_aux, basis.map_apply, power_basis.basis_eq_pow,
-           alg_equiv.to_linear_equiv_apply, alg_equiv.map_pow, adjoin_root.power_basis_gen,
-           adjoin_root_equiv_adjoin_apply_root] }
-
-@[simp] lemma adjoin.power_basis.gen_eq {x : L} (hx : is_integral K x) :
-  (adjoin.power_basis hx).gen = adjoin_simple.gen K x := rfl
-
-lemma adjoin.finite_dimensional {x : L} (hx : is_integral K x) : finite_dimensional K K⟮x⟯ :=
-power_basis.finite_dimensional (adjoin.power_basis hx)
-
-lemma adjoin.finrank {x : L} (hx : is_integral K x) :
-  finite_dimensional.finrank K K⟮x⟯ = (minpoly K x).nat_degree :=
-begin
-  rw power_basis.finrank (adjoin.power_basis hx : _),
-  refl
-end
-
-end intermediate_field
-
 namespace power_basis
 
 open intermediate_field
@@ -774,7 +770,7 @@ noncomputable def equiv_adjoin_simple (pb : power_basis K L) :
 (adjoin.power_basis pb.is_integral_gen).equiv pb
   (minpoly.eq_of_algebra_map_eq (algebra_map K⟮pb.gen⟯ L).injective
     (adjoin.power_basis pb.is_integral_gen).is_integral_gen
-    (by rw [adjoin.power_basis.gen_eq, adjoin_simple.algebra_map_gen]))
+    (by rw [adjoin.power_basis_gen, adjoin_simple.algebra_map_gen]))
 
 @[simp]
 lemma equiv_adjoin_simple_aeval (pb : power_basis K L) (f : polynomial K) :
@@ -789,12 +785,12 @@ equiv_gen _ pb _
 @[simp]
 lemma equiv_adjoin_simple_symm_aeval (pb : power_basis K L) (f : polynomial K) :
   pb.equiv_adjoin_simple.symm (aeval pb.gen f) = aeval (adjoin_simple.gen K pb.gen) f :=
-by rw [equiv_adjoin_simple, equiv_symm, equiv_aeval, adjoin.power_basis.gen_eq]
+by rw [equiv_adjoin_simple, equiv_symm, equiv_aeval, adjoin.power_basis_gen]
 
 @[simp]
 lemma equiv_adjoin_simple_symm_gen (pb : power_basis K L) :
   pb.equiv_adjoin_simple.symm pb.gen = (adjoin_simple.gen K pb.gen) :=
-by rw [equiv_adjoin_simple, equiv_symm, equiv_gen, adjoin.power_basis.gen_eq]
+by rw [equiv_adjoin_simple, equiv_symm, equiv_gen, adjoin.power_basis_gen]
 
 end power_basis
 

src/field_theory/separable.lean

@@ -626,3 +626,22 @@ begin
 end
 
 end is_separable_tower
+
+section card_alg_hom
+
+variables {R S T : Type*} [comm_ring S]
+variables {K L F : Type*} [field K] [field L] [field F]
+variables [algebra K S] [algebra K L]
+
+lemma alg_hom.card_of_power_basis (pb : power_basis K S) (h_sep : (minpoly K pb.gen).separable)
+  (h_splits : (minpoly K pb.gen).splits (algebra_map K L)) :
+  @fintype.card (S →ₐ[K] L) (power_basis.alg_hom.fintype pb) = (minpoly K pb.gen).nat_degree :=
+begin
+  let s := ((minpoly K pb.gen).map (algebra_map K L)).roots.to_finset,
+  have H := λ x, multiset.mem_to_finset,
+  rw [fintype.card_congr pb.lift_equiv', fintype.card_of_subtype s H,
+      nat_degree_eq_card_roots h_splits, multiset.to_finset_card_of_nodup],
+  exact nodup_roots ((separable_map (algebra_map K L)).mpr h_sep)
+end
+
+end card_alg_hom

src/ring_theory/adjoin_root.lean

@@ -109,6 +109,9 @@ by rw [← algebra_map_eq, ← aeval_def, aeval_eq, mk_self]
 lemma is_root_root (f : polynomial R) : is_root (f.map (of f)) (root f) :=
 by rw [is_root, eval_map, eval₂_root]
 
+lemma is_algebraic_root (hf : f ≠ 0) : is_algebraic R (root f) :=
+⟨f, hf, eval₂_root f⟩
+
 variables [comm_ring S]
 
 /-- Lift a ring homomorphism `i : R →+* S` to `adjoin_root f →+* S`. -/
@@ -159,26 +162,6 @@ begin
   exact (@lift_root _ _ _ _ _ _ _ (aeval_alg_hom_eq_zero f ϕ)).symm,
 end
 
-/-- If `E` is a field extension of `F` and `f` is a polynomial over `F` then the set
-of maps from `F[x]/(f)` into `E` is in bijection with the set of roots of `f` in `E`. -/
-def equiv (F E : Type*) [field F] [field E] [algebra F E] (f : polynomial F) (hf : f ≠ 0) :
-  (adjoin_root f →ₐ[F] E) ≃ {x // x ∈ (f.map (algebra_map F E)).roots} :=
-{ to_fun := λ ϕ, ⟨ϕ (root f), begin
-    rw [mem_roots (map_ne_zero hf), is_root.def, ←eval₂_eq_eval_map],
-    exact aeval_alg_hom_eq_zero f ϕ,
-    exact field.to_nontrivial E, end⟩,
-  inv_fun := λ x, lift_hom f ↑x (begin
-    rw [aeval_def, eval₂_eq_eval_map, ←is_root.def, ←mem_roots (map_ne_zero hf)],
-    exact subtype.mem x,
-    exact field.to_nontrivial E end),
-  left_inv := λ ϕ, lift_hom_eq_alg_hom f ϕ,
-  right_inv := λ x, begin
-    ext,
-    refine @lift_root F E _ f _ _ ↑x _,
-    rw [eval₂_eq_eval_map, ←is_root.def, ←mem_roots (map_ne_zero hf), ←multiset.mem_to_finset],
-    exact multiset.mem_to_finset.mpr (subtype.mem x),
-    exact field.to_nontrivial E end }
-
 end comm_ring
 
 section irreducible
@@ -208,6 +191,28 @@ section power_basis
 
 variables [field K] {f : polynomial K}
 
+lemma is_integral_root (hf : f ≠ 0) : is_integral K (root f) :=
+(is_algebraic_iff_is_integral _).mp (is_algebraic_root hf)
+
+lemma minpoly_root (hf : f ≠ 0) : minpoly K (root f) = f * C (f.leading_coeff⁻¹) :=
+begin
+  have f'_monic : monic _ := monic_mul_leading_coeff_inv hf,
+  refine (minpoly.unique K _ f'_monic _ _).symm,
+  { rw [alg_hom.map_mul, aeval_eq, mk_self, zero_mul] },
+  intros q q_monic q_aeval,
+  have commutes : (lift (algebra_map K (adjoin_root f)) (root f) q_aeval).comp (mk q) = mk f,
+  { ext,
+    { simp only [ring_hom.comp_apply, mk_C, lift_of], refl },
+    { simp only [ring_hom.comp_apply, mk_X, lift_root] } },
+  rw [degree_eq_nat_degree f'_monic.ne_zero, degree_eq_nat_degree q_monic.ne_zero,
+      with_bot.coe_le_coe, nat_degree_mul hf, nat_degree_C, add_zero],
+  apply nat_degree_le_of_dvd,
+  { have : mk f q = 0, by rw [←commutes, ring_hom.comp_apply, mk_self, ring_hom.map_zero],
+    rwa [←ideal.mem_span_singleton, ←ideal.quotient.eq_zero_iff_mem] },
+  { exact q_monic.ne_zero },
+  { rwa [ne.def, C_eq_zero, inv_eq_zero, leading_coeff_eq_zero] },
+end
+
 /-- The elements `1, root f, ..., root f ^ (d - 1)` form a basis for `adjoin_root f`,
 where `f` is an irreducible polynomial over a field of degree `d`. -/
 def power_basis_aux (hf : f ≠ 0) : basis (fin f.nat_degree) K (adjoin_root f) :=
@@ -216,30 +221,14 @@ begin
   have deg_f' : f'.nat_degree = f.nat_degree,
   { rw [nat_degree_mul hf, nat_degree_C, add_zero],
     { rwa [ne.def, C_eq_zero, inv_eq_zero, leading_coeff_eq_zero] } },
-  have f'_monic : monic f' := monic_mul_leading_coeff_inv hf,
-  have aeval_f' : aeval (root f) f' = 0,
-  { rw [f'_def, alg_hom.map_mul, aeval_eq, mk_self, zero_mul] },
-  have hx : is_integral K (root f) := ⟨f', f'_monic, aeval_f'⟩,
-  have minpoly_eq : f' = minpoly K (root f),
-  { apply minpoly.unique K _ f'_monic aeval_f',
-    intros q q_monic q_aeval,
-    have commutes : (lift (algebra_map K (adjoin_root f)) (root f) q_aeval).comp (mk q) = mk f,
-    { ext,
-      { simp only [ring_hom.comp_apply, mk_C, lift_of], refl },
-      { simp only [ring_hom.comp_apply, mk_X, lift_root] } },
-    rw [degree_eq_nat_degree f'_monic.ne_zero, degree_eq_nat_degree q_monic.ne_zero,
-        with_bot.coe_le_coe, deg_f'],
-    apply nat_degree_le_of_dvd,
-    { have : mk f q = 0, by rw [←commutes, ring_hom.comp_apply, mk_self, ring_hom.map_zero],
-      rwa [←ideal.mem_span_singleton, ←ideal.quotient.eq_zero_iff_mem] },
-    { exact q_monic.ne_zero } },
+  have minpoly_eq : minpoly K (root f) = f' := minpoly_root hf,
   apply @basis.mk _ _ _ (λ (i : fin f.nat_degree), (root f ^ i.val)),
-  { rw [←deg_f', minpoly_eq],
-    exact hx.linear_independent_pow },
+  { rw [← deg_f', ← minpoly_eq],
+    exact (is_integral_root hf).linear_independent_pow },
   { rw _root_.eq_top_iff,
     rintros y -,
-    rw [←deg_f', minpoly_eq],
-    apply hx.mem_span_pow,
+    rw [← deg_f', ← minpoly_eq],
+    apply (is_integral_root hf).mem_span_pow,
     obtain ⟨g⟩ := y,
     use g,
     rw aeval_eq,
@@ -255,6 +244,32 @@ where `f` is an irreducible polynomial over a field of degree `d`. -/
   basis := power_basis_aux hf,
   basis_eq_pow := basis.mk_apply _ _ }
 
+lemma minpoly_power_basis_gen (hf : f ≠ 0) :
+  minpoly K (power_basis hf).gen = f * C (f.leading_coeff⁻¹) :=
+by rw [power_basis_gen, minpoly_root hf]
+
+lemma minpoly_power_basis_gen_of_monic (hf : f.monic) (hf' : f ≠ 0 := hf.ne_zero) :
+  minpoly K (power_basis hf').gen = f :=
+by rw [minpoly_power_basis_gen hf', hf.leading_coeff, inv_one, C.map_one, mul_one]
+
 end power_basis
 
+section equiv
+
+variables (K) (L F : Type*) [field F] [field K] [field L] [algebra F K] [algebra F L]
+variables (pb : _root_.power_basis F K)
+
+/-- If `L` is a field extension of `F` and `f` is a polynomial over `F` then the set
+of maps from `F[x]/(f)` into `L` is in bijection with the set of roots of `f` in `L`. -/
+def equiv (f : polynomial F) (hf : f ≠ 0) :
+  (adjoin_root f →ₐ[F] L) ≃ {x // x ∈ (f.map (algebra_map F L)).roots} :=
+(power_basis hf).lift_equiv'.trans ((equiv.refl _).subtype_equiv (λ x,
+  begin
+    rw [power_basis_gen, minpoly_root hf, polynomial.map_mul, roots_mul,
+        polynomial.map_C, roots_C, add_zero, equiv.refl_apply],
+    { rw ← polynomial.map_mul, exact map_monic_ne_zero (monic_mul_leading_coeff_inv hf) }
+  end))
+
+end equiv
+
 end adjoin_root

src/ring_theory/power_basis.lean

@@ -316,14 +316,33 @@ pb.constr_pow_aeval hy f
 maps sending `pb.gen` to that root.
 
 This is the bundled equiv version of `power_basis.lift`.
+If the codomain of the `alg_hom`s is an integral domain, then the roots form a multiset,
+see `lift_equiv'` for the corresponding statement.
 -/
 @[simps]
 noncomputable def lift_equiv (pb : power_basis A S) :
-  {y : S' // aeval y (minpoly A pb.gen) = 0} ≃ (S →ₐ[A] S') :=
-{ to_fun := λ y, pb.lift y y.2,
-  inv_fun := λ f, ⟨f pb.gen, by rw [aeval_alg_hom_apply, minpoly.aeval, f.map_zero]⟩,
-  left_inv := λ y, subtype.ext $ lift_gen _ _ y.prop,
-  right_inv := λ f, pb.alg_hom_ext $ lift_gen _ _ _  }
+  (S →ₐ[A] S') ≃ {y : S' // aeval y (minpoly A pb.gen) = 0} :=
+{ to_fun := λ f, ⟨f pb.gen, by rw [aeval_alg_hom_apply, minpoly.aeval, f.map_zero]⟩,
+  inv_fun := λ y, pb.lift y y.2,
+  left_inv := λ f, pb.alg_hom_ext $ lift_gen _ _ _,
+  right_inv := λ y, subtype.ext $ lift_gen _ _ y.prop }
+
+/-- `pb.lift_equiv'` states that elements of the root set of the minimal
+polynomial of `pb.gen` correspond to maps sending `pb.gen` to that root. -/
+noncomputable def lift_equiv' (pb : power_basis A S) :
+  (S →ₐ[A] B) ≃ {y : B // y ∈ ((minpoly A pb.gen).map (algebra_map A B)).roots} :=
+pb.lift_equiv.trans ((equiv.refl _).subtype_equiv (λ x,
+  begin
+    rw [mem_roots, is_root.def, equiv.refl_apply, ← eval₂_eq_eval_map, ← aeval_def],
+    exact map_monic_ne_zero (minpoly.monic pb.is_integral_gen)
+  end))
+
+/-- There are finitely many algebra homomorphisms `S →ₐ[A] B` if `S` is of the form `A[x]`
+and `B` is an integral domain. -/
+noncomputable def alg_hom.fintype (pb : power_basis A S) :
+  fintype (S →ₐ[A] B) :=
+by letI := classical.dec_eq B; exact
+fintype.of_equiv _ pb.lift_equiv'.symm
 
 /-- `pb.equiv pb' h` is an equivalence of algebras with the same power basis. -/
 noncomputable def equiv