begin
This theory provides basic facts about monoids.
Definition and basic properties
In this section we talk about monoids. The notion of a monoid is similar to the notion of a semigroup except that we require the existence of a neutral element. It is also similar to the notion of group except that we don't require existence of the inverse.
Monoid is a set \(G\) with an associative operation and a neutral element. The operation is a function on \(G\times G\) with values in \(G\). In the context of ZF set theory this means that it is a set of pairs \(\langle x,y \rangle\), where \(x\in G\times G\) and \(y\in G\). In other words the operation is a certain subset of \((G\times G)\times G\). We express all this by defing a predicate \( \text{IsAmonoid}(G,f) \). Here \(G\) is the ''carrier'' of the monoid and \(f\) is the binary operation on it.
definition
\( \text{IsAmonoid}(G,f) \equiv \) \( f \text{ is associative on } G \wedge \) \( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)
The next locale called ''monoid0'' defines a context for theorems that concern monoids. In this contex we assume that the pair \((G,f)\) is a monoid. We will use the \( \oplus \) symbol to denote the monoid operation (for no particular reason).
locale monoid0
assumes monoidAssum: \( \text{IsAmonoid}(G,f) \)
defines \( a \oplus b \equiv f\langle a,b\rangle \)
Propositions proven in the semigr0 locale are valid in the monoid0 locale.
lemma (in monoid0) semigr0_valid_in_monoid0:
shows \( semigr0(G,f) \) using monoidAssum, IsAmonoid_def, semigr0_defThe result of the monoid operation is in the monoid (carrier).
lemma (in monoid0) group0_1_L1:
assumes \( a\in G \), \( b\in G \)
shows \( a\oplus b \in G \) using assms, monoidAssum, IsAmonoid_def, IsAssociative_def, apply_funtypeThere is only one neutral element in a monoid.
lemma (in monoid0) group0_1_L2:
shows \( \exists !e.\ e\in G \wedge (\forall g\in G.\ ( (e\oplus g = g) \wedge g\oplus e = g)) \)proof fix \( e \) \( y \)
assume \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \) and \( y \in G \wedge (\forall g\in G.\ y \oplus g = g \wedge g \oplus y = g) \)
then have \( y\oplus e = y \), \( y\oplus e = e \)
thus \( e = y \)
next
from monoidAssum show \( \exists e.\ e\in G \wedge (\forall g\in G.\ e\oplus g = g \wedge g\oplus e = g) \) using IsAmonoid_def
qed
The neutral element is neutral.
lemma (in monoid0) unit_is_neutral:
assumes A1: \( e = \text{ TheNeutralElement}(G,f) \)
shows \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \)proof let \( n = \text{The } b.\ b\in G \wedge (\forall g\in G.\ b\oplus g = g \wedge g\oplus b = g) \)
have \( \exists !b.\ b\in G \wedge (\forall g\in G.\ b\oplus g = g \wedge g\oplus b = g) \) using group0_1_L2
then have \( n\in G \wedge (\forall g\in G.\ n\oplus g = g \wedge g\oplus n = g) \) by (rule theI )
with A1 show \( thesis \) using TheNeutralElement_def
qed
The monoid carrier is not empty.
lemma (in monoid0) group0_1_L3A:
shows \( G\neq 0 \)proof have \( \text{ TheNeutralElement}(G,f) \in G \) using unit_is_neutral
thus \( thesis \)
qed
The monoid operation is a binary function on the carrier with values in the carrier.
lemma (in monoid0) monoid_oper_fun:
shows \( f:G\times G\rightarrow G \) using monoidAssum unfolding IsAmonoid_def, IsAssociative_defThe range of the monoid operation is the whole monoid carrier.
lemma (in monoid0) group0_1_L3B:
shows \( \text{range}(f) = G \)proof from monoidAssum have \( f : G\times G\rightarrow G \) using IsAmonoid_def, IsAssociative_def
then show \( \text{range}(f) \subseteq G \) using func1_1_L5B
show \( G \subseteq \text{range}(f) \)proof
qed
fix \( g \)
assume A1: \( g\in G \)
let \( e = \text{ TheNeutralElement}(G,f) \)
from A1 have \( \langle e,g\rangle \in G\times G \), \( g = f\langle e,g\rangle \) using unit_is_neutral
with \( f : G\times G\rightarrow G \) show \( g \in \text{range}(f) \) using func1_1_L5A
qed
Another way to state that the range of the monoid operation is the whole monoid carrier.
lemma (in monoid0) range_carr:
shows \( f(G\times G) = G \) using monoidAssum, IsAmonoid_def, IsAssociative_def, group0_1_L3B, range_image_domainIn a monoid any neutral element is the neutral element.
lemma (in monoid0) group0_1_L4:
assumes A1: \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \)
shows \( e = \text{ TheNeutralElement}(G,f) \)proof let \( n = \text{The } b.\ b\in G \wedge (\forall g\in G.\ b\oplus g = g \wedge g\oplus b = g) \)
have \( \exists !b.\ b\in G \wedge (\forall g\in G.\ b\oplus g = g \wedge g\oplus b = g) \) using group0_1_L2
moreover
qed
note A1
ultimately have \( n = e \) by (rule the_equality2 )
then show \( thesis \) using TheNeutralElement_def
The next lemma shows that if the if we restrict the monoid operation to a subset of \(G\) that contains the neutral element, then the neutral element of the monoid operation is also neutral with the restricted operation.
lemma (in monoid0) group0_1_L5:
assumes A1: \( \forall x\in H.\ \forall y\in H.\ x\oplus y \in H \) and A2: \( H\subseteq G \) and A3: \( e = \text{ TheNeutralElement}(G,f) \) and A4: \( g = \text{restrict}(f,H\times H) \) and A5: \( e\in H \) and A6: \( h\in H \)
shows \( g\langle e,h\rangle = h \wedge g\langle h,e\rangle = h \)proof from A4, A6, A5 have \( g\langle e,h\rangle = e\oplus h \wedge g\langle h,e\rangle = h\oplus e \) using restrict_if
with A3, A4, A6, A2 show \( g\langle e,h\rangle = h \wedge g\langle h,e\rangle = h \) using unit_is_neutral
qed
The next theorem shows that if the monoid operation is closed on a subset of \(G\) then this set is a (sub)monoid (although we do not define this notion). This fact will be useful when we study subgroups.
theorem (in monoid0) group0_1_T1:
assumes A1: \( H \text{ is closed under } f \) and A2: \( H\subseteq G \) and A3: \( \text{ TheNeutralElement}(G,f) \in H \)
shows \( \text{IsAmonoid}(H,\text{restrict}(f,H\times H)) \)proof let \( g = \text{restrict}(f,H\times H) \)
let \( e = \text{ TheNeutralElement}(G,f) \)
from monoidAssum have \( f \in G\times G\rightarrow G \) using IsAmonoid_def, IsAssociative_def
moreover
from A2 have \( H\times H \subseteq G\times G \)
moreover from A1 have \( \forall p \in H\times H.\ f(p) \in H \) using IsOpClosed_def
ultimately have \( g \in H\times H\rightarrow H \) using func1_2_L4
moreover
qed
have \( \forall x\in H.\ \forall y\in H.\ \forall z\in H.\ \)
\( g\langle g\langle x,y\rangle ,z\rangle = g\langle x,g\langle y,z\rangle \rangle \)proof
moreover from A1 have \( \forall x\in H.\ \forall y\in H.\ \forall z\in H.\ \)
\( g\langle g\langle x,y\rangle ,z\rangle = x\oplus y\oplus z \) using IsOpClosed_def, restrict_if
moreover
qed
have \( \forall x\in H.\ \forall y\in H.\ \forall z\in H.\ x\oplus y\oplus z = x\oplus (y\oplus z) \)proof
moreover from monoidAssum have \( \forall x\in G.\ \forall y\in G.\ \forall z\in G.\ x\oplus y\oplus z = x\oplus (y\oplus z) \) using IsAmonoid_def, IsAssociative_def
with A2 show \( thesis \)
qed
from A1 have \( \forall x\in H.\ \forall y\in H.\ \forall z\in H.\ x\oplus (y\oplus z) = g\langle x,g\langle y,z\rangle \rangle \) using IsOpClosed_def, restrict_if
ultimately show \( thesis \)
have \( \exists n\in H.\ (\forall h\in H.\ g\langle n,h\rangle = h \wedge g\langle h,n\rangle = h) \)proof
ultimately show \( thesis \) using IsAmonoid_def, IsAssociative_def
from A1 have \( \forall x\in H.\ \forall y\in H.\ x\oplus y \in H \) using IsOpClosed_def
with A2, A3 have \( \forall h\in H.\ g\langle e,h\rangle = h \wedge g\langle h,e\rangle = h \) using group0_1_L5
with A3 show \( thesis \)
qed
Under the assumptions of group0_1_T1 the neutral element of a submonoid is the same as that of the monoid.
lemma group0_1_L6:
assumes A1: \( \text{IsAmonoid}(G,f) \) and A2: \( H \text{ is closed under } f \) and A3: \( H\subseteq G \) and A4: \( \text{ TheNeutralElement}(G,f) \in H \)
shows \( \text{ TheNeutralElement}(H,\text{restrict}(f,H\times H)) = \text{ TheNeutralElement}(G,f) \)proof let \( e = \text{ TheNeutralElement}(G,f) \)
let \( g = \text{restrict}(f,H\times H) \)
from assms have \( monoid0(H,g) \) using monoid0_def, group0_1_T1
moreover
qed
have \( e \in H \wedge (\forall h\in H.\ g\langle e,h\rangle = h \wedge g\langle h,e\rangle = h) \)proof
ultimately have \( e = \text{ TheNeutralElement}(H,g) \) by (rule group0_1_L4 )
{
}
fix \( h \)
assume \( h \in H \)
with assms have \( monoid0(G,f) \), \( \forall x\in H.\ \forall y\in H.\ f\langle x,y\rangle \in H \), \( H\subseteq G \), \( e = \text{ TheNeutralElement}(G,f) \), \( g = \text{restrict}(f,H\times H) \), \( e \in H \), \( h \in H \) using monoid0_def, IsOpClosed_def
then have \( g\langle e,h\rangle = h \wedge g\langle h,e\rangle = h \) by (rule group0_1_L5 )
hence \( \forall h\in H.\ g\langle e,h\rangle = h \wedge g\langle h,e\rangle = h \)
with A4 show \( thesis \)
qed
thus \( thesis \)
If a sum of two elements is not zero, then at least one has to be nonzero.
lemma (in monoid0) sum_nonzero_elmnt_nonzero:
assumes \( a \oplus b \neq \text{ TheNeutralElement}(G,f) \)
shows \( a \neq \text{ TheNeutralElement}(G,f) \vee b \neq \text{ TheNeutralElement}(G,f) \) using assms, unit_is_neutralThe monoid operation is associative.
lemma (in monoid0) sum_associative:
assumes \( a\in G \), \( b\in G \), \( c\in G \)
shows \( (a\oplus b)\oplus c = a\oplus (b\oplus c) \) using assms, monoidAssum unfolding IsAmonoid_def, IsAssociative_defA simple rearrangement of four monoid elements transferred from the semigr0 locale:
lemma (in monoid0) rearr4elem_monoid:
assumes \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)
shows \( a\oplus b\oplus (c\oplus d) = a\oplus (b\oplus c)\oplus d \) using assms, semigr0_valid_in_monoid0, rearr4elem_assoc end
Definition of IsAmonoid:
\( \text{IsAmonoid}(G,f) \equiv \)
\( f \text{ is associative on } G \wedge \)
\( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)
Definition of IsAssociative:
\( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \)
\( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \)
\( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)
lemma (in monoid0) group0_1_L2: shows \( \exists !e.\ e\in G \wedge (\forall g\in G.\ ( (e\oplus g = g) \wedge g\oplus e = g)) \)
Definition of TheNeutralElement:
\( \text{ TheNeutralElement}(G,f) \equiv \)
\( ( \text{The } e.\ e\in G \wedge (\forall g\in G.\ f\langle e,g\rangle = g \wedge f\langle g,e\rangle = g)) \)
lemma (in monoid0) unit_is_neutral:
assumes \( e = \text{ TheNeutralElement}(G,f) \)
shows \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \) lemma func1_1_L5B:
assumes \( f:X\rightarrow Y \)
shows \( \text{range}(f) \subseteq Y \) lemma func1_1_L5A:
assumes \( f:X\rightarrow Y \), \( x\in X \), \( y = f(x) \)
shows \( \langle x,y\rangle \in f \), \( y \in \text{range}(f) \) lemma (in monoid0) group0_1_L3B: shows \( \text{range}(f) = G \)
lemma range_image_domain:
assumes \( f:X\rightarrow Y \)
shows \( f(X) = \text{range}(f) \)Definition of IsOpClosed:
\( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
lemma func1_2_L4:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall x\in A.\ f(x) \in Z \)
shows \( \text{restrict}(f,A) : A\rightarrow Z \) lemma (in monoid0) group0_1_L5:
assumes \( \forall x\in H.\ \forall y\in H.\ x\oplus y \in H \) and \( H\subseteq G \) and \( e = \text{ TheNeutralElement}(G,f) \) and \( g = \text{restrict}(f,H\times H) \) and \( e\in H \) and \( h\in H \)
shows \( g\langle e,h\rangle = h \wedge g\langle h,e\rangle = h \) theorem (in monoid0) group0_1_T1:
assumes \( H \text{ is closed under } f \) and \( H\subseteq G \) and \( \text{ TheNeutralElement}(G,f) \in H \)
shows \( \text{IsAmonoid}(H,\text{restrict}(f,H\times H)) \) lemma (in monoid0) group0_1_L4:
assumes \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \)
shows \( e = \text{ TheNeutralElement}(G,f) \) lemma (in monoid0) semigr0_valid_in_monoid0: shows \( semigr0(G,f) \)
lemma (in semigr0) rearr4elem_assoc:
assumes \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)
shows \( a\cdot b\cdot (c\cdot d) = a\cdot (b\cdot c)\cdot d \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8