Subsemigroups: definition

This file defines bundled multiplicative and additive subsemigroups.

Main definitions

• Subsemigroup M: the type of bundled subsemigroup of a magma M; the underlying set is given in the carrier field of the structure, and should be accessed through coercion as in (S : Set M).
• AddSubsemigroup M : the type of bundled subsemigroups of an additive magma M.

For each of the following definitions in the Subsemigroup namespace, there is a corresponding definition in the AddSubsemigroup namespace.

• Subsemigroup.copy : copy of a subsemigroup with carrier replaced by a set that is equal but possibly not definitionally equal to the carrier of the original Subsemigroup.

Similarly, for each of these definitions in the MulHom namespace, there is a corresponding definition in the AddHom namespace.

• MulHom.eqLocus f g: the subsemigroup of those x such that f x = g x

Implementation notes

Subsemigroup inclusion is denoted ≤ rather than ⊆, although ∈ is defined as membership of a subsemigroup's underlying set.

Note that Subsemigroup M does not actually require Semigroup M, instead requiring only the weaker Mul M.

This file is designed to have very few dependencies. In particular, it should not use natural numbers.

Tags

subsemigroup, subsemigroups

class MulMemClass (S : Type u_3) (M : outParam (Type u_4)) [Mul M] [SetLike S M] : Prop

MulMemClass S M says S is a type of sets s : Set M that are closed under (*)

• mul_mem {s : S} {a b : M} : a ∈ s → b ∈ s → a * b ∈ s

  A substructure satisfying MulMemClass is closed under multiplication.

class AddMemClass (S : Type u_3) (M : outParam (Type u_4)) [Add M] [SetLike S M] : Prop

AddMemClass S M says S is a type of sets s : Set M that are closed under (+)

• add_mem {s : S} {a b : M} : a ∈ s → b ∈ s → a + b ∈ s

  A substructure satisfying AddMemClass is closed under addition.

structure Subsemigroup (M : Type u_3) [Mul M] : Type u_3

A subsemigroup of a magma M is a subset closed under multiplication.

• carrier : Set M

  The carrier of a subsemigroup.

• mul_mem' {a b : M} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier

  The product of two elements of a subsemigroup belongs to the subsemigroup.

structure AddSubsemigroup (M : Type u_3) [Add M] : Type u_3

An additive subsemigroup of an additive magma M is a subset closed under addition.

• carrier : Set M

  The carrier of an additive subsemigroup.

• add_mem' {a b : M} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier

  The sum of two elements of an additive subsemigroup belongs to the subsemigroup.

instance Subsemigroup.instSetLike {M : Type u_1} [Mul M] : SetLike (Subsemigroup M) M

Equations

• Subsemigroup.instSetLike = { coe := Subsemigroup.carrier, coe_injective' := ⋯ }

instance AddSubsemigroup.instSetLike {M : Type u_1} [Add M] : SetLike (AddSubsemigroup M) M

Equations

• AddSubsemigroup.instSetLike = { coe := AddSubsemigroup.carrier, coe_injective' := ⋯ }

def Subsemigroup.ofClass {S : Type u_3} {M : Type u_4} [Mul M] [SetLike S M] [MulMemClass S M] (s : S) : Subsemigroup M

The actual Subsemigroup obtained from an element of a MulMemClass.

Equations

• Subsemigroup.ofClass s = { carrier := ↑s, mul_mem' := ⋯ }

def AddSubsemigroup.ofClass {S : Type u_3} {M : Type u_4} [Add M] [SetLike S M] [AddMemClass S M] (s : S) : AddSubsemigroup M

The actual AddSubsemigroup obtained from an element of a AddMemClass

Equations

• AddSubsemigroup.ofClass s = { carrier := ↑s, add_mem' := ⋯ }

@[simp]

theorem AddSubsemigroup.coe_ofClass {S : Type u_3} {M : Type u_4} [Add M] [SetLike S M] [AddMemClass S M] (s : S) : ↑(ofClass s) = ↑s

@[simp]

theorem Subsemigroup.coe_ofClass {S : Type u_3} {M : Type u_4} [Mul M] [SetLike S M] [MulMemClass S M] (s : S) : ↑(ofClass s) = ↑s

@[instance 100]

instance Subsemigroup.instCanLiftSetCoeForallForallForallMemForallHMul {M : Type u_1} [Mul M] : CanLift (Set M) (Subsemigroup M) SetLike.coe fun (s : Set M) => ∀ {x y : M}, x ∈ s → y ∈ s → x * y ∈ s

@[instance 100]

instance AddSubsemigroup.instCanLiftSetCoeForallForallForallMemForallHAdd {M : Type u_1} [Add M] : CanLift (Set M) (AddSubsemigroup M) SetLike.coe fun (s : Set M) => ∀ {x y : M}, x ∈ s → y ∈ s → x + y ∈ s

instance Subsemigroup.instMulMemClass {M : Type u_1} [Mul M] : MulMemClass (Subsemigroup M) M

instance AddSubsemigroup.instAddMemClass {M : Type u_1} [Add M] : AddMemClass (AddSubsemigroup M) M

@[simp]

theorem Subsemigroup.mem_carrier {M : Type u_1} [Mul M] {s : Subsemigroup M} {x : M} : x ∈ s.carrier ↔ x ∈ s

@[simp]

theorem AddSubsemigroup.mem_carrier {M : Type u_1} [Add M] {s : AddSubsemigroup M} {x : M} : x ∈ s.carrier ↔ x ∈ s

@[simp]

theorem Subsemigroup.mem_mk {M : Type u_1} [Mul M] {s : Set M} {x : M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) : x ∈ { carrier := s, mul_mem' := h_mul } ↔ x ∈ s

@[simp]

theorem AddSubsemigroup.mem_mk {M : Type u_1} [Add M] {s : Set M} {x : M} (h_add : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) : x ∈ { carrier := s, add_mem' := h_add } ↔ x ∈ s

@[simp]

theorem Subsemigroup.coe_set_mk {M : Type u_1} [Mul M] (s : Set M) (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) : ↑{ carrier := s, mul_mem' := h_mul } = s

@[simp]

theorem AddSubsemigroup.coe_set_mk {M : Type u_1} [Add M] (s : Set M) (h_add : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) : ↑{ carrier := s, add_mem' := h_add } = s

@[simp]

theorem Subsemigroup.mk_le_mk {M : Type u_1} [Mul M] {s t : Set M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) (h_mul' : ∀ {a b : M}, a ∈ t → b ∈ t → a * b ∈ t) : { carrier := s, mul_mem' := h_mul } ≤ { carrier := t, mul_mem' := h_mul' } ↔ s ⊆ t

@[simp]

theorem AddSubsemigroup.mk_le_mk {M : Type u_1} [Add M] {s t : Set M} (h_add : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) (h_add' : ∀ {a b : M}, a ∈ t → b ∈ t → a + b ∈ t) : { carrier := s, add_mem' := h_add } ≤ { carrier := t, add_mem' := h_add' } ↔ s ⊆ t

theorem Subsemigroup.ext {M : Type u_1} [Mul M] {S T : Subsemigroup M} (h : ∀ (x : M), x ∈ S ↔ x ∈ T) : S = T

Two subsemigroups are equal if they have the same elements.

theorem AddSubsemigroup.ext {M : Type u_1} [Add M] {S T : AddSubsemigroup M} (h : ∀ (x : M), x ∈ S ↔ x ∈ T) : S = T

Two AddSubsemigroups are equal if they have the same elements.

theorem Subsemigroup.ext_iff {M : Type u_1} [Mul M] {S T : Subsemigroup M} : S = T ↔ ∀ (x : M), x ∈ S ↔ x ∈ T

theorem AddSubsemigroup.ext_iff {M : Type u_1} [Add M] {S T : AddSubsemigroup M} : S = T ↔ ∀ (x : M), x ∈ S ↔ x ∈ T

def Subsemigroup.copy {M : Type u_1} [Mul M] (S : Subsemigroup M) (s : Set M) (hs : s = ↑S) : Subsemigroup M

Copy a subsemigroup replacing carrier with a set that is equal to it.

Equations

• S.copy s hs = { carrier := s, mul_mem' := ⋯ }

def AddSubsemigroup.copy {M : Type u_1} [Add M] (S : AddSubsemigroup M) (s : Set M) (hs : s = ↑S) : AddSubsemigroup M

Copy an additive subsemigroup replacing carrier with a set that is equal to it.

Equations

• S.copy s hs = { carrier := s, add_mem' := ⋯ }

@[simp]

theorem Subsemigroup.coe_copy {M : Type u_1} [Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = ↑S) : ↑(S.copy s hs) = s

@[simp]

theorem AddSubsemigroup.coe_copy {M : Type u_1} [Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = ↑S) : ↑(S.copy s hs) = s

theorem Subsemigroup.copy_eq {M : Type u_1} [Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = ↑S) : S.copy s hs = S

theorem AddSubsemigroup.copy_eq {M : Type u_1} [Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = ↑S) : S.copy s hs = S

theorem Subsemigroup.mul_mem {M : Type u_1} [Mul M] (S : Subsemigroup M) {x y : M} : x ∈ S → y ∈ S → x * y ∈ S

A subsemigroup is closed under multiplication.

theorem AddSubsemigroup.add_mem {M : Type u_1} [Add M] (S : AddSubsemigroup M) {x y : M} : x ∈ S → y ∈ S → x + y ∈ S

An AddSubsemigroup is closed under addition.

instance Subsemigroup.instTop {M : Type u_1} [Mul M] : Top (Subsemigroup M)

The subsemigroup M of the magma M.

Equations

• Subsemigroup.instTop = { top := { carrier := Set.univ, mul_mem' := ⋯ } }

instance AddSubsemigroup.instTop {M : Type u_1} [Add M] : Top (AddSubsemigroup M)

The additive subsemigroup M of the magma M.

Equations

• AddSubsemigroup.instTop = { top := { carrier := Set.univ, add_mem' := ⋯ } }

instance Subsemigroup.instBot {M : Type u_1} [Mul M] : Bot (Subsemigroup M)

The trivial subsemigroup ∅ of a magma M.

Equations

• Subsemigroup.instBot = { bot := { carrier := ∅, mul_mem' := ⋯ } }

instance AddSubsemigroup.instBot {M : Type u_1} [Add M] : Bot (AddSubsemigroup M)

The trivial AddSubsemigroup ∅ of an additive magma M.

Equations

• AddSubsemigroup.instBot = { bot := { carrier := ∅, add_mem' := ⋯ } }

instance Subsemigroup.instInhabited {M : Type u_1} [Mul M] : Inhabited (Subsemigroup M)

Equations

• Subsemigroup.instInhabited = { default := ⊥ }

instance AddSubsemigroup.instInhabited {M : Type u_1} [Add M] : Inhabited (AddSubsemigroup M)

Equations

• AddSubsemigroup.instInhabited = { default := ⊥ }

theorem Subsemigroup.notMem_bot {M : Type u_1} [Mul M] {x : M} : x ∉ ⊥

theorem AddSubsemigroup.notMem_bot {M : Type u_1} [Add M] {x : M} : x ∉ ⊥

@[deprecated AddSubsemigroup.notMem_bot (since := "2025-05-23")]

theorem AddSubsemigroup.not_mem_bot {M : Type u_1} [Add M] {x : M} : x ∉ ⊥

Alias of AddSubsemigroup.notMem_bot.

@[deprecated Subsemigroup.notMem_bot (since := "2025-05-23")]

theorem Subsemigroup.not_mem_bot {M : Type u_1} [Mul M] {x : M} : x ∉ ⊥

Alias of Subsemigroup.notMem_bot.

@[simp]

theorem Subsemigroup.mem_top {M : Type u_1} [Mul M] (x : M) : x ∈ ⊤

@[simp]

theorem AddSubsemigroup.mem_top {M : Type u_1} [Add M] (x : M) : x ∈ ⊤

@[simp]

theorem Subsemigroup.coe_top {M : Type u_1} [Mul M] : ↑⊤ = Set.univ

@[simp]

theorem AddSubsemigroup.coe_top {M : Type u_1} [Add M] : ↑⊤ = Set.univ

@[simp]

theorem Subsemigroup.coe_bot {M : Type u_1} [Mul M] : ↑⊥ = ∅

@[simp]

theorem AddSubsemigroup.coe_bot {M : Type u_1} [Add M] : ↑⊥ = ∅

instance Subsemigroup.instMin {M : Type u_1} [Mul M] : Min (Subsemigroup M)

The inf of two subsemigroups is their intersection.

Equations

• Subsemigroup.instMin = { min := fun (S₁ S₂ : Subsemigroup M) => { carrier := ↑S₁ ∩ ↑S₂, mul_mem' := ⋯ } }

instance AddSubsemigroup.instMin {M : Type u_1} [Add M] : Min (AddSubsemigroup M)

The inf of two AddSubsemigroups is their intersection.

Equations

• AddSubsemigroup.instMin = { min := fun (S₁ S₂ : AddSubsemigroup M) => { carrier := ↑S₁ ∩ ↑S₂, add_mem' := ⋯ } }

@[simp]

theorem Subsemigroup.coe_inf {M : Type u_1} [Mul M] (p p' : Subsemigroup M) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem AddSubsemigroup.coe_inf {M : Type u_1} [Add M] (p p' : AddSubsemigroup M) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem Subsemigroup.mem_inf {M : Type u_1} [Mul M] {p p' : Subsemigroup M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

@[simp]

theorem AddSubsemigroup.mem_inf {M : Type u_1} [Add M] {p p' : AddSubsemigroup M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

theorem Subsemigroup.subsingleton_of_subsingleton {M : Type u_1} [Mul M] [Subsingleton (Subsemigroup M)] : Subsingleton M

theorem AddSubsemigroup.subsingleton_of_subsingleton {M : Type u_1} [Add M] [Subsingleton (AddSubsemigroup M)] : Subsingleton M

instance Subsemigroup.instNontrivialOfNonempty {M : Type u_1} [Mul M] [hn : Nonempty M] : Nontrivial (Subsemigroup M)

instance AddSubsemigroup.instNontrivialOfNonempty {M : Type u_1} [Add M] [hn : Nonempty M] : Nontrivial (AddSubsemigroup M)

def MulHom.eqLocus {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f g : M →ₙ* N) : Subsemigroup M

The subsemigroup of elements x : M such that f x = g x

Equations

• f.eqLocus g = { carrier := {x : M | f x = g x}, mul_mem' := ⋯ }

def AddHom.eqLocus {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f g : M →ₙ+ N) : AddSubsemigroup M

The additive subsemigroup of elements x : M such that f x = g x

Equations

• f.eqLocus g = { carrier := {x : M | f x = g x}, add_mem' := ⋯ }

@[simp]

theorem MulHom.mem_eqLocus {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f g : M →ₙ* N} {x : M} : x ∈ f.eqLocus g ↔ f x = g x

@[simp]

theorem AddHom.mem_eqLocus {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f g : M →ₙ+ N} {x : M} : x ∈ f.eqLocus g ↔ f x = g x

theorem MulHom.eq_of_eqOn_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f g : M →ₙ* N} (h : Set.EqOn ⇑f ⇑g ↑⊤) : f = g

theorem AddHom.eq_of_eqOn_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f g : M →ₙ+ N} (h : Set.EqOn ⇑f ⇑g ↑⊤) : f = g

@[instance 900]

instance MulMemClass.mul {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) : Mul ↥S'

A submagma of a magma inherits a multiplication.

Equations

• MulMemClass.mul S' = { mul := fun (a b : ↥S') => ⟨↑a * ↑b, ⋯⟩ }

@[instance 900]

instance AddMemClass.add {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) : Add ↥S'

An additive submagma of an additive magma inherits an addition.

Equations

• AddMemClass.add S' = { add := fun (a b : ↥S') => ⟨↑a + ↑b, ⋯⟩ }

@[simp]

theorem MulMemClass.coe_mul {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) (x y : ↥S') : ↑(x * y) = ↑x * ↑y

@[simp]

theorem AddMemClass.coe_add {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x y : ↥S') : ↑(x + y) = ↑x + ↑y

@[simp]

theorem MulMemClass.mk_mul_mk {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) (x y : M) (hx : x ∈ S') (hy : y ∈ S') : ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩

@[simp]

theorem AddMemClass.mk_add_mk {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x y : M) (hx : x ∈ S') (hy : y ∈ S') : ⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩

theorem MulMemClass.mul_def {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) (x y : ↥S') : x * y = ⟨↑x * ↑y, ⋯⟩

theorem AddMemClass.add_def {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x y : ↥S') : x + y = ⟨↑x + ↑y, ⋯⟩

instance MulMemClass.toSemigroup {M : Type u_4} [Semigroup M] {A : Type u_5} [SetLike A M] [MulMemClass A M] (S : A) : Semigroup ↥S

A subsemigroup of a semigroup inherits a semigroup structure.

Equations

• MulMemClass.toSemigroup S = { toMul := MulMemClass.mul S, mul_assoc := ⋯ }

instance AddMemClass.toAddSemigroup {M : Type u_4} [AddSemigroup M] {A : Type u_5} [SetLike A M] [AddMemClass A M] (S : A) : AddSemigroup ↥S

An AddSubsemigroup of an AddSemigroup inherits an AddSemigroup structure.

Equations

• AddMemClass.toAddSemigroup S = { toAdd := AddMemClass.add S, add_assoc := ⋯ }

instance MulMemClass.toCommSemigroup {M : Type u_5} [CommSemigroup M] {A : Type u_4} [SetLike A M] [MulMemClass A M] (S : A) : CommSemigroup ↥S

A subsemigroup of a CommSemigroup is a CommSemigroup.

Equations

• MulMemClass.toCommSemigroup S = { toSemigroup := MulMemClass.toSemigroup S, mul_comm := ⋯ }

instance AddMemClass.toAddCommSemigroup {M : Type u_5} [AddCommSemigroup M] {A : Type u_4} [SetLike A M] [AddMemClass A M] (S : A) : AddCommSemigroup ↥S

An AddSubsemigroup of an AddCommSemigroup is an AddCommSemigroup.

Equations

• AddMemClass.toAddCommSemigroup S = { toAddSemigroup := AddMemClass.toAddSemigroup S, add_comm := ⋯ }

instance MulMemClass.isLeftCancelMul {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] [IsLeftCancelMul M] (S : A) : IsLeftCancelMul ↥S

A submagma of a left cancellative magma inherits left cancellation.

instance AddMemClass.isLeftCancelAdd {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] [IsLeftCancelAdd M] (S : A) : IsLeftCancelAdd ↥S

An additive submagma of a left cancellative additive magma inherits left cancellation.

instance MulMemClass.isRightCancelMul {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] [IsRightCancelMul M] (S : A) : IsRightCancelMul ↥S

A submagma of a right cancellative magma inherits right cancellation.

instance AddMemClass.isRightCancelAdd {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] [IsRightCancelAdd M] (S : A) : IsRightCancelAdd ↥S

An additive submagma of a right cancellative additive magma inherits right cancellation.

instance MulMemClass.isCancelMul {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] [IsCancelMul M] (S : A) : IsCancelMul ↥S

A submagma of a cancellative magma inherits cancellation.

instance AddMemClass.isCancelAdd {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] [IsCancelAdd M] (S : A) : IsCancelAdd ↥S

An additive submagma of a cancellative additive magma inherits cancellation.

def MulMemClass.subtype {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) : ↥S' →ₙ* M

The natural semigroup hom from a subsemigroup of semigroup M to M.

Equations

• MulMemClass.subtype S' = { toFun := Subtype.val, map_mul' := ⋯ }

def AddMemClass.subtype {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) : ↥S' →ₙ+ M

The natural semigroup hom from an AddSubsemigroup of AddSubsemigroup M to M.

Equations

• AddMemClass.subtype S' = { toFun := Subtype.val, map_add' := ⋯ }

@[simp]

theorem MulMemClass.subtype_apply {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] {S' : A} (x : ↥S') : (subtype S') x = ↑x

@[simp]

theorem AddMemClass.subtype_apply {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] {S' : A} (x : ↥S') : (subtype S') x = ↑x

theorem MulMemClass.subtype_injective {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) : Function.Injective ⇑(subtype S')

theorem AddMemClass.subtype_injective {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) : Function.Injective ⇑(subtype S')

@[simp]

theorem MulMemClass.coe_subtype {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) : ⇑(subtype S') = Subtype.val

@[simp]

theorem AddMemClass.coe_subtype {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) : ⇑(subtype S') = Subtype.val