quotientEquivQuotientMvPolynomial_rightInverse

English

There is a left inverse map to the quotient equivalence for polynomials with MV variables: the left inverse composed with the forward map yields the identity on the quotient.

Русский

Существует левый обратный отображение к эквивалентности полиномов MV; композиция левого с прямым тривиальна на квотированном кольце.

LaTeX

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

Lean4

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

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