Irreducibility pulled back along divisibility-reflecting maps

Mathlib's Irreducible.of_map pulls irreducibility back along a local monoid homomorphism. Comparison maps such as the inclusion of polynomials into restricted or overconvergent power series are not local, but they reflect divisibility by a fixed nonzero element x. In a commutative monoid with zero and left cancellation this already suffices: if f x is irreducible, so is x.

Main results

• Irreducible.of_map_of_dvd: irreducibility of f x implies irreducibility of a nonzero x when f x ∣ f y implies x ∣ y.

theorem Irreducible.of_map_of_dvd {M : Type u_1} {N : Type u_2} {F : Type u_3} [CommMonoidWithZero M] [IsLeftCancelMulZero M] [Monoid N] [FunLike F M N] [MonoidHomClass F M N] {f : F} {x : M} (hx : x ≠ 0) (hdvd : ∀ (y : M), f x ∣ f y → x ∣ y) (h : Irreducible (f x)) : Irreducible x

If a monoid homomorphism f reflects divisibility by a nonzero element x, then x is irreducible whenever f x is. Unlike Irreducible.of_map, f need not be local.