English
Let I be an ideal in the multivariate polynomial ring MvPolynomial σ K over a field K, with I ≠ ⊤. The composite map from K via the canonical embedding C into MvPolynomial, followed by the quotient map by I, is injective.
Русский
Пусть I — идеал в многочленной системе MvPolynomial σ K над полем K, и I ≠ ⊤. Составной отображение из K через естественное вложение C в MvPolynomial, затем в фактор-модуль по I, инъективно.
LaTeX
$$$\\text{Injective}\\bigl( (\\text{Ideal.Quotient.mk } I) \\circ \\text{MvPolynomial.C} \\bigr)\\,,$$$
Lean4
theorem quotient_mk_comp_C_injective [Field K] (I : Ideal (MvPolynomial σ K)) (hI : I ≠ ⊤) :
Function.Injective ((Ideal.Quotient.mk I).comp MvPolynomial.C) :=
by
refine (injective_iff_map_eq_zero _).2 fun x hx => ?_
rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem] at hx
refine _root_.by_contradiction fun hx0 => absurd (I.eq_top_iff_one.2 ?_) hI
have := I.mul_mem_left (MvPolynomial.C x⁻¹) hx
rwa [← MvPolynomial.C.map_mul, inv_mul_cancel₀ hx0, MvPolynomial.C_1] at this
