irreducible_of_irreducible_map_of_injective

English

Let φ: R →+* S be an injective ring homomorphism with R, S commutative rings, and f ∈ R[X] primitive. If map φ f is irreducible in S[X], then f is irreducible in R[X].

Русский

Пусть φ: R →+* S — инъективное кольцевое отображение, R, S — коммутативные кольца, f ∈ R[X] примитивен. Если map φ f неприводен в S[X], то и в R[X] f неприводим.

LaTeX

$$$\\text{Irreducible}(\\mathrm{map}_\\varphi f) \\Rightarrow \\text{Irreducible}(f)$$$

Lean4

theorem irreducible_of_irreducible_map_of_injective (h_irr : Irreducible (map φ f)) : Irreducible f :=
  by
  refine
    ⟨fun h => h_irr.not_isUnit (IsUnit.map (mapRingHom φ) h), fun a b h =>
      (h_irr.isUnit_or_isUnit <| by rw [h, Polynomial.map_mul]).imp ?_ ?_⟩
  all_goals apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr
  exacts [Dvd.intro _ h.symm, Dvd.intro_left _ h.symm]

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