:: Algebra of Morphisms
:: by Grzegorz Bancerek
::
:: Received January 28, 1997
:: Copyright (c) 1997-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 FUNCT_1, PBOOLE, RELAT_1, FUNCOP_1, CARD_3, TARSKI, FUNCT_6,
MEMBER_1, XBOOLE_0, FINSEQ_1, MSUALG_1, STRUCT_0, PROB_2, MSAFREE, NAT_1,
ZFMISC_1, CARD_1, FINSEQ_2, MCART_1, SUBSET_1, ORDINAL4, MSUALG_6, CAT_5,
INSTALG1, NUMBERS, MARGREL1, CAT_1, PUA2MSS1, GRAPH_1, PARTFUN1,
MSUALG_3, CATALG_1, MONOID_0;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1,
ORDINAL1, NUMBERS, MCART_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, FUNCOP_1, NAT_1, MSAFREE1, FINSEQ_1, FINSEQ_2, CARD_3, FINSEQ_4,
FUNCT_6, STRUCT_0, PBOOLE, MSUALG_1, MSUALG_3, MSAFREE, PUA2MSS1,
MSUALG_6, INSTALG1, GRAPH_1, CAT_1;
constructors ENUMSET1, FINSEQ_4, CAT_1, MSUALG_3, MSAFREE1, PUA2MSS1,
MSUALG_6, INSTALG1, RELSET_1, XTUPLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FUNCOP_1, FINSEQ_1, FINSEQ_2, STRUCT_0, MSUALG_1, RELSET_1, MSAFREE,
INSTALG1, MSAFREE1, MSSUBFAM, PBOOLE, XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, STRUCT_0, MSUALG_3, PUA2MSS1, MSUALG_6, INSTALG1, PROB_2,
MSAFREE1, XBOOLE_0, FUNCOP_1, PBOOLE;
equalities TARSKI, MSUALG_1, FUNCOP_1, CAT_1;
expansions TARSKI, XBOOLE_0, PBOOLE;
theorems TARSKI, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
FINSEQ_3, FUNCT_3, MCART_1, ENUMSET1, FUNCT_6, FINSEQ_4, MONOID_1,
CARD_3, PBOOLE, PRALG_2, MSUALG_3, INSTALG1, CAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, FUNCOP_1, PARTFUN1, CARD_1, XTUPLE_0, FUNCT_5;
schemes FUNCT_1, CLASSES1, PBOOLE, XBOOLE_0;
begin :: Preliminaries
definition
let I be set;
let A,f be Function;
func f-MSF(I,A) -> ManySortedFunction of I means
: Def1:
for i being object st i in I holds it.i = f|(A.i);
existence
proof
deffunc f(object) = f|(A.$1);
consider F being ManySortedSet of I such that
A1: for i being object st i in I holds F.i = f(i) from PBOOLE:sch 4;
F is Function-yielding
proof
let x be object;
assume x in dom F;
then x in I;
then F.x = f|(A.x) by A1;
hence thesis;
end;
hence thesis by A1;
end;
uniqueness
proof
let g1,g2 be ManySortedFunction of I such that
A2: for i being object st i in I holds g1.i = f|(A.i) and
A3: for i being object st i in I holds g2.i = f|(A.i);
now
let i be object;
assume
A4: i in I;
then g1.i = f|(A.i) by A2;
hence g1.i = g2.i by A3,A4;
end;
hence thesis;
end;
end;
theorem
for I being set, A being ManySortedSet of I holds (id Union A)-MSF(I,A
) = id A
proof
let I be set, A be ManySortedSet of I;
set f = id Union A, F = f-MSF(I,A);
now
let i be object;
A1: Union A = union rng A by CARD_3:def 4;
assume
A2: i in I;
then i in dom A by PARTFUN1:def 2;
then
A3: A.i in rng A by FUNCT_1:def 3;
F.i = f|(A.i) & (id A).i = id (A.i) by A2,Def1,MSUALG_3:def 1;
hence F.i = (id A).i by A3,A1,FUNCT_3:1,ZFMISC_1:74;
end;
hence thesis;
end;
theorem
for I being set, A,B being ManySortedSet of I for f,g being Function
st rngs (f-MSF(I,A)) c= B holds (g*f)-MSF(I,A) = (g-MSF(I,B))**(f-MSF(I,A))
proof
let I be set, A,B be ManySortedSet of I;
let f,g be Function such that
A1: rngs (f-MSF(I,A)) c= B;
A2: I /\ I = I;
dom (g-MSF(I,B)) = I & dom (f-MSF(I,A)) = I by PARTFUN1:def 2;
then
A3: dom ((g-MSF(I,B))**(f-MSF(I,A))) = I by A2,PBOOLE:def 19;
A4: now
let i be object;
assume
A5: i in I;
then
A6: (f-MSF(I,A)).i = f|(A.i) by Def1;
dom (f-MSF(I,A)) = I by PARTFUN1:def 2;
then (rngs (f-MSF(I,A))).i = rng (f|(A.i)) by A5,A6,FUNCT_6:22;
then rng (f|(A.i)) c= B.i by A1,A5;
then (g*f)|(A.i) = g*(f|(A.i)) & (B.i)|`(f|(A.i)) = f|(A.i)
by RELAT_1:83,94;
then
A7: (g*f)|(A.i) = (g|(B.i))*(f|(A.i)) by MONOID_1:1;
((g*f)-MSF(I,A)).i = (g*f)|(A.i) & (g-MSF(I,B)).i = g|(B.i) by A5,Def1;
hence ((g*f)-MSF(I,A)).i = ((g-MSF(I,B))**(f-MSF(I,A))).i by A3,A5,A6,A7,
PBOOLE:def 19;
end;
dom ((g*f)-MSF(I,A)) = I by PARTFUN1:def 2;
hence thesis by A3,A4,FUNCT_1:2;
end;
theorem
for f being Function, I being set for A,B being ManySortedSet of I st
for i being set st i in I holds A.i c= dom f & f.:(A.i) c= B.i holds f-MSF(I,A)
is ManySortedFunction of A,B
proof
let f be Function, I be set;
let A,B be ManySortedSet of I such that
A1: for i being set st i in I holds A.i c= dom f & f.:(A.i) c= B.i;
let i be object;
assume
A2: i in I;
then
A3: (f-MSF(I,A)).i = f|(A.i) by Def1;
f.:(A.i) c= B.i by A1,A2;
then
A4: rng ((f-MSF(I,A)).i) c= B.i by A3,RELAT_1:115;
dom ((f-MSF(I,A)).i) = A.i by A1,A2,A3,RELAT_1:62;
hence thesis by A4,FUNCT_2:2;
end;
Lm1: now
let x,y be set;
assume <*x*> = <*y*>;
then <*x*>.1 = y by FINSEQ_1:40;
hence x = y;
end;
definition
let S be non empty ManySortedSign;
let A be MSAlgebra over S;
attr A is empty means
: Def2:
the Sorts of A is empty-yielding;
end;
registration
let S be non empty ManySortedSign;
cluster non-empty -> non empty for MSAlgebra over S;
coherence;
end;
registration
let S be non empty non void ManySortedSign;
cluster strict non-empty disjoint_valued for MSAlgebra over S;
existence
proof
set X = the non-empty ManySortedSet of the carrier of S;
take FreeMSA X;
thus thesis;
end;
end;
registration
let S be non empty non void ManySortedSign;
let A be non empty MSAlgebra over S;
cluster the Sorts of A -> non empty-yielding;
coherence by Def2;
end;
registration
cluster non empty-yielding for Function;
existence
proof
set S = the non empty non void ManySortedSign;
set A = the non empty MSAlgebra over S;
take the Sorts of A;
thus thesis;
end;
end;
begin :: Signature of a category
definition
let A be set;
func CatSign A -> strict ManySortedSign means
: Def3:
the carrier of it = [:{0},2-tuples_on A:] &
the carrier' of it = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] &
(for a being set st a in A
holds (the Arity of it).[1,<*a*>] ={} &
(the ResultSort of it).[1,<*a*>] = [0,<*a,a*>]) &
for a,b,c being set st a in A & b in A & c in A
holds (the Arity of it).[2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> &
(the ResultSort of it).[2,<*a,b,c*>] = [0,<*a,c*>];
existence
proof
defpred R[object,object] means
ex y1,y2,y3 being set st y1 in A & y2 in A & y3
in A & ($1 = [1,<*y1*>] & $2 = [0,<*y1,y1*>] or $1 = [2,<*y1,y2,y3*>] & $2 = [0
,<*y1,y3*>]);
defpred P[object,object] means
ex y1,y2,y3 being set st y1 in A & y2 in A & y3
in A & ($1 = [1,<*y1*>] & $2 = {} or $1 = [2,<*y1,y2,y3*>] & $2 = <*[0,<*y2,y3
*>],[0,<*y1,y2*>]*>);
A1: for x being object
st x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:]
ex y being object st y in [:{0},2-tuples_on A:]* & P[x,y]
proof
let x be object;
assume
A2: x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:];
per cases by A2,XBOOLE_0:def 3;
suppose
A3: x in [:{1},1-tuples_on A:];
then x`2 in 1-tuples_on A by MCART_1:10;
then
A4: x`2 in {s where s is Element of A*: len s = 1} by FINSEQ_2:def 4;
take y = {};
thus y in [:{0},2-tuples_on A:]* by FINSEQ_1:49;
consider s being Element of A* such that
A5: x`2 = s and
A6: len s = 1 by A4;
take y1 = s.1, y2 = s.1, y3 = s.1;
A7: s = <*y1*> by A6,FINSEQ_1:40;
then y1 in {y1} & rng s = {y1} by FINSEQ_1:39,TARSKI:def 1;
hence y1 in A & y2 in A & y3 in A;
x`1 in {1} by A3,MCART_1:10;
then x`1 = 1 by TARSKI:def 1;
hence thesis by A3,A5,A7,MCART_1:21;
end;
suppose
A8: x in [:{2},3-tuples_on A:];
then x`2 in 3-tuples_on A by MCART_1:10;
then x`2 in {s where s is Element of A*: len s = 3} by FINSEQ_2:def 4;
then consider s being Element of A* such that
A9: x`2 = s and
A10: len s = 3;
set y1 = s.1, y2 = s.2, y3 = s.3;
A11: s = <*y1,y2,y3*> by A10,FINSEQ_1:45;
then
A12: rng s = {y1,y2,y3} by FINSEQ_2:128;
then reconsider B = A as non empty set;
take y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*>;
A13: y2 in {y1,y2,y3} by ENUMSET1:def 1;
A14: y1 in {y1,y2,y3} by ENUMSET1:def 1;
then
A15: 0 in {0} & <*y1,y2*> in 2-tuples_on B by A13,A12,FINSEQ_2:101
,TARSKI:def 1;
A16: y3 in {y1,y2,y3} by ENUMSET1:def 1;
then <*y2,y3*> in 2-tuples_on B by A13,A12,FINSEQ_2:101;
then reconsider
z1 = [0,<*y2,y3*>], z2 = [0,<*y1,y2*>] as Element of [:{0},
2-tuples_on B:] by A15,ZFMISC_1:87;
y = <*z1*>^<*z2*> by FINSEQ_1:def 9;
hence y in [:{0},2-tuples_on A:]* by FINSEQ_1:def 11;
take y1, y2, y3;
thus y1 in A & y2 in A & y3 in A by A14,A13,A16,A12;
x`1 in {2} by A8,MCART_1:10;
then x`1 = 2 by TARSKI:def 1;
hence thesis by A8,A9,A11,MCART_1:21;
end;
end;
consider Ar being Function such that
A17: dom Ar = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] & rng Ar
c= [:{0},2 -tuples_on A:]* and
A18: for x being object st x in [:{1},1-tuples_on A:] \/ [:{2},3
-tuples_on A:] holds P[x,Ar.x] from FUNCT_1:sch 6(A1);
reconsider Ar as Function of [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
:], [:{0},2-tuples_on A:]* by A17,FUNCT_2:2;
A19: for x being object st x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
:] ex y being object st y in [:{0},2-tuples_on A:] & R[x,y]
proof
let x be object;
assume
A20: x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:];
per cases by A20,XBOOLE_0:def 3;
suppose
A21: x in [:{1},1-tuples_on A:];
then x`2 in 1-tuples_on A by MCART_1:10;
then x`2 in {s where s is Element of A*: len s = 1} by FINSEQ_2:def 4;
then consider s being Element of A* such that
A22: x`2 = s and
A23: len s = 1;
set y1 = s.1, y2 = s.1, y3 = s.1;
A24: s = <*y1*> by A23,FINSEQ_1:40;
then
A25: y1 in {y1} & rng s = {y1} by FINSEQ_1:39,TARSKI:def 1;
take y = [0,<*y1,y1*>];
reconsider B = A as non empty set by A24;
reconsider y1 as Element of B by A25;
0 in {0} & <*y1,y1*> in 2-tuples_on B by FINSEQ_2:101,TARSKI:def 1;
hence y in [:{0},2-tuples_on A:] by ZFMISC_1:87;
take y1, y2, y3;
thus y1 in A & y2 in A & y3 in A by A25;
x`1 in {1} by A21,MCART_1:10;
then x`1 = 1 by TARSKI:def 1;
hence x = [1,<*y1*>] & y = [0,<*y1,y1*>] or x = [2,<*y1,y2,y3*>] & y =
[0,<*y1,y3*>] by A21,A22,A24,MCART_1:21;
end;
suppose
A26: x in [:{2},3-tuples_on A:];
then x`2 in 3-tuples_on A by MCART_1:10;
then x`2 in {s where s is Element of A*: len s = 3} by FINSEQ_2:def 4;
then consider s being Element of A* such that
A27: x`2 = s and
A28: len s = 3;
set y1 = s.1, y2 = s.2, y3 = s.3;
A29: s = <*y1,y2,y3*> by A28,FINSEQ_1:45;
then
A30: rng s = {y1,y2,y3} by FINSEQ_2:128;
then reconsider B = A as non empty set;
take y = [0,<*y1,y3*>];
A31: y1 in {y1,y2,y3} & y3 in {y1,y2,y3} by ENUMSET1:def 1;
then 0 in {0} & <*y1,y3*> in 2-tuples_on B by A30,FINSEQ_2:101
,TARSKI:def 1;
hence y in [:{0},2-tuples_on A:] by ZFMISC_1:87;
take y1, y2, y3;
y2 in {y1,y2,y3} by ENUMSET1:def 1;
hence y1 in A & y2 in A & y3 in A by A31,A30;
x`1 in {2} by A26,MCART_1:10;
then x`1 = 2 by TARSKI:def 1;
hence thesis by A26,A27,A29,MCART_1:21;
end;
end;
consider R being Function such that
A32: dom R = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] & rng R c=
[:{0},2 -tuples_on A:] and
A33: for x being object st x in [:{1},1-tuples_on A:] \/ [:{2},3
-tuples_on A:] holds R[x,R.x] from FUNCT_1:sch 6(A19);
reconsider R as Function of [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:]
, [:{0},2-tuples_on A:] by A32,FUNCT_2:2;
take S = ManySortedSign (#[:{0},2-tuples_on A:], [:{1},1-tuples_on A:]\/[:
{2},3-tuples_on A:], Ar, R#);
thus the carrier of S = [:{0},2-tuples_on A:];
thus the carrier' of S = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:];
hereby
let a be set;
assume
A34: a in A;
then reconsider B = A as non empty set;
reconsider x = a as Element of B by A34;
<*x*> is Element of 1-tuples_on B & 1 in {1} by FINSEQ_2:98,TARSKI:def 1;
then [1,<*a*>] in [:{1},1-tuples_on A:] by ZFMISC_1:87;
then
A35: [1,<*a*>] in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
then consider y1,y2,y3 being set such that
y1 in A and
y2 in A and
y3 in A and
A36: [1,<*a*>] = [1,<*y1*>] & R.[1,<*a*>] = [0,<*y1,y1*>] or [1,<*a
*>] = [2,<*y1,y2,y3*>] & R.[1,<*a*>] = [0,<*y1,y3*>] by A33;
ex y1,y2,y3 being set st y1 in A & y2 in A & y3 in A & ([1,<*a*>] =
[1, <*y1*>] & Ar.[1,<*a*>] = {} or [1,<*a*>] = [2,<*y1,y2,y3*>] & Ar.[1,<*a*>]
= <* [0,<*y2,y3*>],[0,<*y1,y2*>]*>) by A18,A35;
hence (the Arity of S).[1,<*a*>] = {} by XTUPLE_0:1;
A37: <*a*>.1 = a & <*y1*>.1 = y1;
<*a*> = <*y1*> by A36,XTUPLE_0:1;
hence (the ResultSort of S).[1,<*a*>] = [0,<*a,a*>] by A36,A37,XTUPLE_0:1
;
end;
let a,b,c be set;
assume that
A38: a in A and
A39: b in A & c in A;
reconsider B = A as non empty set by A38;
reconsider x = a, y = b, z = c as Element of B by A38,A39;
<*x,y,z*> is Element of 3-tuples_on B & 2 in {2} by FINSEQ_2:104
,TARSKI:def 1;
then [2,<*a,b,c*>] in [:{2},3-tuples_on A:] by ZFMISC_1:87;
then
A40: [2,<*a,b,c*>] in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
then consider y1,y2,y3 being set such that
y1 in A and
y2 in A and
y3 in A and
A41: [2,<*a,b,c*>] = [1,<*y1*>] & Ar.[2,<*a,b,c*>] = {} or [2,<*a,b,c
*>] = [2,<*y1,y2,y3*>] & Ar.[2,<*a,b,c*>] = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> by
A18;
A42: <*a,b,c*> = <*a*>^<*b*>^<*c*> & <*y1,y2,y3*> = <*y1*>^<*y2*>^<*y3*>
by FINSEQ_1:def 10;
A43: <*a,b,c*> = <*y1,y2,y3*> by A41,XTUPLE_0:1;
then
A44: <*a*>^<*b*> = <*y1*>^<*y2*> by A42,FINSEQ_2:17;
then <*a*> = <*y1*> by FINSEQ_2:17;
then
A45: a = y1 by Lm1;
b = y2 by A44,FINSEQ_2:17;
hence
(the Arity of S).[2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> by A41,A43,A42
,A45,FINSEQ_2:17,XTUPLE_0:1;
consider y1,y2,y3 being set such that
y1 in A and
y2 in A and
y3 in A and
A46: [2,<*a,b,c*>] = [1,<*y1*>] & R.[2,<*a,b,c*>] = [0,<*y1,y1*>] or [
2,<*a,b,c*>] = [2,<*y1,y2,y3*>] & R.[2,<*a,b,c*>] = [0,<*y1,y3*>] by A33,A40;
A47: <*a,b,c*>.1 = a & <*y1,y2,y3*>.1 = y1;
A48: <*a,b,c*>.3 = c;
<*a,b,c*> = <*y1,y2,y3*> by A46,XTUPLE_0:1;
hence thesis by A46,A47,A48,FINSEQ_1:45,XTUPLE_0:1;
end;
correctness
proof
let S1,S2 be strict ManySortedSign such that
A49: the carrier of S1 = [:{0},2-tuples_on A:] and
A50: the carrier' of S1 = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A :] and
A51: for a being set st a in A holds (the Arity of S1).[1,<*a*>] = {}
& (the ResultSort of S1).[1,<*a*>] = [0,<*a,a*>] and
A52: for a,b,c being set st a in A & b in A & c in A holds (the Arity
of S1).[2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & (the ResultSort of S1).[2,
<*a,b,c*>] = [0,<*a,c*>] and
A53: the carrier of S2 = [:{0},2-tuples_on A:] and
A54: the carrier' of S2 = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A :] and
A55: for a being set st a in A holds (the Arity of S2).[1,<*a*>] = {}
& (the ResultSort of S2).[1,<*a*>] = [0,<*a,a*>] and
A56: for a,b,c being set st a in A & b in A & c in A holds (the Arity
of S2).[2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & (the ResultSort of S2).[2,
<*a,b,c*>] = [0,<*a,c*>];
A57: now
let x be object;
assume x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:];
then
A58: x in [:{1},1-tuples_on A:] or x in [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
then x`1 in {1} & x`2 in 1-tuples_on A or x`1 in {2} & x`2 in 3
-tuples_on A by MCART_1:10;
then
A59: x`1 = 1 & x`2 in 1-tuples_on A or x`1 = 2 & x`2 in 3-tuples_on A by
TARSKI:def 1;
A60: now
assume x`2 in 3-tuples_on A;
then consider a,b,c being object such that
A61: a in A & b in A & c in A & x`2 = <*a,b,c*> by FINSEQ_2:139;
thus (the Arity of S1).[2,x`2] = <*[0,<*b,c*>],[0,<*a,b*>]*> by A52,A61
.= (the Arity of S2).[2,x`2] by A56,A61;
end;
A62: now
assume x`2 in 1-tuples_on A;
then
A63: ex a being set st a in A & x`2 = <*a*> by FINSEQ_2:135;
hence (the Arity of S1).[1,x`2] = {} by A51
.= (the Arity of S2).[1,x`2] by A55,A63;
end;
x = [x`1,x`2] by A58,MCART_1:21;
hence (the Arity of S1).x = (the Arity of S2).x by A59,A62,A60;
end;
A64: now
let x be object;
assume x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:];
then
A65: x in [:{1},1-tuples_on A:] or x in [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
then x`1 in {1} & x`2 in 1-tuples_on A or x`1 in {2} & x`2 in 3
-tuples_on A by MCART_1:10;
then
A66: x`1 = 1 & x`2 in 1-tuples_on A or x`1 = 2 & x`2 in 3-tuples_on A
by TARSKI:def 1;
A67: now
assume x`2 in 3-tuples_on A;
then consider a,b,c being object such that
A68: a in A & b in A & c in A & x`2 = <*a,b,c*> by FINSEQ_2:139;
thus (the ResultSort of S1).[2,x`2] = [0,<*a,c*>] by A52,A68
.= (the ResultSort of S2).[2,x`2] by A56,A68;
end;
A69: now
assume x`2 in 1-tuples_on A;
then consider a being set such that
A70: a in A & x`2 = <*a*> by FINSEQ_2:135;
thus (the ResultSort of S1).[1,x`2] = [0,<*a,a*>] by A51,A70
.= (the ResultSort of S2).[1,x`2] by A55,A70;
end;
x = [x`1,x`2] by A65,MCART_1:21;
hence (the ResultSort of S1).x = (the ResultSort of S2).x by A66,A69,A67;
end;
dom the Arity of S1 = the carrier' of S1 & dom the Arity of S2 = the
carrier' of S2 by FUNCT_2:def 1;
then
A71: the Arity of S1 = the Arity of S2 by A50,A54,A57,FUNCT_1:2;
now
assume [:{0},2-tuples_on A:] = {};
then A = {};
then
A72: 1 <> 0 & 3 <> 0 implies 1-tuples_on A = {} & 3-tuples_on A = {} by
FINSEQ_3:119;
then [:{1},1-tuples_on A:] = {} by ZFMISC_1:90;
hence [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] = {} by A72,
ZFMISC_1:90;
end;
then dom the ResultSort of S1 = the carrier' of S1 & dom the ResultSort
of S2 = the carrier' of S2 by A49,A50,A53,A54,FUNCT_2:def 1;
hence thesis by A49,A50,A53,A54,A71,A64,FUNCT_1:2;
end;
end;
registration
let A be set;
cluster CatSign A -> feasible;
coherence
proof
assume the carrier of CatSign A = {};
then [:{0},2-tuples_on A:] = {} by Def3;
then A = {};
then
A1: 1 <> 0 & 3 <> 0 implies 1-tuples_on A = {} & 3-tuples_on A = {} by
FINSEQ_3:119;
then [:{1},1-tuples_on A:] = {} by ZFMISC_1:90;
then [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] = {} by A1,ZFMISC_1:90;
hence thesis by Def3;
end;
end;
registration
let A be non empty set;
cluster CatSign A -> non empty non void;
coherence
proof
the carrier of CatSign A = [:{0},2-tuples_on A:] by Def3;
hence the carrier of CatSign A is non empty;
the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on
A:] by Def3;
hence the carrier' of CatSign A is non empty;
end;
end;
definition
mode Signature is feasible ManySortedSign;
end;
definition
let S be Signature;
attr S is Categorial means
: Def4:
ex A being set st CatSign A is
Subsignature of S & the carrier of S = [:{0},2-tuples_on A:];
end;
registration
cluster Categorial -> non void for non empty Signature;
coherence
proof
let S be non empty Signature;
given A being set such that
A1: CatSign A is Subsignature of S and
A2: the carrier of S = [:{0},2-tuples_on A:];
set s = the SortSymbol of S;
consider z,p being object such that
z in {0} and
A3: p in 2-tuples_on A and
s = [z,p] by A2,ZFMISC_1:84;
2-tuples_on A = {q where q is Element of A*: len q = 2} by FINSEQ_2:def 4;
then consider q being Element of A* such that
p = q and
A4: len q = 2 by A3;
A5: dom q = Seg 2 by A4,FINSEQ_1:def 3;
then reconsider A9 = A as non empty set;
1 in dom q by A5,FINSEQ_1:2,TARSKI:def 2;
then q.1 in rng q by FUNCT_1:def 3;
then reconsider a = q.1 as Element of A9;
the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on
A :] by Def3;
then
<*a*> is Element of 1-tuples_on A9 & [:{1},1-tuples_on A:] \/ [:{2},3
-tuples_on A:] c= the carrier' of S by A1,FINSEQ_2:98,INSTALG1:10;
hence the carrier' of S is non empty;
end;
end;
registration
cluster Categorial non empty strict for Signature;
existence
proof
take S = CatSign {{}};
thus S is Categorial
proof
take {{}};
thus thesis by Def3,INSTALG1:15;
end;
thus thesis;
end;
end;
definition
mode CatSignature is Categorial Signature;
end;
definition
let A be set;
mode CatSignature of A -> Signature means
: Def5:
CatSign A is Subsignature
of it & the carrier of it = [:{0},2-tuples_on A:];
existence
proof
set S = CatSign A;
S is Subsignature of S & the carrier of S = [:{0},2-tuples_on A:] by Def3,
INSTALG1:15;
then reconsider S as CatSignature by Def4;
take S;
thus thesis by Def3,INSTALG1:15;
end;
end;
theorem
for A1,A2 being set, S being CatSignature of A1 st S is CatSignature
of A2 holds A1 = A2
proof
let A1,A2 be set, S be CatSignature of A1;
assume that
CatSign A2 is Subsignature of S and
A1: the carrier of S = [:{0},2-tuples_on A2:];
A2: [:{0},2-tuples_on A1:] = [:{0},2-tuples_on A2:] by A1,Def5;
then
A3: 2-tuples_on A1 c= 2-tuples_on A2 by ZFMISC_1:94;
hereby
let x be object;
assume x in A1;
then <*x,x*> in 2-tuples_on A1 by FINSEQ_2:137;
then <*x,x*> in 2-tuples_on A2 by A3;
hence x in A2 by FINSEQ_2:138;
end;
let x be object;
assume x in A2;
then
A4: <*x,x*> in 2-tuples_on A2 by FINSEQ_2:137;
2-tuples_on A2 c= 2-tuples_on A1 by A2,ZFMISC_1:94;
hence thesis by A4,FINSEQ_2:138;
end;
registration
let A be set;
cluster -> Categorial for CatSignature of A;
coherence
proof
let S be CatSignature of A;
take A;
thus thesis by Def5;
end;
end;
registration
let A be non empty set;
cluster -> non empty for CatSignature of A;
coherence
proof
let S be CatSignature of A;
CatSign A is Subsignature of S by Def5;
then the carrier of CatSign A c= the carrier of S by INSTALG1:10;
hence the carrier of S is not empty;
end;
end;
registration
let A be set;
cluster strict for CatSignature of A;
existence
proof
set S = CatSign A;
S is Subsignature of S & the carrier of S = [:{0},2-tuples_on A:] by Def3,
INSTALG1:15;
then S is CatSignature of A by Def5;
hence thesis;
end;
end;
definition
let A be set;
redefine func CatSign A -> strict CatSignature of A; :: redefines CatSign (CATALG_1, definition)
coherence
proof
set S = CatSign A;
S is Subsignature of S & the carrier of S = [:{0}, 2-tuples_on A:] by Def3,
INSTALG1:15;
hence thesis by Def5;
end;
end;
definition
let S be ManySortedSign;
assume
A1: for x being object
st x in proj2((the carrier of S) \/ (the carrier' of S))
holds x is Function;
func underlay S -> set means
:Def6: for x being object holds x in it iff
ex a being set, f being Function
st [a,f] in (the carrier of S) \/ (the carrier' of S) & x in rng f;
existence
proof
set A = (the carrier of S) \/ (the carrier' of S);
take X = proj2 union proj2 A;
let x be object;
hereby
assume x in X;
then consider a being object such that
A2: [a,x] in union proj2 A by XTUPLE_0:def 13;
consider b being set such that
A3: [a,x] in b and
A4: b in proj2 A by A2,TARSKI:def 4;
reconsider b as Function by A4,A1;
b in proj2 A by A4;
then consider c being object such that
A5: [c,b] in A by XTUPLE_0:def 13;
reconsider c as set by TARSKI:1;
take c,b;
thus [c,b] in A & x in rng b by A3,A5,XTUPLE_0:def 13;
end;
given a being set, f being Function such that
A6: [a,f] in (the carrier of S) \/ (the carrier' of S) and
A7: x in rng f;
consider b being object such that
A8: [b,x] in f by A7,XTUPLE_0:def 13;
f in proj2 A by A6,XTUPLE_0:def 13;
then f in proj2 A ;
then [b,x] in union proj2 A by A8,TARSKI:def 4;
hence thesis by XTUPLE_0:def 13;
end;
uniqueness
proof
defpred P[object] means ex a being set, f being Function st [a,f] in (the
carrier of S) \/ (the carrier' of S) & $1 in rng f;
thus for X1,X2 being set st
(for x being object holds x in X1 iff P[ x]) & (
for x being object holds x in X2 iff P[ x]) holds X1 = X2
from XBOOLE_0:sch 3;
end;
end;
definition
let S be ManySortedSign;
attr S is delta-concrete means
: Def7:
ex f being sequence of NAT st
( for s being object st s in the carrier of S
ex i being (Element of NAT), p being FinSequence st s = [i,p]
& len p = f.i & [:{i}, (f.i)-tuples_on underlay S:] c= the carrier of S)
& (for o being object st o in the carrier' of S
ex i being (Element of NAT), p being FinSequence st o = [i,p] &
len p = f.i & [:{i}, (f.i) -tuples_on underlay S:] c= the carrier' of S);
end;
Lm2: for A being set, x being object
st x in proj2((the carrier of CatSign A) \/ (the carrier' of CatSign A))
holds x is Function
proof let A being set, x being object;
set C1 = the carrier of CatSign A, C2 = the carrier' of CatSign A;
A1: C1 = [:{0},2-tuples_on A:] by Def3;
A2: C2 = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] by Def3;
assume x in proj2(C1 \/ C2);
then x in proj2 C1 \/ proj2 C2 by XTUPLE_0:27;
then per cases by XBOOLE_0:def 3;
suppose x in proj2 C1;
then x in 2-tuples_on A by A1,FUNCT_5:9;
hence x is Function;
end;
suppose x in proj2 C2;
then x in proj2 [:{1},1-tuples_on A:] \/ proj2 [:{2},3-tuples_on A:]
by A2,XTUPLE_0:27;
then per cases by XBOOLE_0:def 3;
suppose x in proj2 [:{1},1-tuples_on A:];
then x in 1-tuples_on A by FUNCT_5:9;
hence x is Function;
end;
suppose x in proj2 [:{2},3-tuples_on A:];
then x in 3-tuples_on A by FUNCT_5:9;
hence x is Function;
end;
end;
end;
theorem Th5:
for A being set holds underlay CatSign A = A
proof
let A be set;
set S = CatSign A;
A1: the carrier' of S = [:{1},1-tuples_on A:] \/ [:{2}, 3-tuples_on A:]
by Def3;
A2: for x being object
st x in proj2((the carrier of CatSign A) \/ (the carrier' of CatSign A))
holds x is Function by Lm2;
hereby
let x be object;
assume x in underlay CatSign A;
then consider a being set, f being Function such that
A3: [a,f] in (the carrier of S) \/ (the carrier' of S) and
A4: x in rng f by Def6,A2;
[a,f] in the carrier of S or [a,f] in the carrier' of S by A3,
XBOOLE_0:def 3;
then
[a,f] in [:{0},2-tuples_on A:] or [a,f] in [:{1},1-tuples_on A:] or [a
,f] in [:{2},3-tuples_on A:] by A1,Def3,XBOOLE_0:def 3;
then f in 2-tuples_on A or f in 1-tuples_on A or f in 3-tuples_on A by
ZFMISC_1:87;
then f is FinSequence of A by FINSEQ_2:def 3;
then rng f c= A by FINSEQ_1:def 4;
hence x in A by A4;
end;
let x be object;
assume x in A;
then
A5: <*x,x*> in 2-tuples_on A by FINSEQ_2:137;
the carrier of S = [:{0},2-tuples_on A:] by Def3;
then [0,<*x,x*>] in the carrier of S by A5,ZFMISC_1:105;
then
A6: [0,<*x,x*>] in (the carrier of S) \/ (the carrier' of S) by XBOOLE_0:def 3;
rng <*x,x*> = {x,x} by FINSEQ_2:127;
then x in rng <*x,x*> by TARSKI:def 2;
hence thesis by A6,Def6,A2;
end;
registration
let A be set;
cluster CatSign A -> delta-concrete;
coherence
proof
defpred P[object,object] means
($1 = 0 implies $2 = 2) & ($1 = 1 implies $2 = 1)
& ($1 = 2 implies $2 = 3);
set S = CatSign A;
A1: for x be object st x in NAT ex y be object st y in NAT & P[x,y]
proof
reconsider j0 = 2, j1 = 1, j2 = 3 as set;
let i be object;
assume i in NAT;
per cases;
suppose
A2: i = 0;
take j0;
thus thesis by A2;
end;
suppose
A3: i = 1;
take j1;
thus thesis by A3;
end;
suppose
A4: i = 2;
take j2;
thus thesis by A4;
end;
suppose
A5: i <> 0 & i <> 1 & i <> 2;
take j0;
thus thesis by A5;
end;
end;
consider f being Function such that
A6: dom f = NAT & rng f c= NAT and
A7: for i being object st i in NAT holds P[i,f.i] from FUNCT_1:sch 6(A1);
reconsider f as sequence of NAT by A6,FUNCT_2:2;
take f;
A8: A = underlay S by Th5;
A9: the carrier of S = [:{0},2-tuples_on A:] by Def3;
hereby
let s be object;
assume s in the carrier of S;
then consider i, p being object such that
A10: i in {0} and
A11: p in 2-tuples_on A and
A12: s = [i,p] by A9,ZFMISC_1:84;
reconsider p as FinSequence by A11;
take i = 0, p;
f.i = 2 by A7;
hence s = [i,p] & len p = f.i by A10,A11,A12,FINSEQ_2:132,TARSKI:def 1;
thus [:{i}, (f.i)-tuples_on underlay S:] c= the carrier of S by A7,A9,A8;
end;
let o be object;
A13: the carrier' of S = [:{1},1-tuples_on A:] \/ [:{2}, 3-tuples_on A:] by
Def3;
assume
A14: o in the carrier' of S;
per cases by A13,A14,XBOOLE_0:def 3;
suppose
o in [:{1}, 1-tuples_on A:];
then consider i,p being object such that
A15: i in {1} and
A16: p in 1-tuples_on A and
A17: o = [i,p] by ZFMISC_1:84;
reconsider p as FinSequence of A by A16,FINSEQ_2:def 3;
take i = 1, p;
f.i = 1 by A7;
hence thesis by A13,A8,A15,A16,A17,FINSEQ_2:132,TARSKI:def 1,XBOOLE_1:7;
end;
suppose
o in [:{2}, 3-tuples_on A:];
then consider i,p being object such that
A18: i in {2} and
A19: p in 3-tuples_on A and
A20: o = [i,p] by ZFMISC_1:84;
reconsider p as FinSequence of A by A19,FINSEQ_2:def 3;
take i = 2, p;
f.i = 3 by A7;
hence thesis by A13,A8,A18,A19,A20,FINSEQ_2:132,TARSKI:def 1,XBOOLE_1:7;
end;
end;
end;
registration
cluster delta-concrete non empty strict for CatSignature;
existence
proof
take CatSign {{}};
thus thesis;
end;
let A be set;
cluster delta-concrete strict for CatSignature of A;
existence
proof
take CatSign A;
thus thesis;
end;
end;
theorem
for A being set holds underlay CatSign A = A
proof
let A be set;
set S = CatSign A;
A1: the carrier' of S = [:{1},1-tuples_on A:] \/ [:{2}, 3-tuples_on A:]
by Def3;
A2: for x being object
st x in proj2((the carrier of CatSign A) \/ (the carrier' of CatSign A))
holds x is Function by Lm2;
hereby
let x be object;
assume x in underlay CatSign A;
then consider a being set, f being Function such that
A3: [a,f] in (the carrier of S) \/ (the carrier' of S) and
A4: x in rng f by Def6,A2;
[a,f] in the carrier of S or [a,f] in the carrier' of S by A3,
XBOOLE_0:def 3;
then
[a,f] in [:{0},2-tuples_on A:] or [a,f] in [:{1},1-tuples_on A:] or [a
,f] in [:{2},3-tuples_on A:] by A1,Def3,XBOOLE_0:def 3;
then f in 2-tuples_on A or f in 1-tuples_on A or f in 3-tuples_on A by
ZFMISC_1:87;
then f is FinSequence of A by FINSEQ_2:def 3;
then rng f c= A by FINSEQ_1:def 4;
hence x in A by A4;
end;
let x be object;
assume x in A;
then
A5: <*x,x*> in 2-tuples_on A by FINSEQ_2:137;
the carrier of S = [:{0},2-tuples_on A:] by Def3;
then [0,<*x,x*>] in the carrier of S by A5,ZFMISC_1:105;
then
A6: [0,<*x,x*>] in (the carrier of S) \/ (the carrier' of S) by XBOOLE_0:def 3;
rng <*x,x*> = {x,x} by FINSEQ_2:127;
then x in rng <*x,x*> by TARSKI:def 2;
hence thesis by A6,Def6,A2;
end;
registration
let A be set;
cluster CatSign A -> delta-concrete;
coherence;
end;
registration
cluster delta-concrete non empty strict for CatSignature;
existence
proof
take CatSign {{}};
thus thesis;
end;
let A be set;
cluster delta-concrete strict for CatSignature of A;
existence
proof
take CatSign A;
thus thesis;
end;
end;
Lm3: for S being delta-concrete ManySortedSign, x being object
st x in proj2((the carrier of S) \/ (the carrier' of S))
holds x is Function
proof let S be delta-concrete ManySortedSign, x being object;
consider f being sequence of NAT such that
A1: for s being object st s in the carrier of S
ex i being (Element of NAT), p being FinSequence st s = [i,p]
& len p = f.i & [:{i}, (f.i)-tuples_on underlay S:] c= the carrier of S
and
A2: for o being object st o in the carrier' of S
ex i being (Element of NAT), p being FinSequence st o = [i,p] &
len p = f.i & [:{i}, (f.i) -tuples_on underlay S:] c= the carrier' of S
by Def7;
set C1 = the carrier of S, C2 = the carrier' of S;
assume x in proj2((the carrier of S) \/ (the carrier' of S));
then consider y being object such that
A3: [y,x] in (the carrier of S) \/ (the carrier' of S) by XTUPLE_0:def 13;
per cases by XBOOLE_0:def 3,A3;
suppose [y,x] in C1;
then consider i being (Element of NAT), p being FinSequence such that
A4: [y,x] = [i,p] and
len p = f.i & [:{i}, (f.i)-tuples_on underlay S:] c= the carrier of S
by A1;
x = p by A4, XTUPLE_0:1;
hence x is Function;
end;
suppose [y,x] in C2;
then consider i being (Element of NAT), p being FinSequence such that
A5: [y,x] = [i,p] and
len p = f.i & [:{i}, (f.i) -tuples_on underlay S:] c= the carrier' of S
by A2;
x = p by A5, XTUPLE_0:1;
hence x is Function;
end;
end;
theorem Th7:
for S being delta-concrete ManySortedSign, x being set st x in
the carrier of S or x in the carrier' of S ex i being (Element of NAT), p being
FinSequence st x = [i,p] & rng p c= underlay S
proof
let S be delta-concrete ManySortedSign, x be set such that
A1: x in the carrier of S or x in the carrier' of S;
A2: x in (the carrier of S) \/ the carrier' of S by A1,XBOOLE_0:def 3;
consider f being sequence of NAT such that
A3: for s being object st s in the carrier of S ex i being (Element of NAT)
, p being FinSequence st s = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
underlay S:] c= the carrier of S and
A4: for o being object st o in the carrier' of S ex i being (Element of NAT
), p being FinSequence st o = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
underlay S:] c= the carrier' of S by Def7;
A5: for x being object
st x in proj2((the carrier of S) \/ (the carrier' of S))
holds x is Function by Lm3;
per cases by A1;
suppose
x in the carrier of S;
then consider i being (Element of NAT), p being FinSequence such that
A6: x = [i,p] and
len p = f.i and
[:{i}, (f.i)-tuples_on underlay S:] c= the carrier of S by A3;
take i,p;
thus x = [i,p] by A6;
let a be object;
thus thesis by A2,A6,Def6,A5;
end;
suppose
x in the carrier' of S;
then consider i being (Element of NAT), p being FinSequence such that
A7: x = [i,p] and
len p = f.i and
[:{i}, (f.i)-tuples_on underlay S:] c= the carrier' of S by A4;
take i,p;
thus x = [i,p] by A7;
let a be object;
thus thesis by A2,A7,Def6,A5;
end;
end;
theorem
for S being delta-concrete ManySortedSign, i being set, p1,p2 being
FinSequence st [i,p1] in the carrier of S & [i,p2] in the carrier of S or [i,p1
] in the carrier' of S & [i,p2] in the carrier' of S holds len p1 = len p2
proof
let S be delta-concrete ManySortedSign, i be set, p1,p2 be FinSequence such
that
A1: [i,p1] in the carrier of S & [i,p2] in the carrier of S or [i,p1] in
the carrier' of S & [i,p2] in the carrier' of S;
consider f being sequence of NAT such that
A2: for s being object st s in the carrier of S ex i being (Element of NAT)
, p being FinSequence st s = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
underlay S:] c= the carrier of S and
A3: for o being object st o in the carrier' of S ex i being (Element of NAT
), p being FinSequence st o = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
underlay S:] c= the carrier' of S by Def7;
per cases by A1;
suppose
A4: [i,p1] in the carrier of S & [i,p2] in the carrier of S;
then consider j1 being (Element of NAT), q1 being FinSequence such that
A5: [i,p1] = [j1,q1] and
A6: len q1 = f.j1 and
[:{j1}, (f.j1)-tuples_on underlay S:] c= the carrier of S by A2;
A7: i = j1 & p1 = q1 by A5,XTUPLE_0:1;
consider j2 being (Element of NAT), q2 being FinSequence such that
A8: [i,p2] = [j2,q2] and
A9: len q2 = f.j2 and
[:{j2}, (f.j2)-tuples_on underlay S:] c= the carrier of S by A2,A4;
i = j2 by A8,XTUPLE_0:1;
hence thesis by A6,A8,A9,A7,XTUPLE_0:1;
end;
suppose
A10: [i,p1] in the carrier' of S & [i,p2] in the carrier' of S;
then consider j1 being (Element of NAT), q1 being FinSequence such that
A11: [i,p1] = [j1,q1] and
A12: len q1 = f.j1 and
[:{j1}, (f.j1)-tuples_on underlay S:] c= the carrier' of S by A3;
A13: i = j1 & p1 = q1 by A11,XTUPLE_0:1;
consider j2 being (Element of NAT), q2 being FinSequence such that
A14: [i,p2] = [j2,q2] and
A15: len q2 = f.j2 and
[:{j2}, (f.j2)-tuples_on underlay S:] c= the carrier' of S by A3,A10;
i = j2 by A14,XTUPLE_0:1;
hence thesis by A12,A14,A15,A13,XTUPLE_0:1;
end;
end;
theorem
for S being delta-concrete ManySortedSign, i being set, p1,p2 being
FinSequence st len p2 = len p1 & rng p2 c= underlay S holds ([i,p1] in the
carrier of S implies [i,p2] in the carrier of S) & ([i,p1] in the carrier' of S
implies [i,p2] in the carrier' of S)
proof
let S be delta-concrete ManySortedSign, i be set, p1,p2 be FinSequence such
that
A1: len p2 = len p1 & rng p2 c= underlay S;
consider f being sequence of NAT such that
A2: for s being object st s in the carrier of S ex i being (Element of NAT)
, p being FinSequence st s = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
underlay S:] c= the carrier of S and
A3: for o being object st o in the carrier' of S ex i being (Element of NAT
), p being FinSequence st o = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
underlay S:] c= the carrier' of S by Def7;
hereby
assume [i,p1] in the carrier of S;
then consider j1 being (Element of NAT), q1 being FinSequence such that
A4: [i,p1] = [j1,q1] and
A5: len q1 = f.j1 and
A6: [:{j1}, (f.j1)-tuples_on underlay S:] c= the carrier of S by A2;
p1 = q1 by A4,XTUPLE_0:1;
then
A7: p2 in (f.j1)-tuples_on underlay S by A1,A5,FINSEQ_2:132;
i = j1 by A4,XTUPLE_0:1;
then [i,p2] in [:{j1}, (f.j1)-tuples_on underlay S:] by A7,ZFMISC_1:105;
hence [i,p2] in the carrier of S by A6;
end;
assume [i,p1] in the carrier' of S;
then consider j1 being (Element of NAT), q1 being FinSequence such that
A8: [i,p1] = [j1,q1] and
A9: len q1 = f.j1 and
A10: [:{j1}, (f.j1)-tuples_on underlay S:] c= the carrier' of S by A3;
p1 = q1 by A8,XTUPLE_0:1;
then
A11: p2 in (f.j1)-tuples_on underlay S by A1,A9,FINSEQ_2:132;
i = j1 by A8,XTUPLE_0:1;
then [i,p2] in [:{j1}, (f.j1)-tuples_on underlay S:] by A11,ZFMISC_1:105;
hence thesis by A10;
end;
theorem
for S being delta-concrete Categorial non empty Signature holds S is
CatSignature of underlay S
proof
let S be delta-concrete Categorial non empty Signature;
set s = the SortSymbol of S;
consider A being set such that
A1: CatSign A is Subsignature of S and
A2: the carrier of S = [:{0},2-tuples_on A:] by Def4;
consider f being sequence of NAT such that
A3: for s being object st s in the carrier of S ex i being (Element of NAT)
, p being FinSequence st s = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
underlay S:] c= the carrier of S and
for o being object st o in the carrier' of S ex i being (Element of NAT), p
being FinSequence st o = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on underlay
S:] c= the carrier' of S by Def7;
consider i being (Element of NAT), p being FinSequence such that
A4: s = [i,p] and
A5: len p = f.i & [:{i}, (f.i)-tuples_on underlay S:] c= the carrier of
S by A3;
p in 2-tuples_on A by A2,A4,ZFMISC_1:105;
then
A6: len p = 2 by FINSEQ_2:132;
A7: for x being object
st x in proj2((the carrier of S) \/ (the carrier' of S))
holds x is Function by Lm3;
A8: A c= underlay S
proof
let x be object;
assume x in A;
then <*x,x*> in 2-tuples_on A by FINSEQ_2:137;
then [0,<*x,x*>] in the carrier of S by A2,ZFMISC_1:105;
then
A9: [0,<*x,x*>] in (the carrier of S) \/ the carrier' of S by XBOOLE_0:def 3;
rng <*x,x*> = {x,x} by FINSEQ_2:127;
then x in rng <*x,x*> by TARSKI:def 2;
hence thesis by A9,Def6,A7;
end;
i = 0 by A2,A4,ZFMISC_1:105;
then
A10: 2-tuples_on underlay S c= 2-tuples_on A by A2,A5,A6,ZFMISC_1:94;
underlay S c= A
proof
let x be object;
assume x in underlay S;
then <*x,x*> in 2-tuples_on underlay S by FINSEQ_2:137;
hence thesis by A10,FINSEQ_2:138;
end;
then A = underlay S by A8;
hence thesis by A1,A2,Def5;
end;
begin :: Symbols of categorial sygnature
registration
let S be non empty CatSignature;
let s be SortSymbol of S;
cluster s`2 -> Relation-like Function-like for set;
coherence
proof
consider A being set such that
CatSign A is Subsignature of S and
A1: the carrier of S = [:{0},2-tuples_on A:] by Def4;
s`2 in 2-tuples_on A by A1,MCART_1:10;
hence thesis;
end;
end;
registration
let S be non empty delta-concrete ManySortedSign;
let s be SortSymbol of S;
cluster s`2 -> Relation-like Function-like for set;
coherence
proof
ex i being (Element of NAT), p being FinSequence st ( s = [ i,p])&( rng
p c= underlay S) by Th7;
hence thesis;
end;
end;
registration
let S be non void delta-concrete ManySortedSign;
let o be Element of the carrier' of S;
cluster o`2 -> Relation-like Function-like for set;
coherence
proof
ex i being (Element of NAT), p being FinSequence st ( o = [ i,p])&( rng
p c= underlay S) by Th7;
hence thesis;
end;
end;
registration
let S be non empty CatSignature;
let s be SortSymbol of S;
cluster s`2 -> FinSequence-like for Function;
coherence
proof
consider A being set such that
CatSign A is Subsignature of S and
A1: the carrier of S = [:{0},2-tuples_on A:] by Def4;
s`2 in 2-tuples_on A by A1,MCART_1:10;
then ex a,b being object st a in A & b in A & s`2 = <*a,b*>
by FINSEQ_2:137;
hence thesis;
end;
end;
registration
let S be non empty delta-concrete ManySortedSign;
let s be SortSymbol of S;
cluster s`2 -> FinSequence-like for Function;
coherence
proof
ex i being (Element of NAT), p being FinSequence st ( s = [ i,p])&( rng
p c= underlay S) by Th7;
hence thesis;
end;
end;
registration
let S be non void delta-concrete ManySortedSign;
let o be Element of the carrier' of S;
cluster o`2 -> FinSequence-like for Function;
coherence
proof
ex i being (Element of NAT), p being FinSequence st ( o = [ i,p])&( rng
p c= underlay S) by Th7;
hence thesis;
end;
end;
definition
let a be set;
func idsym a -> set equals
[1,<*a*>];
correctness;
let b be set;
func homsym(a,b) -> set equals
[0,<*a,b*>];
correctness;
let c be set;
func compsym(a,b,c) -> set equals
[2,<*a,b,c*>];
correctness;
end;
theorem Th11:
for A being non empty set, S being CatSignature of A for a being
Element of A holds idsym a in the carrier' of S & for b being Element of A
holds homsym(a,b) in the carrier of S & for c being Element of A holds compsym(
a,b,c) in the carrier' of S
proof
let A be non empty set, S be CatSignature of A;
let a be Element of A;
A1: the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
:] by Def3;
A2: CatSign A is Subsignature of S by Def5;
then
A3: the carrier of CatSign A c= the carrier of S by INSTALG1:10;
A4: the carrier' of CatSign A c= the carrier' of S by A2,INSTALG1:10;
<*a*> in 1-tuples_on A by FINSEQ_2:135;
then [1,<*a*>] in [:{1},1-tuples_on A:] by ZFMISC_1:105;
then [1,<*a*>] in the carrier' of CatSign A by A1,XBOOLE_0:def 3;
hence idsym a in the carrier' of S by A4;
let b be Element of A;
A5: the carrier of CatSign A = [:{0},2-tuples_on A:] by Def3;
<*a,b*> in 2-tuples_on A by FINSEQ_2:137;
then [0,<*a,b*>] in [:{0},2-tuples_on A:] by ZFMISC_1:105;
hence homsym(a,b) in the carrier of S by A3,A5;
let c be Element of A;
<*a,b,c*> in 3-tuples_on A by FINSEQ_2:139;
then [2,<*a,b,c*>] in [:{2},3-tuples_on A:] by ZFMISC_1:105;
then [2,<*a,b,c*>] in the carrier' of CatSign A by A1,XBOOLE_0:def 3;
hence thesis by A4;
end;
definition
let A be non empty set;
let a be Element of A;
redefine func idsym a -> OperSymbol of CatSign A; :: redefines idsym (CATALG_1, definition)
correctness by Th11;
let b be Element of A;
redefine func homsym(a,b) -> SortSymbol of CatSign A; :: redefines homsym (CATALG_1, definition)
correctness by Th11;
let c be Element of A;
redefine func compsym(a,b,c) -> OperSymbol of CatSign A; :: redefines compsym (CATALG_1, definition)
correctness by Th11;
end;
theorem Th12:
for a,b being set st idsym(a) = idsym(b) holds a = b
proof
let a,b be set;
assume idsym(a) = idsym(b);
then <*a*> = <*b*> by XTUPLE_0:1;
hence thesis by Lm1;
end;
theorem Th13:
for a1,b1,a2,b2 being set st homsym(a1,a2) = homsym(b1,b2) holds
a1 = b1 & a2 = b2
proof
let a1,b1,a2,b2 be set;
assume homsym(a1,a2) = homsym(b1,b2);
then
A1: <*a1,a2*> = <*b1,b2*> by XTUPLE_0:1;
<*a1,a2*>.1 = a1 & <*a1,a2*>.2 = a2;
hence thesis by A1,FINSEQ_1:44;
end;
theorem Th14:
for a1,b1,a2,b2,a3,b3 being set st compsym(a1,a2,a3) = compsym(
b1,b2,b3) holds a1 = b1 & a2 = b2 & a3 = b3
proof
let a1,b1,a2,b2,a3,b3 be set;
A1: <*a1,a2,a3*>.3 = a3;
assume compsym(a1,a2,a3) = compsym(b1,b2,b3);
then
A2: <*a1,a2,a3*> = <*b1,b2,b3*> by XTUPLE_0:1;
<*a1,a2,a3*>.1 = a1 & <*a1,a2,a3*>.2 = a2;
hence thesis by A2,A1,FINSEQ_1:45;
end;
theorem Th15:
for A being non empty set, S being CatSignature of A for s being
SortSymbol of S ex a,b being Element of A st s = homsym(a,b)
proof
let A be non empty set, S be CatSignature of A;
let s be SortSymbol of S;
A1: the carrier of S = [:{0},2-tuples_on A:] by Def5;
then s`2 in 2-tuples_on A by MCART_1:10;
then s`2 in {z where z is Element of A*: len z = 2} by FINSEQ_2:def 4;
then consider z being Element of A* such that
A2: s`2 = z and
A3: len z = 2;
A4: z.1 in {z.1,z.2} & z.2 in {z.1,z.2} by TARSKI:def 2;
A5: z = <*z.1,z.2*> by A3,FINSEQ_1:44;
then rng z = {z.1,z.2} by FINSEQ_2:127;
then reconsider a = z.1, b = z.2 as Element of A by A4;
take a,b;
s = [s`1,s`2] & s`1 in {0} by A1,MCART_1:10,21;
hence thesis by A2,A5,TARSKI:def 1;
end;
theorem Th16:
for A being non empty set, o being OperSymbol of CatSign A holds
o`1 = 1 & len o`2 = 1 or o`1 = 2 & len o`2 = 3
proof
let A be non empty set, o be OperSymbol of CatSign A;
the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
:] by Def3;
then o in [:{1},1-tuples_on A:] or o in [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
then o`1 in {1} & o`2 in 1-tuples_on A or o`1 in {2} & o`2 in 3-tuples_on A
by MCART_1:10;
hence thesis by CARD_1:def 7,TARSKI:def 1;
end;
theorem Th17:
for A being non empty set, o being OperSymbol of CatSign A st o
`1 = 1 or len o`2 = 1 ex a being Element of A st o = idsym(a)
proof
let A be non empty set, o be OperSymbol of CatSign A such that
A1: o`1 = 1 or len o`2 = 1;
the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
:] by Def3;
then o in [:{1},1-tuples_on A:] or o in [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
then
A2: o`1 in {1} & o`2 in 1-tuples_on A & o = [o`1,o`2] or o`1 in {2} & o`2 in
3-tuples_on A by MCART_1:10,21;
then consider a being set such that
A3: a in A and
A4: o`2 = <*a*> by A1,CARD_1:def 7,FINSEQ_2:135,TARSKI:def 1;
reconsider a as Element of A by A3;
take a;
thus thesis by A1,A2,A4,CARD_1:def 7,TARSKI:def 1;
end;
theorem Th18:
for A being non empty set, o being OperSymbol of CatSign A st o
`1 = 2 or len o`2 = 3 ex a,b,c being Element of A st o = compsym(a,b,c)
proof
let A be non empty set, o be OperSymbol of CatSign A such that
A1: o`1 = 2 or len o`2 = 3;
the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
:] by Def3;
then o in [:{1},1-tuples_on A:] or o in [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
then
A2: o`1 in {1} & o`2 in 1-tuples_on A or o`1 in {2} & o`2 in 3-tuples_on A &
o = [o`1,o`2] by MCART_1:10,21;
then consider a,b,c being object such that
A3: a in A & b in A & c in A and
A4: o`2 = <*a,b,c*> by A1,CARD_1:def 7,FINSEQ_2:139,TARSKI:def 1;
reconsider a,b,c as Element of A by A3;
take a,b,c;
thus thesis by A1,A2,A4,CARD_1:def 7,TARSKI:def 1;
end;
theorem
for A being non empty set, a being Element of A holds the_arity_of
idsym(a) = {} & the_result_sort_of idsym(a) = homsym(a,a) by Def3;
theorem
for A being non empty set, a,b,c being Element of A holds the_arity_of
compsym(a,b,c) = <*homsym(b,c),homsym(a,b)*> & the_result_sort_of compsym(a,b,c
) = homsym(a,c) by Def3;
begin :: Signature homomorphism generated by a functor
definition
let C1,C2 be Category;
let F be Functor of C1,C2;
func Upsilon F -> Function of the carrier of CatSign the carrier of C1, the
carrier of CatSign the carrier of C2 means
: Def11:
for s being SortSymbol of
CatSign the carrier of C1 holds it.s = [0,(Obj F)*s`2];
uniqueness
proof
let U1,U2 be Function of the carrier of CatSign the carrier of C1, the
carrier of CatSign the carrier of C2 such that
A1: for s being SortSymbol of CatSign the carrier of C1 holds U1.s = [
0,(Obj F)*s`2] and
A2: for s being SortSymbol of CatSign the carrier of C1 holds U2.s = [
0,(Obj F)*s`2];
now
let s be SortSymbol of CatSign the carrier of C1;
thus U1.s = [0,(Obj F)*s`2] by A1
.= U2.s by A2;
end;
hence thesis;
end;
existence
proof
deffunc f(SortSymbol of CatSign the carrier of C1) = [0,(Obj F)*$1`2];
consider Up being Function such that
A3: dom Up = the carrier of CatSign the carrier of C1 and
A4: for s being SortSymbol of CatSign the carrier of C1 holds Up.s = f
(s) from FUNCT_1:sch 4;
rng Up c= the carrier of CatSign the carrier of C2
proof
let x be object;
assume x in rng Up;
then consider a being object such that
A5: a in dom Up and
A6: x = Up.a by FUNCT_1:def 3;
reconsider a as SortSymbol of CatSign the carrier of C1 by A3,A5;
the carrier of CatSign the carrier of C1 = [:{0},2-tuples_on the
carrier of C1:] by Def3;
then a`2 in 2-tuples_on the carrier of C1 by MCART_1:12;
then consider a1,a2 being object such that
A7: a1 in the carrier of C1 & a2 in the carrier of C1 and
A8: a`2 = <*a1,a2*> by FINSEQ_2:137;
reconsider a1,a2 as Object of C1 by A7;
rng <*a1,a2*> c= the carrier of C1 & dom Obj F = the carrier of C1
by FUNCT_2:def 1;
then
A9: dom ((Obj F)*<*a1,a2*>) = dom <*a1,a2*> by RELAT_1:27
.= Seg 2 by FINSEQ_1:89;
then reconsider p = (Obj F)*<*a1,a2*> as FinSequence by FINSEQ_1:def 2;
<*a1,a2*>.1 = a1 & 1 in {1,2} by TARSKI:def 2;
then
A10: p.1 = (Obj F).a1 by A9,FINSEQ_1:2,FUNCT_1:12;
A11: the carrier of CatSign the carrier of C2 = [:{0},2-tuples_on the
carrier of C2:] by Def3;
<*a1,a2*>.2 = a2 & 2 in {1,2} by TARSKI:def 2;
then
A12: p.2 = (Obj F).a2 by A9,FINSEQ_1:2,FUNCT_1:12;
len p = 2 by A9,FINSEQ_1:def 3;
then p = <*(Obj F).a1, (Obj F).a2*> by A10,A12,FINSEQ_1:44;
then p in 2-tuples_on the carrier of C2 by FINSEQ_2:101;
then [0,p] in the carrier of CatSign the carrier of C2 by A11,
ZFMISC_1:105;
hence thesis by A4,A6,A8;
end;
then Up is Function of the carrier of CatSign the carrier of C1, the
carrier of CatSign the carrier of C2 by A3,FUNCT_2:def 1,RELSET_1:4;
hence thesis by A4;
end;
func Psi F -> Function of the carrier' of CatSign the carrier of C1, the
carrier' of CatSign the carrier of C2 means
: Def12:
for o being OperSymbol of
CatSign the carrier of C1 holds it.o = [o`1,(Obj F)*o`2];
uniqueness
proof
let U1,U2 be Function of the carrier' of CatSign the carrier of C1, the
carrier' of CatSign the carrier of C2 such that
A13: for s being OperSymbol of CatSign the carrier of C1 holds U1.s =
[s`1,(Obj F)*s`2] and
A14: for s being OperSymbol of CatSign the carrier of C1 holds U2.s =
[s`1,(Obj F)*s`2];
now
let s be OperSymbol of CatSign the carrier of C1;
thus U1.s = [s`1,(Obj F)*s`2] by A13
.= U2.s by A14;
end;
hence thesis;
end;
existence
proof
deffunc f(OperSymbol of CatSign the carrier of C1) = [ $1`1,(Obj F)*$1`2 ];
consider Up being Function such that
A15: dom Up = the carrier' of CatSign the carrier of C1 and
A16: for s being OperSymbol of CatSign the carrier of C1 holds Up.s =
f(s) from FUNCT_1:sch 4;
rng Up c= the carrier' of CatSign the carrier of C2
proof
let x be object;
assume x in rng Up;
then consider a being object such that
A17: a in dom Up and
A18: x = Up.a by FUNCT_1:def 3;
A19: the carrier' of CatSign the carrier of C1 = [:{1},1-tuples_on the
carrier of C1:] \/ [:{2},3-tuples_on the carrier of C1:] by Def3;
reconsider a as OperSymbol of CatSign the carrier of C1 by A15,A17;
per cases by A19,XBOOLE_0:def 3;
suppose
A20: a in [:{1},1-tuples_on the carrier of C1:];
then a`2 in 1-tuples_on the carrier of C1 by MCART_1:12;
then consider a1 being set such that
A21: a1 in the carrier of C1 and
A22: a`2 = <*a1*> by FINSEQ_2:135;
reconsider a1 as Object of C1 by A21;
rng <*a1*> c= the carrier of C1 & dom Obj F = the carrier of C1
by FUNCT_2:def 1;
then
A23: dom ((Obj F)*<*a1*>) = dom <*a1*> by RELAT_1:27
.= Seg 1 by FINSEQ_1:38;
then reconsider p = (Obj F)*<*a1*> as FinSequence by FINSEQ_1:def 2;
A24: len p = 1 by A23,FINSEQ_1:def 3;
<*a1*>.1 = a1 & 1 in {1} by TARSKI:def 1;
then p.1 = (Obj F).a1 by A23,FINSEQ_1:2,FUNCT_1:12;
then p = <*(Obj F).a1*> by A24,FINSEQ_1:40;
then p is Element of 1-tuples_on the carrier of C2 by FINSEQ_2:98;
then
A25: [1,p] in [:{1},1-tuples_on the carrier of C2:] by ZFMISC_1:105;
A26: a`1 = 1 by A20,MCART_1:12;
the carrier' of CatSign the carrier of C2 = [:{1},1-tuples_on the
carrier of C2:] \/ [:{2},3-tuples_on the carrier of C2:] by Def3;
then [1,p] in the carrier' of CatSign the carrier of C2 by A25,
XBOOLE_0:def 3;
hence thesis by A16,A18,A26,A22;
end;
suppose
A27: a in [:{2},3-tuples_on the carrier of C1:];
then a`2 in 3-tuples_on the carrier of C1 by MCART_1:12;
then consider a1,a2,a3 being object such that
A28: a1 in the carrier of C1 & a2 in the carrier of C1 & a3 in the
carrier of C1 and
A29: a`2 = <*a1,a2,a3*> by FINSEQ_2:139;
reconsider a1,a2,a3 as Object of C1 by A28;
rng <*a1,a2,a3*> c= the carrier of C1 & dom Obj F = the carrier
of C1 by FUNCT_2:def 1;
then
A30: dom ((Obj F)*<*a1,a2,a3*>) = dom <*a1,a2,a3*> by RELAT_1:27
.= Seg 3 by FINSEQ_1:89;
then reconsider p = (Obj F)*<*a1,a2,a3*> as FinSequence by
FINSEQ_1:def 2;
<*a1,a2,a3*>.1 = a1 & 1 in {1,2,3} by ENUMSET1:def 1;
then
A31: p.1 = (Obj F).a1 by A30,FINSEQ_3:1,FUNCT_1:12;
<*a1,a2,a3*>.3 = a3 & 3 in {1,2,3} by ENUMSET1:def 1;
then
A32: p.3 = (Obj F). a3 by A30,FINSEQ_3:1,FUNCT_1:12;
<*a1,a2,a3*>.2 = a2 & 2 in {1,2,3} by ENUMSET1:def 1;
then
A33: p.2 = (Obj F).a2 by A30,FINSEQ_3:1,FUNCT_1:12;
len p = 3 by A30,FINSEQ_1:def 3;
then p = <*(Obj F).a1, (Obj F).a2, (Obj F).a3*> by A31,A33,A32,
FINSEQ_1:45;
then p is Element of 3-tuples_on the carrier of C2 by FINSEQ_2:104;
then
A34: [2,p] in [:{2},3-tuples_on the carrier of C2:] by ZFMISC_1:105;
A35: a`1 = 2 by A27,MCART_1:12;
the carrier' of CatSign the carrier of C2 = [:{1},1-tuples_on the
carrier of C2:] \/ [:{2},3-tuples_on the carrier of C2:] by Def3;
then [2,p] in the carrier' of CatSign the carrier of C2 by A34,
XBOOLE_0:def 3;
hence thesis by A16,A18,A35,A29;
end;
end;
then Up is Function of the carrier' of CatSign the carrier of C1, the
carrier' of CatSign the carrier of C2 by A15,FUNCT_2:def 1,RELSET_1:4;
hence thesis by A16;
end;
end;
Lm4: now
let x be set, f be Function;
assume x in dom f;
then rng <*x*> = {x} & {x} c= dom f by FINSEQ_1:39,ZFMISC_1:31;
then
A1: dom (f*<*x*>) = dom <*x*> by RELAT_1:27
.= Seg 1 by FINSEQ_1:38;
then reconsider p = f*<*x*> as FinSequence by FINSEQ_1:def 2;
A2: len p = 1 by A1,FINSEQ_1:def 3;
1 in {1} & <*x*>.1 = x by TARSKI:def 1;
then p.1 = f.x by A1,FINSEQ_1:2,FUNCT_1:12;
hence f*<*x*> = <*f.x*> by A2,FINSEQ_1:40;
end;
theorem Th21:
for C1,C2 being Category, F being Functor of C1,C2 for a,b being
Object of C1 holds (Upsilon F).homsym(a,b) = homsym(F.a,F.b)
proof
let C1,C2 be Category, F be Functor of C1,C2;
let a,b be Object of C1;
A1: dom Obj F = the carrier of C1 by FUNCT_2:def 1;
thus (Upsilon F).homsym(a,b) = [0,(Obj F)*(homsym(a,b))`2] by Def11
.= [0,(Obj F)*<*a,b*>]
.= [0,<*(Obj F).a,(Obj F).b*>] by A1,FINSEQ_2:125
.= [0,<*F.a,(Obj F).b*>]
.= homsym(F.a,F.b);
end;
theorem Th22:
for C1,C2 being Category, F being Functor of C1,C2 for a being
Object of C1 holds (Psi F).idsym(a) = idsym(F.a)
proof
let C1,C2 be Category, F be Functor of C1,C2;
let a be Object of C1;
A1: dom Obj F = the carrier of C1 by FUNCT_2:def 1;
(idsym a)`1 = 1 & (idsym a)`2 = <*a*>;
hence (Psi F).idsym(a) = [1,(Obj F)*<*a*>] by Def12
.= [1,<*(Obj F).a*>] by A1,Lm4
.= idsym(F.a);
end;
theorem Th23:
for C1,C2 being Category, F being Functor of C1,C2 for a,b,c
being Object of C1 holds (Psi F).compsym(a,b,c) = compsym(F.a,F.b,F.c)
proof
let C1,C2 be Category, F be Functor of C1,C2;
let a,b,c be Object of C1;
A1: dom Obj F = the carrier of C1 by FUNCT_2:def 1;
(compsym(a,b,c))`1 = 2 & (compsym(a,b,c))`2 = <*a,b,c*>;
hence (Psi F).compsym(a,b,c) = [2,(Obj F)*<*a,b,c*>] by Def12
.= [2,<*(Obj F).a,(Obj F).b,(Obj F).c*>] by A1,FINSEQ_2:126
.= [2,<*F.a,(Obj F).b,(Obj F).c*>]
.= [2,<*F.a,F.b,(Obj F).c*>]
.= compsym(F.a,F.b,F.c);
end;
theorem Th24:
for C1,C2 being Category, F being Functor of C1,C2 holds Upsilon
F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier
of C2
proof
let C1,C2 be Category, F be Functor of C1,C2;
set f = Upsilon F, g = Psi F;
set S1 = CatSign the carrier of C1, S2 = CatSign the carrier of C2;
thus dom f = the carrier of S1 & dom g = the carrier' of S1 by FUNCT_2:def 1;
thus rng f c= the carrier of S2 & rng g c= the carrier' of S2;
now
let o be OperSymbol of CatSign the carrier of C1;
per cases by Th16;
suppose
o`1 = 1;
then consider a being Object of C1 such that
A1: o = idsym(a) by Th17;
thus (f*the ResultSort of S1).o = f.the_result_sort_of o by FUNCT_2:15
.= f.homsym(a,a) by A1,Def3
.= homsym(F.a,F.a) by Th21
.= the_result_sort_of idsym(F.a) by Def3
.= (the ResultSort of S2).(g.idsym a) by Th22
.= ((the ResultSort of S2)*g).o by A1,FUNCT_2:15;
end;
suppose
o`1 = 2;
then consider a,b,c being Object of C1 such that
A2: o = compsym(a,b,c) by Th18;
thus (f*the ResultSort of S1).o = f.the_result_sort_of o by FUNCT_2:15
.= f.homsym(a,c) by A2,Def3
.= homsym(F.a,F.c) by Th21
.= the_result_sort_of compsym(F.a,F.b,F.c) by Def3
.= (the ResultSort of S2).(g.compsym(a,b,c)) by Th23
.= ((the ResultSort of S2)*g).o by A2,FUNCT_2:15;
end;
end;
hence f*the ResultSort of S1 = (the ResultSort of S2)*g;
let o be set, p be Function;
assume o in the carrier' of S1;
then reconsider o9 = o as OperSymbol of S1;
assume
A3: p = (the Arity of S1).o;
per cases by Th16;
suppose
o9`1 = 1;
then consider a being Object of C1 such that
A4: o = idsym(a) by Th17;
A5: f*{} = {};
p = {} by A3,A4,Def3;
hence f*p = the_arity_of idsym(F.a) by A5,Def3
.= (the Arity of S2).(g.o) by A4,Th22;
end;
suppose
o9`1 = 2;
then consider a,b,c being Object of C1 such that
A6: o = compsym(a,b,c) by Th18;
dom f = the carrier of S1 & p = <*homsym(b,c),homsym(a,b)*> by A3,A6,Def3,
FUNCT_2:def 1;
hence f*p = <*f.homsym(b,c),f.homsym(a,b)*> by FINSEQ_2:125
.= <*homsym(F.b,F.c),f.homsym(a,b)*> by Th21
.= <*homsym(F.b,F.c),homsym(F.a,F.b)*> by Th21
.= the_arity_of compsym(F.a,F.b,F.c) by Def3
.= (the Arity of S2).(g.o) by A6,Th23;
end;
end;
begin :: Algebra of morphisms
theorem Th25:
for C being non empty set, A being MSAlgebra over CatSign C for
a being Element of C holds Args(idsym(a), A) = {{}}
proof
let C be non empty set, A be MSAlgebra over CatSign C;
let a be Element of C;
thus Args(idsym(a), A) = product ((the Sorts of A)*the_arity_of idsym a) by
PRALG_2:3
.= product ((the Sorts of A)*{}) by Def3
.= {{}} by CARD_3:10;
end;
Lm5: for C being Category, A being MSAlgebra over CatSign the carrier of C st
for a,b being Object of C holds (the Sorts of A).homsym(a,b) = Hom(a,b) for a,b
,c being Object of C holds Args(compsym(a,b,c), A) = product <*Hom(b,c),Hom(a,b
)*> & Result(compsym(a,b,c), A) = Hom(a,c)
proof
let C be Category, A be MSAlgebra over CatSign the carrier of C;
assume
A1: for a,b being Object of C holds (the Sorts of A).homsym(a,b) = Hom(a ,b);
let a,b,c be Object of C;
A2: the carrier of CatSign the carrier of C = dom the Sorts of A by
PARTFUN1:def 2;
thus Args(compsym(a,b,c), A) = product ((the Sorts of A)*the_arity_of
compsym(a,b,c)) by PRALG_2:3
.= product ((the Sorts of A)*<*homsym(b,c),homsym(a,b)*>) by Def3
.= product <*(the Sorts of A).homsym(b,c), (the Sorts of A).homsym(a,b)
*> by A2,FINSEQ_2:125
.= product <*Hom(b,c), (the Sorts of A).homsym(a,b)*> by A1
.= product <*Hom(b,c), Hom(a,b)*> by A1;
thus Result(compsym(a,b,c), A) = (the Sorts of A).the_result_sort_of compsym
(a,b,c) by PRALG_2:3
.= (the Sorts of A).homsym(a,c) by Def3
.= Hom(a,c) by A1;
end;
scheme
CatAlgEx { X, Y() -> non empty set, H(set,set) -> set,
R(set,set,set,object,object) -> set, I(set) -> set}:
ex A being strict MSAlgebra over CatSign X() st (for
a,b being Element of X() holds (the Sorts of A).homsym(a,b) = H(a,b)) & (for a
being Element of X() holds Den(idsym(a),A).{} = I(a)) & for a,b,c being Element
of X() for f,g being Element of Y() st f in H(a,b) & g in H(b,c) holds Den(
compsym(a,b,c),A).<*g,f*> = R(a,b,c,g,f)
provided
A1: for a,b being Element of X() holds H(a,b) c= Y() and
A2: for a being Element of X() holds I(a) in H(a,a) and
A3: for a,b,c being Element of X() for f,g being Element of Y() st f in
H(a,b) & g in H(b,c) holds R(a,b,c,g,f) in H(a,c)
proof
defpred Z[object,object] means
($1`1 = 1 & ex a being Element of X() st $1 = idsym
(a) & ex F being Function of {{}}, H(a,a) st F = $2 & F.{} = I(a)) or ($1`1 = 2
& ex a,b,c being Element of X() st $1 = compsym(a,b,c) & ex F being Function of
product<*H(b,c),H(a,b)*>, H(a,c) st F = $2 & for f,g being set st f in H(a,b) &
g in H(b,c) holds F.<*g,f*> = R(a,b,c,g,f));
set CS = CatSign X();
A4: for o be object st o in the carrier' of CS ex u be object st Z[o,u]
proof
let o be object;
assume
A5: o in the carrier' of CS;
A6: now
assume o`1 = 1;
then consider a being Element of X() such that
A7: o = idsym a by A5,Th17;
set F = {} :-> I(a);
reconsider u = F as set;
take u, a;
thus o = idsym(a) by A7;
I(a) in H(a,a) by A2;
then {I(a)} c= H(a,a) by ZFMISC_1:31;
then dom F = {{}} & rng F c= H(a,a);
then reconsider F as Function of {{}}, H(a,a) by FUNCT_2:2;
take F;
{} in {{}} by TARSKI:def 1;
hence F = u & F.{} = I(a) by FUNCOP_1:7;
end;
A8: now
assume o`1 = 2;
then consider a,b,c being Element of X() such that
A9: o = compsym(a,b,c) by A5,Th18;
defpred P[object,object] means
ex f,g being set st f in H(a,b) & g in H(b,c) &
$1 = <*g,f*> & $2 = R(a,b,c,g,f);
A10: now
let x be object;
assume x in product<*H(b,c),H(a,b)*>;
then consider g,f being object such that
A11: g in H(b,c) & f in H(a,b) and
A12: x = <*g,f*> by FINSEQ_3:124;
reconsider u = R(a,b,c,g,f) as object;
take u;
H(a,b) c= Y() & H(b,c) c= Y() by A1;
hence u in H(a,c) by A3,A11;
thus P[x,u] by A11,A12;
end;
consider F being Function such that
A13: dom F = product<*H(b,c),H(a,b)*> & rng F c= H(a,c) and
A14: for x being object st x in product<*H(b,c),H(a,b)*> holds P[x,F.x]
from FUNCT_1:sch 6(A10);
reconsider u = F as set;
take u, a, b, c;
thus o = compsym(a,b,c) by A9;
reconsider F as Function of product<*H(b,c),H(a,b)*>, H(a,c) by A13,
FUNCT_2:2;
take F;
thus F = u;
let f,g be set;
assume f in H(a,b) & g in H(b,c);
then <*g,f*> in product<*H(b,c),H(a,b)*> by FINSEQ_3:124;
then consider f9,g9 being set such that
f9 in H(a,b) and
g9 in H(b,c) and
A15: <*g,f*> = <*g9,f9*> and
A16: F.<*g,f*> = R(a,b,c,g9,f9) by A14;
A17: <*g,f*>.1 = g & <*g,f*>.2 = f;
<*g,f*>.1 = g9 by A15,FINSEQ_1:44;
hence F.<*g,f*> = R(a,b,c,g,f) by A15,A16,A17,FINSEQ_1:44;
end;
o`1 = 1 or o`1 = 2 by A5,Th16;
hence thesis by A6,A8;
end;
consider O being Function such that
A18: dom O = the carrier' of CS and
A19: for o being object st o in the carrier' of CS holds Z[o,O.o] from
CLASSES1:sch 1(A4);
reconsider O as ManySortedSet of the carrier' of CS by A18,PARTFUN1:def 2
,RELAT_1:def 18;
defpred P[object,object] means
ex a,b being Element of X() st $1 = homsym(a,b) &
$2 = H(a,b);
A20: now
let s be object;
assume s in the carrier of CS;
then consider a,b being Element of X() such that
A21: s = homsym(a,b) by Th15;
reconsider u = H(a,b) as object;
take u;
thus P[s,u] by A21;
end;
consider S being Function such that
A22: dom S = the carrier of CS and
A23: for s being object st s in the carrier of CS holds P[s,S.s] from
CLASSES1:sch 1(A20);
reconsider S as ManySortedSet of the carrier of CS by A22,PARTFUN1:def 2
,RELAT_1:def 18;
O is ManySortedFunction of S#*the Arity of CS, S*the ResultSort of CS
proof
let o be object;
assume o in the carrier' of CS;
then reconsider o as OperSymbol of CS;
A24: (S#*the Arity of CS).o = S#.the_arity_of o by FUNCT_2:15
.= product (S*the_arity_of o) by FINSEQ_2:def 5;
A25: (S*the ResultSort of CS).o = S.the_result_sort_of o by FUNCT_2:15;
per cases by Th16;
suppose
o`1 = 1 & 1 <> 2;
then consider a being Element of X() such that
A26: o = idsym a & ex F being Function of {{}}, H(a,a) st F = O.o &
F.{} = I(a) by A19;
A27: the_arity_of idsym(a) = {} & {} = S*{} by Def3;
A28: the_result_sort_of idsym(a) = homsym(a,a) by Def3;
consider c,b being Element of X() such that
A29: homsym(a,a) = homsym(c,b) and
A30: S.homsym(a,a) = H(c,b) by A23;
a = b & a = c by A29,Th13;
hence thesis by A24,A25,A26,A30,A27,A28,CARD_3:10;
end;
suppose
o`1 = 2 & 1 <> 2;
then consider a,b,c being Element of X() such that
A31: o = compsym(a,b,c) and
A32: ex F being Function of product<*H(b,c),H(a,b)*>, H(a,c) st F =
O.o & for f,g being set st f in H(a,b) & g in H(b,c) holds F.<*g,f*> = R(a,b,c,
g,f) by A19;
A33: the_result_sort_of compsym(a,b,c) = homsym(a,c) by Def3;
consider ax,cx being Element of X() such that
A34: homsym(a,c) = homsym(ax,cx) and
A35: S.homsym(a,c) = H(ax,cx) by A23;
ax = a & cx = c by A34,Th13;
then
A36: (S*the ResultSort of CS).o = H(a,c) by A31,A35,A33,FUNCT_2:15;
A37: the_arity_of compsym(a,b,c) = <*homsym(b,c),homsym(a,b)*> by Def3;
consider a9,b9 being Element of X() such that
A38: homsym(a,b) = homsym(a9,b9) and
A39: S.homsym(a,b) = H(a9,b9) by A23;
consider b99,c9 being Element of X() such that
A40: homsym(b,c) = homsym(b99,c9) and
A41: S.homsym(b,c) = H(b99,c9) by A23;
A42: b99 = b & c9 = c by A40,Th13;
a9 = a & b9 = b by A38,Th13;
then
(S#*the Arity of CS).o = product<*H(b,c),H(a,b)*> by A22,A24,A31,A39,A41
,A42,A37,FINSEQ_2:125;
hence thesis by A32,A36;
end;
end;
then reconsider
O as ManySortedFunction of S#*the Arity of CS, S*the ResultSort
of CS;
take A = MSAlgebra(#S, O#);
hereby
let a,b be Element of X();
consider a9,b9 being Element of X() such that
A43: homsym(a,b) = homsym(a9,b9) and
A44: S.homsym(a,b) = H(a9,b9) by A23;
a = a9 by A43,Th13;
hence (the Sorts of A).homsym(a,b) = H(a,b) by A43,A44,Th13;
end;
hereby
let a be Element of X();
(idsym a)`1 = 1;
then ex b being Element of X() st idsym a = idsym b & ex F being Function
of {{}}, H(b,b) st F = O.idsym a & F.{} = I(b) by A19;
hence Den(idsym(a),A).{} = I(a) by Th12;
end;
let a,b,c be Element of X();
set o = compsym(a,b,c);
o`1 = 2;
then consider a9,b9,c9 being Element of X() such that
A45: o = compsym(a9,b9,c9) and
A46: ex F being Function of product<*H(b9,c9),H(a9,b9)*>, H(a9,c9) st F
= O.o & for f,g being set st f in H(a9,b9) & g in H(b9,c9) holds F.<*g,f*> = R(
a9,b9,c9,g,f) by A19;
A47: c = c9 by A45,Th14;
let f,g be Element of Y();
assume
A48: f in H(a,b) & g in H(b,c);
a = a9 & b = b9 by A45,Th14;
hence thesis by A46,A47,A48;
end;
definition
let C be Category;
func MSAlg C -> strict MSAlgebra over CatSign the carrier of C means
: Def13
:
( for a,b being Object of C holds (the Sorts of it).homsym(a,b) = Hom(a,b)) &
(for a being Object of C holds Den(idsym(a),it).{} = id a) & for a,b,c being
Object of C for f,g being Morphism of C st dom f = a & cod f = b & dom g = b &
cod g = c holds Den(compsym(a,b,c),it).<*g,f*> = g(*)f;
uniqueness
proof
let A1,A2 be strict MSAlgebra over CatSign the carrier of C such that
A1: for a,b being Object of C holds (the Sorts of A1).homsym(a,b) =
Hom(a,b) and
A2: for a being Object of C holds Den(idsym(a),A1).{} = id a and
A3: for a,b,c being Object of C for f,g being Morphism of C st dom f =
a & cod f = b & dom g = b & cod g = c
holds Den(compsym(a,b,c),A1).<*g,f*> = g(*)
f and
A4: for a,b being Object of C holds (the Sorts of A2).homsym(a,b) =
Hom(a,b) and
A5: for a being Object of C holds Den(idsym(a),A2).{} = id a and
A6: for a,b,c being Object of C for f,g being Morphism of C st dom f =
a & cod f = b & dom g = b & cod g = c
holds Den(compsym(a,b,c),A2).<*g,f*> = g(*)
f;
A7: now
let i be object;
assume i in the carrier' of CatSign the carrier of C;
then reconsider o = i as OperSymbol of CatSign the carrier of C;
per cases by Th16;
suppose
o`1 = 1;
then consider a being Object of C such that
A8: o = idsym(a) by Th17;
A9: id a in Hom(a,a) by CAT_1:27;
A10: the_result_sort_of idsym a = homsym(a,a) by Def3;
(the Sorts of A1).homsym(a,a) = Hom(a,a) by A1;
then Result(idsym a,A1) = Hom(a,a) by A10,PRALG_2:3;
then
A11: dom Den(idsym a,A1) = Args(idsym a,A1) by A9,FUNCT_2:def 1;
A12: now
let x be object;
assume x in {{}};
then
A13: x = {} by TARSKI:def 1;
then Den(idsym a,A1).x = id a by A2;
hence Den(idsym a,A1).x = Den(idsym a,A2).x by A5,A13;
end;
(the Sorts of A2).homsym(a,a) = Hom(a,a) by A4;
then Result(idsym a,A2) = Hom(a,a) by A10,PRALG_2:3;
then
A14: dom Den(idsym a,A2) = Args(idsym a,A2) by A9,FUNCT_2:def 1;
Args(idsym a,A1) = {{}} & Args(idsym a,A2) = {{}} by Th25;
hence (the Charact of A1).i = (the Charact of A2).i by A8,A11,A14,A12,
FUNCT_1:2;
end;
suppose
o`1 = 2;
then consider a,b,c being Object of C such that
A15: o = compsym(a,b,c) by Th18;
A16: now
assume product <*Hom(b,c),Hom(a,b)*> <> {};
then reconsider X = product <*Hom(b,c),Hom(a,b)*> as non empty set;
set x = the Element of X;
consider g,f being object such that
A17: g in Hom(b,c) and
A18: f in Hom(a,b) and
x = <*g,f*> by FINSEQ_3:124;
reconsider g,f as Morphism of C by A17,A18;
A19: cod f = b & dom g = b by A17,A18,CAT_1:1;
cod g = c by A17,CAT_1:1;
then
A20: cod (g(*)f) = c by A19,CAT_1:17;
dom f = a by A18,CAT_1:1;
then dom (g(*)f) = a by A19,CAT_1:17;
hence Hom(a,c) <> {} by A20,CAT_1:1;
end;
A21: now
let x be object;
assume x in product <*Hom(b,c),Hom(a,b)*>;
then consider g,f being object such that
A22: g in Hom(b,c) and
A23: f in Hom(a,b) and
A24: x = <*g,f*> by FINSEQ_3:124;
reconsider g,f as Morphism of C by A22,A23;
A25: dom g = b & cod g = c by A22,CAT_1:1;
A26: dom f = a & cod f = b by A23,CAT_1:1;
then Den(compsym(a,b,c),A1).x = g(*)f by A3,A24,A25;
hence Den(compsym(a,b,c),A1).x = Den(compsym(a,b,c),A2).x by A6,A24
,A26,A25;
end;
A27: Args(compsym(a,b,c),A1) = product <*Hom(b,c),Hom(a,b)*> by A1,Lm5;
A28: Args(compsym(a,b,c),A2) = product <*Hom(b,c),Hom(a,b)*> by A4,Lm5;
Result(compsym(a,b,c),A2) = Hom(a,c) by A4,Lm5;
then
A29: dom Den(compsym(a,b,c),A2) = Args(compsym(a,b,c),A2) by A28,A16,
FUNCT_2:def 1;
Result(compsym(a,b,c),A1) = Hom(a,c) by A1,Lm5;
then dom Den(compsym(a,b,c),A1) = Args(compsym(a,b,c),A1) by A27,A16,
FUNCT_2:def 1;
hence (the Charact of A1).i = (the Charact of A2).i by A15,A27,A28,A29
,A21,FUNCT_1:2;
end;
end;
now
let i be object;
assume i in the carrier of CatSign the carrier of C;
then consider a,b being Object of C such that
A30: i = homsym(a,b) by Th15;
thus (the Sorts of A1).i = Hom(a,b) by A1,A30
.= (the Sorts of A2).i by A4,A30;
end;
then the Sorts of A1 = the Sorts of A2;
hence thesis by A7,PBOOLE:3;
end;
correctness
proof
deffunc I(Object of C) = id $1;
deffunc R(Object of C,Object of C,Object of C, (Morphism of C), Morphism
of C) = $4(*)$5;
deffunc H(Object of C,Object of C) = Hom($1,$2);
A31: for a being Object of C holds I(a) in H(a,a) by CAT_1:27;
A32: now
let a,b,c be Object of C, f,g be Morphism of C;
assume that
A33: f in H(a,b) and
A34: g in H(b,c);
A35: cod f = b & dom g = b by A33,A34,CAT_1:1;
cod g = c by A34,CAT_1:1;
then
A36: cod (g(*)f) = c by A35,CAT_1:17;
dom f = a by A33,CAT_1:1;
then dom (g(*)f) = a by A35,CAT_1:17;
hence R(a,b,c,g,f) in H(a,c) by A36;
end;
A37: for a,b being Object of C holds H(a,b) c= the carrier' of C;
consider A being strict MSAlgebra over CatSign the carrier of C such that
A38: ( for a,b being Element of C holds (the Sorts of A
).homsym(a,b) = H(a,b))& for a being Element of C holds Den(
idsym(a),A).{} = I(a) and
A39: for a,b,c being Element of C for f,g being Element
of the carrier' of C st f in H(a,b) & g in H(b,c) holds Den(compsym(a,b,c),A).
<*g,f*> = R(a,b,c,g,f) from CatAlgEx(A37,A31,A32);
take A;
now
let a,b,c be Object of C, f,g be Morphism of C;
assume dom f = a & cod f = b & dom g = b & cod g = c;
then f in Hom(a,b) & g in Hom(b,c);
hence Den(compsym(a,b,c),A).<*g,f*> = g(*)f by A39;
end;
hence thesis by A38;
end;
end;
theorem Th26:
for A being Category, a being Object of A holds Result(idsym a,
MSAlg A) = Hom(a,a)
proof
let A be Category, a be Object of A;
thus Result(idsym a, MSAlg A) = (the Sorts of MSAlg A).the_result_sort_of
idsym a by PRALG_2:3
.= (the Sorts of MSAlg A).homsym(a,a) by Def3
.= Hom(a,a) by Def13;
end;
theorem Th27:
for A being Category, a,b,c being Object of A holds Args(compsym
(a,b,c), MSAlg A) = product <*Hom(b,c), Hom(a,b)*> & Result(compsym(a,b,c),
MSAlg A) = Hom(a,c)
proof
let A be Category, a,b,c be Object of A;
for a,b being Object of A holds (the Sorts of MSAlg A).homsym(a,b) = Hom
(a,b) by Def13;
hence thesis by Lm5;
end;
registration
let C be Category;
cluster MSAlg C -> disjoint_valued feasible;
coherence
proof
hereby
let x,y be object;
assume that
A1: x <> y and
A2: (the Sorts of MSAlg C).x meets (the Sorts of MSAlg C).y;
consider z being object such that
A3: z in (the Sorts of MSAlg C).x and
A4: z in (the Sorts of MSAlg C).y by A2,XBOOLE_0:3;
dom the Sorts of MSAlg C = the carrier of CatSign the carrier of C
by PARTFUN1:def 2;
then reconsider x,y as SortSymbol of CatSign the carrier of C by A3,A4,
FUNCT_1:def 2;
consider a,b being Object of C such that
A5: x = homsym(a,b) by Th15;
A6: z in Hom(a,b) by A3,A5,Def13;
consider c,d being Object of C such that
A7: y = homsym(c,d) by Th15;
A8: z in Hom(c,d) by A4,A7,Def13;
reconsider z as Morphism of C by A6;
A9: dom z = a & cod z = b by A6,CAT_1:1;
dom z = c by A8,CAT_1:1;
hence contradiction by A1,A5,A7,A8,A9,CAT_1:1;
end;
let o be OperSymbol of CatSign the carrier of C;
per cases by Th16;
suppose
o`1 = 1;
then consider a being Object of C such that
A10: o = idsym a by Th17;
Result(o, MSAlg C) = Hom(a,a) by A10,Th26;
hence thesis by CAT_1:27;
end;
suppose
o`1 = 2;
then consider a,b,c being Object of C such that
A11: o = compsym(a,b,c) by Th18;
set A = the Element of Args(o, MSAlg C);
assume
A12: Args(o, MSAlg C) <> {};
Args(o, MSAlg C) = product <*Hom(b,c), Hom(a,b)*> by A11,Th27;
then
A13: ex g,f being object st g in Hom(b,c) & f in Hom(a,b) & A = <*g,f*>
by A12,FINSEQ_3:124;
Result(o, MSAlg C) = Hom(a,c) by A11,Th27;
hence thesis by A13,CAT_1:24;
end;
end;
end;
theorem Th28:
for C1,C2 being Category, F being Functor of C1,C2 holds F-MSF(
the carrier of CatSign the carrier of C1, the Sorts of MSAlg C1) is
ManySortedFunction of MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1, Upsilon
F, Psi F)
proof
let C1,C2 be Category, F be Functor of C1,C2;
set S1 = CatSign the carrier of C1, S2 = CatSign the carrier of C2;
set A1 = MSAlg C1, A2 = MSAlg C2;
set f = Upsilon F, g = Psi F, B1 = A2|(S1, f, g);
set H = F-MSF(the carrier of S1, the Sorts of A1);
let i be object;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
consider a,b being Object of C1 such that
A1: s = homsym(a,b) by Th15;
f, g form_morphism_between S1,S2 by Th24;
then the Sorts of B1 = (the Sorts of A2)*f by INSTALG1:def 3;
then
A2: (the Sorts of A2).(f.s) = (the Sorts of B1).s by FUNCT_2:15;
f.s = homsym(F.a,F.b) by A1,Th21;
then
A3: (the Sorts of A2).(f.s) = Hom(F.a,F.b) by Def13;
A4: (the Sorts of A1).s = Hom(a,b) by A1,Def13;
H.s = F|((the Sorts of A1).s) by Def1;
then H.s = hom(F,a,b) by A4;
hence thesis by A2,A4,A3;
end;
theorem Th29:
for C being Category, a,b,c being Object of C for x being set
holds x in Args(compsym(a,b,c), MSAlg C) iff ex g,f being Morphism of C st x =
<*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c
proof
let C be Category, a,b,c be Object of C, x be set;
set A = MSAlg C;
for a,b being Object of C holds (the Sorts of A).homsym(a,b) = Hom(a,b )
by Def13;
then
A1: Args(compsym(a,b,c), A) = product <*Hom(b,c),Hom(a,b)*> by Lm5;
hereby
assume x in Args(compsym(a,b,c), A);
then consider g,f being object such that
A2: g in Hom(b,c) & f in Hom(a,b) and
A3: x = <*g,f*> by A1,FINSEQ_3:124;
reconsider g,f as Morphism of C by A2;
take g,f;
thus x = <*g,f*> by A3;
thus dom f = a & cod f = b & dom g = b & cod g = c by A2,CAT_1:1;
end;
given g,f being Morphism of C such that
A4: x = <*g,f*> and
A5: dom f = a & cod f = b & dom g = b & cod g = c;
f in Hom(a,b) & g in Hom(b,c) by A5;
hence thesis by A1,A4,FINSEQ_3:124;
end;
theorem Th30:
for C1,C2 being Category, F being Functor of C1,C2 for a,b,c
being Object of C1 for f,g being Morphism of C1 st f in Hom(a,b) & g in Hom(b,c
) for x being Element of Args(compsym(a,b,c),MSAlg C1) st x = <*g,f*> for H
being ManySortedFunction of MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1,
Upsilon F, Psi F) st H = F-MSF(the carrier of CatSign the carrier of C1, the
Sorts of MSAlg C1) holds H#x = <*F.g,F.f*>
proof
let C1,C2 be Category, F be Functor of C1,C2;
set CS1 = CatSign the carrier of C1, CS2 = CatSign the carrier of C2;
set A1 = MSAlg C1, A2 = MSAlg C2;
set u = Upsilon F, p = Psi F;
set B = A2|(CS1, u, p);
let a,b,c be Object of C1;
set o = compsym(a,b,c);
let f,g be Morphism of C1 such that
A1: f in Hom(a,b) and
A2: g in Hom(b,c);
let x be Element of Args(o, A1) such that
A3: x = <*g,f*>;
F.g in Hom(F.b,F.c) by A2,CAT_1:81;
then
A4: dom (F.g) = F.b & cod (F.g) = F.c by CAT_1:1;
F.f in Hom(F.a,F.b) by A1,CAT_1:81;
then dom (F.f) = F.a & cod (F.f) = F.b by CAT_1:1;
then
A5: <*F.g,F.f*> in Args(compsym(F.a,F.b,F.c), A2) by A4,Th29;
A6: dom g = b & cod g = c by A2,CAT_1:1;
dom f = a & cod f = b by A1,CAT_1:1;
then
A7: x in Args(o, A1) by A3,A6,Th29;
let H be ManySortedFunction of A1, B such that
A8: H = F-MSF(the carrier of CS1, the Sorts of A1);
(the Sorts of A1).homsym(b,c) = Hom(b,c) by Def13;
then H.homsym(b,c) = F|Hom(b,c) by A8,Def1;
then
A9: (H.homsym(b,c)).g = F.g by A2,FUNCT_1:49;
A10: dom <*g,f*> = Seg 2 by FINSEQ_1:89;
then
A11: 1 in dom <*g,f*> by FINSEQ_1:2,TARSKI:def 2;
(the Sorts of A1).homsym(a,b) = Hom(a,b) by Def13;
then H.homsym(a,b) = F|Hom(a,b) by A8,Def1;
then
A12: (H.homsym(a,b)).f = F.f by A1,FUNCT_1:49;
A13: 2 in dom <*g,f*> by A10,FINSEQ_1:2,TARSKI:def 2;
u,p form_morphism_between CS1, CS2 by Th24;
then
A14: Args(o, B) = Args(p.o, A2) by INSTALG1:24
.= Args(compsym(F.a,F.b,F.c), A2) by Th23;
then consider g9,f9 being Morphism of C2 such that
A15: H#x = <*g9,f9*> and
dom f9 = F.a and
cod f9 = F.b and
dom g9 = F.b and
cod g9 = F. c by A5,Th29;
A17: the_arity_of o = <*homsym(b,c),homsym(a,b)*> by Def3;
then <*g,f*>.1 = g & (the_arity_of o)/.1 = homsym(b,c) by FINSEQ_4:17;
then
A18: <*g9,f9*>.1 = F.g by A3,A7,A5,A14,A15,A9,A11,MSUALG_3:24;
<*g,f*>.2 = f & (the_arity_of o)/.2 = homsym(a,b ) by A17,FINSEQ_4:17;
then <*g9,f9*>.2 = F.f by A3,A7,A5,A14,A15,A12,A13,MSUALG_3:24;
hence thesis by A15,A18;
end;
theorem Th31:
for C being Category, a,b,c being Object of C, f,g being
Morphism of C st f in Hom(a,b) & g in Hom(b,c) holds Den(compsym(a,b,c), MSAlg
C).<*g,f*> = g(*)f
proof
let C be Category, a,b,c be Object of C, f,g be Morphism of C;
assume that
A1: f in Hom(a,b) and
A2: g in Hom(b,c);
A3: dom g = b & cod g = c by A2,CAT_1:1;
dom f = a & cod f = b by A1,CAT_1:1;
hence thesis by A3,Def13;
end;
theorem
for C being Category, a,b,c,d being Object of C, f,g,h being Morphism
of C st f in Hom(a,b) & g in Hom(b,c) & h in Hom(c,d) holds Den(compsym(a,c,d),
MSAlg C).<*h, Den(compsym(a,b,c), MSAlg C).<*g,f*>*> = Den(compsym(a,b,d),
MSAlg C).<*Den(compsym(b,c,d), MSAlg C).<*h,g*>, f*>
proof
let C be Category, a,b,c,d be Object of C, f,g,h be Morphism of C;
assume that
A1: f in Hom(a,b) and
A2: g in Hom(b,c) and
A3: h in Hom(c,d);
A4: cod g = c by A2,CAT_1:1;
A5: Den(compsym(b,c,d), MSAlg C).<*h,g*> = h(*)g by A2,A3,Th31;
A6: cod f = b by A1,CAT_1:1;
A7: dom h = c by A3,CAT_1:1;
cod h = d by A3,CAT_1:1;
then
A8: cod (h(*)g) = d by A4,A7,CAT_1:17;
A9: dom g = b by A2,CAT_1:1;
then dom (h(*)g) = b by A4,A7,CAT_1:17;
then
A10: h(*)g in Hom(b,d) by A8;
dom f = a by A1,CAT_1:1;
then
A11: dom (g(*)f) = a by A6,A9,CAT_1:17;
cod (g(*)f) = c by A6,A9,A4,CAT_1:17;
then
A12: g(*)f in Hom(a,c) by A11;
Den(compsym(a,b,c), MSAlg C).<*g,f*> = g(*)f by A1,A2,Th31;
hence Den(compsym(a,c,d), MSAlg C).<*h, Den(compsym(a,b,c), MSAlg C).<*g,f*>
*> = h(*)(g(*)f) by A3,A12,Th31
.= (h(*)g)(*)f by A6,A9,A4,A7,CAT_1:18
.= Den(compsym(a,b,d),MSAlg C).<*Den(compsym(b,c,d),MSAlg C).<*h,g*>,f*>
by A1,A5,A10,Th31;
end;
theorem
for C being Category, a,b being Object of C, f being Morphism of C st
f in Hom(a,b) holds Den(compsym(a,b,b), MSAlg C).<*id b, f*> = f & Den(compsym(
a,a,b), MSAlg C).<*f, id a*> = f
proof
let C be Category, a,b be Object of C, f be Morphism of C;
assume
A1: f in Hom(a,b);
then dom f = a by CAT_1:1;
then
A2: f(*)id a = f by CAT_1:22;
cod f = b by A1,CAT_1:1;
then
A3: (id b)(*)f = f by CAT_1:21;
id b in Hom(b,b) & id a in Hom(a,a) by CAT_1:27;
hence thesis by A1,A3,A2,Th31;
end;
theorem
for C1,C2 being Category, F being Functor of C1,C2 ex H being
ManySortedFunction of MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1, Upsilon
F, Psi F) st H = F-MSF(the carrier of CatSign the carrier of C1, the Sorts of
MSAlg C1) & H is_homomorphism MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1,
Upsilon F, Psi F)
proof
let C1,C2 be Category, F be Functor of C1,C2;
set S1 = CatSign the carrier of C1, S2 = CatSign the carrier of C2;
set A1 = MSAlg C1, A2 = MSAlg C2;
set f = Upsilon F, G = Psi F;
set B1 = A2|(S1, f, G);
A1: f, G form_morphism_between S1,S2 by Th24;
reconsider H = F-MSF(the carrier of S1, the Sorts of A1) as
ManySortedFunction of A1,B1 by Th28;
take H;
thus H = F-MSF(the carrier of S1, the Sorts of A1);
let o be OperSymbol of S1;
assume
A2: Args(o,A1) <> {};
per cases by Th16;
suppose
o`1 = 1;
then consider a being Object of C1 such that
A3: o = idsym(a) by Th17;
let x be Element of Args(o,A1);
A4: Args(G.o,A2) = Args(o,B1) by A1,INSTALG1:24;
A5: G.o = idsym(F.a) by A3,Th22;
then Args(G.o,A2) = {{}} by Th25;
then
A6: H#x = {} by A4,TARSKI:def 1;
reconsider h = id a as Morphism of a,a;
dom id a = a & cod id a = a by CAT_1:58;
then
A7: id a in Hom(a,a);
Args(o,A1) = {{}} by A3,Th25;
then x = {} by TARSKI:def 1;
hence
(H.(the_result_sort_of o)).(Den(o,A1).x) = (H.(the_result_sort_of o))
.h by A3,Def13
.= (H.homsym(a,a)).h by A3,Def3
.= (F|((the Sorts of A1).homsym(a,a))).h by Def1
.= (F|Hom(a,a)).h by Def13
.= hom(F,a,a).h
.= F.h by A7,CAT_1:88
.= id (F.a) by CAT_1:71
.= Den(G.o,A2).(H#x) by A5,A6,Def13
.= Den(o,B1).(H#x) by Th24,INSTALG1:23;
end;
suppose
A8: o`1 = 2;
let x be Element of Args(o,A1);
consider a,b,c being Object of C1 such that
A9: o = compsym(a,b,c) by A8,Th18;
A10: G.o = compsym(F.a,F.b,F.c) by A9,Th23;
consider g,h being Morphism of C1 such that
A11: x = <*g,h*> and
A12: dom h = a and
A13: cod h = b and
A14: dom g = b and
A15: cod g = c by A2,A9,Th29;
A16: g in Hom(b,c) & h in Hom(a,b) by A12,A13,A14,A15;
dom (g(*)h) = a & cod (g(*)h) = c by A12,A13,A14,A15,CAT_1:17;
then
A17: g(*)h in Hom(a,c);
then reconsider gh = g(*)h as Morphism of a,c by CAT_1:def 5;
A18: dom (F.h) = F.a & cod (F.h) = F.b by A12,A13,CAT_1:72;
A19: dom (F.g) = F.b & cod (F.g) = F.c by A14,A15,CAT_1:72;
thus (H.(the_result_sort_of o)).(Den(o,A1).x) = (H.(the_result_sort_of o))
.gh by A9,A11,A12,A13,A14,A15,Def13
.= (H.homsym(a,c)).gh by A9,Def3
.= (F|((the Sorts of A1).homsym(a,c))).gh by Def1
.= (F|Hom(a,c)).gh by Def13
.= hom(F,a,c).gh
.= F.gh by A17,CAT_1:88
.= (F.g)(*)(F.h) by A13,A14,CAT_1:64
.= Den(G.o,A2).<*F.g,F.h*> by A10,A18,A19,Def13
.= Den(G.o,A2).(H#x) by A9,A11,A16,Th30
.= Den(o,B1).(H#x) by Th24,INSTALG1:23;
end;
end;