Data.Semigroup.Property

Required properties of semigroups

associative_addition_on :: (Additive - Semigroup) r => Rel r b -> r -> r -> r -> b

\( \forall a, b, c \in R: (a + b) + c \sim a + (b + c) \)

All semigroups must right-associate addition.

This is a required property.

associative_multiplication_on :: (Multiplicative - Semigroup) r => Rel r b -> r -> r -> r -> b

\( \forall a, b, c \in R: (a * b) * c \sim a * (b * c) \)

All semigroups must right-associate multiplication.

This is a required property.

Required properties of monoids

neutral_addition_on :: (Additive - Monoid) r => Rel r b -> r -> b

\( \forall a \in R: (z + a) \sim a \)

A semigroup with a right-neutral additive identity must satisfy:

neutral_addition zero = const True

Or, equivalently:

zero + r = r

This is a required property for additive monoids.

neutral_multiplication_on :: (Multiplicative - Monoid) r => Rel r b -> r -> b

\( \forall a \in R: (o * a) \sim a \)

A semigroup with a right-neutral multiplicative identity must satisfy:

neutral_multiplication one = const True

Or, equivalently:

one * r = r

This is a required propert for multiplicative monoids.

Properties of commuative semigroups

commutative_addition_on :: (Additive - Semigroup) r => Rel r b -> r -> r -> b

\( \forall a, b \in R: a + b \sim b + a \)

This is a an optional property for semigroups, and a required property for semirings.

commutative_multiplication_on :: (Multiplicative - Semigroup) r => Rel r b -> r -> r -> b

\( \forall a, b \in R: a * b \sim b * a \)

This is a an optional property for semigroups, and a optional property for semirings. It is a required property for rings.

Properties of cancellative semigroups

cancellative_addition_on :: (Additive - Semigroup) r => Rel r Bool -> r -> r -> r -> Bool

\( \forall a, b, c \in R: b + a \sim c + a \Rightarrow b = c \)

If R is right-cancellative wrt addition then for all a the section (a +) is injective.

See https://en.wikipedia.org/wiki/Cancellation_property

cancellative_multiplication_on :: (Multiplicative - Semigroup) r => Rel r Bool -> r -> r -> r -> Bool

\( \forall a, b, c \in R: b * a \sim c * a \Rightarrow b = c \)

If R is right-cancellative wrt multiplication then for all a the section (a *) is injective.

Properties of idempotent semigroups

idempotent_addition_on :: (Additive - Semigroup) r => Rel r b -> r -> b

Idempotency property for additive semigroups.

 idempotent_addition = absorbative_addition one

See https://en.wikipedia.org/wiki/Band_(mathematics).

This is a required property for lattices.

idempotent_multiplication_on :: (Multiplicative - Semigroup) r => Rel r b -> r -> b

Idempotency property for multplicative semigroups.

 idempotent_multiplication = absorbative_multiplication zero

See https://en.wikipedia.org/wiki/Band_(mathematics).

This is a an optional property for semigroups, and a optional property for semirings.

This is a required property for lattices.

Required properties of semigroup & monoid morphisms

morphism_additive_on :: (Additive - Semigroup) r => (Additive - Semigroup) s => Rel s b -> (r -> s) -> r -> r -> b

morphism_multiplicative_on :: (Multiplicative - Semigroup) r => (Multiplicative - Semigroup) s => Rel s b -> (r -> s) -> r -> r -> b

morphism_additive_on' :: (Additive - Monoid) r => (Additive - Monoid) s => Rel s b -> (r -> s) -> b

morphism_multiplicative_on' :: (Multiplicative - Monoid) r => (Multiplicative - Monoid) s => Rel s b -> (r -> s) -> b