Theorems · Theorem · group theory

Irreducible.map

∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] {x : M} [inst_2 : EquivLike F M N]
  [MulEquivClass F M N] (f : F), Irreducible x → Irreducible (f x)

Irreducibility is preserved by multiplicative equivalences. Note that surjective + local hom is not enough. Consider the additive monoids M = ℕ ⊕ ℕ, N = ℕ, with x surjective local (additive) hom f : M →+ N sending (m, n) to 2m + n. It is local because the only add unit in N is 0, with preimage {(0, 0)} also an add unit. Then x = (1, 0) is irreducible in M, but f x = 2 = 1 + 1 is not irreducible in N.

Defined in

Mathlib.Algebra.Group.Irreducible.Lemmas

Cited by

1 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Quot.sound

Assumes

MonoidMonoidEquivLikeMulEquivClass