Semigroups and algebraic structures without identities

This file defines additive and multiplicative semigroups and related structures that do not require a distinguished one or zero. This includes cancellation and commutativity mixins and their basic supporting lemmas and instances.

class IsLeftCancelMul (G : Type u_2) [Mul G] : Prop

A mixin for left cancellative multiplication.

• mul_left_cancel (a : G) : IsLeftRegular a

  Multiplication is left cancellative (i.e. left regular).

theorem isLeftCancelMul_iff (G : Type u_2) [Mul G] : IsLeftCancelMul G ↔ ∀ (a : G), IsLeftRegular a

class IsRightCancelMul (G : Type u_2) [Mul G] : Prop

A mixin for right cancellative multiplication.

• mul_right_cancel (a : G) : IsRightRegular a

  Multiplication is right cancellative (i.e. right regular).

theorem isRightCancelMul_iff (G : Type u_2) [Mul G] : IsRightCancelMul G ↔ ∀ (a : G), IsRightRegular a

class IsCancelMul (G : Type u_2) [Mul G] extends IsLeftCancelMul G, IsRightCancelMul G : Prop

A mixin for cancellative multiplication.

• mul_left_cancel (a : G) : IsLeftRegular a
• mul_right_cancel (a : G) : IsRightRegular a

theorem isCancelMul_iff (G : Type u_2) [Mul G] : IsCancelMul G ↔ IsLeftCancelMul G ∧ IsRightCancelMul G

class IsLeftCancelAdd (G : Type u_2) [Add G] : Prop

A mixin for left cancellative addition.

• add_left_cancel (a : G) : IsAddLeftRegular a

  Addition is left cancellative (i.e. left regular).

theorem isLeftCancelAdd_iff (G : Type u_2) [Add G] : IsLeftCancelAdd G ↔ ∀ (a : G), IsAddLeftRegular a

class IsRightCancelAdd (G : Type u_2) [Add G] : Prop

A mixin for right cancellative addition.

• add_right_cancel (a : G) : IsAddRightRegular a

  Addition is right cancellative (i.e. right regular).

theorem isRightCancelAdd_iff (G : Type u_2) [Add G] : IsRightCancelAdd G ↔ ∀ (a : G), IsAddRightRegular a

class IsCancelAdd (G : Type u_2) [Add G] extends IsLeftCancelAdd G, IsRightCancelAdd G : Prop

A mixin for cancellative addition.

• add_left_cancel (a : G) : IsAddLeftRegular a
• add_right_cancel (a : G) : IsAddRightRegular a

theorem isCancelAdd_iff (G : Type u_2) [Add G] : IsCancelAdd G ↔ IsLeftCancelAdd G ∧ IsRightCancelAdd G

theorem isCancelMul_iff_forall_isRegular {R : Type u_2} [Mul R] : IsCancelMul R ↔ ∀ (r : R), IsRegular r

theorem isCancelAdd_iff_forall_isAddRegular {R : Type u_2} [Add R] : IsCancelAdd R ↔ ∀ (r : R), IsAddRegular r

theorem IsLeftRegular.all {R : Type u_2} [Mul R] [IsLeftCancelMul R] (g : R) : IsLeftRegular g

If all multiplications cancel on the left then every element is left-regular.

theorem IsAddLeftRegular.all {R : Type u_2} [Add R] [IsLeftCancelAdd R] (g : R) : IsAddLeftRegular g

If all additions cancel on the left then every element is add-left-regular.

theorem IsRightRegular.all {R : Type u_2} [Mul R] [IsRightCancelMul R] (g : R) : IsRightRegular g

If all multiplications cancel on the right then every element is right-regular.

theorem IsAddRightRegular.all {R : Type u_2} [Add R] [IsRightCancelAdd R] (g : R) : IsAddRightRegular g

If all additions cancel on the right then every element is add-right-regular.

theorem IsRegular.all {R : Type u_2} [Mul R] [IsCancelMul R] (g : R) : IsRegular g

If all multiplications cancel then every element is regular.

theorem IsAddRegular.all {R : Type u_2} [Add R] [IsCancelAdd R] (g : R) : IsAddRegular g

If all additions cancel then every element is add-regular.

theorem mul_left_cancel {G : Type u_1} [Mul G] [IsLeftCancelMul G] {a b c : G} : a * b = a * c → b = c

theorem add_left_cancel {G : Type u_1} [Add G] [IsLeftCancelAdd G] {a b c : G} : a + b = a + c → b = c

theorem mul_left_cancel_iff {G : Type u_1} [Mul G] [IsLeftCancelMul G] {a b c : G} : a * b = a * c ↔ b = c

theorem add_left_cancel_iff {G : Type u_1} [Add G] [IsLeftCancelAdd G] {a b c : G} : a + b = a + c ↔ b = c

theorem mul_right_injective {G : Type u_1} [Mul G] [IsLeftCancelMul G] (a : G) : Function.Injective fun (x : G) => a * x

theorem add_right_injective {G : Type u_1} [Add G] [IsLeftCancelAdd G] (a : G) : Function.Injective fun (x : G) => a + x

@[simp]

theorem mul_right_inj {G : Type u_1} [Mul G] [IsLeftCancelMul G] (a : G) {b c : G} : a * b = a * c ↔ b = c

@[simp]

theorem add_right_inj {G : Type u_1} [Add G] [IsLeftCancelAdd G] (a : G) {b c : G} : a + b = a + c ↔ b = c

theorem mul_ne_mul_right {G : Type u_1} [Mul G] [IsLeftCancelMul G] (a : G) {b c : G} : a * b ≠ a * c ↔ b ≠ c

theorem add_ne_add_right {G : Type u_1} [Add G] [IsLeftCancelAdd G] (a : G) {b c : G} : a + b ≠ a + c ↔ b ≠ c

theorem mul_right_cancel {G : Type u_1} [Mul G] [IsRightCancelMul G] {a b c : G} : a * b = c * b → a = c

theorem add_right_cancel {G : Type u_1} [Add G] [IsRightCancelAdd G] {a b c : G} : a + b = c + b → a = c

theorem mul_right_cancel_iff {G : Type u_1} [Mul G] [IsRightCancelMul G] {a b c : G} : b * a = c * a ↔ b = c

theorem add_right_cancel_iff {G : Type u_1} [Add G] [IsRightCancelAdd G] {a b c : G} : b + a = c + a ↔ b = c

theorem mul_left_injective {G : Type u_1} [Mul G] [IsRightCancelMul G] (a : G) : Function.Injective fun (x : G) => x * a

theorem add_left_injective {G : Type u_1} [Add G] [IsRightCancelAdd G] (a : G) : Function.Injective fun (x : G) => x + a

@[simp]

theorem mul_left_inj {G : Type u_1} [Mul G] [IsRightCancelMul G] (a : G) {b c : G} : b * a = c * a ↔ b = c

@[simp]

theorem add_left_inj {G : Type u_1} [Add G] [IsRightCancelAdd G] (a : G) {b c : G} : b + a = c + a ↔ b = c

theorem mul_ne_mul_left {G : Type u_1} [Mul G] [IsRightCancelMul G] (a : G) {b c : G} : b * a ≠ c * a ↔ b ≠ c

theorem add_ne_add_left {G : Type u_1} [Add G] [IsRightCancelAdd G] (a : G) {b c : G} : b + a ≠ c + a ↔ b ≠ c

class Semigroup (G : Type u_2) extends Mul G : Type u_2

A semigroup is a type with an associative (*).

• mul : G → G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)

  Multiplication is associative

theorem Semigroup.ext_iff {G : Type u_2} {x y : Semigroup G} : x = y ↔ Mul.mul = Mul.mul

theorem Semigroup.ext {G : Type u_2} {x y : Semigroup G} (mul : Mul.mul = Mul.mul) : x = y

class AddSemigroup (G : Type u_2) extends Add G : Type u_2

An additive semigroup is a type with an associative (+).

• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)

  Addition is associative

theorem AddSemigroup.ext {G : Type u_2} {x y : AddSemigroup G} (add : Add.add = Add.add) : x = y

theorem AddSemigroup.ext_iff {G : Type u_2} {x y : AddSemigroup G} : x = y ↔ Add.add = Add.add

theorem mul_assoc {G : Type u_1} [Semigroup G] (a b c : G) : a * b * c = a * (b * c)

theorem add_assoc {G : Type u_1} [AddSemigroup G] (a b c : G) : a + b + c = a + (b + c)

class IsAddCommutative (M : Type u_2) [Add M] : Prop

A Prop stating that the addition is commutative.

• is_comm : Std.Commutative fun (x1 x2 : M) => x1 + x2

class IsMulCommutative (M : Type u_2) [Mul M] : Prop

A Prop stating that the multiplication is commutative.

• is_comm : Std.Commutative fun (x1 x2 : M) => x1 * x2

theorem isMulCommutative_iff {M : Type u_2} [Mul M] : IsMulCommutative M ↔ ∀ (a b : M), a * b = b * a

theorem isAddCommutative_iff {M : Type u_2} [Add M] : IsAddCommutative M ↔ ∀ (a b : M), a + b = b + a

theorem IsMulCommutative.of_comm {M : Type u_2} [Mul M] : (∀ (a b : M), a * b = b * a) → IsMulCommutative M

Alias of the reverse direction of isMulCommutative_iff.

theorem IsAddCommutative.of_comm {M : Type u_2} [Add M] : (∀ (a b : M), a + b = b + a) → IsAddCommutative M

Alias of the reverse direction of isAddCommutative_iff.

theorem mul_comm' {M : Type u_2} [Mul M] [IsMulCommutative M] (a b : M) : a * b = b * a

An alternative to mul_comm which uses the mixin IsMulCommutative instead of bundled commutative algebraic structures. In general, you should prefer mul_comm unless you are working with commutative subobjects in a noncommutative algebraic structure.

theorem add_comm' {M : Type u_2} [Add M] [IsAddCommutative M] (a b : M) : a + b = b + a

An alternative to add_comm which uses the mixin IsAddCommutative instead of bundled commutative algebraic structures. In general, you should prefer add_comm unless you are working with commutative subobjects in a noncommutative algebraic structure.

class AddCommMagma (G : Type u_2) extends Add G : Type u_2

A commutative additive magma is a type with an addition which commutes.

• add : G → G → G
• add_comm (a b : G) : a + b = b + a

  Addition is commutative in a commutative additive magma.

theorem AddCommMagma.ext {G : Type u_2} {x y : AddCommMagma G} (add : Add.add = Add.add) : x = y

theorem AddCommMagma.ext_iff {G : Type u_2} {x y : AddCommMagma G} : x = y ↔ Add.add = Add.add

class CommMagma (G : Type u_2) extends Mul G : Type u_2

A commutative multiplicative magma is a type with a multiplication which commutes.

• mul : G → G → G
• mul_comm (a b : G) : a * b = b * a

  Multiplication is commutative in a commutative multiplicative magma.

theorem CommMagma.ext_iff {G : Type u_2} {x y : CommMagma G} : x = y ↔ Mul.mul = Mul.mul

theorem CommMagma.ext {G : Type u_2} {x y : CommMagma G} (mul : Mul.mul = Mul.mul) : x = y

class CommSemigroup (G : Type u_2) extends Semigroup G, CommMagma G : Type u_2

A commutative semigroup is a type with an associative commutative (*).

• mul : G → G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)
• mul_comm (a b : G) : a * b = b * a

theorem CommSemigroup.ext_iff {G : Type u_2} {x y : CommSemigroup G} : x = y ↔ Mul.mul = Mul.mul

theorem CommSemigroup.ext {G : Type u_2} {x y : CommSemigroup G} (mul : Mul.mul = Mul.mul) : x = y

class AddCommSemigroup (G : Type u_2) extends AddSemigroup G, AddCommMagma G : Type u_2

A commutative additive semigroup is a type with an associative commutative (+).

• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)
• add_comm (a b : G) : a + b = b + a

theorem AddCommSemigroup.ext {G : Type u_2} {x y : AddCommSemigroup G} (add : Add.add = Add.add) : x = y

theorem AddCommSemigroup.ext_iff {G : Type u_2} {x y : AddCommSemigroup G} : x = y ↔ Add.add = Add.add

theorem mul_comm {G : Type u_1} [CommMagma G] (a b : G) : a * b = b * a

theorem add_comm {G : Type u_1} [AddCommMagma G] (a b : G) : a + b = b + a

instance CommMagma.to_isCommutative {G : Type u_1} [CommMagma G] : IsMulCommutative G

instance AddCommMagma.to_isCommutative {G : Type u_1} [AddCommMagma G] : IsAddCommutative G

@[simp]

theorem isLeftRegular_iff_isRegular {G : Type u_1} [CommMagma G] {a : G} : IsLeftRegular a ↔ IsRegular a

@[simp]

theorem isAddLeftRegular_iff_isAddRegular {G : Type u_1} [AddCommMagma G] {a : G} : IsAddLeftRegular a ↔ IsAddRegular a

@[simp]

theorem isRightRegular_iff_isRegular {G : Type u_1} [CommMagma G] {a : G} : IsRightRegular a ↔ IsRegular a

@[simp]

theorem isAddRightRegular_iff_isAddRegular {G : Type u_1} [AddCommMagma G] {a : G} : IsAddRightRegular a ↔ IsAddRegular a

theorem CommMagma.IsRightCancelMul.toIsLeftCancelMul (G : Type u_2) [CommMagma G] [IsRightCancelMul G] : IsLeftCancelMul G

Any CommMagma G that satisfies IsRightCancelMul G also satisfies IsLeftCancelMul G.

theorem AddCommMagma.IsRightCancelAdd.toIsLeftCancelAdd (G : Type u_2) [AddCommMagma G] [IsRightCancelAdd G] : IsLeftCancelAdd G

Any AddCommMagma G that satisfies IsRightCancelAdd G also satisfies IsLeftCancelAdd G.

theorem CommMagma.IsLeftCancelMul.toIsRightCancelMul (G : Type u_2) [CommMagma G] [IsLeftCancelMul G] : IsRightCancelMul G

Any CommMagma G that satisfies IsLeftCancelMul G also satisfies IsRightCancelMul G.

theorem AddCommMagma.IsLeftCancelAdd.toIsRightCancelAdd (G : Type u_2) [AddCommMagma G] [IsLeftCancelAdd G] : IsRightCancelAdd G

Any AddCommMagma G that satisfies IsLeftCancelAdd G also satisfies IsRightCancelAdd G.

theorem CommMagma.IsLeftCancelMul.toIsCancelMul (G : Type u_2) [CommMagma G] [IsLeftCancelMul G] : IsCancelMul G

Any CommMagma G that satisfies IsLeftCancelMul G also satisfies IsCancelMul G.

theorem AddCommMagma.IsLeftCancelAdd.toIsCancelAdd (G : Type u_2) [AddCommMagma G] [IsLeftCancelAdd G] : IsCancelAdd G

Any AddCommMagma G that satisfies IsLeftCancelAdd G also satisfies IsCancelAdd G.

theorem CommMagma.IsRightCancelMul.toIsCancelMul (G : Type u_2) [CommMagma G] [IsRightCancelMul G] : IsCancelMul G

Any CommMagma G that satisfies IsRightCancelMul G also satisfies IsCancelMul G.

theorem AddCommMagma.IsRightCancelAdd.toIsCancelAdd (G : Type u_2) [AddCommMagma G] [IsRightCancelAdd G] : IsCancelAdd G

Any AddCommMagma G that satisfies IsRightCancelAdd G also satisfies IsCancelAdd G.

class LeftCancelSemigroup (G : Type u_2) extends Semigroup G, IsLeftCancelMul G : Type u_2

A LeftCancelSemigroup is a semigroup such that a * b = a * c implies b = c.

• mul : G → G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)
• mul_left_cancel (a : G) : IsLeftRegular a

theorem LeftCancelSemigroup.ext {G : Type u_2} {x y : LeftCancelSemigroup G} (mul : Mul.mul = Mul.mul) : x = y

theorem LeftCancelSemigroup.ext_iff {G : Type u_2} {x y : LeftCancelSemigroup G} : x = y ↔ Mul.mul = Mul.mul

def LibraryNote.lower_cancel_priority : Batteries.Util.LibraryNote

We lower the priority of inheriting from cancellative structures. This attempts to avoid expensive checks involving bundling and unbundling with the IsDomain class. since IsDomain already depends on Semiring, we can synthesize that one first. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Why.20is.20.60simpNF.60.20complaining.20here.3F

Equations

• LibraryNote.lower_cancel_priority = default

class AddLeftCancelSemigroup (G : Type u_2) extends AddSemigroup G, IsLeftCancelAdd G : Type u_2

An AddLeftCancelSemigroup is an additive semigroup such that a + b = a + c implies b = c.

• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)
• add_left_cancel (a : G) : IsAddLeftRegular a

theorem AddLeftCancelSemigroup.ext {G : Type u_2} {x y : AddLeftCancelSemigroup G} (add : Add.add = Add.add) : x = y

theorem AddLeftCancelSemigroup.ext_iff {G : Type u_2} {x y : AddLeftCancelSemigroup G} : x = y ↔ Add.add = Add.add

class RightCancelSemigroup (G : Type u_2) extends Semigroup G, IsRightCancelMul G : Type u_2

A RightCancelSemigroup is a semigroup such that a * b = c * b implies a = c.

• mul : G → G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)
• mul_right_cancel (a : G) : IsRightRegular a

theorem RightCancelSemigroup.ext {G : Type u_2} {x y : RightCancelSemigroup G} (mul : Mul.mul = Mul.mul) : x = y

theorem RightCancelSemigroup.ext_iff {G : Type u_2} {x y : RightCancelSemigroup G} : x = y ↔ Mul.mul = Mul.mul

class AddRightCancelSemigroup (G : Type u_2) extends AddSemigroup G, IsRightCancelAdd G : Type u_2

An AddRightCancelSemigroup is an additive semigroup such that a + b = c + b implies a = c.

• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)
• add_right_cancel (a : G) : IsAddRightRegular a

theorem AddRightCancelSemigroup.ext {G : Type u_2} {x y : AddRightCancelSemigroup G} (add : Add.add = Add.add) : x = y

theorem AddRightCancelSemigroup.ext_iff {G : Type u_2} {x y : AddRightCancelSemigroup G} : x = y ↔ Add.add = Add.add

We initialize the projections for the semigroup structures for @[simps] here.