Mathlib.RingTheory.Polynomial.Quotient

Polynomial.quotientSpanXSubCAlgEquiv definition

(x : R) : (R[X] ⧸ Ideal.span ({X - C x} : Set R[X])) ≃ₐ[R] R

Full source

/-- For a commutative ring $R$, evaluating a polynomial at an element $x \in R$ induces an
isomorphism of $R$-algebras $R[X] / \langle X - x \rangle \cong R$. -/
noncomputable def quotientSpanXSubCAlgEquiv (x : R) :
    (R[X] ⧸ Ideal.span ({X - C x} : Set R[X])) ≃ₐ[R] R :=
  (quotientSpanXSubCAlgEquivAux1 x).trans (quotientSpanXSubCAlgEquivAux2 x)

Isomorphism between $R[X]/\langle X - x \rangle$ and $R$ via evaluation at $x$

Informal description

For a commutative ring $R$ and an element $x \in R$, the evaluation of a polynomial at $x$ induces an isomorphism of $R$-algebras between the quotient ring $R[X] / \langle X - x \rangle$ and $R$. More precisely, the isomorphism maps the equivalence class of a polynomial $p$ modulo the ideal $\langle X - x \rangle$ to the evaluation $p(x)$. Its inverse maps an element $y \in R$ to the constant polynomial $y$ in the quotient ring.

Polynomial.quotientSpanXSubCAlgEquiv_mk theorem

(x : R) (p : R[X]) : quotientSpanXSubCAlgEquiv x (Ideal.Quotient.mk _ p) = p.eval x

Full source

@[simp]
theorem quotientSpanXSubCAlgEquiv_mk (x : R) (p : R[X]) :
    quotientSpanXSubCAlgEquiv x (Ideal.Quotient.mk _ p) = p.eval x :=
  rfl

Evaluation of Polynomials via Quotient Isomorphism: $\varphi([p]) = p(x)$

Informal description

For any commutative ring $R$, element $x \in R$, and polynomial $p \in R[X]$, the image of the equivalence class of $p$ under the isomorphism $R[X]/\langle X - x \rangle \cong R$ is equal to the evaluation of $p$ at $x$, i.e., $$ \varphi([p]) = p(x) $$ where $\varphi$ is the isomorphism $R[X]/\langle X - x \rangle \to R$ and $[p]$ denotes the equivalence class of $p$ in the quotient ring.

Polynomial.quotientSpanXSubCAlgEquiv_symm_apply theorem

(x : R) (y : R) : (quotientSpanXSubCAlgEquiv x).symm y = algebraMap R _ y

Full source

@[simp]
theorem quotientSpanXSubCAlgEquiv_symm_apply (x : R) (y : R) :
    (quotientSpanXSubCAlgEquiv x).symm y = algebraMap R _ y :=
  rfl

Inverse of Polynomial Evaluation Isomorphism Maps Constants to Constants

Informal description

For any element $x$ in a commutative ring $R$ and any element $y \in R$, the inverse of the algebra isomorphism $R[X] / \langle X - x \rangle \simeq R$ maps $y$ to the equivalence class of the constant polynomial $y$ in the quotient ring $R[X] / \langle X - x \rangle$.

Polynomial.quotientSpanCXSubCAlgEquiv definition

(x y : R) : (R[X] ⧸ (Ideal.span {C x, X - C y} : Ideal R[X])) ≃ₐ[R] R ⧸ (Ideal.span { x } : Ideal R)

Full source

/-- For a commutative ring $R$, evaluating a polynomial at an element $y \in R$ induces an
isomorphism of $R$-algebras $R[X] / \langle x, X - y \rangle \cong R / \langle x \rangle$. -/
noncomputable def quotientSpanCXSubCAlgEquiv (x y : R) :
    (R[X] ⧸ (Ideal.span {C x, X - C y} : Ideal R[X])) ≃ₐ[R] R ⧸ (Ideal.span {x} : Ideal R) :=
  (Ideal.quotientEquivAlgOfEq R <| by rw [Ideal.span_insert, sup_comm]).trans <|
    (DoubleQuot.quotQuotEquivQuotSupₐ R _ _).symm.trans <|
      (Ideal.quotientEquivAlg _ _ (quotientSpanXSubCAlgEquiv y) rfl).trans <|
        Ideal.quotientEquivAlgOfEq R <| by
          simp only [Ideal.map_span, Set.image_singleton]; congr 2; exact eval_C

Isomorphism between $R[X]/\langle x, X - y \rangle$ and $R/\langle x \rangle$ via evaluation at $y$

Informal description

For a commutative ring $R$ and elements $x, y \in R$, evaluating polynomials at $y$ induces an isomorphism of $R$-algebras between the quotient ring $R[X] / \langle x, X - y \rangle$ and the quotient ring $R / \langle x \rangle$. More precisely, the isomorphism maps the equivalence class of a polynomial $p$ modulo the ideal $\langle x, X - y \rangle$ to the equivalence class of $p(y)$ modulo $\langle x \rangle$. Its inverse maps the equivalence class of an element $a \in R$ modulo $\langle x \rangle$ to the equivalence class of the constant polynomial $a$ in $R[X] / \langle x, X - y \rangle$.

Polynomial.quotientSpanCXSubCXSubCAlgEquiv definition

 {x : R} {y : R[X]} :
  @AlgEquiv R (R[X][X] ⧸ (Ideal.span {C (X - C x), X - C y} : Ideal <| R[X][X])) R _ _ _ (Ideal.Quotient.algebra R) _

Full source

/-- For a commutative ring $R$, evaluating a polynomial at elements $y(X) \in R[X]$ and $x \in R$
induces an isomorphism of $R$-algebras $R[X, Y] / \langle X - x, Y - y(X) \rangle \cong R$. -/
noncomputable def quotientSpanCXSubCXSubCAlgEquiv {x : R} {y : R[X]} :
    @AlgEquiv R (R[X]R[X][X]R[X][X] ⧸ (Ideal.span {C (X - C x), X - C y} : Ideal <| R[X][X])) R _ _ _
      (Ideal.Quotient.algebra R) _ :=
((quotientSpanCXSubCAlgEquiv (X - C x) y).restrictScalars R).trans <| quotientSpanXSubCAlgEquiv x

Isomorphism between $R[X][X]/\langle X - x, X - y \rangle$ and $R$ via evaluation at $(x, y)$

Informal description

For a commutative ring $R$, elements $x \in R$ and $y \in R[X]$, evaluating bivariate polynomials at $(x, y)$ induces an isomorphism of $R$-algebras between the quotient ring $R[X][X] / \langle X - x, X - y \rangle$ and $R$. More precisely, the isomorphism maps the equivalence class of a bivariate polynomial $p$ modulo the ideal $\langle X - x, X - y \rangle$ to the evaluation $p(x, y)$. Its inverse maps an element $a \in R$ to the equivalence class of the constant polynomial $a$ in the quotient ring.

Polynomial.modByMonic_eq_zero_iff_quotient_eq_zero theorem

(p q : R[X]) (hq : q.Monic) : p %ₘ q = 0 ↔ (p : R[X] ⧸ Ideal.span { q }) = 0

Full source

lemma modByMonic_eq_zero_iff_quotient_eq_zero (p q : R[X]) (hq : q.Monic) :
    p %ₘ qp %ₘ q = 0 ↔ (p : R[X] ⧸ Ideal.span {q}) = 0 := by
  rw [modByMonic_eq_zero_iff_dvd hq, Ideal.Quotient.eq_zero_iff_dvd]

Remainder Zero iff Zero in Quotient by Monic Polynomial

Informal description

Let $R$ be a commutative ring and $p, q \in R[X]$ be polynomials with $q$ monic. Then the remainder of $p$ modulo $q$ is zero if and only if the image of $p$ in the quotient ring $R[X]/(q)$ is zero.

Ideal.quotient_map_C_eq_zero theorem

{I : Ideal R} : ∀ a ∈ I, ((Quotient.mk (map (C : R →+* R[X]) I : Ideal R[X])).comp C) a = 0

Full source

theorem quotient_map_C_eq_zero {I : Ideal R} :
    ∀ a ∈ I, ((Quotient.mk (map (C : R →+* R[X]) I : Ideal R[X])).comp C) a = 0 := by
  intro a ha
  rw [RingHom.comp_apply, Quotient.eq_zero_iff_mem]
  exact mem_map_of_mem _ ha

Vanishing of Ideal Elements in Polynomial Quotient via Canonical Embedding

Informal description

For any commutative ring $R$ and any ideal $I$ of $R$, the composition of the canonical embedding $C : R \to R[X]$ with the quotient map $\text{Quotient.mk} : R[X] \to R[X]/(C(I))$ sends every element $a \in I$ to zero in the quotient ring $R[X]/(C(I))$.

Ideal.eval₂_C_mk_eq_zero theorem

{I : Ideal R} : ∀ f ∈ (map (C : R →+* R[X]) I : Ideal R[X]), eval₂RingHom (C.comp (Quotient.mk I)) X f = 0

Full source

theorem eval₂_C_mk_eq_zero {I : Ideal R} :
    ∀ f ∈ (map (C : R →+* R[X]) I : Ideal R[X]), eval₂RingHom (C.comp (Quotient.mk I)) X f = 0 := by
  intro a ha
  rw [← sum_monomial_eq a]
  dsimp
  rw [eval₂_sum]
  refine Finset.sum_eq_zero fun n _ => ?_
  dsimp
  rw [eval₂_monomial (C.comp (Quotient.mk I)) X]
  refine mul_eq_zero_of_left (Polynomial.ext fun m => ?_) (X ^ n)
  rw [RingHom.comp_apply, coeff_C]
  by_cases h : m = 0
  · simpa [h] using Quotient.eq_zero_iff_mem.2 ((mem_map_C_iff.1 ha) n)
  · simp [h]

Vanishing of Polynomial Evaluation for Ideal Elements in Quotient Ring

Informal description

Let $R$ be a commutative ring and $I$ an ideal of $R$. For any polynomial $f$ in the image of the ideal $I$ under the canonical embedding $C : R \to R[X]$, the evaluation of $f$ at $X$ via the ring homomorphism $\text{eval₂RingHom}(C \circ \text{Quotient.mk}(I), X)$ yields zero. In other words, if $f \in C(I) \subseteq R[X]$, then evaluating $f$ with coefficients reduced modulo $I$ and the variable $X$ gives zero.

Ideal.polynomialQuotientEquivQuotientPolynomial definition

(I : Ideal R) : (R ⧸ I)[X] ≃+* R[X] ⧸ (map C I : Ideal R[X])

Full source

/-- If `I` is an ideal of `R`, then the ring polynomials over the quotient ring `I.quotient` is
isomorphic to the quotient of `R[X]` by the ideal `map C I`,
where `map C I` contains exactly the polynomials whose coefficients all lie in `I`. -/
def polynomialQuotientEquivQuotientPolynomial (I : Ideal R) :
    (R ⧸ I)[X](R ⧸ I)[X] ≃+* R[X] ⧸ (map C I : Ideal R[X]) where
  toFun :=
    eval₂RingHom
      (Quotient.lift I ((Quotient.mk (map C I : Ideal R[X])).comp C) quotient_map_C_eq_zero)
      (Quotient.mk (map C I : Ideal R[X]) X)
  invFun :=
    Quotient.lift (map C I : Ideal R[X]) (eval₂RingHom (C.comp (Quotient.mk I)) X)
      eval₂_C_mk_eq_zero
  map_mul' f g := by simp only [coe_eval₂RingHom, eval₂_mul]
  map_add' f g := by simp only [eval₂_add, coe_eval₂RingHom]
  left_inv := by
    intro f
    refine Polynomial.induction_on' f ?_ ?_
    · intro p q hp hq
      simp only [coe_eval₂RingHom] at hp hq
      simp only [coe_eval₂RingHom, hp, hq, RingHom.map_add]
    · rintro n ⟨x⟩
      simp only [← smul_X_eq_monomial, C_mul', Quotient.lift_mk, Submodule.Quotient.quot_mk_eq_mk,
        Quotient.mk_eq_mk, eval₂_X_pow, eval₂_smul, coe_eval₂RingHom, RingHom.map_pow, eval₂_C,
        RingHom.coe_comp, RingHom.map_mul, eval₂_X, Function.comp_apply]
  right_inv := by
    rintro ⟨f⟩
    refine Polynomial.induction_on' f ?_ ?_
    · -- Porting note: was `simp_intro p q hp hq`
      intros p q hp hq
      simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, map_add, Quotient.lift_mk,
        coe_eval₂RingHom] at hp hq ⊢
      rw [hp, hq]
    · intro n a
      simp only [← smul_X_eq_monomial, ← C_mul' a (X ^ n), Quotient.lift_mk,
        Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, eval₂_X_pow, eval₂_smul,
        coe_eval₂RingHom, RingHom.map_pow, eval₂_C, RingHom.coe_comp, RingHom.map_mul, eval₂_X,
        Function.comp_apply]

Isomorphism between polynomial ring over quotient and quotient of polynomial ring

Informal description

For any commutative ring $ R $ and any ideal $ I $ of $ R $, there is a ring isomorphism between the polynomial ring over the quotient ring $ R/I $ and the quotient of the polynomial ring $ R[X] $ by the ideal generated by the image of $ I $ under the canonical embedding $ C : R \to R[X] $. More precisely, the isomorphism is given by: \[ (R/I)[X] \cong R[X] / (C(I)) \] where $ C(I) $ consists of all polynomials in $ R[X] $ whose coefficients lie in $ I $.

Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk theorem

(I : Ideal R) (f : R[X]) : I.polynomialQuotientEquivQuotientPolynomial.symm (Quotient.mk _ f) = f.map (Quotient.mk I)

Full source

@[simp]
theorem polynomialQuotientEquivQuotientPolynomial_symm_mk (I : Ideal R) (f : R[X]) :
    I.polynomialQuotientEquivQuotientPolynomial.symm (Quotient.mk _ f) = f.map (Quotient.mk I) := by
  rw [polynomialQuotientEquivQuotientPolynomial, RingEquiv.symm_mk, RingEquiv.coe_mk,
    Equiv.coe_fn_mk, Quotient.lift_mk, coe_eval₂RingHom, eval₂_eq_eval_map, ← Polynomial.map_map,
    ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]

Inverse Isomorphism of Polynomial Quotient Rings Evaluates to Coefficient Reduction

Informal description

Let $R$ be a commutative ring and $I$ an ideal of $R$. For any polynomial $f \in R[X]$, the inverse of the isomorphism $(R/I)[X] \cong R[X]/(C(I))$ applied to the equivalence class of $f$ in $R[X]/(C(I))$ equals the polynomial obtained by reducing each coefficient of $f$ modulo $I$. In symbols: \[ \varphi^{-1}([f]) = f \mod I \] where $\varphi$ is the isomorphism $(R/I)[X] \cong R[X]/(C(I))$ and $[f]$ denotes the equivalence class of $f$ in $R[X]/(C(I))$.

Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk theorem

 (I : Ideal R) (f : R[X]) :
  I.polynomialQuotientEquivQuotientPolynomial (f.map <| Quotient.mk I) = Quotient.mk (map C I : Ideal R[X]) f

Full source

@[simp]
theorem polynomialQuotientEquivQuotientPolynomial_map_mk (I : Ideal R) (f : R[X]) :
    I.polynomialQuotientEquivQuotientPolynomial (f.map <| Quotient.mk I) =
    Quotient.mk (map C I : Ideal R[X]) f := by
  apply (polynomialQuotientEquivQuotientPolynomial I).symm.injective
  rw [RingEquiv.symm_apply_apply, polynomialQuotientEquivQuotientPolynomial_symm_mk]

Isomorphism Maps Reduced Polynomial to Equivalence Class

Informal description

Let $R$ be a commutative ring and $I$ an ideal of $R$. For any polynomial $f \in R[X]$, the image of the polynomial $f \mod I$ (obtained by reducing each coefficient modulo $I$) under the isomorphism $(R/I)[X] \cong R[X]/(C(I))$ is equal to the equivalence class of $f$ in $R[X]/(C(I))$. In symbols: \[ \varphi(f \mod I) = [f] \] where $\varphi$ is the isomorphism $(R/I)[X] \cong R[X]/(C(I))$ and $[f]$ denotes the equivalence class of $f$ in $R[X]/(C(I))$.

Ideal.isDomain_map_C_quotient theorem

{P : Ideal R} (_ : IsPrime P) : IsDomain (R[X] ⧸ (map (C : R →+* R[X]) P : Ideal R[X]))

Full source

/-- If `P` is a prime ideal of `R`, then `R[x]/(P)` is an integral domain. -/
theorem isDomain_map_C_quotient {P : Ideal R} (_ : IsPrime P) :
    IsDomain (R[X]R[X] ⧸ (map (C : R →+* R[X]) P : Ideal R[X])) :=
  MulEquiv.isDomain (Polynomial (R ⧸ P)) (polynomialQuotientEquivQuotientPolynomial P).symm

Quotient of Polynomial Ring by Prime Ideal is an Integral Domain

Informal description

Let $R$ be a commutative ring and $P$ a prime ideal of $R$. Then the quotient ring $R[X]/(P)$ is an integral domain, where $(P)$ denotes the ideal of $R[X]$ generated by the image of $P$ under the canonical embedding $C: R \to R[X]$.

MvPolynomial.quotient_map_C_eq_zero theorem

 {I : Ideal R} {i : R} (hi : i ∈ I) :
  (Ideal.Quotient.mk (Ideal.map (C : R →+* MvPolynomial σ R) I : Ideal (MvPolynomial σ R))).comp C i = 0

Full source

theorem quotient_map_C_eq_zero {I : Ideal R} {i : R} (hi : i ∈ I) :
    (Ideal.Quotient.mk (Ideal.map (C : R →+* MvPolynomial σ R) I :
      Ideal (MvPolynomial σ R))).comp C i = 0 := by
  simp only [Function.comp_apply, RingHom.coe_comp, Ideal.Quotient.eq_zero_iff_mem]
  exact Ideal.mem_map_of_mem _ hi

Vanishing of Canonical Embedding in Quotient Polynomial Ring

Informal description

Let $R$ be a commutative ring, $I$ an ideal of $R$, and $C : R \to R[X_1, \dots, X_n]$ the canonical embedding of $R$ into the polynomial ring in variables $X_1, \dots, X_n$. For any element $i \in I$, the composition of the quotient map $R[X_1, \dots, X_n] \to R[X_1, \dots, X_n]/(C(I))$ with $C$ evaluated at $i$ equals zero, i.e., $\overline{C}(i) = 0$ in $R[X_1, \dots, X_n]/(C(I))$.

MvPolynomial.eval₂_C_mk_eq_zero theorem

 {I : Ideal R} {a : MvPolynomial σ R} (ha : a ∈ (Ideal.map (C : R →+* MvPolynomial σ R) I : Ideal (MvPolynomial σ R))) :
  eval₂Hom (C.comp (Ideal.Quotient.mk I)) X a = 0

Full source

theorem eval₂_C_mk_eq_zero {I : Ideal R} {a : MvPolynomial σ R}
    (ha : a ∈ (Ideal.map (C : R →+* MvPolynomial σ R) I : Ideal (MvPolynomial σ R))) :
    eval₂Hom (C.comp (Ideal.Quotient.mk I)) X a = 0 := by
  rw [as_sum a]
  rw [coe_eval₂Hom, eval₂_sum]
  refine Finset.sum_eq_zero fun n _ => ?_
  simp only [eval₂_monomial, Function.comp_apply, RingHom.coe_comp]
  refine mul_eq_zero_of_left ?_ _
  suffices coeffcoeff n a ∈ I by
    rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this
    simp only [this, C_0]
  exact mem_map_C_iff.1 ha n

Vanishing of Polynomial Evaluation in Quotient Ring

Informal description

Let $R$ be a commutative ring, $I$ an ideal of $R$, and $C : R \to R[X_1, \dots, X_n]$ the canonical embedding of $R$ into the polynomial ring in variables $X_1, \dots, X_n$. For any polynomial $a \in R[X_1, \dots, X_n]$ that belongs to the ideal generated by $C(I)$, the evaluation of $a$ under the homomorphism $\text{eval₂Hom}(C \circ \pi_I, X)$ is zero, where $\pi_I : R \to R/I$ is the quotient map and $X$ denotes the variables.

MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse theorem

 (I : Ideal R) :
  Function.RightInverse
    (eval₂
      (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R))).comp C) fun _ hi =>
        quotient_map_C_eq_zero hi)
      fun i => Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R)) (X i))
    (Ideal.Quotient.lift (Ideal.map C I : Ideal (MvPolynomial σ R)) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X)
      fun _ ha => eval₂_C_mk_eq_zero ha)

Full source

lemma quotientEquivQuotientMvPolynomial_rightInverse (I : Ideal R) :
    Function.RightInverse
      (eval₂ (Ideal.Quotient.lift I
        ((Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R))).comp C)
          fun _ hi => quotient_map_C_eq_zero hi)
          fun i => Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R)) (X i))
      (Ideal.Quotient.lift (Ideal.map C I : Ideal (MvPolynomial σ R))
        (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) fun _ ha => eval₂_C_mk_eq_zero ha) := by
  intro f
  apply induction_on f
  · intro r
    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
    rw [eval₂_C, Ideal.Quotient.lift_mk, RingHom.comp_apply, Ideal.Quotient.lift_mk, eval₂Hom_C,
      RingHom.comp_apply]
  · intros p q hp hq
    simp only [RingHom.map_add, MvPolynomial.coe_eval₂Hom, coe_eval₂Hom, MvPolynomial.eval₂_add]
      at hp hq ⊢
    rw [hp, hq]
  · intros p i hp
    simp only [coe_eval₂Hom] at hp
    simp only [hp, coe_eval₂Hom, Ideal.Quotient.lift_mk, eval₂_mul, RingHom.map_mul, eval₂_X]

Right Inverse Property of Polynomial Evaluation in Quotient Rings

Informal description

Let $R$ be a commutative ring and $I$ an ideal of $R$. The evaluation map \[ \text{eval}_2 \left( \text{lift}_I \left( \pi_{C(I)} \circ C \right) \right) \left( \lambda i, \pi_{C(I)}(X_i) \right) \] is a right inverse of the lifted homomorphism \[ \text{lift}_{C(I)} \left( \text{eval}_2 (C \circ \pi_I) (X) \right), \] where: - $C : R \to R[X_1, \dots, X_n]$ is the canonical embedding, - $\pi_I : R \to R/I$ and $\pi_{C(I)} : R[X_1, \dots, X_n] \to R[X_1, \dots, X_n]/C(I)$ are the quotient maps, - $\text{lift}_I$ and $\text{lift}_{C(I)}$ are the lifting homomorphisms induced by the respective quotient maps, - $\text{eval}_2$ denotes the evaluation of polynomials at given ring homomorphisms and variable assignments.

MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse theorem

 (I : Ideal R) :
  Function.LeftInverse
    (eval₂
      (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R))).comp C) fun _ hi =>
        quotient_map_C_eq_zero hi)
      fun i => Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R)) (X i))
    (Ideal.Quotient.lift (Ideal.map C I : Ideal (MvPolynomial σ R)) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X)
      fun _ ha => eval₂_C_mk_eq_zero ha)

Full source

lemma quotientEquivQuotientMvPolynomial_leftInverse (I : Ideal R) :
    Function.LeftInverse
      (eval₂ (Ideal.Quotient.lift I
        ((Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R))).comp C)
          fun _ hi => quotient_map_C_eq_zero hi)
          fun i => Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R)) (X i))
      (Ideal.Quotient.lift (Ideal.map C I : Ideal (MvPolynomial σ R))
        (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) fun _ ha => eval₂_C_mk_eq_zero ha) := by
  intro f
  obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
  apply induction_on f
  · intro r
    rw [Ideal.Quotient.lift_mk, eval₂Hom_C, RingHom.comp_apply, eval₂_C, Ideal.Quotient.lift_mk,
      RingHom.comp_apply]
  · intros p q hp hq
    rw [Ideal.Quotient.lift_mk] at hp hq ⊢
    simp only [Submodule.Quotient.quot_mk_eq_mk, eval₂_add, RingHom.map_add, coe_eval₂Hom,
      Ideal.Quotient.lift_mk, Ideal.Quotient.mk_eq_mk] at hp hq ⊢
    rw [hp, hq]
  · intros p i hp
    simp only [Submodule.Quotient.quot_mk_eq_mk, coe_eval₂Hom, Ideal.Quotient.lift_mk,
      Ideal.Quotient.mk_eq_mk, eval₂_mul, RingHom.map_mul, eval₂_X] at hp ⊢
    simp only [hp]

Left Inverse Property of Polynomial Evaluation in Quotient Rings

Informal description

Let $R$ be a commutative ring and $I$ an ideal of $R$. The composition of the evaluation homomorphism $\text{eval}_2$ with the lifted quotient map $\text{lift}(I, \pi \circ C, H)$, where $\pi : R[X_1, \dots, X_n] \to R[X_1, \dots, X_n]/(C(I))$ is the quotient map and $C : R \to R[X_1, \dots, X_n]$ is the canonical embedding, is a left inverse to the lifted evaluation homomorphism $\text{lift}(C(I), \text{eval}_2(C \circ \pi_I, X), H')$ on the quotient ring $R[X_1, \dots, X_n]/(C(I))$.

MvPolynomial.quotientEquivQuotientMvPolynomial definition

(I : Ideal R) : MvPolynomial σ (R ⧸ I) ≃ₐ[R] MvPolynomial σ R ⧸ (Ideal.map C I : Ideal (MvPolynomial σ R))

Full source

/-- If `I` is an ideal of `R`, then the ring `MvPolynomial σ I.quotient` is isomorphic as an
`R`-algebra to the quotient of `MvPolynomial σ R` by the ideal generated by `I`. -/
noncomputable def quotientEquivQuotientMvPolynomial (I : Ideal R) :
    MvPolynomialMvPolynomial σ (R ⧸ I) ≃ₐ[R] MvPolynomial σ R ⧸ (Ideal.map C I : Ideal (MvPolynomial σ R)) :=
  let e : MvPolynomialMvPolynomial σ (R ⧸ I) →ₐ[R]
      MvPolynomial σ R ⧸ (Ideal.map C I : Ideal (MvPolynomial σ R)) :=
    { eval₂Hom
      (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R))).comp C)
        fun _ hi => quotient_map_C_eq_zero hi)
      fun i => Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R)) (X i) with
      commutes' := fun r => eval₂Hom_C _ _ (Ideal.Quotient.mk I r) }
  { e with
    invFun := Ideal.Quotient.lift (Ideal.map C I : Ideal (MvPolynomial σ R))
      (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) fun _ ha => eval₂_C_mk_eq_zero ha
    left_inv := quotientEquivQuotientMvPolynomial_rightInverse I
    right_inv := quotientEquivQuotientMvPolynomial_leftInverse I }

Isomorphism between Polynomial Ring over Quotient and Quotient of Polynomial Ring

Informal description

For a commutative ring $R$ and an ideal $I$ of $R$, there is an $R$-algebra isomorphism between the polynomial ring $\text{MvPolynomial}\,\sigma\,(R/I)$ and the quotient of the polynomial ring $\text{MvPolynomial}\,\sigma\,R$ by the ideal generated by $I$ under the canonical embedding $C : R \to \text{MvPolynomial}\,\sigma\,R$. More precisely, the isomorphism is given by: \[ \text{MvPolynomial}\,\sigma\,(R/I) \simeq \text{MvPolynomial}\,\sigma\,R \big/ \langle C(I) \rangle \] where $\langle C(I) \rangle$ denotes the ideal generated by the image of $I$ under $C$.