feat(ring_theory/{ideal/basic, adjoin_root): some lemmas from #15000 (#…

…16450)

This PR contains some lemmas that were originally in #15000.

The main result that is proven here is `quotient_equiv_quotient_minpoly_map`, which says that if `α` has minimal polynomial `f` over `R` and `I` is an ideal of `R`, then rings  `R[α] / I[α]` and  `(R/I)[X] / (f mod I)` are isomorphic as R-algebras.

Co-authored-by: Anne Baanen <vierkantor@vierkantor.com>

src/algebra/algebra/basic.lean

@@ -907,6 +907,7 @@ rfl
 @[simp] lemma to_ring_equiv_eq_coe : e.to_ring_equiv = e := rfl
 
 @[simp, norm_cast] lemma coe_ring_equiv : ((e : A₁ ≃+* A₂) : A₁ → A₂) = e := rfl
+
 lemma coe_ring_equiv' : (e.to_ring_equiv : A₁ → A₂) = e := rfl
 
 lemma coe_ring_equiv_injective : function.injective (coe : (A₁ ≃ₐ[R] A₂) → (A₁ ≃+* A₂)) :=
@@ -996,8 +997,12 @@ symm_bijective.injective $ ext $ λ x, rfl
   { to_fun := f', inv_fun := f,
     ..(⟨f, f', h₁, h₂, h₃, h₄, h₅⟩ : A₁ ≃ₐ[R] A₂).symm } := rfl
 
-@[simp]
-theorem refl_symm : (alg_equiv.refl : A₁ ≃ₐ[R] A₁).symm = alg_equiv.refl := rfl
+@[simp] theorem refl_symm : (alg_equiv.refl : A₁ ≃ₐ[R] A₁).symm = alg_equiv.refl := rfl
+
+--this should be a simp lemma but causes a lint timeout
+lemma to_ring_equiv_symm (f : A₁ ≃ₐ[R] A₁) : (f : A₁ ≃+* A₁).symm = f.symm := rfl
+
+@[simp] lemma symm_to_ring_equiv : (e.symm : A₂ ≃+* A₁) = (e : A₁ ≃+* A₂).symm := rfl
 
 /-- Algebra equivalences are transitive. -/
 @[trans]
@@ -1166,7 +1171,20 @@ by { ext, refl }
 
 end of_linear_equiv
 
-@[simps mul one inv {attrs := []}] instance aut : group (A₁ ≃ₐ[R] A₁) :=
+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,
   one := refl,

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
@@ -608,7 +609,7 @@ by simp only [polynomial.quot_quot_equiv_comm, quotient_equiv_symm_mk,
   polynomial_quotient_equiv_quotient_polynomial_symm_mk]
 
 /-- The natural isomorphism `R[α]/I[α] ≅ (R/I)[X]/(f mod I)` for `α` a root of `f : polynomial R`
-  and `I : ideal R`-/
+  and `I : ideal R`.-/
 def quot_adjoin_root_equiv_quot_polynomial_quot : (adjoin_root f) ⧸ (I.map (of f)) ≃+*
   polynomial (R ⧸ I) ⧸ (span ({f.map (I^.quotient.mk)} : set (polynomial (R ⧸ I)))) :=
 (quot_map_of_equiv_quot_map_C_map_span_mk I f).trans
@@ -641,6 +642,80 @@ 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 `adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot` to an alg_equiv.  -/
+@[simps apply symm_apply]
+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 (show ∀ x, (quot_adjoin_root_equiv_quot_polynomial_quot I f)
+  (algebra_map R _ x) = algebra_map R _ x, from λ x, begin
+    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,
+    simpa only [this, quot_adjoin_root_equiv_quot_polynomial_quot_mk_of, map_C]
+  end)
+
+@[simp]
+lemma quot_equiv_quot_map_apply_mk (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_apply,
+    adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot_mk_of]
+
+@[simp]
+lemma quot_equiv_quot_map_symm_apply_mk (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_symm_apply,
+    adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot_symm_mk_mk]
+
 end
 
 end adjoin_root
+
+namespace power_basis
+
+open adjoin_root alg_equiv
+
+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)`. -/
+@[simps apply symm_apply]
+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)))) :=
+(of_ring_equiv
+  (show ∀ x, (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]))
+    (algebra_map R (S ⧸ I.map (algebra_map R S)) x) = algebra_map R _ x, from
+  (λ 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]))).trans (adjoin_root.quot_equiv_quot_map _ _)
+
+@[simp]
+lemma quotient_equiv_quotient_minpoly_map_apply_mk (pb : power_basis R S) (I : ideal R)
+  (g : polynomial R) : pb.quotient_equiv_quotient_minpoly_map I
+  (ideal.quotient.mk _ (aeval pb.gen g)) = ideal.quotient.mk _ (g.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_mk]
+
+@[simp]
+lemma quotient_equiv_quotient_minpoly_map_symm_apply_mk (pb : power_basis R S) (I : ideal R)
+  (g : polynomial R) : (pb.quotient_equiv_quotient_minpoly_map I).symm
+  (ideal.quotient.mk _ (g.map I^.quotient.mk)) = (ideal.quotient.mk _ (aeval pb.gen g)) :=
+begin simp only [quotient_equiv_quotient_minpoly_map, to_ring_equiv_eq_coe, symm_trans_apply,
+    quot_equiv_quot_map_symm_apply_mk, of_ring_equiv_symm_apply, quotient_equiv_symm_mk,
+    to_ring_equiv_symm, ring_equiv.symm_symm, adjoin_root.equiv'_apply, coe_ring_equiv,
+    lift_hom_mk, symm_to_ring_equiv],
+
+end
+
+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,26 @@ 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