feat(ring_theory/power_basis): map a power basis through an alg_equiv (…

…#8039)

If `A` is equivalent to `A'` as an `R`-algebra and `A` has a power basis, then `A'` also has a power basis. Included are the relevant `simp` lemmas.

This needs a bit of tweaking to `basis.map` and `alg_equiv.to_linear_equiv` for getting more useful `simp` lemmas.

src/algebra/algebra/basic.lean

@@ -891,15 +891,20 @@ noncomputable def of_bijective (f : A₁ →ₐ[R] A₂) (hf : function.bijectiv
 { .. ring_equiv.of_bijective (f : A₁ →+* A₂) hf, .. f }
 
 /-- Forgetting the multiplicative structures, an equivalence of algebras is a linear equivalence. -/
-def to_linear_equiv (e : A₁ ≃ₐ[R] A₂) : A₁ ≃ₗ[R] A₂ :=
-{ to_fun    := e.to_fun,
-  map_add'  := λ x y, by simp,
+@[simps apply] def to_linear_equiv (e : A₁ ≃ₐ[R] A₂) : A₁ ≃ₗ[R] A₂ :=
+{ to_fun    := e,
   map_smul' := λ r x, by simp [algebra.smul_def''],
-  inv_fun   := e.symm.to_fun,
-  left_inv  := e.left_inv,
-  right_inv := e.right_inv, }
+  inv_fun   := e.symm,
+  .. e }
 
-@[simp] lemma to_linear_equiv_apply (e : A₁ ≃ₐ[R] A₂) (x : A₁) : e.to_linear_equiv x = e x := rfl
+@[simp] lemma to_linear_equiv_refl :
+  (alg_equiv.refl : A₁ ≃ₐ[R] A₁).to_linear_equiv = linear_equiv.refl R A₁ := rfl
+
+@[simp] lemma to_linear_equiv_symm (e : A₁ ≃ₐ[R] A₂) :
+  e.to_linear_equiv.symm = e.symm.to_linear_equiv := rfl
+
+@[simp] lemma to_linear_equiv_trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) :
+  (e₁.trans e₂).to_linear_equiv = e₁.to_linear_equiv.trans e₂.to_linear_equiv := rfl
 
 theorem to_linear_equiv_inj {e₁ e₂ : A₁ ≃ₐ[R] A₂} (H : e₁.to_linear_equiv = e₂.to_linear_equiv) :
   e₁ = e₂ :=

src/linear_algebra/basis.lean

@@ -236,7 +236,7 @@ section map
 variables (f : M ≃ₗ[R] M')
 
 /-- Apply the linear equivalence `f` to the basis vectors. -/
-protected def map : basis ι R M' :=
+@[simps] protected def map : basis ι R M' :=
 of_repr (f.symm.trans b.repr)
 
 @[simp] lemma map_apply (i) : b.map f i = f (b i) := rfl

src/ring_theory/power_basis.lean

@@ -378,3 +378,38 @@ begin
   conv_lhs { rw ← mod_by_monic_add_div f this },
   simp only [add_zero, zero_mul, minpoly.aeval, aeval_add, alg_hom.map_mul]
 end
+
+namespace power_basis
+
+section map
+
+variables {S' : Type*} [comm_ring S'] [algebra R S']
+
+/-- `power_basis.map pb (e : S ≃ₐ[R] S')` is the power basis for `S'` generated by `e pb.gen`. -/
+@[simps]
+noncomputable def map (pb : power_basis R S) (e : S ≃ₐ[R] S') : power_basis R S' :=
+{ dim := pb.dim,
+  basis := pb.basis.map e.to_linear_equiv,
+  gen := e pb.gen,
+  basis_eq_pow :=
+    λ i, by rw [basis.map_apply, pb.basis_eq_pow, e.to_linear_equiv_apply, e.map_pow] }
+
+variables [algebra A S] [algebra A S']
+
+@[simp]
+lemma minpoly_gen_map (pb : power_basis A S) (e : S ≃ₐ[A] S') :
+  (pb.map e).minpoly_gen = pb.minpoly_gen :=
+by { dsimp only [minpoly_gen, map_dim], -- Turn `fin (pb.map e).dim` into `fin pb.dim`
+     simp only [linear_equiv.trans_apply, map_basis, basis.map_repr,
+        map_gen, alg_equiv.to_linear_equiv_apply, e.to_linear_equiv_symm, alg_equiv.map_pow,
+        alg_equiv.symm_apply_apply, sub_right_inj] }
+
+@[simp]
+lemma equiv_map [nontrivial S] [nontrivial S'] (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 :=
+by { ext x, obtain ⟨f, hf, rfl⟩ := pb.exists_eq_aeval x, simp [aeval_alg_equiv] }
+
+end map
+
+end power_basis