quotientEquivQuotientMvPolynomial_leftInverse

English

There is a right inverse map to the MV polynomial quotient isomorphism; the right inverse composed with the forward map yields the identity on the original polynomial ring.

Русский

Существует правый обратный отображение к изоморфизму MV-полиномов; композиция с прямым отображением возвращает исходный полином.

LaTeX

$$$\\text{Right inverse of }\\text{MvPolynomial.quotientEquivQuotientMvPolynomial}$$$

Lean4

/-- Split off from `quotientEquivQuotientMvPolynomial` for speed. -/
theorem 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]
  · intro p q hp hq
    rw [Ideal.Quotient.lift_mk] at hp hq ⊢
    simp only [eval₂_add, RingHom.map_add, coe_eval₂Hom] at hp hq ⊢
    rw [hp, hq]
  · intro p i hp
    simp only [coe_eval₂Hom, Ideal.Quotient.lift_mk, eval₂_mul, RingHom.map_mul, eval₂_X] at hp ⊢
    simp only [hp]

Похожие утверждения