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_valAnd 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_L1Associative 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
qed
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
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) \) and \( b(x)\in Y \) 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 ))) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8