English
The MV polynomial quotient isomorphism admits a right inverse mapping defined by the quotient lift and eval₂Hom.
Русский
Изоморфизм MV-полиномов допускает правое обратное отображение, задаваемое поднятием по квотированию и eval₂Hom.
LaTeX
$$$\\text{Right inverse of MVPolynomial quotient}$$$
Lean4
/-- 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) :
MvPolynomial σ (R ⧸ I) ≃ₐ[R] MvPolynomial σ R ⧸ (Ideal.map C I : Ideal (MvPolynomial σ R)) :=
let e : MvPolynomial σ (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 }
