begin
In this theory file we extend the work on equivalence relations done in the standard Isabelle's EquivClass theory. That development is very good and all, but we really would prefer an approach contained within the a standard ZF set theory, without extensions specific to Isabelle. That is why this theory is written.
Congruent functions and projections on the quotient
Suppose we have a set \(X\) with a relation \(r\subseteq X\times X\) and a function \(f: X\rightarrow X\). The function \(f\) can be compatible (congruent) with \(r\) in the sense that if two elements \(x,y\) are related then the values \(f(x), f(x)\) are also related. This is especially useful if \(r\) is an equivalence relation as it allows to "project" the function to the quotient space \(X/r\) (the set of equivalence classes of \(r\)) and create a new function \(F\) that satifies the formula \(F([x]_r) = [f(x)]_r\). When \(f\) is congruent with respect to \(r\) such definition of the value of \(F\) on the equivalence class \([x]_r\) does not depend on which \(x\) we choose to represent the class. In this section we also consider binary operations that are congruent with respect to a relation. These are important in algebra - the congruency condition allows to project the operation to obtain the operation on the quotient space.
First we define the notion of function that maps equivalent elements to equivalent values. We use similar names as in the Isabelle's standard EquivClass theory to indicate the conceptual correspondence of the notions.
definition
\( \text{Congruent}(r,f) \equiv \) \( (\forall x y.\ \langle x,y\rangle \in r \longrightarrow \langle f(x),f(y)\rangle \in r) \)
Now we will define the projection of a function onto the quotient space. In standard math the equivalence class of \(x\) with respect to relation \(r\) is usually denoted \([x]_r\). Here we reuse notation \(r\{ x\}\) instead. This means the image of the set \(\{ x\}\) with respect to the relation, which, for equivalence relations is exactly its equivalence class if you think about it.
definition
\( \text{ProjFun}(A,r,f) \equiv \) \( \{\langle c,\bigcup x\in c.\ r\{f(x)\}\rangle .\ c \in (A//r)\} \)
Elements of equivalence classes belong to the set.
lemma EquivClass_1_L1:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( C \in A//r \) and A3: \( x\in C \)
shows \( x\in A \)proof from A2 have \( C \subseteq \bigcup (A//r) \)
with A1, A3 show \( x\in A \) using Union_quotient
qed
The image of a subset of \(X\) under projection is a subset of \(A/r\).
lemma EquivClass_1_L1A:
assumes \( A\subseteq X \)
shows \( \{r\{x\}.\ x\in A\} \subseteq X//r \) using assms, quotientIIf an element belongs to an equivalence class, then its image under relation is this equivalence class.
lemma EquivClass_1_L2:
assumes A1: \( \text{equiv}(A,r) \), \( C \in A//r \) and A2: \( x\in C \)
shows \( r\{x\} = C \)proof from A1, A2 have \( x \in r\{x\} \) using EquivClass_1_L1, equiv_class_self
with A2 have I: \( r\{x\}\cap C \neq 0 \)
from A1, A2 have \( r\{x\} \in A//r \) using EquivClass_1_L1, quotientI
with A1, I show \( thesis \) using quotient_disj
qed
Elements that belong to the same equivalence class are equivalent.
lemma EquivClass_1_L2A:
assumes \( \text{equiv}(A,r) \), \( C \in A//r \), \( x\in C \), \( y\in C \)
shows \( \langle x,y\rangle \in r \) using assms, EquivClass_1_L2, EquivClass_1_L1, equiv_class_eq_iffElements that have the same image under an equivalence relation are equivalent. This is the same as eq_equiv_class from standard Isabelle/ZF's EquivClass theory, just copied here to be easier to find.
lemma same_image_equiv:
assumes \( \text{equiv}(A,r) \), \( y\in A \), \( r\{x\} = r\{y\} \)
shows \( \langle x,y\rangle \in r \) using assms, eq_equiv_classEvery \(x\) is in the class of \(y\), then they are equivalent.
lemma EquivClass_1_L2B:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( y\in A \) and A3: \( x \in r\{y\} \)
shows \( \langle x,y\rangle \in r \)proof from A2 have \( r\{y\} \in A//r \) using quotientI
with A1, A3 show \( thesis \) using EquivClass_1_L1, equiv_class_self, equiv_class_nondisjoint
qed
If a function is congruent then the equivalence classes of the values that come from the arguments from the same class are the same.
lemma EquivClass_1_L3:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( \text{Congruent}(r,f) \) and A3: \( C \in A//r \), \( x\in C \), \( y\in C \)
shows \( r\{f(x)\} = r\{f(y)\} \)proof from A1, A3 have \( \langle x,y\rangle \in r \) using EquivClass_1_L2A
with A2 have \( \langle f(x),f(y)\rangle \in r \) using Congruent_def
with A1 show \( thesis \) using equiv_class_eq
qed
The values of congruent functions are in the space.
lemma EquivClass_1_L4:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( C \in A//r \), \( x\in C \) and A3: \( \text{Congruent}(r,f) \)
shows \( f(x) \in A \)proof from A1, A2 have \( x\in A \) using EquivClass_1_L1
with A1 have \( \langle x,x\rangle \in r \) using equiv_def, refl_def
with A3 have \( \langle f(x),f(x)\rangle \in r \) using Congruent_def
with A1 show \( thesis \) using equiv_type
qed
Equivalence classes are not empty.
lemma EquivClass_1_L5:
assumes A1: \( \text{refl}(A,r) \) and A2: \( C \in A//r \)
shows \( C\neq 0 \)proof from A2 obtain \( x \) where I: \( C = r\{x\} \) and \( x\in A \) using quotient_def
from A1, \( x\in A \) have \( x \in r\{x\} \) using refl_def
with I show \( thesis \)
qed
To avoid using an axiom of choice, we define the projection using the expression \(\bigcup _{x\in C} r(\{f(x)\})\). The next lemma shows that for congruent function this is in the quotient space \(A/r\).
lemma EquivClass_1_L6:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( \text{Congruent}(r,f) \) and A3: \( C \in A//r \)
shows \( (\bigcup x\in C.\ r\{f(x)\}) \in A//r \)proof from A1 have \( \text{refl}(A,r) \) unfolding equiv_def
with A3 have \( C\neq 0 \) using EquivClass_1_L5
moreover
qed
from A2, A3, A1 have \( \forall x\in C.\ r\{f(x)\} \in A//r \) using EquivClass_1_L4, quotientI
moreover from A1, A2, A3 have \( \forall x y.\ x\in C \wedge y\in C \longrightarrow r\{f(x)\} = r\{f(y)\} \) using EquivClass_1_L3
ultimately show \( thesis \) by (rule ZF1_1_L2 )
Congruent functions can be projected.
lemma EquivClass_1_T0:
assumes \( \text{equiv}(A,r) \), \( \text{Congruent}(r,f) \)
shows \( \text{ProjFun}(A,r,f) : A//r \rightarrow A//r \) using assms, EquivClass_1_L6, ProjFun_def, ZF_fun_from_totalWe now define congruent functions of two variables (binary funtions). The predicate Congruent2 corresponds to congruent2 in Isabelle's standard EquivClass theory, but uses ZF-functions rather than meta-functions.
definition
\( \text{Congruent2}(r,f) \equiv \) \( (\forall x_1 x_2 y_1 y_2.\ \langle x_1,x_2\rangle \in r \wedge \langle y_1,y_2\rangle \in r \longrightarrow \) \( \langle f\langle x_1,y_1\rangle , f\langle x_2,y_2\rangle \rangle \in r) \)
Next we define the notion of projecting a binary operation to the quotient space. This is a very important concept that allows to define quotient groups, among other things.
definition
\( \text{ProjFun2}(A,r,f) \equiv \) \( \{\langle p,\bigcup z \in \text{fst}(p)\times \text{snd}(p).\ r\{f(z)\}\rangle .\ p \in (A//r)\times (A//r) \} \)
The following lemma is a two-variables equivalent of EquivClass_1_L3.
lemma EquivClass_1_L7:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( \text{Congruent2}(r,f) \) and A3: \( C_1 \in A//r \), \( C_2 \in A//r \) and A4: \( z_1 \in C_1\times C_2 \), \( z_2 \in C_1\times C_2 \)
shows \( r\{f(z_1)\} = r\{f(z_2)\} \)proof from A4 obtain \( x_1 \) \( y_1 \) \( x_2 \) \( y_2 \) where \( x_1\in C_1 \) and \( y_1\in C_2 \) and \( z_1 = \langle x_1,y_1\rangle \) and \( x_2\in C_1 \) and \( y_2\in C_2 \) and \( z_2 = \langle x_2,y_2\rangle \)
with A1, A3 have \( \langle x_1,x_2\rangle \in r \) and \( \langle y_1,y_2\rangle \in r \) using EquivClass_1_L2A
with A2 have \( \langle f\langle x_1,y_1\rangle ,f\langle x_2,y_2\rangle \rangle \in r \) using Congruent2_def
with A1, \( z_1 = \langle x_1,y_1\rangle \), \( z_2 = \langle x_2,y_2\rangle \) show \( thesis \) using equiv_class_eq
qed
The values of congruent functions of two variables are in the space.
lemma EquivClass_1_L8:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( C_1 \in A//r \) and A3: \( C_2 \in A//r \) and A4: \( z \in C_1\times C_2 \) and A5: \( \text{Congruent2}(r,f) \)
shows \( f(z) \in A \)proof from A4 obtain \( x \) \( y \) where \( x\in C_1 \) and \( y\in C_2 \) and \( z = \langle x,y\rangle \)
with A1, A2, A3 have \( x\in A \) and \( y\in A \) using EquivClass_1_L1
with A1, A4 have \( \langle x,x\rangle \in r \) and \( \langle y,y\rangle \in r \) using equiv_def, refl_def
with A5 have \( \langle f\langle x,y\rangle , f\langle x,y\rangle \rangle \in r \) using Congruent2_def
with A1, \( z = \langle x,y\rangle \) show \( thesis \) using equiv_type
qed
The values of congruent functions are in the space. Note that although this lemma is intended to be used with functions, we don't need to assume that \(f\) is a function.
lemma EquivClass_1_L8A:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( x\in A \), \( y\in A \) and A3: \( \text{Congruent2}(r,f) \)
shows \( f\langle x,y\rangle \in A \)proof from A1, A2 have \( r\{x\} \in A//r \), \( r\{y\} \in A//r \), \( \langle x,y\rangle \in r\{x\}\times r\{y\} \) using equiv_class_self, quotientI
with A1, A3 show \( thesis \) using EquivClass_1_L8
qed
The following lemma is a two-variables equivalent of EquivClass_1_L6.
lemma EquivClass_1_L9:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( \text{Congruent2}(r,f) \) and A3: \( p \in (A//r)\times (A//r) \)
shows \( (\bigcup z \in \text{fst}(p)\times \text{snd}(p).\ r\{f(z)\}) \in A//r \)proof from A3 have \( \text{fst}(p) \in A//r \) and \( \text{snd}(p) \in A//r \)
with A1, A2 have I: \( \forall z \in \text{fst}(p)\times \text{snd}(p).\ f(z) \in A \) using EquivClass_1_L8
from A3, A1 have \( \text{fst}(p)\times \text{snd}(p) \neq 0 \) using equiv_def, EquivClass_1_L5, Sigma_empty_iff
moreover
qed
from A1, I have \( \forall z \in \text{fst}(p)\times \text{snd}(p).\ r\{f(z)\} \in A//r \) using quotientI
moreover from A1, A2, \( \text{fst}(p) \in A//r \), \( \text{snd}(p) \in A//r \) have \( \forall z_1 z_2.\ z_1 \in \text{fst}(p)\times \text{snd}(p) \wedge z_2 \in \text{fst}(p)\times \text{snd}(p) \longrightarrow \)
\( r\{f(z_1)\} = r\{f(z_2)\} \) using EquivClass_1_L7
ultimately show \( thesis \) by (rule ZF1_1_L2 )
Congruent functions of two variables can be projected.
theorem EquivClass_1_T1:
assumes \( \text{equiv}(A,r) \), \( \text{Congruent2}(r,f) \)
shows \( \text{ProjFun2}(A,r,f) : (A//r)\times (A//r) \rightarrow A//r \) using assms, EquivClass_1_L9, ProjFun2_def, ZF_fun_from_totalThe projection diagram commutes. I wish I knew how to draw this diagram in LaTeX.
lemma EquivClass_1_L10:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( \text{Congruent2}(r,f) \) and A3: \( x\in A \), \( y\in A \)
shows \( \text{ProjFun2}(A,r,f)\langle r\{x\},r\{y\}\rangle = r\{f\langle x,y\rangle \} \)proof from A3, A1 have \( r\{x\} \times r\{y\} \neq 0 \) using quotientI, equiv_def, EquivClass_1_L5, Sigma_empty_iff
moreover
have \( \forall z \in r\{x\}\times r\{y\}.\ r\{f(z)\} = r\{f\langle x,y\rangle \} \)proof
ultimately have \( (\bigcup z \in r\{x\}\times r\{y\}.\ r\{f(z)\}) = r\{f\langle x,y\rangle \} \) by (rule ZF1_1_L1 )
fix \( z \)
assume A4: \( z \in r\{x\}\times r\{y\} \)
from A1, A3 have \( r\{x\} \in A//r \), \( r\{y\} \in A//r \), \( \langle x,y\rangle \in r\{x\}\times r\{y\} \) using quotientI, equiv_class_self
with A1, A2, A4 show \( r\{f(z)\} = r\{f\langle x,y\rangle \} \) using EquivClass_1_L7
qed
moreover
qed
have \( \text{ProjFun2}(A,r,f)\langle r\{x\},r\{y\}\rangle = (\bigcup z \in r\{x\}\times r\{y\}.\ r\{f(z)\}) \)proof
ultimately show \( thesis \)
from assms have \( \text{ProjFun2}(A,r,f) : (A//r)\times (A//r) \rightarrow A//r \), \( \langle r\{x\},r\{y\}\rangle \in (A//r)\times (A//r) \) using EquivClass_1_T1, quotientI
then show \( thesis \) using ProjFun2_def, ZF_fun_from_tot_val
qed
Projecting commutative, associative and distributive operations.
In this section we show that if the operations are congruent with respect to an equivalence relation then the projection to the quotient space preserves commutativity, associativity and distributivity.
The projection of commutative operation is commutative.
lemma EquivClass_2_L1:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( \text{Congruent2}(r,f) \) and A3: \( f \text{ is commutative on } A \) and A4: \( c1 \in A//r \), \( c2 \in A//r \)
shows \( \text{ProjFun2}(A,r,f)\langle c1,c2\rangle = \text{ProjFun2}(A,r,f)\langle c2,c1\rangle \)proof from A4 obtain \( x \) \( y \) where D1: \( c1 = r\{x\} \), \( c2 = r\{y\} \), \( x\in A \), \( y\in A \) using quotient_def
with A1, A2 have \( \text{ProjFun2}(A,r,f)\langle c1,c2\rangle = r\{f\langle x,y\rangle \} \) using EquivClass_1_L10
also
qed
from A3, D1 have \( r\{f\langle x,y\rangle \} = r\{f\langle y,x\rangle \} \) using IsCommutative_def
also from A1, A2, D1 have \( r\{f\langle y,x\rangle \} = \text{ProjFun2}(A,r,f) \langle c2,c1\rangle \) using EquivClass_1_L10
finally show \( thesis \)
The projection of commutative operation is commutative.
theorem EquivClass_2_T1:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent2}(r,f) \) and \( f \text{ is commutative on } A \)
shows \( \text{ProjFun2}(A,r,f) \text{ is commutative on } A//r \) using assms, IsCommutative_def, EquivClass_2_L1The projection of an associative operation is associative.
lemma EquivClass_2_L2:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( \text{Congruent2}(r,f) \) and A3: \( f \text{ is associative on } A \) and A4: \( c1 \in A//r \), \( c2 \in A//r \), \( c3 \in A//r \) and A5: \( g = \text{ProjFun2}(A,r,f) \)
shows \( g\langle g\langle c1,c2\rangle ,c3\rangle = g\langle c1,g\langle c2,c3\rangle \rangle \)proof from A4 obtain \( x \) \( y \) \( z \) where D1: \( c1 = r\{x\} \), \( c2 = r\{y\} \), \( c3 = r\{z\} \), \( x\in A \), \( y\in A \), \( z\in A \) using quotient_def
with A3 have T1: \( f\langle x,y\rangle \in A \), \( f\langle y,z\rangle \in A \) using IsAssociative_def, apply_type
with A1, A2, D1, A5 have \( g\langle g\langle c1,c2\rangle ,c3\rangle = r\{f\langle f\langle x,y\rangle ,z\rangle \} \) using EquivClass_1_L10
also
qed
from D1, A3 have \( \ldots = r\{f\langle x,f\langle y,z\rangle \rangle \} \) using IsAssociative_def
also from T1, A1, A2, D1, A5 have \( \ldots = g\langle c1,g\langle c2,c3\rangle \rangle \) using EquivClass_1_L10
finally show \( thesis \)
The projection of an associative operation is associative on the quotient.
theorem EquivClass_2_T2:
assumes A1: \( \text{equiv}(A,r) \) and A2: \( \text{Congruent2}(r,f) \) and A3: \( f \text{ is associative on } A \)
shows \( \text{ProjFun2}(A,r,f) \text{ is associative on } A//r \)proof let \( g = \text{ProjFun2}(A,r,f) \)
from A1, A2 have \( g \in (A//r)\times (A//r) \rightarrow A//r \) using EquivClass_1_T1
moreover
qed
from A1, A2, A3 have \( \forall c1 \in A//r.\ \forall c2 \in A//r.\ \forall c3 \in A//r.\ \)
\( g\langle g\langle c1,c2\rangle ,c3\rangle = g\langle c1,g\langle c2,c3\rangle \rangle \) using EquivClass_2_L2
ultimately show \( thesis \) using IsAssociative_def
The essential condition to show that distributivity is preserved by projections to quotient spaces, provided both operations are congruent with respect to the equivalence relation.
lemma EquivClass_2_L3:
assumes A1: \( \text{IsDistributive}(X,A,M) \) and A2: \( \text{equiv}(X,r) \) and A3: \( \text{Congruent2}(r,A) \), \( \text{Congruent2}(r,M) \) and A4: \( a \in X//r \), \( b \in X//r \), \( c \in X//r \) and A5: \( A_p = \text{ProjFun2}(X,r,A) \), \( M_p = \text{ProjFun2}(X,r,M) \)
shows \( M_p\langle a,A_p\langle b,c\rangle \rangle = A_p\langle M_p\langle a,b\rangle ,M_p\langle a,c\rangle \rangle \wedge \) \( M_p\langle A_p\langle b,c\rangle ,a \rangle = A_p\langle M_p\langle b,a\rangle , M_p\langle c,a\rangle \rangle \)proof from A4 obtain \( x \) \( y \) \( z \) where \( x\in X \), \( y\in X \), \( z\in X \), \( a = r\{x\} \), \( b = r\{y\} \), \( c = r\{z\} \) using quotient_def
with A1, A2, A3, A5 show \( M_p\langle a,A_p\langle b,c\rangle \rangle = A_p\langle M_p\langle a,b\rangle ,M_p\langle a,c\rangle \rangle \) and \( M_p\langle A_p\langle b,c\rangle ,a \rangle = A_p\langle M_p\langle b,a\rangle , M_p\langle c,a\rangle \rangle \) using EquivClass_1_L8A, EquivClass_1_L10, IsDistributive_def
qed
Distributivity is preserved by projections to quotient spaces, provided both operations are congruent with respect to the equivalence relation.
lemma EquivClass_2_L4:
assumes A1: \( \text{IsDistributive}(X,A,M) \) and A2: \( \text{equiv}(X,r) \) and A3: \( \text{Congruent2}(r,A) \), \( \text{Congruent2}(r,M) \)
shows \( \text{IsDistributive}(X//r, \text{ProjFun2}(X,r,A), \text{ProjFun2}(X,r,M)) \)proof let \( A_p = \text{ProjFun2}(X,r,A) \)
let \( M_p = \text{ProjFun2}(X,r,M) \)
from A1, A2, A3 have \( \forall a\in X//r.\ \forall b\in X//r.\ \forall c\in X//r.\ \)
\( M_p\langle a,A_p\langle b,c\rangle \rangle = A_p\langle M_p\langle a,b\rangle ,M_p\langle a,c\rangle \rangle \wedge \)
\( M_p\langle A_p\langle b,c\rangle ,a\rangle = A_p\langle M_p\langle b,a\rangle ,M_p\langle c,a\rangle \rangle \) using EquivClass_2_L3
then show \( thesis \) using IsDistributive_def
qed
Saturated sets
In this section we consider sets that are saturated with respect to an equivalence relation. A set \(A\) is saturated with respect to a relation \(r\) if \(A=r^{-1}(r(A))\). For equivalence relations saturated sets are unions of equivalence classes. This makes them useful as a tool to define subsets of the quotient space using properties of representants. Namely, we often define a set \(B\subseteq X/r\) by saying that \([x]_r \in B\) iff \(x\in A\). If \(A\) is a saturated set, this definition is consistent in the sense that it does not depend on the choice of \(x\) to represent \([x]_r\).
The following defines the notion of a saturated set. Recall that in Isabelle \( r^{-1}(A) \) is the inverse image of \(A\) with respect to relation \(r\). This definition is not specific to equivalence relations.
definition
\( \text{IsSaturated}(r,A) \equiv A = r^{-1}(r(A)) \)
For equivalence relations a set is saturated iff it is an image of itself.
lemma EquivClass_3_L1:
assumes A1: \( \text{equiv}(X,r) \)
shows \( \text{IsSaturated}(r,A) \longleftrightarrow A = r(A) \)proof assume \( \text{IsSaturated}(r,A) \)
then have \( A = (converse(r)\circ r)(A) \) using IsSaturated_def, vimage_def, image_comp
also
from A1 have \( \ldots = r(A) \) using equiv_comp_eq
finally show \( A = r(A) \)
next
assume \( A = r(A) \)
with A1 have \( A = (converse(r)\circ r)(A) \) using equiv_comp_eq
also
qed
have \( \ldots = r^{-1}(r(A)) \) using vimage_def, image_comp
finally have \( A = r^{-1}(r(A)) \)
then show \( \text{IsSaturated}(r,A) \) using IsSaturated_def
For equivalence relations sets are contained in their images.
lemma EquivClass_3_L2:
assumes A1: \( \text{equiv}(X,r) \) and A2: \( A\subseteq X \)
shows \( A \subseteq r(A) \)proof fix \( a \)
assume \( a\in A \)
with A1, A2 have \( a \in r\{a\} \) using equiv_class_self
with \( a\in A \) show \( a \in r(A) \)
qed
The next lemma shows that if "\(\sim\)" is an equivalence relation and a set \(A\) is such that \(a\in A\) and \(a\sim b\) implies \(b\in A\), then \(A\) is saturated with respect to the relation.
lemma EquivClass_3_L3:
assumes A1: \( \text{equiv}(X,r) \) and A2: \( r \subseteq X\times X \) and A3: \( A\subseteq X \) and A4: \( \forall x\in A.\ \forall y\in X.\ \langle x,y\rangle \in r \longrightarrow y\in A \)
shows \( \text{IsSaturated}(r,A) \)proof from A2, A4 have \( r(A) \subseteq A \) using image_iff
moreover
qed
from A1, A3 have \( A \subseteq r(A) \) using EquivClass_3_L2
ultimately have \( A = r(A) \)
with A1 show \( \text{IsSaturated}(r,A) \) using EquivClass_3_L1
If \(A\subseteq X\) and \(A\) is saturated and \(x\sim y\), then \(x\in A\) iff \(y\in A\). Here we show only one direction.
lemma EquivClass_3_L4:
assumes A1: \( \text{equiv}(X,r) \) and A2: \( \text{IsSaturated}(r,A) \) and A3: \( A\subseteq X \) and A4: \( \langle x,y\rangle \in r \) and A5: \( x\in X \), \( y\in A \)
shows \( x\in A \)proof from A1, A5 have \( x \in r\{x\} \) using equiv_class_self
with A1, A3, A4, A5 have \( x \in r(A) \) using equiv_class_eq, equiv_class_self
with A1, A2 show \( x\in A \) using EquivClass_3_L1
qed
If \(A\subseteq X\) and \(A\) is saturated and \(x\sim y\), then \(x\in A\) iff \(y\in A\).
lemma EquivClass_3_L5:
assumes A1: \( \text{equiv}(X,r) \) and A2: \( \text{IsSaturated}(r,A) \) and A3: \( A\subseteq X \) and A4: \( x\in X \), \( y\in X \) and A5: \( \langle x,y\rangle \in r \)
shows \( x\in A \longleftrightarrow y\in A \)proof assume \( y\in A \)
with assms show \( x\in A \) using EquivClass_3_L4
next
assume \( x\in A \)
from A1, A5 have \( \langle y,x\rangle \in r \) using equiv_is_sym
with A1, A2, A3, A4, \( x\in A \) show \( y\in A \) using EquivClass_3_L4
qed
If \(A\) is saturated then \(x\in A\) iff its class is in the projection of \(A\).
lemma EquivClass_3_L6:
assumes A1: \( \text{equiv}(X,r) \) and A2: \( \text{IsSaturated}(r,A) \) and A3: \( A\subseteq X \) and A4: \( x\in X \) and A5: \( B = \{r\{x\}.\ x\in A\} \)
shows \( x\in A \longleftrightarrow r\{x\} \in B \)proof assume \( x\in A \)
with A5 show \( r\{x\} \in B \)
next
assume \( r\{x\} \in B \)
with A5 obtain \( y \) where \( y \in A \) and \( r\{x\} = r\{y\} \)
with A1, A3 have \( \langle x,y\rangle \in r \) using eq_equiv_class
with A1, A2, A3, A4, \( y \in A \) show \( x\in A \) using EquivClass_3_L4
qed
A technical lemma involving a projection of a saturated set and a logical epression with exclusive or. Note that we don't really care what Xor is here, this is true for any predicate.
lemma EquivClass_3_L7:
assumes \( \text{equiv}(X,r) \) and \( \text{IsSaturated}(r,A) \) and \( A\subseteq X \) and \( x\in X \), \( y\in X \) and \( B = \{r\{x\}.\ x\in A\} \) and \( (x\in A) \text{ Xor } (y\in A) \)
shows \( (r\{x\} \in B) \text{ Xor } (r\{y\} \in B) \) using assms, EquivClass_3_L6 end
lemma EquivClass_1_L1:
assumes \( \text{equiv}(A,r) \) and \( C \in A//r \) and \( x\in C \)
shows \( x\in A \) lemma EquivClass_1_L2:
assumes \( \text{equiv}(A,r) \), \( C \in A//r \) and \( x\in C \)
shows \( r\{x\} = C \) lemma EquivClass_1_L2A:
assumes \( \text{equiv}(A,r) \), \( C \in A//r \), \( x\in C \), \( y\in C \)
shows \( \langle x,y\rangle \in r \)Definition of Congruent:
\( \text{Congruent}(r,f) \equiv \)
\( (\forall x y.\ \langle x,y\rangle \in r \longrightarrow \langle f(x),f(y)\rangle \in r) \)
lemma EquivClass_1_L5:
assumes \( \text{refl}(A,r) \) and \( C \in A//r \)
shows \( C\neq 0 \) lemma EquivClass_1_L4:
assumes \( \text{equiv}(A,r) \) and \( C \in A//r \), \( x\in C \) and \( \text{Congruent}(r,f) \)
shows \( f(x) \in A \) lemma EquivClass_1_L3:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent}(r,f) \) and \( C \in A//r \), \( x\in C \), \( y\in C \)
shows \( r\{f(x)\} = r\{f(y)\} \) lemma ZF1_1_L2:
assumes \( C\neq \emptyset \) and \( \forall x\in C.\ b(x) \in A \) and \( \forall x y.\ x\in C \wedge y\in C \longrightarrow b(x) = b(y) \)
shows \( (\bigcup x\in C.\ b(x))\in A \) lemma EquivClass_1_L6:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent}(r,f) \) and \( C \in A//r \)
shows \( (\bigcup x\in C.\ r\{f(x)\}) \in A//r \)Definition of ProjFun:
\( \text{ProjFun}(A,r,f) \equiv \)
\( \{\langle c,\bigcup x\in c.\ r\{f(x)\}\rangle .\ c \in (A//r)\} \)
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 Congruent2:
\( \text{Congruent2}(r,f) \equiv \)
\( (\forall x_1 x_2 y_1 y_2.\ \langle x_1,x_2\rangle \in r \wedge \langle y_1,y_2\rangle \in r \longrightarrow \)
\( \langle f\langle x_1,y_1\rangle , f\langle x_2,y_2\rangle \rangle \in r) \)
lemma EquivClass_1_L8:
assumes \( \text{equiv}(A,r) \) and \( C_1 \in A//r \) and \( C_2 \in A//r \) and \( z \in C_1\times C_2 \) and \( \text{Congruent2}(r,f) \)
shows \( f(z) \in A \) lemma EquivClass_1_L7:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent2}(r,f) \) and \( C_1 \in A//r \), \( C_2 \in A//r \) and \( z_1 \in C_1\times C_2 \), \( z_2 \in C_1\times C_2 \)
shows \( r\{f(z_1)\} = r\{f(z_2)\} \) lemma EquivClass_1_L9:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent2}(r,f) \) and \( p \in (A//r)\times (A//r) \)
shows \( (\bigcup z \in \text{fst}(p)\times \text{snd}(p).\ r\{f(z)\}) \in A//r \)Definition of ProjFun2:
\( \text{ProjFun2}(A,r,f) \equiv \)
\( \{\langle p,\bigcup z \in \text{fst}(p)\times \text{snd}(p).\ r\{f(z)\}\rangle .\ p \in (A//r)\times (A//r) \} \)
lemma ZF1_1_L1:
assumes \( C\neq \emptyset \) and \( \forall y\in C.\ b(y) = A \)
shows \( (\bigcup y\in C.\ b(y)) = A \) theorem EquivClass_1_T1:
assumes \( \text{equiv}(A,r) \), \( \text{Congruent2}(r,f) \)
shows \( \text{ProjFun2}(A,r,f) : (A//r)\times (A//r) \rightarrow A//r \) 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 EquivClass_1_L10:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent2}(r,f) \) and \( x\in A \), \( y\in A \)
shows \( \text{ProjFun2}(A,r,f)\langle r\{x\},r\{y\}\rangle = r\{f\langle x,y\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 EquivClass_2_L1:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent2}(r,f) \) and \( f \text{ is commutative on } A \) and \( c1 \in A//r \), \( c2 \in A//r \)
shows \( \text{ProjFun2}(A,r,f)\langle c1,c2\rangle = \text{ProjFun2}(A,r,f)\langle c2,c1\rangle \)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 EquivClass_2_L2:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent2}(r,f) \) and \( f \text{ is associative on } A \) and \( c1 \in A//r \), \( c2 \in A//r \), \( c3 \in A//r \) and \( g = \text{ProjFun2}(A,r,f) \)
shows \( g\langle g\langle c1,c2\rangle ,c3\rangle = g\langle c1,g\langle c2,c3\rangle \rangle \) lemma EquivClass_1_L8A:
assumes \( \text{equiv}(A,r) \) and \( x\in A \), \( y\in A \) and \( \text{Congruent2}(r,f) \)
shows \( f\langle x,y\rangle \in A \)Definition of IsDistributive:
\( \text{IsDistributive}(X,A,M) \equiv (\forall a\in X.\ \forall b\in X.\ \forall c\in X.\ \)
\( M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \wedge \)
\( M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle ) \)
lemma EquivClass_2_L3:
assumes \( \text{IsDistributive}(X,A,M) \) and \( \text{equiv}(X,r) \) and \( \text{Congruent2}(r,A) \), \( \text{Congruent2}(r,M) \) and \( a \in X//r \), \( b \in X//r \), \( c \in X//r \) and \( A_p = \text{ProjFun2}(X,r,A) \), \( M_p = \text{ProjFun2}(X,r,M) \)
shows \( M_p\langle a,A_p\langle b,c\rangle \rangle = A_p\langle M_p\langle a,b\rangle ,M_p\langle a,c\rangle \rangle \wedge \) \( M_p\langle A_p\langle b,c\rangle ,a \rangle = A_p\langle M_p\langle b,a\rangle , M_p\langle c,a\rangle \rangle \)Definition of IsSaturated:
\( \text{IsSaturated}(r,A) \equiv A = r^{-1}(r(A)) \)
lemma EquivClass_3_L2:
assumes \( \text{equiv}(X,r) \) and \( A\subseteq X \)
shows \( A \subseteq r(A) \) lemma EquivClass_3_L1:
assumes \( \text{equiv}(X,r) \)
shows \( \text{IsSaturated}(r,A) \longleftrightarrow A = r(A) \) lemma EquivClass_3_L4:
assumes \( \text{equiv}(X,r) \) and \( \text{IsSaturated}(r,A) \) and \( A\subseteq X \) and \( \langle x,y\rangle \in r \) and \( x\in X \), \( y\in A \)
shows \( x\in A \) lemma equiv_is_sym:
assumes \( \text{equiv}(X,r) \) and \( \langle x,y\rangle \in r \)
shows \( \langle y,x\rangle \in r \) lemma EquivClass_3_L6:
assumes \( \text{equiv}(X,r) \) and \( \text{IsSaturated}(r,A) \) and \( A\subseteq X \) and \( x\in X \) and \( B = \{r\{x\}.\ x\in A\} \)
shows \( x\in A \longleftrightarrow r\{x\} \in B \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8