Semigroup division: transitivity and embeddings

• sgDiv_trans — semigroup division is transitive;
• sgDiv_of_injective_monoidHom — an injective monoid homomorphism A →* T shows that A divides T;
• instMulActionPUnit — the trivial monoid acting on the one-point type;
• sgDiv_of_injective_hom — if S divides T and T embeds into W by an injective semigroup homomorphism, then S divides W.

Transitivity and embeddings

theorem LeanPool.KrohnRhodes.sgDiv_trans {S T U : Type u} [Mul S] [Mul T] [Mul U] (hST : SgDiv S T) (hTU : SgDiv T U) : SgDiv S U

SgDiv is transitive.

theorem LeanPool.KrohnRhodes.sgDiv_of_injective_monoidHom {A T : Type u} [Monoid A] [Monoid T] (f : A →* T) (hf : Function.Injective ⇑f) : SgDiv A T

An injective monoid homomorphism f : A →* T exhibits A as a division of T: the subsemigroup MonoidHom.mrange f together with the inverse (via Function.invFun) is a surjective →ₙ* onto A.

Semigroup division along injective homomorphisms

@[instance_reducible]

instance LeanPool.KrohnRhodes.instMulActionPUnit : MulAction PUnit.{u + 1} PUnit.{u + 1}

A trivial one-element monoid acts on a trivial one-element type.

Equations

• LeanPool.KrohnRhodes.instMulActionPUnit = Monoid.toMulAction PUnit.{?u.1 + 1}

theorem LeanPool.KrohnRhodes.sgDiv_of_injective_hom {S T W : Type u} [Mul S] [Mul T] [Mul W] (h : SgDiv S T) (ι : T →ₙ* W) (hι : Function.Injective ⇑ι) : SgDiv S W

If S divides T and there is an injective semigroup homomorphism ι : T →ₙ* W, then S divides W.