IsarMathLib

A library of formalized mathematics for Isabelle/ZF theorem proving environment

theory DirectProduct_ZF imports func_ZF
begin

This theory considers the direct product of binary operations. Contributed by Seo Sanghyeon.

Definition

In group theory the notion of direct product provides a natural way of creating a new group from two given groups.

Given \((G,\cdot)\) and \((H,\circ)\) a new operation \((G\times H, \times )\) is defined as \((g, h) \times (g', h') = (g \cdot g', h \circ h')\).

Definition

\( \text{DirectProduct}(P,Q,G,H) \equiv \) \( \{\langle x,\langle P\langle \text{fst}(\text{fst}(x)),\text{fst}(\text{snd}(x))\rangle , Q\langle \text{snd}(\text{fst}(x)),\text{snd}(\text{snd}(x))\rangle \rangle \rangle .\ \) \( x \in (G\times H)\times (G\times H)\} \)

We define a context called direct0 which holds an assumption that \(P, Q\) are binary operations on \(G,H\), resp. and denotes \(R\) as the direct product of \((G,P)\) and \((H,Q)\).

Locale direct0

assumes Pfun: \( P : G\times G\rightarrow G \)

assumes Qfun: \( Q : H\times H\rightarrow H \)

defines \( R \equiv \text{DirectProduct}(P,Q,G,H) \)

The direct product of binary operations is a binary operation.

lemma (in direct0) DirectProduct_ZF_1_L1:

shows \( R : (G\times H)\times (G\times H)\rightarrow G\times H \)proof
from Pfun, Qfun have \( \forall x\in (G\times H)\times (G\times H).\ \) \( \langle P\langle \text{fst}(\text{fst}(x)),\text{fst}(\text{snd}(x))\rangle ,Q\langle \text{snd}(\text{fst}(x)),\text{snd}(\text{snd}(x))\rangle \rangle \in G\times H \)
then show \( thesis \) using ZF_fun_from_total , DirectProduct_def
qed

And it has the intended value.

lemma (in direct0) DirectProduct_ZF_1_L2:

shows \( \forall x\in (G\times H).\ \forall y\in (G\times H).\ \) \( R\langle x,y\rangle = \langle P\langle \text{fst}(x),\text{fst}(y)\rangle ,Q\langle \text{snd}(x),\text{snd}(y)\rangle \rangle \) using DirectProduct_def , DirectProduct_ZF_1_L1 , ZF_fun_from_tot_val

And the value belongs to the set the operation is defined on.

lemma (in direct0) DirectProduct_ZF_1_L3:

shows \( \forall x\in (G\times H).\ \forall y\in (G\times H).\ R\langle x,y\rangle \in G\times H \) using DirectProduct_ZF_1_L1

Associative and commutative operations

If P and Q are both associative or commutative operations, the direct product of P and Q has the same property.

Direct product of commutative operations is commutative.

lemma (in direct0) DirectProduct_ZF_2_L1:

assumes \( P \text{ is commutative on } G \) and \( Q \text{ is commutative on } H \)

shows \( R \text{ is commutative on } G\times H \)proof
from assms have \( \forall x\in (G\times H).\ \forall y\in (G\times H).\ R\langle x,y\rangle = R\langle y,x\rangle \) using DirectProduct_ZF_1_L2 , IsCommutative_def
then show \( thesis \) using IsCommutative_def
qed

Direct product of associative operations is associative.

lemma (in direct0) DirectProduct_ZF_2_L2:

assumes \( P \text{ is associative on } G \) and \( Q \text{ is associative on } H \)

shows \( R \text{ is associative on } G\times H \)proof
have \( \forall x\in G\times H.\ \forall y\in G\times H.\ \forall z\in G\times H.\ R\langle R\langle x,y\rangle ,z\rangle =\) \( \langle P\langle P\langle \text{fst}(x),\text{fst}(y)\rangle ,\text{fst}(z)\rangle ,Q\langle Q\langle \text{snd}(x),\text{snd}(y)\rangle ,\text{snd}(z)\rangle \rangle \) using DirectProduct_ZF_1_L2 , DirectProduct_ZF_1_L3
moreover
have \( \forall x\in G\times H.\ \forall y\in G\times H.\ \forall z\in G\times H.\ R\langle x,R\langle y,z\rangle \rangle =\) \( \langle P\langle \text{fst}(x),P\langle \text{fst}(y),\text{fst}(z)\rangle \rangle ,Q\langle \text{snd}(x),Q\langle \text{snd}(y),\text{snd}(z)\rangle \rangle \rangle \) using DirectProduct_ZF_1_L2 , DirectProduct_ZF_1_L3
ultimately have \( \forall x\in G\times H.\ \forall y\in G\times H.\ \forall z\in G\times H.\ R\langle R\langle x,y\rangle ,z\rangle = R\langle x,R\langle y,z\rangle \rangle \) using assms , IsAssociative_def
then show \( thesis \) using DirectProduct_ZF_1_L1 , IsAssociative_def
qed
end
lemma ZF_fun_from_total:

assumes \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)
Definition of DirectProduct: \( \text{DirectProduct}(P,Q,G,H) \equiv \) \( \{\langle x,\langle P\langle \text{fst}(\text{fst}(x)),\text{fst}(\text{snd}(x))\rangle , Q\langle \text{snd}(\text{fst}(x)),\text{snd}(\text{snd}(x))\rangle \rangle \rangle .\ \) \( x \in (G\times H)\times (G\times H)\} \)
lemma (in direct0) DirectProduct_ZF_1_L1: shows \( R : (G\times H)\times (G\times H)\rightarrow G\times H \)
lemma ZF_fun_from_tot_val:

assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

shows \( f(x) = b(x) \)
lemma (in direct0) DirectProduct_ZF_1_L2: shows \( \forall x\in (G\times H).\ \forall y\in (G\times H).\ \) \( R\langle x,y\rangle = \langle P\langle \text{fst}(x),\text{fst}(y)\rangle ,Q\langle \text{snd}(x),\text{snd}(y)\rangle \rangle \)
Definition of IsCommutative: \( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
lemma (in direct0) DirectProduct_ZF_1_L3: shows \( \forall x\in (G\times H).\ \forall y\in (G\times H).\ R\langle x,y\rangle \in G\times H \)
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 ))) \)
8
16
3
3