Theory Monoid_ZF
section ‹Monoids›
theory Monoid_ZF imports func_ZF Loop_ZF Semigroup_ZF
begin
text‹This theory provides basic facts about monoids.›
subsection‹Definition and basic properties›
text‹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.›
text‹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 ‹IsAmonoid(G,f)›. Here $G$ is the
''carrier'' of the monoid and $f$ is the binary operation on it.
›
definition
"IsAmonoid(G,f) ≡
f {is associative on} G ∧
(∃e∈G. (∀g∈G. ( (f`(⟨e,g⟩) = g) ∧ (f`(⟨g,e⟩) = g))))"
text‹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 ‹⊕› symbol to denote the monoid operation (for
no particular reason).›
locale monoid0 =
fixes G f
assumes monoidAssum: "IsAmonoid(G,f)"
fixes monoper (infixl "⊕" 70)
defines monoper_def [simp]: "a ⊕ b ≡ f`⟨a,b⟩"
text‹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 by simp
text‹The result of the monoid operation is in the monoid (carrier).›
lemma (in monoid0) group0_1_L1:
assumes "a∈G" "b∈G" shows "a⊕b ∈ G"
using assms monoidAssum IsAmonoid_def IsAssociative_def apply_funtype
by auto
text‹There is only one neutral element in a monoid.›
lemma (in monoid0) group0_1_L2: shows
"∃!e. e∈G ∧ (∀ g∈G. ( (e⊕g = g) ∧ g⊕e = g))"
proof
fix e y
assume "e ∈ G ∧ (∀g∈G. e ⊕ g = g ∧ g ⊕ e = g)"
and "y ∈ G ∧ (∀g∈G. y ⊕ g = g ∧ g ⊕ y = g)"
then have "y⊕e = y" "y⊕e = e" by auto
thus "e = y" by simp
next from monoidAssum show
"∃e. e∈ G ∧ (∀ g∈G. e⊕g = g ∧ g⊕e = g)"
using IsAmonoid_def by auto
qed
text‹The neutral element is neutral.›
lemma (in monoid0) unit_is_neutral:
assumes A1: "e = TheNeutralElement(G,f)"
shows "e ∈ G ∧ (∀g∈G. e ⊕ g = g ∧ g ⊕ e = g)"
proof -
let ?n = "THE b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)"
have "∃!b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)"
using group0_1_L2 by simp
then have "?n∈ G ∧ (∀ g∈G. ?n⊕g = g ∧ g⊕?n = g)"
by (rule theI)
with A1 show ?thesis
using TheNeutralElement_def by simp
qed
text‹The monoid carrier is not empty.›
lemma (in monoid0) group0_1_L3A: shows "G≠0"
proof -
have "TheNeutralElement(G,f) ∈ G" using unit_is_neutral
by simp
thus ?thesis by auto
qed
text‹The monoid operation is a binary function on the carrier with values in the carrier. ›
lemma (in monoid0) monoid_oper_fun: shows "f:G×G→G"
using monoidAssum unfolding IsAmonoid_def IsAssociative_def
by simp
text‹The range of the monoid operation is the whole monoid carrier.›
lemma (in monoid0) group0_1_L3B: shows "range(f) = G"
proof
from monoidAssum have "f : G×G→G"
using IsAmonoid_def IsAssociative_def by simp
then show "range(f) ⊆ G"
using func1_1_L5B by simp
show "G ⊆ range(f)"
proof
fix g assume A1: "g∈G"
let ?e = "TheNeutralElement(G,f)"
from A1 have "⟨?e,g⟩ ∈ G×G" "g = f`⟨?e,g⟩"
using unit_is_neutral by auto
with ‹f : G×G→G› show "g ∈ range(f)"
using func1_1_L5A by blast
qed
qed
text‹Another way to state that the range of the monoid operation
is the whole monoid carrier.›
lemma (in monoid0) range_carr: shows "f``(G×G) = G"
using monoidAssum IsAmonoid_def IsAssociative_def
group0_1_L3B range_image_domain by auto
text‹In a monoid any neutral element is the neutral element.›
lemma (in monoid0) group0_1_L4:
assumes A1: "e ∈ G ∧ (∀g∈G. e ⊕ g = g ∧ g ⊕ e = g)"
shows "e = TheNeutralElement(G,f)"
proof -
let ?n = "THE b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)"
have "∃!b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)"
using group0_1_L2 by simp
moreover note A1
ultimately have "?n = e" by (rule the_equality2)
then show ?thesis using TheNeutralElement_def by simp
qed
text‹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: "∀x∈H.∀y∈H. x⊕y ∈ H"
and A2: "H⊆G"
and A3: "e = TheNeutralElement(G,f)"
and A4: "g = restrict(f,H×H)"
and A5: "e∈H"
and A6: "h∈H"
shows "g`⟨e,h⟩ = h ∧ g`⟨h,e⟩ = h"
proof -
from A4 A6 A5 have
"g`⟨e,h⟩ = e⊕h ∧ g`⟨h,e⟩ = h⊕e"
using restrict_if by simp
with A3 A4 A6 A2 show
"g`⟨e,h⟩ = h ∧ g`⟨h,e⟩ = h"
using unit_is_neutral by auto
qed
text‹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 {is closed under} f"
and A2: "H⊆G"
and A3: "TheNeutralElement(G,f) ∈ H"
shows "IsAmonoid(H,restrict(f,H×H))"
proof -
let ?g = "restrict(f,H×H)"
let ?e = "TheNeutralElement(G,f)"
from monoidAssum have "f ∈ G×G→G"
using IsAmonoid_def IsAssociative_def by simp
moreover from A2 have "H×H ⊆ G×G" by auto
moreover from A1 have "∀p ∈ H×H. f`(p) ∈ H"
using IsOpClosed_def by auto
ultimately have "?g ∈ H×H→H"
using func1_2_L4 by simp
moreover have "∀x∈H.∀y∈H.∀z∈H.
?g`⟨?g`⟨x,y⟩ ,z⟩ = ?g`⟨x,?g`⟨y,z⟩⟩"
proof -
from A1 have "∀x∈H.∀y∈H.∀z∈H.
?g`⟨?g`⟨x,y⟩,z⟩ = x⊕y⊕z"
using IsOpClosed_def restrict_if by simp
moreover have "∀x∈H.∀y∈H.∀z∈H. x⊕y⊕z = x⊕(y⊕z)"
proof -
from monoidAssum have
"∀x∈G.∀y∈G.∀z∈G. x⊕y⊕z = x⊕(y⊕z)"
using IsAmonoid_def IsAssociative_def
by simp
with A2 show ?thesis by auto
qed
moreover from A1 have
"∀x∈H.∀y∈H.∀z∈H. x⊕(y⊕z) = ?g`⟨ x,?g`⟨y,z⟩ ⟩"
using IsOpClosed_def restrict_if by simp
ultimately show ?thesis by simp
qed
moreover have
"∃n∈H. (∀h∈H. ?g`⟨n,h⟩ = h ∧ ?g`⟨h,n⟩ = h)"
proof -
from A1 have "∀x∈H.∀y∈H. x⊕y ∈ H"
using IsOpClosed_def by simp
with A2 A3 have
"∀ h∈H. ?g`⟨?e,h⟩ = h ∧ ?g`⟨h,?e⟩ = h"
using group0_1_L5 by blast
with A3 show ?thesis by auto
qed
ultimately show ?thesis using IsAmonoid_def IsAssociative_def
by simp
qed
text‹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: "IsAmonoid(G,f)"
and A2: "H {is closed under} f"
and A3: "H⊆G"
and A4: "TheNeutralElement(G,f) ∈ H"
shows "TheNeutralElement(H,restrict(f,H×H)) = TheNeutralElement(G,f)"
proof -
let ?e = "TheNeutralElement(G,f)"
let ?g = "restrict(f,H×H)"
from assms have "monoid0(H,?g)"
using monoid0_def monoid0.group0_1_T1
by simp
moreover have
"?e ∈ H ∧ (∀h∈H. ?g`⟨?e,h⟩ = h ∧ ?g`⟨h,?e⟩ = h)"
proof -
{ fix h assume "h ∈ H"
with assms have
"monoid0(G,f)" "∀x∈H.∀y∈H. f`⟨x,y⟩ ∈ H"
"H⊆G" "?e = TheNeutralElement(G,f)" "?g = restrict(f,H×H)"
"?e ∈ H" "h ∈ H"
using monoid0_def IsOpClosed_def by auto
then have "?g`⟨?e,h⟩ = h ∧ ?g`⟨h,?e⟩ = h"
by (rule monoid0.group0_1_L5)
} hence "∀h∈H. ?g`⟨?e,h⟩ = h ∧ ?g`⟨h,?e⟩ = h" by simp
with A4 show ?thesis by simp
qed
ultimately have "?e = TheNeutralElement(H,?g)"
by (rule monoid0.group0_1_L4)
thus ?thesis by simp
qed
text‹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 ⊕ b ≠ TheNeutralElement(G,f)"
shows "a ≠ TheNeutralElement(G,f) ∨ b ≠ TheNeutralElement(G,f)"
using assms unit_is_neutral by auto
text‹The monoid operation is associative.›
lemma (in monoid0) sum_associative:
assumes "a∈G" "b∈G" "c∈G"
shows "(a⊕b)⊕c = a⊕(b⊕c)"
using assms monoidAssum unfolding IsAmonoid_def IsAssociative_def
by auto
text‹A simple rearrangement of four monoid elements transferred from the ‹semigr0› locale: ›
lemma (in monoid0) rearr4elem_monoid:
assumes "a∈G" "b∈G" "c∈G" "d∈G"
shows "a⊕b⊕(c⊕d) = a⊕(b⊕c)⊕d"
using assms semigr0_valid_in_monoid0 semigr0.rearr4elem_assoc
by simp
end