English
If φ is injective on polynomials and hφ is as above, then the induced map RatFunc.map φ hφ is injective.
Русский
Если φ инъективна на многочленах и выполнены условия hφ, то индуцированное отображение RatFunc.map φ hφ инъективно.
LaTeX
$$$\mathrm{Injective}\bigl(\mathrm{map}\,\phi\,\mathrm{h}\phi\bigr)$$$
Lean4
theorem map_injective [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap φ) (hf : Function.Injective φ) :
Function.Injective (map φ hφ) := by
rintro ⟨x⟩ ⟨y⟩ h
induction x using Localization.induction_on
induction y using Localization.induction_on
simpa only [map_apply_ofFractionRing_mk, ofFractionRing_injective.eq_iff, Localization.mk_eq_mk_iff,
Localization.r_iff_exists, mul_cancel_left_coe_nonZeroDivisors, exists_const, ← map_mul, hf.eq_iff] using h
