feat(ring_theory): generalize power_basis.equiv (#9528)

`power_basis.equiv'` is an alternate formulation of `power_basis.equiv` that is somewhat more general when not over a field: instead of requiring the minimal polynomials are equal, we only require the generators are the roots of each other's minimal polynomials.

This is not quite enough to show `adjoin_root (minpoly R (pb : power_basis R S).gen)` is isomorphic to `S`, since `minpoly R (adjoin_root.root g)` is not guaranteed to have the same exact roots as `g` itself. So in a follow-up PR I will strengthen `power_basis.equiv'` to `adjoin_root.equiv'` that requires the correct hypothesis.

src/field_theory/adjoin.lean

@@ -770,30 +770,30 @@ open intermediate_field
 /-- `pb.equiv_adjoin_simple` is the equivalence between `K⟮pb.gen⟯` and `L` itself. -/
 noncomputable def equiv_adjoin_simple (pb : power_basis K L) :
   K⟮pb.gen⟯ ≃ₐ[K] L :=
-(adjoin.power_basis pb.is_integral_gen).equiv pb
+(adjoin.power_basis pb.is_integral_gen).equiv_of_minpoly 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, adjoin_simple.algebra_map_gen]))
 
 @[simp]
 lemma equiv_adjoin_simple_aeval (pb : power_basis K L) (f : polynomial K) :
   pb.equiv_adjoin_simple (aeval (adjoin_simple.gen K pb.gen) f) = aeval pb.gen f :=
-equiv_aeval _ pb _ f
+equiv_of_minpoly_aeval _ pb _ f
 
 @[simp]
 lemma equiv_adjoin_simple_gen (pb : power_basis K L) :
   pb.equiv_adjoin_simple (adjoin_simple.gen K pb.gen) = pb.gen :=
-equiv_gen _ pb _
+equiv_of_minpoly_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]
+by rw [equiv_adjoin_simple, equiv_of_minpoly_symm, equiv_of_minpoly_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]
+by rw [equiv_adjoin_simple, equiv_of_minpoly_symm, equiv_of_minpoly_gen, adjoin.power_basis_gen]
 
 end power_basis
 

src/ring_theory/power_basis.lean

@@ -337,39 +337,78 @@ noncomputable def alg_hom.fintype (pb : power_basis A S) :
 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
+local attribute [irreducible] power_basis.lift
+
+/-- `pb.equiv_of_root pb' h₁ h₂` is an equivalence of algebras with the same power basis,
+where "the same" means that `pb` is a root of `pb'`s minimal polynomial and vice versa.
+
+See also `power_basis.equiv_of_minpoly` which takes the hypothesis that the
+minimal polynomials are identical.
+-/
+noncomputable def equiv_of_root
   (pb : power_basis A S) (pb' : power_basis A S')
-  (h : minpoly A pb.gen = minpoly A pb'.gen) :
+  (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0) (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) :
   S ≃ₐ[A] S' :=
 alg_equiv.of_alg_hom
-  (pb.lift pb'.gen (h.symm ▸ minpoly.aeval A pb'.gen))
-  (pb'.lift pb.gen (h ▸ minpoly.aeval A pb.gen))
+  (pb.lift pb'.gen h₂)
+  (pb'.lift pb.gen h₁)
   (by { ext x, obtain ⟨f, hf, rfl⟩ := pb'.exists_eq_aeval' x, simp })
   (by { ext x, obtain ⟨f, hf, rfl⟩ := pb.exists_eq_aeval' x, simp })
 
 @[simp]
-lemma equiv_aeval
+lemma equiv_of_root_aeval
   (pb : power_basis A S) (pb' : power_basis A S')
-  (h : minpoly A pb.gen = minpoly A pb'.gen)
+  (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0) (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0)
   (f : polynomial A) :
-  pb.equiv pb' h (aeval pb.gen f) = aeval pb'.gen f :=
-pb.lift_aeval _ (h.symm ▸ minpoly.aeval A _) _
+  pb.equiv_of_root pb' h₁ h₂ (aeval pb.gen f) = aeval pb'.gen f :=
+pb.lift_aeval _ h₂ _
+
+@[simp]
+lemma equiv_of_root_gen
+  (pb : power_basis A S) (pb' : power_basis A S')
+  (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0) (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) :
+  pb.equiv_of_root pb' h₁ h₂ pb.gen = pb'.gen :=
+pb.lift_gen _ h₂
 
 @[simp]
-lemma equiv_gen
+lemma equiv_of_root_symm
+  (pb : power_basis A S) (pb' : power_basis A S')
+  (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0) (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) :
+  (pb.equiv_of_root pb' h₁ h₂).symm = pb'.equiv_of_root pb h₂ h₁ :=
+rfl
+
+/-- `pb.equiv_of_minpoly pb' h` is an equivalence of algebras with the same power basis,
+where "the same" means that they have identical minimal polynomials.
+
+See also `power_basis.equiv_of_root` which takes the hypothesis that each generator is a root of the
+other basis' minimal polynomial; `power_basis.equiv_root` is more general if `A` is not a field.
+-/
+noncomputable def equiv_of_minpoly
   (pb : power_basis A S) (pb' : power_basis A S')
   (h : minpoly A pb.gen = minpoly A pb'.gen) :
-  pb.equiv pb' h pb.gen = pb'.gen :=
-pb.lift_gen _ (h.symm ▸ minpoly.aeval A _)
+  S ≃ₐ[A] S' :=
+pb.equiv_of_root pb' (h ▸ minpoly.aeval _ _) (h.symm ▸ minpoly.aeval _ _)
 
-local attribute [irreducible] power_basis.lift
+@[simp]
+lemma equiv_of_minpoly_aeval
+  (pb : power_basis A S) (pb' : power_basis A S')
+  (h : minpoly A pb.gen = minpoly A pb'.gen)
+  (f : polynomial A) :
+  pb.equiv_of_minpoly pb' h (aeval pb.gen f) = aeval pb'.gen f :=
+pb.equiv_of_root_aeval pb' _ _ _
+
+@[simp]
+lemma equiv_of_minpoly_gen
+  (pb : power_basis A S) (pb' : power_basis A S')
+  (h : minpoly A pb.gen = minpoly A pb'.gen) :
+  pb.equiv_of_minpoly pb' h pb.gen = pb'.gen :=
+pb.equiv_of_root_gen pb' _ _
 
 @[simp]
-lemma equiv_symm
+lemma equiv_of_minpoly_symm
   (pb : power_basis A S) (pb' : power_basis A S')
   (h : minpoly A pb.gen = minpoly A pb'.gen) :
-  (pb.equiv pb' h).symm = pb'.equiv pb h.symm :=
+  (pb.equiv_of_minpoly pb' h).symm = pb'.equiv_of_minpoly pb h.symm :=
 rfl
 
 end equiv
@@ -466,11 +505,17 @@ by { dsimp only [minpoly_gen, map_dim], -- Turn `fin (pb.map e).dim` into `fin p
         alg_equiv.symm_apply_apply, sub_right_inj] }
 
 @[simp]
-lemma equiv_map (pb : power_basis A S) (e : S ≃ₐ[A] S')
-  (h : minpoly A pb.gen = minpoly A (pb.map e).gen) :
-  pb.equiv (pb.map e) h = e :=
+lemma equiv_of_root_map (pb : power_basis A S) (e : S ≃ₐ[A] S')
+  (h₁ h₂) :
+  pb.equiv_of_root (pb.map e) h₁ h₂ = e :=
 by { ext x, obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x, simp [aeval_alg_equiv] }
 
+@[simp]
+lemma equiv_of_minpoly_map (pb : power_basis A S) (e : S ≃ₐ[A] S')
+  (h : minpoly A pb.gen = minpoly A (pb.map e).gen) :
+  pb.equiv_of_minpoly (pb.map e) h = e :=
+pb.equiv_of_root_map _ _ _
+
 end map
 
 end power_basis