English
Let R and S be commutative rings, with S an integral domain, and φ: R →+* S injective. If f ∈ R[X] is primitive (i.e., its content is a unit in R), then f is a unit of R[X] if and only if its image under map φ, namely map φ f ∈ S[X], is a unit of S[X].
Русский
Пусть R, S — коммутативные кольца, S — интегрально домен, φ: R →+* S инъективно. Пусть f ∈ R[X] примитивен (содержимое содержится в модуле единицы). Тогда f является единицей в R[X] тогда и только тогда, когда образ map φ f является единицей в S[X].
LaTeX
$$$\\text{IsUnit}(f) \\iff \\text{IsUnit}(\\mathrm{map}_\\varphi f)$$$
Lean4
theorem isUnit_iff_isUnit_map_of_injective : IsUnit f ↔ IsUnit (map φ f) :=
by
refine ⟨(mapRingHom φ).isUnit_map, fun h => ?_⟩
rcases isUnit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩
have hdeg := degree_C u.ne_zero
rw [hu, degree_map_eq_of_injective hinj] at hdeg
rw [eq_C_of_degree_eq_zero hdeg] at hf ⊢
exact isUnit_C.mpr (isPrimitive_iff_isUnit_of_C_dvd.mp hf (f.coeff 0) dvd_rfl)
