IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Monoid_ZF imports func_ZF Loop_ZF Semigroup_ZF
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_def

The 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_funtype

There 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_def

The 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
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
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_domain

In 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
note A1
ultimately have \( n = e \) by (rule the_equality2 )
then show \( thesis \) using TheNeutralElement_def
qed

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
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
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
have \( \forall x\in H.\ \forall y\in H.\ \forall z\in H.\ x\oplus y\oplus z = x\oplus (y\oplus z) \)proof
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
moreover
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 \)
qed
moreover
have \( \exists n\in H.\ (\forall h\in H.\ g\langle n,h\rangle = h \wedge g\langle h,n\rangle = h) \)proof
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
ultimately show \( thesis \) using IsAmonoid_def, IsAssociative_def
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
have \( e \in H \wedge (\forall h\in H.\ g\langle e,h\rangle = h \wedge g\langle h,e\rangle = h) \)proof
{
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
ultimately have \( e = \text{ TheNeutralElement}(H,g) \) by (rule group0_1_L4 )
thus \( thesis \)
qed

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_neutral

The 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_def

A 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 \)