[Merged by Bors] - feat(ring_theory/{ideal/basic, adjoin_root): some lemmas from #15000

src/algebra/algebra/basic.lean

@@ -999,6 +999,11 @@ symm_bijective.injective $ ext $ λ x, rfl
 @[simp]
 theorem refl_symm : (alg_equiv.refl : A₁ ≃ₐ[R] A₁).symm = alg_equiv.refl := rfl
 
+@[simp]
+lemma to_ring_equiv_symm (f : A₁ ≃ₐ[R] A₁) :
+  (f : A₁ ≃+* A₁).symm = f.symm :=
+rfl
+
 /-- Algebra equivalences are transitive. -/
 @[trans]
 def trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : A₁ ≃ₐ[R] A₃ :=
@@ -1166,6 +1171,19 @@ by { ext, refl }
 
 end of_linear_equiv
 
+section of_ring_equiv
+
+/-- Promotes a linear ring_equiv to an alg_equiv -/
+@[simps]
+def of_ring_equiv (f : A₁ ≃+* A₂)
+  (hf : ∀ x, f (algebra_map R A₁ x) = algebra_map R A₂ x) : A₁ ≃ₐ[R] A₂ :=
+{ to_fun := f,
+  inv_fun := f.symm,
+  commutes' := hf,
+  .. f }
+
+end of_ring_equiv
+
 @[simps mul one {attrs := []}] instance aut : group (A₁ ≃ₐ[R] A₁) :=
 { mul := λ ϕ ψ, ψ.trans ϕ,
   mul_assoc := λ ϕ ψ χ, rfl,

src/ring_theory/adjoin_root.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Chris Hughes
 -/
+import algebra.algebra.basic
 import data.polynomial.field_division
 import linear_algebra.finite_dimensional
 import ring_theory.adjoin.basic
@@ -641,6 +642,68 @@ by rw [quot_adjoin_root_equiv_quot_polynomial_quot, ring_equiv.symm_trans_apply,
     quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk_symm_quot_quot_mk,
     quot_map_of_equiv_quot_map_C_map_span_mk_symm_mk]
 
+/-- Promote `quot_adjoin_root_equiv_quot_polynomial_quot` to an alg_equiv  -/
+noncomputable def quot_equiv_quot_map (f : R[X]) (I : ideal R) :
+  ((adjoin_root f) ⧸ (ideal.map (of f) I)) ≃ₐ[R]
+     ((R ⧸ I) [X]) ⧸ (ideal.span ({polynomial.map I^.quotient.mk f} : set ((R ⧸ I) [X]))) :=
+alg_equiv.of_ring_equiv (quot_adjoin_root_equiv_quot_polynomial_quot I f)
+begin
+  intros x,
+  have : algebra_map R (adjoin_root f ⧸ (ideal.map (of f) I)) x =
+    ideal.quotient.mk (ideal.map (adjoin_root.of f) I) ((mk f) (C x)) := rfl,
+  rw [this, quot_adjoin_root_equiv_quot_polynomial_quot_mk_of, map_C],
+  refl,
+end
+
+@[simp]
+lemma quot_equiv_quot_map_apply (f g : polynomial R) (I : ideal R)  :
+  adjoin_root.quot_equiv_quot_map f I (ideal.quotient.mk _ (adjoin_root.mk f g)) =
+    ideal.quotient.mk _ (g.map I^.quotient.mk) :=
+by rw [adjoin_root.quot_equiv_quot_map, alg_equiv.of_ring_equiv_apply,
+    adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot_mk_of]
+
+lemma quot_equiv_quot_map_symm_apply (f g : polynomial R) (I : ideal R)  :
+  (adjoin_root.quot_equiv_quot_map f I).symm (ideal.quotient.mk _ (map (ideal.quotient.mk I) g)) =
+    ideal.quotient.mk _ (adjoin_root.mk f g) :=
+by rw [adjoin_root.quot_equiv_quot_map, alg_equiv.of_ring_equiv_symm_apply,
+    adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot_symm_mk_mk]
+
 end
 
 end adjoin_root
+
+namespace power_basis
+
+variables [comm_ring R] [is_domain R] [comm_ring S] [is_domain S] [algebra R S]
+
+/-- Let `α` have minimal polynomial `f` over `R` and `I` be an ideal of `R`,
+then `R[α] / (I) = (R[x] / (f)) / pS = (R/p)[x] / (f mod p)` -/
+noncomputable def quotient_equiv_quotient_minpoly_map (pb : power_basis R S)
+  (I : ideal R) :
+  (S ⧸ I.map (algebra_map R S)) ≃ₐ[R] (polynomial (R ⧸ I)) ⧸
+    (ideal.span ({(minpoly R pb.gen).map I^.quotient.mk} : set (polynomial (R ⧸ I)))) :=
+alg_equiv.trans
+  (alg_equiv.of_ring_equiv
+    (ideal.quotient_equiv _ (ideal.map (adjoin_root.of (minpoly R pb.gen)) I)
+    (adjoin_root.equiv' (minpoly R pb.gen) pb
+    (by rw [adjoin_root.aeval_eq, adjoin_root.mk_self])
+    (minpoly.aeval _ _)).symm.to_ring_equiv
+    (by rw [ideal.map_map, alg_equiv.to_ring_equiv_eq_coe, ← alg_equiv.coe_ring_hom_commutes,
+            ← adjoin_root.algebra_map_eq, alg_hom.comp_algebra_map]))
+  (λ x, by rw [← ideal.quotient.mk_algebra_map, ideal.quotient_equiv_apply,
+    ring_hom.to_fun_eq_coe, ideal.quotient_map_mk, alg_equiv.to_ring_equiv_eq_coe,
+    ring_equiv.coe_to_ring_hom, alg_equiv.coe_ring_equiv, alg_equiv.commutes,
+    quotient.mk_algebra_map]))
+  (adjoin_root.quot_equiv_quot_map _ _)
+
+@[simp]
+lemma quotient_equiv_quotient_minpoly_map_apply
+  (pb : power_basis R S) (I : ideal R) (x : polynomial R) :
+  pb.quotient_equiv_quotient_minpoly_map I (ideal.quotient.mk _ (aeval pb.gen x)) =
+    ideal.quotient.mk _ (x.map I^.quotient.mk) :=
+by rw [power_basis.quotient_equiv_quotient_minpoly_map, alg_equiv.trans_apply,
+    alg_equiv.of_ring_equiv_apply, quotient_equiv_mk, alg_equiv.coe_ring_equiv',
+    adjoin_root.equiv'_symm_apply, power_basis.lift_aeval,
+    adjoin_root.aeval_eq, adjoin_root.quot_equiv_quot_map_apply]
+
+end power_basis

src/ring_theory/ideal/operations.lean

@@ -2109,7 +2109,11 @@ end ring_hom
 
 namespace double_quot
 open ideal
-variables {R : Type u} [comm_ring R] (I J : ideal R)
+variable {R : Type u}
+
+section
+
+variables [comm_ring R] (I J : ideal R)
 
 /-- The obvious ring hom `R/I → R/(I ⊔ J)` -/
 def quot_left_to_quot_sup : R ⧸ I →+* R ⧸ (I ⊔ J) :=
@@ -2178,4 +2182,28 @@ lemma quot_quot_equiv_comm_symm :
   (quot_quot_equiv_comm I J).symm = quot_quot_equiv_comm J I :=
 rfl
 
+end
+
+section algebra
+
+@[simp]
+lemma quot_quot_equiv_comm_mk_mk [comm_ring R] (I J : ideal R) (x : R) :
+  quot_quot_equiv_comm I J (ideal.quotient.mk _ (ideal.quotient.mk _ x)) =
+    algebra_map R _ x :=
+rfl
+
+variables [comm_semiring R] {A : Type v} [comm_ring A] [algebra R A] (I J : ideal A)
+
+@[simp]
+lemma quot_quot_equiv_quot_sup_quot_quot_algebra_map  (x : R) :
+  double_quot.quot_quot_equiv_quot_sup I J (algebra_map R _ x) = algebra_map _ _ x :=
+rfl
+
+@[simp]
+lemma quot_quot_equiv_comm_algebra_map  (x : R) :
+  quot_quot_equiv_comm I J (algebra_map R _ x) = algebra_map _ _ x :=
+rfl
+
+end algebra
+
 end double_quot