# 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$$