:: Coherent Space
:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski
::
:: Received December 29, 1992
:: Copyright (c) 1992-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TARSKI, XBOOLE_0, CLASSES1, ZFMISC_1, EQREL_1, TOLER_1, SETFAM_1,
SUBSET_1, FUNCT_2, FUNCT_1, RELAT_1, MCART_1, GRAPH_1, ENS_1, PARTFUN1,
CAT_1, COH_SP, STRUCT_0, MONOID_0, RELAT_2, BINOP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, SETFAM_1,
RELAT_1, RELSET_1, MCART_1, FUNCT_1, PARTFUN1, CLASSES1, FUNCT_2,
BINOP_1, EQREL_1, TOLER_1, STRUCT_0, GRAPH_1, CAT_1;
constructors BINOP_1, EQREL_1, CLASSES1, TOLER_1, CAT_1, RELSET_1, XTUPLE_0,
XFAMILY;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
EQREL_1, CAT_2, CAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, CLASSES1, XBOOLE_0, RELAT_1, CAT_1;
equalities BINOP_1, CAT_1, GRAPH_1;
expansions TARSKI, RELAT_1, CAT_1;
theorems TARSKI, ZFMISC_1, TOLER_1, ENUMSET1, RELAT_1, FUNCT_2, CLASSES1,
PARTFUN1, FUNCT_1, DOMAIN_1, CAT_1, XBOOLE_0, XBOOLE_1, EQREL_1,
XTUPLE_0;
schemes TOLER_1, TARSKI, FUNCT_2, BINOP_1, XBOOLE_0, XFAMILY;
begin
reserve x,y,z,a,b,c,X,A for set;
:: Coherent Space and Web of Coherent Space
definition
let IT be set;
attr IT is binary_complete means
:Def1:
for A st A c= IT & (for a,b st a in
A & b in A holds a \/ b in IT) holds union A in IT;
end;
registration
cluster subset-closed binary_complete non empty for set;
existence
proof
take X={{}};
thus for a,b st a in X & b c= a holds b in X
proof
let a,b;
assume that
A1: a in X and
A2: b c= a;
a = {} by A1,TARSKI:def 1;
hence thesis by A1,A2;
end;
thus for A st A c= X & (for a,b st a in A & b in A holds a \/ b in X)
holds union A in X
proof
let A such that
A3: A c= X and
for a,b st a in A & b in A holds a \/ b in X;
now
per cases by A3,ZFMISC_1:33;
suppose
A = {};
hence thesis by TARSKI:def 1,ZFMISC_1:2;
end;
suppose
A = {{}};
then union A = {} by ZFMISC_1:25;
hence thesis by TARSKI:def 1;
end;
end;
hence thesis;
end;
thus thesis;
end;
end;
definition
mode Coherence_Space is subset-closed binary_complete non empty set;
end;
reserve C,D for Coherence_Space;
theorem
{} in C
proof
{} c= C & for a,b st a in {} & b in {} holds a \/ b in C;
hence thesis by Def1,ZFMISC_1:2;
end;
theorem Th2:
bool X is Coherence_Space
proof
A1: for A st A c= bool X & (for a,b st a in A & b in A holds a \/ b in bool
X) holds union A in bool X
proof
let A;
assume that
A2: A c= bool X and
for a,b st a in A & b in A holds a \/ b in bool X;
for a st a in A holds a c= X by A2;
then union A c= X by ZFMISC_1:76;
hence thesis;
end;
for a, b st a in bool X & b c= a holds b in bool X
proof
let a,b;
assume a in bool X & b c= a;
then b c= X by XBOOLE_1:1;
hence thesis;
end;
hence thesis by A1,Def1,CLASSES1:def 1;
end;
theorem
{{}} is Coherence_Space by Th2,ZFMISC_1:1;
theorem Th4:
x in union C implies {x} in C
proof
assume x in union C;
then consider X such that
A1: x in X and
A2: X in C by TARSKI:def 4;
{x} c= X by A1,ZFMISC_1:31;
hence thesis by A2,CLASSES1:def 1;
end;
definition
let C be Coherence_Space;
func Web(C) -> Tolerance of union C means
:Def2:
for x,y being object holds [x,y] in it
iff ex X st X in C & x in X & y in X;
existence
proof
defpred P[set,set] means ex X st X in C & $1 in X & $2 in X;
A1: for x st x in union C holds P[x,x]
proof
let x such that
A2: x in union C;
take {x};
thus thesis by A2,Th4,TARSKI:def 1;
end;
A3: for x,y st x in union C & y in union C & P[x,y] holds P[y,x];
consider T be Tolerance of union C such that
A4: for x,y st x in union C & y in union C holds [x,y] in T iff P[x,y]
from TOLER_1:sch 1(A1,A3);
take T;
let x,y be object;
thus [x,y] in T implies ex X st X in C & x in X & y in X
proof
assume
A5: [x,y] in T;
then x in union C & y in union C by ZFMISC_1:87;
hence thesis by A4,A5;
end;
given X such that
A6: X in C & x in X & y in X;
x in union C & y in union C by A6,TARSKI:def 4;
hence thesis by A4,A6;
end;
uniqueness by TOLER_1:25;
end;
reserve T for Tolerance of union C;
theorem Th5:
T = Web(C) iff for x,y being object holds [x,y] in T iff {x,y} in C
proof
thus T = Web(C) implies
for x,y being object holds [x,y] in T iff {x,y} in C
proof
assume
A1: T = Web(C);
let x,y be object;
thus [x,y] in T implies {x,y} in C
proof
assume [x,y] in T;
then consider X such that
A2: X in C and
A3: x in X & y in X by A1,Def2;
{x,y} c= X by A3,ZFMISC_1:32;
hence thesis by A2,CLASSES1:def 1;
end;
A4: x in {x,y} & y in {x,y} by TARSKI:def 2;
assume {x,y} in C;
hence thesis by A1,A4,Def2;
end;
assume
A5: for x,y being object holds [x,y] in T iff {x,y} in C;
for x,y being object holds [x,y] in T iff ex X st X in C & x in X & y in X
proof
let x,y be object;
thus [x,y] in T implies ex X st X in C & x in X & y in X
proof
assume
A6: [x,y] in T;
take {x,y};
thus thesis by A5,A6,TARSKI:def 2;
end;
given X such that
A7: X in C and
A8: x in X & y in X;
{x,y} c= X by A8,ZFMISC_1:32;
then {x,y} in C by A7,CLASSES1:def 1;
hence thesis by A5;
end;
hence thesis by Def2;
end;
theorem Th6:
a in C iff for x,y st x in a & y in a holds {x,y} in C
proof
defpred P[object,object] means {$1} = $2;
thus a in C implies for x,y st x in a & y in a holds {x,y} in C
proof
assume
A1: a in C;
let x,y;
assume x in a & y in a;
then {x,y} c= a by ZFMISC_1:32;
hence thesis by A1,CLASSES1:def 1;
end;
A2: for x,y,z being object st P[x,y] & P[x,z] holds y = z;
consider X such that
A3: for x being object holds x in X iff
ex y being object st y in a & P[y,x] from TARSKI:sch 1(A2);
assume
A4: for x,y st x in a & y in a holds {x,y} in C;
A5: for b,c st b in X & c in X holds b \/ c in C
proof
let b,c;
assume that
A6: b in X and
A7: c in X;
consider z being object such that
A8: z in a and
A9: {z} = c by A3,A7;
consider y being object such that
A10: y in a and
A11: {y} = b by A3,A6;
{y,z} in C by A4,A10,A8;
hence thesis by A11,A9,ENUMSET1:1;
end;
A12: union X = a
proof
thus union X c= a
proof
let x be object;
assume x in union X;
then consider Z be set such that
A13: x in Z and
A14: Z in X by TARSKI:def 4;
ex y being object st y in a & Z = {y} by A3,A14;
hence thesis by A13,TARSKI:def 1;
end;
let x be object;
assume x in a;
then
A15: {x} in X by A3;
x in {x} by TARSKI:def 1;
hence thesis by A15,TARSKI:def 4;
end;
X c= C
proof
let x be object;
assume x in X;
then consider y being object such that
A16: y in a and
A17: {y} = x by A3;
{y,y} in C by A4,A16;
hence thesis by A17,ENUMSET1:29;
end;
hence thesis by A5,A12,Def1;
end;
theorem Th7:
a in C iff for x,y st x in a & y in a holds [x,y] in Web(C)
proof
thus a in C implies for x,y st x in a & y in a holds [x,y] in Web(C)
proof
assume
A1: a in C;
let x,y;
assume x in a & y in a;
then {x,y} in C by A1,Th6;
hence thesis by Th5;
end;
assume
A2: for x,y st x in a & y in a holds [x,y] in Web(C);
now
let x,y;
assume x in a & y in a;
then [x,y] in Web(C) by A2;
hence {x,y} in C by Th5;
end;
hence thesis by Th6;
end;
theorem
(for x,y st x in a & y in a holds {x,y} in C) implies a c= union C
proof
assume
A1: for x,y st x in a & y in a holds {x,y} in C;
let x be object;
assume x in a;
then {x,x} in C by A1;
then
A2: {x} in C by ENUMSET1:29;
x in {x} by TARSKI:def 1;
hence thesis by A2,TARSKI:def 4;
end;
theorem
Web(C) = Web(D) implies C = D
proof
assume
A1: Web(C) = Web(D);
thus C c= D
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in C;
then for z,y st z in xx & y in xx holds [z,y] in Web(D) by A1,Th7;
hence thesis by Th7;
end;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in D;
then for z,y st z in xx & y in xx holds [z,y] in Web(C) by A1,Th7;
hence thesis by Th7;
end;
theorem
union C in C implies C = bool union C
proof
assume
A1: union C in C;
thus C c= bool union C by ZFMISC_1:82;
let x be object;
assume x in bool union C;
hence thesis by A1,CLASSES1:def 1;
end;
theorem
C = bool union C implies Web(C) = Total union C
proof
reconsider t = Total union C as Tolerance of union C;
assume
A1: C = bool union C;
now
let x,y be object;
thus [x,y] in t implies {x,y} in C
proof
assume [x,y] in t;
then
A2: x in union C & y in union C by ZFMISC_1:87;
{x,y} c= union C
by A2,TARSKI:def 2;
hence thesis by A1;
end;
assume {x,y} in C;
then x in union C & y in union C by A1,ZFMISC_1:32;
hence [x,y] in t by TOLER_1:2;
end;
hence thesis by Th5;
end;
definition
let X be set;
let E be Tolerance of X;
func CohSp(E) -> Coherence_Space means
:Def3:
for a holds a in it iff for x, y st x in a & y in a holds [x,y] in E;
existence
proof
defpred P[set] means for x,y st x in $1 & y in $1 holds [x,y] in E;
consider Z be set such that
A1: for x holds x in Z iff x in bool X & P[x] from XFAMILY:sch 1;
A2: for A st A c= Z & (for a,b st a in A & b in A holds a \/ b in Z) holds
union A in Z
proof
let A such that
A3: A c= Z and
A4: for a,b st a in A & b in A holds a \/ b in Z;
A5: now
let x,y;
assume that
A6: x in union A and
A7: y in union A;
consider Y1 be set such that
A8: y in Y1 and
A9: Y1 in A by A7,TARSKI:def 4;
consider X1 be set such that
A10: x in X1 and
A11: X1 in A by A6,TARSKI:def 4;
A12: x in X1 \/ Y1 by A10,XBOOLE_0:def 3;
A13: y in X1 \/ Y1 by A8,XBOOLE_0:def 3;
X1 \/ Y1 in Z by A4,A11,A9;
hence [x,y] in E by A1,A12,A13;
end;
now
let a;
assume a in A;
then a in bool X by A1,A3;
hence a c= X;
end;
then union A c= X by ZFMISC_1:76;
hence thesis by A1,A5;
end;
A14: for a,b st a in Z & b c= a holds b in Z
proof
let a,b;
assume that
A15: a in Z and
A16: b c= a;
a in bool X by A1,A15;
then
A17: b c= X by A16,XBOOLE_1:1;
for x,y st x in b & y in b holds [x,y] in E by A1,A15,A16;
hence thesis by A1,A17;
end;
( P[{}])& {} c= X;
then reconsider Z as Coherence_Space by A1,A14,A2,Def1,CLASSES1:def 1;
take Z;
let a;
thus a in Z implies for x,y st x in a & y in a holds [x,y] in E by A1;
assume
A18: for x,y st x in a & y in a holds [x,y] in E;
then a c= X by TOLER_1:18,def 1;
hence thesis by A1,A18;
end;
uniqueness
proof
let C,D;
assume that
A19: for a holds a in C iff for x,y st x in a & y in a holds [x,y] in E and
A20: for a holds a in D iff for x,y st x in a & y in a holds [x,y] in E;
thus C c= D
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in C;
then for z,y st z in xx & y in xx holds [z,y] in E by A19;
hence thesis by A20;
end;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in D;
then for z,y st z in xx & y in xx holds [z,y] in E by A20;
hence thesis by A19;
end;
end;
reserve E for Tolerance of X;
theorem
Web(CohSp(E)) = E
proof
now
let x,y be object;
thus [x,y] in Web(CohSp(E)) implies [x,y] in E
proof
assume [x,y] in Web(CohSp(E));
then
A1: {x,y} in CohSp(E) by Th5;
x in {x,y} & y in {x,y} by TARSKI:def 2;
hence thesis by A1,Def3;
end;
assume
A2: [x,y] in E;
then
A3: x in X & y in X by ZFMISC_1:87;
for u,v be set st u in {x,y} & v in {x,y} holds [u,v] in E
proof
let u,v be set;
assume that
A4: u in {x,y} and
A5: v in {x,y};
A6: v = x or v = y by A5,TARSKI:def 2;
u = x or u = y by A4,TARSKI:def 2;
hence thesis by A2,A3,A6,EQREL_1:6,TOLER_1:7;
end;
then {x,y} in CohSp(E) by Def3;
hence [x,y] in Web(CohSp(E)) by Th5;
end;
hence thesis;
end;
theorem
CohSp(Web(C)) = C
proof
thus CohSp(Web(C)) c= C
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in CohSp(Web(C));
then for y,z st y in xx & z in xx holds [y,z] in Web(C) by Def3;
hence thesis by Th7;
end;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in C;
then for y,z st y in xx & z in xx holds [y,z] in Web(C) by Th7;
hence thesis by Def3;
end;
theorem Th14:
a in CohSp(E) iff a is TolSet of E
proof
thus a in CohSp(E) implies a is TolSet of E
proof
assume a in CohSp(E);
then for x,y st x in a & y in a holds [x,y] in E by Def3;
hence thesis by TOLER_1:def 1;
end;
assume a is TolSet of E;
then for x,y st x in a & y in a holds [x,y] in E by TOLER_1:def 1;
hence thesis by Def3;
end;
theorem
CohSp(E) = TolSets E
proof
thus CohSp(E) c= TolSets E
proof
let x be object;
assume x in CohSp(E);
then x is TolSet of E by Th14;
hence thesis by TOLER_1:def 3;
end;
let x be object;
assume x in TolSets E;
then x is TolSet of E by TOLER_1:def 3;
hence thesis by Th14;
end;
begin :: Category of Coherence Spaces
definition
let X;
func CSp(X) -> set equals
{ x where x is Subset-Family of X : x is
Coherence_Space };
coherence;
end;
registration
let X;
cluster CSp(X) -> non empty;
coherence
proof
reconsider b = bool X as Subset-Family of X;
set F = { x where x is Subset-Family of X: x is Coherence_Space };
b is Coherence_Space by Th2;
then b in F;
hence thesis;
end;
end;
registration
let X be set;
cluster -> subset-closed binary_complete non empty for Element of CSp(X);
coherence
proof
let C be Element of CSp(X);
C in { x where x is Subset-Family of X : x is Coherence_Space };
then ex x be Subset-Family of X st C = x & x is Coherence_Space;
hence thesis;
end;
end;
reserve C,C1,C2 for Element of CSp(X);
theorem Th16:
{x,y} in C implies x in union C & y in union C
proof
A1: {x} c= {x,y} & {y} c= {x,y} by ZFMISC_1:7;
A2: x in {x} & y in {y} by TARSKI:def 1;
assume {x,y} in C;
hence thesis by A1,A2,TARSKI:def 4;
end;
definition
let X;
func FuncsC(X) -> set equals
union the set of all Funcs(union x,union y) where x is
Element of CSp(X), y is Element of CSp(X);
coherence;
end;
registration
let X;
cluster FuncsC(X) -> non empty functional;
coherence
proof
reconsider A = bool X as Subset-Family of X;
A is Coherence_Space by Th2;
then A in { x where x is Subset-Family of X: x is Coherence_Space};
then reconsider A as Element of CSp(X);
set F = the set of all
Funcs(union T,union TT) where T is Element of CSp(X), TT is
Element of CSp(X);
id union A in Funcs(union A,union A) & Funcs(union A,union A) in F by
FUNCT_2:9;
then reconsider UF = union F as non empty set by TARSKI:def 4;
now
let f be object;
assume f in UF;
then consider C being set such that
A1: f in C and
A2: C in F by TARSKI:def 4;
ex A,B be Element of CSp(X) st C = Funcs(union A,union B) by A2;
hence f is Function by A1;
end;
hence thesis by FUNCT_1:def 13;
end;
end;
reserve g for Element of FuncsC(X);
theorem Th17:
x in FuncsC(X) iff ex C1,C2 st (union C2 = {} implies union C1 =
{}) & x is Function of union C1,union C2
proof
set F = the set of all
Funcs(union xx,union y) where xx is Element of CSp(X), y is
Element of CSp(X);
thus x in FuncsC(X) implies ex C1,C2 st (union C2 = {} implies union C1 = {}
) & x is Function of union C1,union C2
proof
assume x in FuncsC(X);
then consider C being set such that
A1: x in C and
A2: C in F by TARSKI:def 4;
consider A,B be Element of CSp(X) such that
A3: C = Funcs(union A,union B) by A2;
take A,B;
thus thesis by A1,A3,FUNCT_2:66;
end;
given A,B be Element of CSp(X) such that
A4: ( union B={} implies union A={})& x is Function of union A,union B;
A5: Funcs(union A,union B) in F;
x in Funcs(union A,union B) by A4,FUNCT_2:8;
hence thesis by A5,TARSKI:def 4;
end;
definition
let X;
func MapsC(X) -> set equals
{ [[C,CC],f] where C is Element of CSp(X), CC is
Element of CSp(X), f is Element of FuncsC(X) : (union CC = {} implies union C =
{}) & f is Function of union C,union CC & for x,y st {x,y} in C holds {f.x,f.y}
in CC};
coherence;
end;
registration
let X;
cluster MapsC(X) -> non empty;
coherence
proof
set FV = { [[T,TT],f] where T is Element of CSp(X), TT is Element of CSp(X
), f is Element of FuncsC(X) : (union TT = {} implies union T = {} ) & f is
Function of union T,union TT & for x,y st {x,y} in T holds {f.x,f.y} in TT};
now
reconsider A = bool X as Subset-Family of X;
A is Coherence_Space by Th2;
then A in { xx where xx is Subset-Family of X: xx is Coherence_Space};
then reconsider A as Element of CSp(X);
set f = id union A;
take m = [[A,A],f];
A1: union A = {} implies union A = {};
reconsider f as Element of FuncsC(X) by Th17;
now
let x,y;
assume
A2: {x,y} in A;
then x in union A by Th16;
then
A3: f.x = x by FUNCT_1:18;
y in union A by A2,Th16;
hence {f.x,f.y} in A by A2,A3,FUNCT_1:18;
end;
hence m in FV by A1;
end;
hence thesis;
end;
end;
reserve l,l1,l2,l3 for Element of MapsC(X);
theorem Th18:
ex g,C1,C2 st l = [[C1,C2],g] & (union C2 = {} implies union C1
= {}) & g is Function of union C1,union C2 & for x,y st {x,y} in C1 holds {g.x,
g.y} in C2
proof
l in {[[C1,C2],g]: (union C2={} implies union C1={}) & g is Function of
union C1,union C2 & for x,y st {x,y} in C1 holds {g.x,g.y} in C2};
then
ex C1,C2,g st l = [[C1,C2],g] & (union C2={} implies union C1={}) & g is
Function of union C1,union C2 & for x,y st {x,y} in C1 holds {g.x,g.y} in C2;
hence thesis;
end;
theorem Th19:
for f being Function of union C1,union C2 st (union C2={}
implies union C1={}) & (for x,y st {x,y} in C1 holds {f.x,f.y} in C2) holds [[
C1,C2],f] in MapsC(X)
proof
let f be Function of union C1,union C2;
assume that
A1: union C2={} implies union C1={} and
A2: for x,y st {x,y} in C1 holds {f.x,f.y} in C2;
reconsider f9 = f as Element of FuncsC(X) by A1,Th17;
for x,y st {x,y} in C1 holds {f9.x,f9.y} in C2 by A2;
hence thesis by A1;
end;
registration
let X be set, l be Element of MapsC(X);
cluster l`2 -> Function-like Relation-like for set;
coherence
proof
consider g be Element of FuncsC(X), C1,C2 be Element of CSp(X) such that
A1: l = [[C1,C2],g] &
( union C2 = {} implies union C1 = {})& g is Function of union C1,union
C2 & for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
thus thesis by A1;
end;
end;
definition
let X,l;
func dom l -> Element of CSp(X) equals
l`1`1;
coherence
proof
consider g,C1,C2 such that
A1: l = [[C1,C2],g] and
union C2 = {} implies union C1 = {} and
g is Function of union C1,union C2 and
for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
thus thesis by A1;
end;
func cod l -> Element of CSp(X) equals
l`1`2;
coherence
proof
consider g,C1,C2 such that
A2: l = [[C1,C2],g] and
union C2 = {} implies union C1 = {} and
g is Function of union C1,union C2 and
for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
thus thesis by A2;
end;
end;
theorem Th20:
l = [[dom l,cod l],l`2]
proof
consider g,C1,C2 such that
A1: l = [[C1,C2],g] and
union C2 = {} implies union C1 = {} and
g is Function of union C1,union C2 and
for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
thus thesis by A1;
end;
Lm1: l`2 = l1`2 & dom l = dom l1 & cod l = cod l1 implies l = l1
proof
l = [[dom l,cod l],l`2] by Th20;
hence thesis by Th20;
end;
definition
let X,C;
func id$ C -> Element of MapsC(X) equals
[[C,C],id union C];
coherence
proof
set f = id union C;
now
let x,y;
assume
A1: {x,y} in C;
then x in union C by Th16;
then
A2: (id union C).x = x by FUNCT_1:18;
y in union C by A1,Th16;
hence {f.x,f.y} in C by A1,A2,FUNCT_1:18;
end;
hence thesis by Th19;
end;
end;
Lm2: for x1,y1,x2,y2,x3,y3 being set st [[x1,x2],x3] = [[y1,y2],y3] holds x1 =
y1 & x2 = y2
proof
let x1,y1,x2,y2,x3,y3 be set;
assume [[x1,x2],x3] = [[y1,y2],y3];
then [x1,x2] = [y1,y2] by XTUPLE_0:1;
hence thesis by XTUPLE_0:1;
end;
theorem Th21:
(union cod l <> {} or union dom l = {}) & l`2 is Function of
union dom l,union cod l &
for x,y st {x,y} in dom l holds {(l`2).x,(l`2).y} in cod
l
proof
consider g,C1,C2 such that
A1: l = [[C1,C2],g] and
A2: ( union C2={} implies union C1 = {})& g is Function of union C1,
union C2 and
A3: for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
A4: C2 = cod l by A1;
A5: g = l`2 & C1 = dom l by A1;
thus (union cod l <> {} or union dom l = {}) & l`2 is Function of union dom
l,union cod l by A1,A2;
let x,y;
assume {x,y} in dom l;
hence thesis by A3,A5,A4;
end;
definition
let X,l1,l2;
assume
A1: cod l1 = dom l2;
func l2*l1 -> Element of MapsC(X) equals
:Def10:
[[dom l1,cod l2],l2`2*l1`2];
coherence
proof
A2: union cod l2 <> {} or union dom l2 = {} by Th21;
A3: union cod l1 <> {} or union dom l1 = {} by Th21;
A4: l1`2 is Function of union dom l1,union cod l1 by Th21;
A5: now
let x,y;
assume
A6: {x,y} in dom l1;
then x in union dom l1 by Th16;
then
A7: x in dom l1`2 by A3,A4,FUNCT_2:def 1;
y in union dom l1 by A6,Th16;
then
A8: y in dom l1`2 by A3,A4,FUNCT_2:def 1;
{l1`2.x,l1`2.y} in cod l1 by A6,Th21;
then {l2`2.(l1`2.x),l2`2.(l1`2.y)} in cod l2 by A1,Th21;
then {(l2`2*l1`2).x,l2`2.(l1`2.y)} in cod l2 by A7,FUNCT_1:13;
hence {(l2`2*l1`2).x,(l2`2*l1`2).y} in cod l2 by A8,FUNCT_1:13;
end;
l2`2 is Function of union dom l2,union cod l2 by Th21;
then l2`2*l1`2 is Function of union dom l1,union cod l2 by A1,A3,A4,
FUNCT_2:13;
hence thesis by A1,A3,A2,A5,Th19;
end;
end;
theorem Th22:
dom l2 = cod l1 implies (l2*l1)`2 = l2`2*l1`2 & dom(l2*l1) = dom
l1 & cod(l2*l1) = cod l2
proof
assume dom l2 = cod l1;
then [[dom l1,cod l2],l2`2*l1`2] = l2*l1 by Def10
.= [[dom(l2*l1),cod(l2*l1)],(l2*l1)`2] by Th20;
hence thesis by Lm2,XTUPLE_0:1;
end;
theorem Th23:
dom l2 = cod l1 & dom l3 = cod l2 implies l3*(l2*l1) = (l3*l2)* l1
proof
assume that
A1: dom l2 = cod l1 and
A2: dom l3 = cod l2;
A3: cod(l2*l1) = cod l2 by A1,Th22;
(l2*l1)`2 = l2`2*l1`2 by A1,Th22;
then
A4: (l3*(l2*l1))`2 = l3`2*(l2`2*l1`2) by A2,A3,Th22;
A5: dom(l3*l2) = dom l2 by A2,Th22;
then
A6: dom((l3*l2)*l1) = dom l1 by A1,Th22;
dom(l2*l1) = dom l1 by A1,Th22;
then
A7: dom(l3*(l2*l1)) = dom l1 by A2,A3,Th22;
cod(l3*l2) = cod l3 by A2,Th22;
then
A8: cod((l3*l2)*l1) = cod l3 by A1,A5,Th22;
(l3*l2)`2 = l3`2*l2`2 by A2,Th22;
then
A9: ((l3*l2)*l1)`2 = (l3`2*l2`2)*l1`2 by A1,A5,Th22;
cod(l3*(l2*l1)) = cod l3 by A2,A3,Th22;
hence thesis by A4,A7,A9,A6,A8,Lm1,RELAT_1:36;
end;
theorem
(id$ C)`2 = id union C & dom id$ C = C & cod id$ C = C;
theorem Th25:
l*(id$ dom l) = l & (id$ cod l)*l = l
proof
set i1 = id$ dom l, i2 = id$ cod l;
A1: l`2 is Function of union dom l,union cod l by Th21;
then
A2: rng l`2 c= union cod l by RELAT_1:def 19;
union cod l <> {} or union dom l = {} by Th21;
then
A3: dom l`2 = union dom l by A1,FUNCT_2:def 1;
A4: cod i1 = dom l;
then
A5: cod(l*i1) = cod l by Th22;
(l*i1)`2 = l`2*i1`2 & dom(l*i1) = dom i1 by A4,Th22;
hence l*i1 = l by A3,A5,Lm1,RELAT_1:52;
A6: dom i2 = cod l;
then
A7: cod(i2*l) = cod i2 by Th22;
(i2*l)`2 = i2`2*l`2 & dom(i2*l) = dom l by A6,Th22;
hence thesis by A2,A7,Lm1,RELAT_1:53;
end;
definition
let X;
func CDom X -> Function of MapsC(X),CSp(X) means
:Def11:
for l holds it.l = dom l;
existence
proof
deffunc F(Element of MapsC(X)) = dom $1;
thus ex f being Function of MapsC(X),CSp(X) st for x being Element of
MapsC(X) holds f.x = F(x) from FUNCT_2:sch 4;
end;
uniqueness
proof
let h1,h2 be Function of MapsC(X),CSp(X) such that
A1: for l holds h1.l = dom l and
A2: for l holds h2.l = dom l;
now
let l;
thus h1.l = dom l by A1
.= h2.l by A2;
end;
hence thesis by FUNCT_2:63;
end;
func CCod X -> Function of MapsC(X),CSp(X) means
:Def12:
for l holds it.l = cod l;
existence
proof
deffunc F(Element of MapsC(X)) = cod $1;
thus ex f being Function of MapsC(X),CSp(X) st for x being Element of
MapsC(X) holds f.x = F(x) from FUNCT_2:sch 4;
end;
uniqueness
proof
let h1,h2 be Function of MapsC(X),CSp(X) such that
A3: for l holds h1.l = cod l and
A4: for l holds h2.l = cod l;
now
let l;
thus h1.l = cod l by A3
.= h2.l by A4;
end;
hence thesis by FUNCT_2:63;
end;
func CComp X -> PartFunc of [:MapsC(X),MapsC(X):],MapsC(X) means
:Def13:
(for l2,l1 holds [l2,l1] in dom it iff dom l2 = cod l1) &
for l2,l1 st dom l2 = cod l1 holds it.[l2,l1] = l2*l1;
existence
proof
defpred P[object,object,object] means
for l2,l1 st l2=$1 & l1=$2 holds dom l2 = cod
l1 & $3 = l2*l1;
A5: for x,y,z1,z2 being object st x in MapsC(X) & y in MapsC(X) & P[x,y,z1]
& P[x,y,z2] holds z1 = z2
proof
let x,y,z1,z2 be object;
assume x in MapsC(X) & y in MapsC(X);
then reconsider l2 = x, l1 = y as Element of MapsC(X);
assume that
A6: P[x,y,z1] and
A7: P[x,y,z2];
z1 = l2*l1 by A6;
hence thesis by A7;
end;
A8: for x,y,z being object st x in MapsC(X) & y in MapsC(X) & P[x,y,z] holds
z in MapsC(X)
proof
let x,y,z be object;
assume x in MapsC(X) & y in MapsC(X);
then reconsider l2 = x, l1 = y as Element of MapsC(X);
assume P[x,y,z];
then z = l2*l1;
hence thesis;
end;
consider h being PartFunc of [:MapsC(X),MapsC(X):],MapsC(X) such that
A9: for x,y being object
holds [x,y] in dom h iff x in MapsC(X) & y in MapsC(X) &
ex z being object st P[x,y,z] and
A10: for x,y being object
st [x,y] in dom h holds P[x,y,h.(x,y)] from BINOP_1:sch 5
(A8, A5);
take h;
thus
A11: for l2,l1 holds [l2,l1] in dom h iff dom l2 = cod l1
proof
let l2,l1;
thus [l2,l1] in dom h implies dom l2 = cod l1
proof
assume [l2,l1] in dom h;
then ex z being object st P[l2,l1,z] by A9;
hence thesis;
end;
assume dom l2 = cod l1;
then P[l2,l1,l2*l1];
hence thesis by A9;
end;
let l2,l1;
assume dom l2 = cod l1;
then [l2,l1] in dom h by A11;
then P[l2,l1,h.(l2,l1)] by A10;
hence thesis;
end;
uniqueness
proof
let h1,h2 be PartFunc of [:MapsC(X),MapsC(X):],MapsC(X) such that
A12: for l2,l1 holds [l2,l1] in dom h1 iff dom l2 = cod l1 and
A13: for l2,l1 st dom l2 = cod l1 holds h1.[l2,l1] = l2*l1 and
A14: for l2,l1 holds [l2,l1] in dom h2 iff dom l2 = cod l1 and
A15: for l2,l1 st dom l2 = cod l1 holds h2.[l2,l1] = l2*l1;
A16: dom h1 = dom h2
proof
let x,y be object;
thus [x,y] in dom h1 implies [x,y] in dom h2
proof
assume
A17: [x,y] in dom h1;
then reconsider l2 = x, l1 = y as Element of MapsC(X) by ZFMISC_1:87;
dom l2 = cod l1 by A12,A17;
hence thesis by A14;
end;
assume
A18: [x,y] in dom h2;
then reconsider l2 = x, l1 = y as Element of MapsC(X) by ZFMISC_1:87;
dom l2 = cod l1 by A14,A18;
hence thesis by A12;
end;
now
let l be Element of [:MapsC(X),MapsC(X):] such that
A19: l in dom h1;
consider l2,l1 be Element of MapsC(X) such that
A20: l = [l2,l1] by DOMAIN_1:1;
A21: dom l2 = cod l1 by A12,A19,A20;
then h1.[l2,l1] = l2*l1 by A13;
hence h1.l = h2.l by A15,A20,A21;
end;
hence thesis by A16,PARTFUN1:5;
end;
end;
::$CT
definition
::$CD
let X;
func CohCat(X) -> non empty non void strict CatStr equals
CatStr(# CSp(X),MapsC(X),CDom X,CCod X,CComp X #);
coherence;
end;
registration let X;
cluster CohCat X -> Category-like transitive associative reflexive;
coherence
proof
set M = MapsC(X), d = CDom X, c = CCod X, p = CComp X;
set C = CohCat X;
thus
A1: C is Category-like
proof
let ff,gg be Morphism of C;
reconsider f=ff, g=gg as Element of M;
d.gg = dom g & c.ff = cod f by Def11,Def12;
hence thesis by Def13;
end;
thus
A2: C is transitive
proof
let ff,gg be Morphism of C such that
A3: dom gg=cod ff;
[gg,ff] in dom the Comp of C by A3,A1;
then
A4: (the Comp of C).(gg,ff) = gg(*)ff by CAT_1:def 1;
reconsider f=ff, g=gg as Element of M;
A5: d.g = dom g & c.f = cod f by Def11,Def12;
then
A6: p.[g,f] = g*f by A3,Def13;
A7: d.f = dom f & c.g = cod g by Def11,Def12;
dom(g*f) = dom f & cod(g*f) = cod g by A3,A5,Th22;
hence thesis by A6,A7,Def11,Def12,A4;
end;
thus
C is associative
proof
let ff,gg,hh be Morphism of C such that
A8: dom hh = cod gg and
A9: dom gg = cod ff;
reconsider f=ff, g=gg, h=hh as Element of M;
A10: dom h = d.h & cod g = c.g by Def11,Def12;
then
A11: dom(h*g) = dom g by A8,Th22;
A12: dom g = d.g & cod f = c.f by Def11,Def12;
then
A13: cod(g*f) = dom h by A8,A9,A10,Th22;
[hh,gg] in dom the Comp of C by A1,A8;
then
A14: hh(*)gg =(the Comp of C).(hh,gg) by CAT_1:def 1;
dom(hh(*)gg) = dom gg by A2,A8;
then
A15: [hh(*)gg,ff] in dom the Comp of C by A1,A9;
[gg,ff] in dom the Comp of C by A1,A9;
then
A16: gg(*)ff =(the Comp of C).(gg,ff) by CAT_1:def 1;
cod(gg(*)ff) = cod gg by A2,A9;
then [hh,gg(*)ff] in dom the Comp of C by A1,A8;
hence hh(*)(gg(*)ff)
= (the Comp of C).(hh,(the Comp of C).(gg,ff)) by A16,CAT_1:def 1
.= p.[h,g*f] by A9,A12,Def13
.= h*(g*f) by A13,Def13
.= (h*g)*f by A8,A9,A10,A12,Th23
.= p.[h*g,f] by A9,A12,A11,Def13
.= (the Comp of C).((the Comp of C).(hh,gg),ff) by A8,A10,Def13
.= hh(*)gg(*)ff by A14,A15,CAT_1:def 1;
end;
let a be Object of C;
reconsider aa = a as Element of CSp X;
reconsider ii = id$ aa as Morphism of C;
A17: cod ii = cod id$ aa by Def12 .= aa;
dom ii = dom id$ aa by Def11 .= aa;
then id$ aa in Hom(a,a) by A17;
hence Hom(a,a)<>{};
end;
end;
Lm3:
for a being Element of CohCat X, aa being Element of CSp X st a = aa
for i being Morphism of a,a st i = id$ aa
for b being Element of CohCat X holds
(Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g) &
(Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f)
proof let a be Element of CohCat X, aa be Element of CSp X such that
A1: a = aa;
let i be Morphism of a,a such that
A2: i = id$ aa;
let b be Element of CohCat X;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g
proof assume
A3: Hom(a,b)<>{};
let g be Morphism of a,b;
reconsider gg = g as Element of MapsC X;
Hom(a,a)<>{};
then
A4: cod i = a by CAT_1:5 .= dom g by A3,CAT_1:5;
A5: dom gg = dom g by Def11 .= aa by A1,A3,CAT_1:5;
then
A6: cod id$ aa = dom gg;
[g,i] in dom the Comp of CohCat X by A4,CAT_1:def 6;
hence g(*)i = (the Comp of CohCat X).(g,i) by CAT_1:def 1
.= gg*id$ aa by A6,A2,Def13
.= g by A5,Th25;
end;
thus Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f
proof assume
A7: Hom(b,a)<>{};
let g be Morphism of b,a;
reconsider gg = g as Element of MapsC X;
Hom(a,a)<>{};
then
A8: dom i = a by CAT_1:5 .= cod g by A7,CAT_1:5;
A9: cod gg = cod g by Def12 .= aa by A1,A7,CAT_1:5;
then
A10: dom id$ aa = cod gg;
[i,g] in dom the Comp of CohCat X by A8,CAT_1:def 6;
hence i(*)g = (the Comp of CohCat X).(i,g) by CAT_1:def 1
.= (id$ aa)*gg by A2,A10,Def13
.= g by A9,Th25;
end;
end;
registration let X;
cluster CohCat X -> with_identities;
coherence
proof let a being Element of CohCat X;
reconsider aa = a as Element of CSp X;
reconsider ii = id$ aa as Morphism of CohCat X;
A1: cod ii = cod id$ aa by Def12 .= aa;
dom ii = dom id$ aa by Def11 .= aa;
then ii in Hom(a,a) by A1;
then reconsider ii as Morphism of a,a by CAT_1:def 5;
take ii;
thus thesis by Lm3;
end;
end;
begin :: Category of Tolerances
definition
let X be set;
func Toler(X) -> set means
:Def15:
x in it iff x is Tolerance of X;
existence
proof
defpred P[object] means $1 is Tolerance of X;
consider a such that
A1: for x being object
holds x in a iff x in bool [:X,X:] & P[x] from XBOOLE_0:sch
1;
take a;
let x;
thus x in a implies x is Tolerance of X by A1;
assume x is Tolerance of X;
hence thesis by A1;
end;
uniqueness
proof
let a,b be set;
assume that
A2: x in a iff x is Tolerance of X and
A3: x in b iff x is Tolerance of X;
now
let x be object;
A4: now
assume x in b;
then x is Tolerance of X by A3;
hence x in a by A2;
end;
now
assume x in a;
then x is Tolerance of X by A2;
hence x in b by A3;
end;
hence x in a iff x in b by A4;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let X be set;
cluster Toler(X) -> non empty;
coherence
proof
set T = the Tolerance of X;
T in Toler X by Def15;
hence thesis;
end;
end;
definition
let X be set;
func Toler_on_subsets(X) -> set equals
union the set of all Toler(Y) where Y is Subset of
X;
coherence;
end;
registration
let X be set;
cluster Toler_on_subsets(X) -> non empty;
coherence
proof
set F = the set of all Toler(Y) where Y is Subset of X;
{} c= X;
then
A1: Toler({}) in F;
{} in Toler({}) by Def15,TOLER_1:14;
hence thesis by A1,TARSKI:def 4;
end;
end;
theorem
x in Toler_on_subsets(X) iff ex A st A c= X & x is Tolerance of A
proof
set f = the set of all Toler(Y) where Y is Subset of X;
thus x in Toler_on_subsets(X) implies ex A st A c= X & x is Tolerance of A
proof
assume x in Toler_on_subsets(X);
then consider a such that
A1: x in a and
A2: a in f by TARSKI:def 4;
consider Y be Subset of X such that
A3: a = Toler(Y) by A2;
take Y;
thus thesis by A1,A3,Def15;
end;
given A such that
A4: A c= X and
A5: x is Tolerance of A;
reconsider A as Subset of X by A4;
A6: Toler(A) in f;
x in Toler(A) by A5,Def15;
hence thesis by A6,TARSKI:def 4;
end;
theorem
Total a in Toler(a) by Def15;
theorem Th28:
{} in Toler_on_subsets(X)
proof
set F = the set of all Toler(Y) where Y is Subset of X;
{} c= X;
then
A1: Toler({}) in F;
{} in Toler({}) by Def15,TOLER_1:14;
hence thesis by A1,TARSKI:def 4;
end;
theorem Th29:
a c= X implies Total a in Toler_on_subsets(X)
proof
set F = the set of all Toler(Y) where Y is Subset of X;
assume a c= X;
then
A1: Toler(a) in F;
Total a in Toler(a) by Def15;
hence thesis by A1,TARSKI:def 4;
end;
theorem Th30:
a c= X implies id a in Toler_on_subsets(X)
proof
set F = the set of all Toler(Y) where Y is Subset of X;
assume a c= X;
then
A1: Toler(a) in F;
id a in Toler(a) by Def15;
hence thesis by A1,TARSKI:def 4;
end;
theorem
Total X in Toler_on_subsets(X) by Th29;
theorem
id X in Toler_on_subsets(X) by Th30;
definition
let X;
func TOL(X) -> set equals
{ [t,Y] where t is Element of Toler_on_subsets(X),
Y is Subset of X : t is Tolerance of Y};
coherence;
end;
registration
let X;
cluster TOL(X) -> non empty;
coherence
proof
set FV = { [t,Y] where t is Element of Toler_on_subsets(X), Y is Subset of
X: t is Tolerance of Y};
now
reconsider o = {} as Subset of X by XBOOLE_1:2;
reconsider e = {} as Element of Toler_on_subsets(X) by Th28;
take m = [e,o];
thus m in FV by TOLER_1:14;
end;
hence thesis;
end;
end;
reserve T,T1,T2 for Element of TOL(X);
theorem
[{},{}] in TOL(X)
proof
{} in Toler_on_subsets(X) & {} c= X by Th28;
hence thesis by TOLER_1:14;
end;
theorem Th34:
a c= X implies [id a,a] in TOL(X)
proof
assume
A1: a c= X;
then id a in Toler_on_subsets(X) by Th30;
hence thesis by A1;
end;
theorem Th35:
a c= X implies [Total a,a] in TOL(X)
proof
assume
A1: a c= X;
then Total a in Toler_on_subsets(X) by Th29;
hence thesis by A1;
end;
theorem
[id X,X] in TOL(X) by Th34;
theorem
[Total X,X] in TOL(X) by Th35;
definition
let X,T;
redefine func T`2 -> Subset of X; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
T in { [t,Y] where t is Element of Toler_on_subsets(X), Y is Subset of
X: t is Tolerance of Y};
then consider t be Element of Toler_on_subsets(X),Y be Subset of X
such that
A1: T = [t,Y] & t is Tolerance of Y;
thus thesis by A1;
end;
redefine func T`1 -> Tolerance of T`2; :: redefines `1 (XTUPLE_0, definition)
coherence
proof
T in { [t,Y] where t is Element of Toler_on_subsets(X), Y is Subset of
X: t is Tolerance of Y};
then consider
t be Element of Toler_on_subsets(X),Y be Subset of X such that
A2: T = [t,Y] and
A3: t is Tolerance of Y;
thus thesis by A2,A3;
end;
end;
definition
let X;
func FuncsT(X) -> set equals
union the set of all Funcs(T`2,TT`2) where T is Element of
TOL(X), TT is Element of TOL(X);
coherence;
end;
registration
let X;
cluster FuncsT(X) -> non empty functional;
coherence
proof
set F = the set of all
Funcs(T`2,TT`2) where T is Element of TOL(X), TT is Element of
TOL(X);
reconsider T = [Total {}X,{}X] as Element of TOL(X) by Th35;
A1: id {}X in Funcs(T`2,T`2) by FUNCT_2:9;
Funcs(T`2,T`2) in F;
then reconsider UF = union F as non empty set by A1,TARSKI:def 4;
now
let f be object;
assume f in UF;
then consider C being set such that
A2: f in C and
A3: C in F by TARSKI:def 4;
ex A,B be Element of TOL(X) st C = Funcs(A`2,B`2) by A3;
hence f is Function by A2;
end;
hence thesis by FUNCT_1:def 13;
end;
end;
reserve f for Element of FuncsT(X);
theorem Th38:
x in FuncsT(X) iff ex T1,T2 st (T2`2 = {} implies T1`2 = {}) & x
is Function of T1`2,T2`2
proof
set F = the set of all
Funcs(T`2,TT`2) where T is Element of TOL(X), TT is Element of TOL
(X);
thus x in FuncsT(X) implies ex A,B be Element of TOL(X) st (B`2={} implies A
`2={}) & x is Function of A`2,B`2
proof
assume x in FuncsT(X);
then consider C being set such that
A1: x in C and
A2: C in F by TARSKI:def 4;
consider A,B be Element of TOL(X) such that
A3: C = Funcs(A`2,B`2) by A2;
take A,B;
thus thesis by A1,A3,FUNCT_2:66;
end;
given A,B be Element of TOL(X) such that
A4: ( B`2={} implies A`2={})& x is Function of A`2,B`2;
A5: Funcs(A`2,B`2) in F;
x in Funcs(A`2,B`2) by A4,FUNCT_2:8;
hence thesis by A5,TARSKI:def 4;
end;
definition
let X;
func MapsT(X) -> set equals
{ [[T,TT],f] where T is Element of TOL(X), TT is
Element of TOL(X), f is Element of FuncsT(X) : (TT`2 = {} implies T`2 = {}) & f
is Function of T`2,TT`2 & for x,y st [x,y] in T`1 holds [f.x,f.y] in TT`1};
coherence;
end;
registration
let X;
cluster MapsT(X) -> non empty;
coherence
proof
set FV = { [[T,TT],f] where T is Element of TOL(X), TT is Element of TOL(X
), f is Element of FuncsT(X) : (TT`2 = {} implies T`2 = {}) & f is Function of
T`2,TT`2 & for x,y st [x,y] in T`1 holds [f.x,f.y] in TT`1};
now
set a = [Total {}X,{}X], f = id a`2;
take m = [[a,a],f];
reconsider a as Element of TOL(X) by Th35;
a`2 = {} implies a`2 = {};
then reconsider f as Element of FuncsT(X) by Th38;
for x,y st [x,y] in a`1 holds [f.x,f.y] in a`1;
hence m in FV;
end;
hence thesis;
end;
end;
reserve m,m1,m2,m3 for Element of MapsT(X);
theorem Th39:
ex f,T1,T2 st m = [[T1,T2],f] & (T2`2 = {} implies T1`2 = {}) &
f is Function of T1`2,T2`2 & for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1
proof
m in {[[T1,T2],f]: (T2`2={} implies T1`2={}) & f is Function of T1`2,T2
`2 & for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1};
then ex T1,T2,f st m = [[T1,T2],f] & (T2`2={} implies T1`2={}) & f is
Function of T1`2,T2`2 & for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1;
hence thesis;
end;
theorem Th40:
for f being Function of T1`2,T2`2 st (T2`2={} implies T1`2={}) &
(for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1) holds [[T1,T2],f] in MapsT(X
)
proof
let f be Function of T1`2,T2`2;
assume that
A1: T2`2={} implies T1`2={} and
A2: for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1;
reconsider f9 = f as Element of FuncsT(X) by A1,Th38;
for x,y st [x,y] in T1`1 holds [f9.x,f9.y] in T2`1 by A2;
hence thesis by A1;
end;
registration
let X be set,m be Element of MapsT(X);
cluster m`2 -> Function-like Relation-like for set;
coherence
proof
consider f be Element of FuncsT(X), T1,T2 be Element of TOL(X) such that
A1: m = [[T1,T2],f] &
( T2`2 = {} implies T1`2 = {})& f is Function of T1`2,T2`2 & for x,y st [
x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th39;
thus thesis by A1;
end;
end;
definition
let X,m;
func dom m -> Element of TOL(X) equals
m`1`1;
coherence
proof
consider f,T1,T2 such that
A1: m = [[T1,T2],f] and
T2`2 = {} implies T1`2 = {} and
f is Function of T1`2,T2`2 and
for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th39;
thus thesis by A1;
end;
func cod m -> Element of TOL(X) equals
m`1`2;
coherence
proof
consider f be Element of FuncsT(X),T1,T2 such that
A2: m = [[T1,T2],f] and
T2`2 = {} implies T1`2 = {} and
f is Function of T1`2,T2`2 and
for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th39;
thus thesis by A2;
end;
end;
theorem Th41:
m = [[dom m,cod m],m`2]
proof
consider f,T1,T2 such that
A1: m = [[T1,T2],f] and
T2`2 = {} implies T1`2 = {} and
f is Function of T1`2,T2`2 and
for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th39;
thus thesis by A1;
end;
Lm4: m`2 = m1`2 & dom m = dom m1 & cod m = cod m1 implies m = m1
proof
m = [[dom m,cod m],m`2] by Th41;
hence thesis by Th41;
end;
definition
let X,T;
func id$ T -> Element of MapsT(X) equals
[[T,T],id T`2];
coherence
proof
set f = id T`2;
now
let x,y;
assume
A1: [x,y] in T`1;
then x in T`2 by ZFMISC_1:87;
then
A2: (id T`2).x = x by FUNCT_1:18;
y in T`2 by A1,ZFMISC_1:87;
hence [f.x,f.y] in T`1 by A1,A2,FUNCT_1:18;
end;
hence thesis by Th40;
end;
end;
theorem Th42:
((cod m)`2 <> {} or (dom m)`2 = {}) & m`2 is Function of (dom m)
`2,(cod m)`2 & for x,y st [x,y] in (dom m)`1 holds [m`2.x,m`2.y] in (cod m)`1
proof
consider f,T1,T2 such that
A1: m = [[T1,T2],f] and
A2: ( T2`2 = {} implies T1`2 = {})& f is Function of T1`2,T2`2 and
A3: for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th39;
A4: T2 = cod m by A1;
A5: f = m`2 & T1 = dom m by A1;
thus
((cod m)`2<>{} or (dom m)`2={} ) & m`2 is Function of (dom m)`2,(cod m)
`2 by A1,A2;
let x,y;
assume [x,y] in (dom m)`1;
hence thesis by A3,A5,A4;
end;
definition
let X,m1,m2;
assume
A1: cod m1 = dom m2;
func m2*m1 -> Element of MapsT(X) equals
:Def23:
[[dom m1,cod m2],m2`2*m1`2];
coherence
proof
A2: (cod m2)`2 <> {} or (dom m2)`2 = {} by Th42;
A3: (cod m1)`2 <> {} or (dom m1)`2 = {} by Th42;
A4: m1`2 is Function of (dom m1)`2,(cod m1)`2 by Th42;
A5: now
let x,y;
assume
A6: [x,y] in (dom m1)`1;
then x in (dom m1)`2 by ZFMISC_1:87;
then
A7: x in dom m1`2 by A3,A4,FUNCT_2:def 1;
y in (dom m1)`2 by A6,ZFMISC_1:87;
then
A8: y in dom m1`2 by A3,A4,FUNCT_2:def 1;
[m1`2.x,m1`2.y] in (cod m1)`1 by A6,Th42;
then [m2`2.(m1`2.x),m2`2.(m1`2.y)] in (cod m2)`1 by A1,Th42;
then [(m2`2*m1`2).x,m2`2.(m1`2.y)] in (cod m2)`1 by A7,FUNCT_1:13;
hence [(m2`2*m1`2).x,(m2`2*m1`2).y] in (cod m2)`1 by A8,FUNCT_1:13;
end;
m2`2 is Function of (dom m2)`2,(cod m2)`2 by Th42;
then m2`2*m1`2 is Function of (dom m1)`2,(cod m2)`2 by A1,A3,A4,FUNCT_2:13;
hence thesis by A1,A3,A2,A5,Th40;
end;
end;
theorem Th43:
dom m2 = cod m1 implies (m2*m1)`2 = m2`2*m1`2 & dom(m2*m1) = dom
m1 & cod(m2*m1) = cod m2
proof
assume dom m2 = cod m1;
then [[dom m1,cod m2],m2`2*m1`2] = m2*m1 by Def23
.= [[dom(m2*m1),cod(m2*m1)],(m2*m1)`2] by Th41;
hence thesis by Lm2,XTUPLE_0:1;
end;
theorem Th44:
dom m2 = cod m1 & dom m3 = cod m2 implies m3*(m2*m1) = (m3*m2)* m1
proof
assume that
A1: dom m2 = cod m1 and
A2: dom m3 = cod m2;
A3: cod(m2*m1) = cod m2 by A1,Th43;
(m2*m1)`2 = m2`2*m1`2 by A1,Th43;
then
A4: (m3*(m2*m1))`2 = m3`2*(m2`2*m1`2) by A2,A3,Th43;
A5: dom(m3*m2) = dom m2 by A2,Th43;
then
A6: dom((m3*m2)*m1) = dom m1 by A1,Th43;
dom(m2*m1) = dom m1 by A1,Th43;
then
A7: dom(m3*(m2*m1)) = dom m1 by A2,A3,Th43;
cod(m3*m2) = cod m3 by A2,Th43;
then
A8: cod((m3*m2)*m1) = cod m3 by A1,A5,Th43;
(m3*m2)`2 = m3`2*m2`2 by A2,Th43;
then
A9: ((m3*m2)*m1)`2 = (m3`2*m2`2)*m1`2 by A1,A5,Th43;
cod(m3*(m2*m1)) = cod m3 by A2,A3,Th43;
hence thesis by A4,A7,A9,A6,A8,Lm4,RELAT_1:36;
end;
theorem
(id$ T)`2 = id T`2 & dom id$ T = T & cod id$ T = T;
theorem Th46:
m*(id$ dom m) = m & (id$ cod m)*m = m
proof
set i1 = id$ dom m, i2 = id$ cod m;
A1: m`2 is Function of (dom m)`2,(cod m)`2 by Th42;
then
A2: rng m`2 c= (cod m)`2 by RELAT_1:def 19;
(cod m)`2 <> {} or (dom m)`2 = {} by Th42;
then
A3: dom m`2 = (dom m)`2 by A1,FUNCT_2:def 1;
A4: cod i1 = dom m;
then
A5: cod(m*i1) = cod m by Th43;
(m*i1)`2 = m`2*i1`2 & dom(m*i1) = dom i1 by A4,Th43;
hence m*i1 = m by A3,A5,Lm4,RELAT_1:52;
A6: dom i2 = cod m;
then
A7: cod(i2*m) = cod i2 by Th43;
(i2*m)`2 = i2`2*m`2 & dom(i2*m) = dom m by A6,Th43;
hence thesis by A2,A7,Lm4,RELAT_1:53;
end;
definition
let X;
func fDom X -> Function of MapsT(X),TOL(X) means
:Def24:
for m holds it.m = dom m;
existence
proof
deffunc F(Element of MapsT(X)) = dom $1;
thus ex f being Function of MapsT(X),TOL(X) st for x being Element of
MapsT(X) holds f.x = F(x) from FUNCT_2:sch 4;
end;
uniqueness
proof
let h1,h2 be Function of MapsT(X),TOL(X) such that
A1: for m holds h1.m = dom m and
A2: for m holds h2.m = dom m;
now
let m;
thus h1.m = dom m by A1
.= h2.m by A2;
end;
hence thesis by FUNCT_2:63;
end;
func fCod X -> Function of MapsT(X),TOL(X) means
:Def25:
for m holds it.m = cod m;
existence
proof
deffunc F(Element of MapsT(X)) = cod $1;
thus ex f being Function of MapsT(X),TOL(X) st for x being Element of
MapsT(X) holds f.x = F(x) from FUNCT_2:sch 4;
end;
uniqueness
proof
let h1,h2 be Function of MapsT(X),TOL(X) such that
A3: for m holds h1.m = cod m and
A4: for m holds h2.m = cod m;
now
let m;
thus h1.m = cod m by A3
.= h2.m by A4;
end;
hence thesis by FUNCT_2:63;
end;
func fComp X -> PartFunc of [:MapsT(X),MapsT(X):],MapsT(X) means
:Def26:
(
for m2,m1 holds [m2,m1] in dom it iff dom m2 = cod m1) & for m2,m1 st dom m2 =
cod m1 holds it.[m2,m1] = m2*m1;
existence
proof
defpred P[object,object,object] means
for m2,m1 st m2=$1 & m1=$2 holds dom m2 = cod
m1 & $3 = m2*m1;
A5: for x,y,z1,z2 being object st x in MapsT(X) & y in MapsT(X) & P[x,y,z1]
& P[x,y,z2] holds z1 = z2
proof
let x,y,z1,z2 be object;
assume x in MapsT(X) & y in MapsT(X);
then reconsider m2 = x, m1 = y as Element of MapsT(X);
assume that
A6: P[x,y,z1] and
A7: P[x,y,z2];
z1 = m2*m1 by A6;
hence thesis by A7;
end;
A8: for x,y,z being object st x in MapsT(X) & y in MapsT(X) & P[x,y,z] holds
z in MapsT(X)
proof
let x,y,z be object;
assume x in MapsT(X) & y in MapsT(X);
then reconsider m2 = x, m1 = y as Element of MapsT(X);
assume P[x,y,z];
then z = m2*m1;
hence thesis;
end;
consider h being PartFunc of [:MapsT(X),MapsT(X):],MapsT(X) such that
A9: for x,y being object
holds [x,y] in dom h iff x in MapsT(X) & y in MapsT(X) &
ex z being object st P[x,y,z] and
A10: for x,y being object st [x,y] in dom h holds P[x,y,h.(x,y)]
from BINOP_1:sch 5
(A8, A5);
take h;
thus
A11: for m2,m1 holds [m2,m1] in dom h iff dom m2 = cod m1
proof
let m2,m1;
thus [m2,m1] in dom h implies dom m2 = cod m1
proof
assume [m2,m1] in dom h;
then ex z being object st P[m2,m1,z] by A9;
hence thesis;
end;
assume dom m2 = cod m1;
then P[m2,m1,m2*m1];
hence thesis by A9;
end;
let m2,m1;
assume dom m2 = cod m1;
then [m2,m1] in dom h by A11;
then P[m2,m1,h.(m2,m1)] by A10;
hence thesis;
end;
uniqueness
proof
let h1,h2 be PartFunc of [:MapsT(X),MapsT(X):],MapsT(X) such that
A12: for m2,m1 holds [m2,m1] in dom h1 iff dom m2 = cod m1 and
A13: for m2,m1 st dom m2 = cod m1 holds h1.[m2,m1] = m2*m1 and
A14: for m2,m1 holds [m2,m1] in dom h2 iff dom m2 = cod m1 and
A15: for m2,m1 st dom m2 = cod m1 holds h2.[m2,m1] = m2*m1;
A16: dom h1 = dom h2
proof
let x,y be object;
thus [x,y] in dom h1 implies [x,y] in dom h2
proof
assume
A17: [x,y] in dom h1;
then reconsider m2 = x, m1 = y as Element of MapsT(X) by ZFMISC_1:87;
dom m2 = cod m1 by A12,A17;
hence thesis by A14;
end;
assume
A18: [x,y] in dom h2;
then reconsider m2 = x, m1 = y as Element of MapsT(X) by ZFMISC_1:87;
dom m2 = cod m1 by A14,A18;
hence thesis by A12;
end;
now
let m be Element of [:MapsT(X),MapsT(X):] such that
A19: m in dom h1;
consider m2,m1 be Element of MapsT(X) such that
A20: m = [m2,m1] by DOMAIN_1:1;
A21: dom m2 = cod m1 by A12,A19,A20;
then h1.[m2,m1] = m2*m1 by A13;
hence h1.m = h2.m by A15,A20,A21;
end;
hence thesis by A16,PARTFUN1:5;
end;
end;
definition
::$CD
let X;
func TolCat(X) -> non empty non void strict CatStr equals
CatStr(# TOL(X),MapsT(X),fDom X,fCod X,fComp X#);
coherence;
end;
registration
let X;
cluster TolCat(X) -> Category-like transitive associative reflexive;
coherence
proof set C = TolCat X;
set M = MapsT(X), d = fDom X, c = fCod X, p = fComp X;
thus A1: C is Category-like
proof
let ff,gg be Morphism of C;
reconsider f=ff, g=gg as Element of M;
d.g = dom g & c.f = cod f by Def24,Def25;
hence thesis by Def26;
end;
thus A2: C is transitive
proof
let ff,gg be Morphism of C such that
A3: dom gg=cod ff;
[gg,ff] in dom the Comp of C by A3,A1;
then
A4: (the Comp of C).(gg,ff) = gg(*)ff by CAT_1:def 1;
reconsider f=ff, g=gg as Element of M;
A5: d.g = dom g & c.f = cod f by Def24,Def25;
then
A6: p.[g,f] = g*f by A3,Def26;
A7: d.f = dom f & c.g = cod g by Def24,Def25;
dom(g*f) = dom f & cod(g*f) = cod g by A3,A5,Th43;
hence thesis by A6,A7,Def24,Def25,A4;
end;
thus C is associative
proof
let ff,gg,hh be Morphism of C such that
A8: dom hh = cod gg and
A9: dom gg = cod ff;
reconsider f=ff, g=gg, h=hh as Element of M;
A10: dom h = d.h & cod g = c.g by Def24,Def25;
then
A11: dom(h*g) = dom g by A8,Th43;
A12: dom g = d.g & cod f = c.f by Def24,Def25;
then
A13: cod(g*f) = dom h by A8,A9,A10,Th43;
[hh,gg] in dom the Comp of C by A8,A1;
then
A14: hh(*)gg = (the Comp of C).(hh,gg) by CAT_1:def 1;
[gg,ff] in dom the Comp of C by A9,A1;
then
A15: gg(*)ff = (the Comp of C).(gg,ff) by CAT_1:def 1;
dom(hh(*)gg) = dom gg by A2,A8;
then
A16: [hh(*)gg,ff] in dom the Comp of C by A1,A9;
cod(gg(*)ff) = cod gg by A2,A9;
then [hh,gg(*)ff] in dom the Comp of C by A1,A8;
hence hh(*)(gg(*)ff)
= (the Comp of C).(hh,(the Comp of C).(gg,ff)) by A15,CAT_1:def 1
.= p.[h,g*f] by A9,A12,Def26
.= h*(g*f) by A13,Def26
.= (h*g)*f by A8,A9,A10,A12,Th44
.= p.[h*g,f] by A9,A12,A11,Def26
.= (the Comp of C).((the Comp of C).(hh,gg),ff) by A8,A10,Def26
.= hh(*)gg(*)ff by A14,A16,CAT_1:def 1;
end;
let a be Object of C;
reconsider aa = a as Element of TOL X;
reconsider ii = id$ aa as Morphism of C;
A17: cod ii = cod id$ aa by Def25 .= aa;
dom ii = dom id$ aa by Def24 .= aa;
then id$ aa in Hom(a,a) by A17;
hence Hom(a,a)<>{};
end;
end;
Lm5:
for a being Element of TolCat X, aa being Element of TOL X st a = aa
for i being Morphism of a,a st i = id$ aa
for b being Element of TolCat X holds
(Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g) &
(Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f)
proof let a be Element of TolCat X, aa be Element of TOL X such that
A1: a = aa;
let i be Morphism of a,a such that
A2: i = id$ aa;
let b be Element of TolCat X;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g
proof assume
A3: Hom(a,b)<>{};
let g be Morphism of a,b;
reconsider gg = g as Element of MapsT X;
Hom(a,a)<>{};
then
A4: cod i = a by CAT_1:5 .= dom g by A3,CAT_1:5;
A5: dom gg = dom g by Def24 .= aa by A1,A3,CAT_1:5;
then
A6: cod id$ aa = dom gg;
[g,i] in dom the Comp of TolCat X by A4,CAT_1:def 6;
hence g(*)i = (the Comp of TolCat X).(g,i) by CAT_1:def 1
.= gg*id$ aa by A6,A2,Def26
.= g by A5,Th46;
end;
thus Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f
proof assume
A7: Hom(b,a)<>{};
let g be Morphism of b,a;
reconsider gg = g as Element of MapsT X;
Hom(a,a)<>{};
then
A8: dom i = a by CAT_1:5 .= cod g by A7,CAT_1:5;
A9: cod gg = cod g by Def25 .= aa by A1,A7,CAT_1:5;
then
A10: dom id$ aa = cod gg;
[i,g] in dom the Comp of TolCat X by A8,CAT_1:def 6;
hence i(*)g = (the Comp of TolCat X).(i,g) by CAT_1:def 1
.= (id$ aa)*gg by A2,A10,Def26
.= g by A9,Th46;
end;
end;
registration
let X;
cluster TolCat(X) -> with_identities;
coherence
proof let a being Element of TolCat X;
reconsider aa = a as Element of TOL X;
reconsider ii = id$ aa as Morphism of TolCat X;
A1: cod ii = cod id$ aa by Def25 .= aa;
dom ii = dom id$ aa by Def24 .= aa;
then ii in Hom(a,a) by A1;
then reconsider ii as Morphism of a,a by CAT_1:def 5;
take ii;
thus thesis by Lm5;
end;
end;