:: Functors for Alternative Categories
:: by Andrzej Trybulec
::
:: Received April 24, 1996
:: Copyright (c) 1996-2019 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 XBOOLE_0, FUNCT_1, SUBSET_1, MCART_1, ZFMISC_1, TARSKI, PBOOLE,
RELAT_1, FUNCT_2, FUNCOP_1, MEMBER_1, STRUCT_0, ALTCAT_1, RELAT_2,
MSUALG_6, CAT_1, ALTCAT_2, FUNCT_3, MSUALG_3, ENS_1, WELLORD1, FUNCTOR0;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, MCART_1,
FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FUNCT_3,
FUNCT_4, STRUCT_0, MSUALG_3, ALTCAT_1, ALTCAT_2;
constructors FUNCT_3, MSUALG_3, ALTCAT_2, RELSET_1, XTUPLE_0;
registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE, STRUCT_0,
ALTCAT_1, ALTCAT_2, PARTFUN1, RELSET_1, FUNCT_3, XTUPLE_0, FUNCT_4;
requirements SUBSET, BOOLE;
definitions TARSKI, MSUALG_3, FUNCT_1, FUNCT_2, XBOOLE_0, PBOOLE;
equalities XBOOLE_0, BINOP_1;
expansions MSUALG_3, FUNCT_1, FUNCT_2, XBOOLE_0;
theorems ALTCAT_2, FUNCT_4, FUNCOP_1, ZFMISC_1, ALTCAT_1, FUNCT_2, FUNCT_1,
PBOOLE, FUNCT_3, RELAT_1, MCART_1, DOMAIN_1, MSUALG_3, RELSET_1,
XBOOLE_0, XBOOLE_1, PARTFUN1, XTUPLE_0;
schemes ALTCAT_2;
begin :: Preliminaries
scheme ValOnPair {X()-> non empty set,f()-> Function,
x1,x2()-> Element of X(), F(object,object)-> set, P[object,object]}:
f().(x1(),x2()) = F(x1(),x2())
provided
A1: f() = { [[o,o9],F(o,o9)]
where o is Element of X(), o9 is Element of X(): P[o,o9] } and
A2: P[x1(),x2()]
proof
defpred R[set] means P[ $1`1,$1`2];
deffunc G(set) = F($1`1,$1`2);
A3: f() = { [o,G(o)] where o is Element of [:X(),X():]: R[o] }
proof
thus
f() c= {[o,F(o`1,o`2)] where o is Element of [:X(),X():]: P[o`1,o`2]}
proof
let y be object;
assume y in f();
then consider o1,o2 being Element of X() such that
A4: y = [[o1,o2],F(o1,o2)] and
A5: P[o1,o2] by A1;
reconsider p =[o1,o2] as Element of [:X(),X():] by ZFMISC_1:87;
A6: p`1 = o1;
p`2 = o2;
hence thesis by A4,A5,A6;
end;
let y be object;
assume y in {[o,F(o`1,o`2)] where o is Element of [:X(),X():]: P[o`1,o`2]};
then consider o being Element of [:X(),X():] such that
A7: y = [o,F(o`1,o`2)] and
A8: P[o`1,o`2];
reconsider o1 = o`1, o2 = o`2 as Element of X() by MCART_1:10;
o = [o1,o2] by MCART_1:21;
hence thesis by A1,A7,A8;
end;
reconsider x = [x1(),x2()] as Element of [:X(),X():] by ZFMISC_1:87;
A9: R[ x] by A2;
thus f().(x1(),x2()) = f().x .= G(x) from ALTCAT_2:sch 3(A3,A9)
.= F(x1(),x2());
end;
theorem Th1:
for A being set holds {} is Function of A,{} by FUNCT_2:130;
theorem Th2:
for I being set for M being ManySortedSet of I holds M*id I = M
proof
let I be set;
let M be ManySortedSet of I;
I = dom M by PARTFUN1:def 2;
hence thesis by RELAT_1:52;
end;
registration
let f be empty Function;
cluster ~f -> empty;
coherence;
let g be Function;
cluster [:f,g:] -> empty;
coherence
proof dom f = {};
then dom[:f,g:] = [:{},dom g:] by FUNCT_3:def 8;
hence thesis;
end;
cluster [:g,f:] -> empty;
coherence
proof dom f = {};
then dom[:g,f:] = [:dom g,{}:] by FUNCT_3:def 8;
hence thesis;
end;
end;
theorem Th3:
for A being set, f being Function holds f.:id A = (~f).:id A
proof
let A be set, f be Function;
thus f.:id A c= (~f).:id A
proof
let y be object;
assume y in f.:id A;
then consider x being object such that
A1: x in dom f and
A2: x in id A and
A3: y = f.x by FUNCT_1:def 6;
consider x1,x2 being object such that
A4: x = [x1,x2] by A2,RELAT_1:def 1;
A5: x1 = x2 by A2,A4,RELAT_1:def 10;
then
A6: x in dom~f by A1,A4,FUNCT_4:42;
then f.(x1,x2) = (~f).(x1,x2) by A4,A5,FUNCT_4:43;
hence thesis by A2,A3,A4,A6,FUNCT_1:def 6;
end;
let y be object;
assume y in (~f).:id A;
then consider x being object such that
A7: x in dom~f and
A8: x in id A and
A9: y = (~f).x by FUNCT_1:def 6;
consider x1,x2 being object such that
A10: x = [x1,x2] by A8,RELAT_1:def 1;
A11: x1 = x2 by A8,A10,RELAT_1:def 10;
then
A12: x in dom f by A7,A10,FUNCT_4:42;
then ~f.(x1,x2) = f.(x1,x2) by A10,A11,FUNCT_4:def 2;
hence thesis by A8,A9,A10,A12,FUNCT_1:def 6;
end;
theorem Th4:
for X,Y being set, f being Function of X,Y holds
f is onto iff [:f,f:] is onto
proof
let X,Y be set, f be Function of X,Y;
rng[:f,f:] = [:rng f, rng f:] by FUNCT_3:67;
then rng f = Y iff rng[:f,f:] = [:Y,Y:] by ZFMISC_1:92;
hence thesis;
end;
registration
let f be Function-yielding Function;
cluster ~f -> Function-yielding;
coherence;
end;
theorem Th5:
for A,B being set, a being object holds ~([:A,B:] --> a) = [:B,A:] --> a
proof
let A,B be set, a be object;
A1: now
let x be object;
hereby
assume x in dom([:B,A:] --> a);
then consider z,y being object such that
A2: z in B and
A3: y in A and
A4: x = [z,y] by ZFMISC_1:def 2;
take y,z;
thus x = [z,y] by A4;
[y,z] in [:A,B:] by A2,A3,ZFMISC_1:87;
hence [y,z] in dom([:A,B:] --> a);
end;
given y,z being object such that
A5: x = [z,y] and
A6: [y,z] in dom([:A,B:] --> a);
A7: y in A by A6,ZFMISC_1:87;
z in B by A6,ZFMISC_1:87;
then x in [:B,A:] by A5,A7,ZFMISC_1:87;
hence x in dom([:B,A:] --> a);
end;
now
let y,z be object;
assume
A8: [y,z] in dom([:A,B:] --> a);
then
A9: y in A by ZFMISC_1:87;
z in B by A8,ZFMISC_1:87;
hence ([:B,A:] --> a).(z,y) = a by A9,FUNCOP_1:7,ZFMISC_1:87
.= ([:A,B:] --> a).(y,z) by A8,FUNCOP_1:7;
end;
hence thesis by A1,FUNCT_4:def 2;
end;
theorem Th6:
for f,g being Function st f is one-to-one & g is one-to-one holds
[:f,g:]" = [:f",g":]
proof
let f,g be Function;
assume that
A1: f is one-to-one and
A2: g is one-to-one;
A3: [:f,g:] is one-to-one by A1,A2;
A4: dom(f") = rng f by A1,FUNCT_1:33;
A5: dom(g") = rng g by A2,FUNCT_1:33;
A6: dom([:f,g:]") = rng[:f,g:] by A3,FUNCT_1:33
.= [:dom(f"), dom(g"):] by A4,A5,FUNCT_3:67;
for x,y being object st x in dom(f") & y in dom(g")
holds [:f,g:]".(x,y) = [f".x,g".y]
proof
let x,y be object such that
A7: x in dom(f") and
A8: y in dom(g");
A9: dom[:f,g:] = [:dom f, dom g:] by FUNCT_3:def 8;
A10: f".x in rng(f") by A7,FUNCT_1:def 3;
A11: g".y in rng(g") by A8,FUNCT_1:def 3;
A12: f".x in dom f by A1,A10,FUNCT_1:33;
g".y in dom g by A2,A11,FUNCT_1:33;
then
A13: [f".x,g".y] in dom[:f,g:] by A9,A12,ZFMISC_1:87;
A14: f.(f".x) = (f*f").x by A7,FUNCT_1:13
.= ((f")"*f").x by A1,FUNCT_1:43
.= (id dom(f")).x by A1,FUNCT_1:39
.= x by A7,FUNCT_1:18;
g.(g".y) = (g*g").y by A8,FUNCT_1:13
.= ((g")"*g").y by A2,FUNCT_1:43
.= (id dom(g")).y by A2,FUNCT_1:39
.= y by A8,FUNCT_1:18;
then [:f,g:].(f".x,g".y) = [x,y] by A9,A13,A14,FUNCT_3:65;
hence thesis by A1,A2,A13,FUNCT_1:32;
end;
hence thesis by A6,FUNCT_3:def 8;
end;
theorem Th7:
for f being Function st [:f,f:] is one-to-one holds f is one-to-one
proof
let f be Function such that
A1: [:f,f:] is one-to-one;
let x1,x2 be object such that
A2: x1 in dom f and
A3: x2 in dom f and
A4: f.x1 = f.x2;
A5: dom[:f,f:] = [:dom f,dom f:] by FUNCT_3:def 8;
then
A6: [x1,x1] in dom[:f,f:] by A2,ZFMISC_1:87;
A7: [x2,x2] in dom[:f,f:] by A3,A5,ZFMISC_1:87;
[:f,f:].(x1,x1) = [f.x2,f.x2] by A4,A5,A6,FUNCT_3:65
.= [:f,f:].(x2,x2) by A5,A7,FUNCT_3:65;
then [x1,x1] = [x2,x2] by A1,A6,A7;
hence thesis by XTUPLE_0:1;
end;
theorem Th8:
for f being Function st f is one-to-one holds ~f is one-to-one
proof
let f be Function such that
A1: f is one-to-one;
let x1,x2 be object;
consider X,Y being set such that
A2: dom~f c= [:X,Y:] by FUNCT_4:44;
assume
A3: x1 in dom~f;
then consider x11,x12 being object such that x11 in X and x12 in Y and
A4: x1 = [x11,x12] by A2,ZFMISC_1:84;
assume
A5: x2 in dom~f;
then consider x21,x22 being object such that x21 in X and x22 in Y and
A6: x2 = [x21,x22] by A2,ZFMISC_1:84;
assume
A7: (~f).x1 = (~f).x2;
A8: [x12,x11] in dom f by A3,A4,FUNCT_4:42;
A9: [x22,x21] in dom f by A5,A6,FUNCT_4:42;
f.(x12,x11) = ~f.(x11,x12) by A3,A4,FUNCT_4:43
.= (~f).(x21,x22) by A4,A6,A7
.= f.(x22,x21) by A5,A6,FUNCT_4:43;
then
A10: [x12,x11] = [x22,x21] by A1,A8,A9;
then x12 = x22 by XTUPLE_0:1;
hence thesis by A4,A6,A10,XTUPLE_0:1;
end;
theorem Th9:
for f,g being Function st ~[:f,g:] is one-to-one holds [:g,f:] is one-to-one
proof
let f,g be Function such that
A1: ~[:f,g:] is one-to-one;
let x1,x2 be object;
A2: dom[:g,f:] = [:dom g, dom f:] by FUNCT_3:def 8;
A3: dom[:f,g:] = [:dom f, dom g:] by FUNCT_3:def 8;
assume x1 in dom[:g,f:];
then consider x11,x12 being object such that
A4: x11 in dom g and
A5: x12 in dom f and
A6: x1 = [x11,x12] by A2,ZFMISC_1:84;
assume x2 in dom[:g,f:];
then consider x21,x22 being object such that
A7: x21 in dom g and
A8: x22 in dom f and
A9: x2 = [x21,x22] by A2,ZFMISC_1:84;
x1 in dom[:g,f:] by A2,A4,A5,A6,ZFMISC_1:87;
then
A10: x1 in dom~[:f,g:] by A2,A3,FUNCT_4:46;
x2 in dom[:g,f:] by A2,A7,A8,A9,ZFMISC_1:87;
then
A11: x2 in dom~[:f,g:] by A2,A3,FUNCT_4:46;
assume
A12: [:g,f:].x1 = [:g,f:].x2;
A13: [:g,f:].(x11,x12) = [g.x11,f.x12] by A4,A5,FUNCT_3:def 8;
A14: [:g,f:].(x21,x22) = [g.x21,f.x22] by A7,A8,FUNCT_3:def 8;
then
A15: f.x22 = f.x12 by A6,A9,A12,A13,XTUPLE_0:1;
A16: g.x11 = g.x21 by A6,A9,A12,A13,A14,XTUPLE_0:1;
(~[:f,g:]).[x11,x12] = (~[:f,g:]).(x11,x12)
.= [:f,g:].(x12,x11) by A6,A10,FUNCT_4:43
.= [f.x22,g.x21] by A4,A5,A15,A16,FUNCT_3:def 8
.= [:f,g:].(x22,x21) by A7,A8,FUNCT_3:def 8
.= (~[:f,g:]).(x21,x22) by A9,A11,FUNCT_4:43
.= (~[:f,g:]).[x21,x22];
hence thesis by A1,A6,A9,A10,A11;
end;
theorem Th10:
for f,g being Function st f is one-to-one & g is one-to-one holds
~[:f,g:]" = ~([:g,f:]")
proof
let f,g be Function such that
A1: f is one-to-one and
A2: g is one-to-one;
A3: [:g,f:]" = [:g",f":] by A1,A2,Th6;
then
A4: dom([:g,f:]") = [:dom(g"), dom(f"):] by FUNCT_3:def 8;
A5: dom[:f,g:] = [:dom f, dom g:] by FUNCT_3:def 8;
A6: dom[:g,f:] = [:dom g, dom f:] by FUNCT_3:def 8;
A7: [:g,f:] is one-to-one by A1,A2;
A8: ~[:f,g:] is one-to-one by Th8,A1,A2;
A9: [:f,g:]" = [:f",g":] by A1,A2,Th6;
A10: dom~([:g,f:]") = [:dom(f"), dom(g"):] by A4,FUNCT_4:46
.= dom [:f", g":] by FUNCT_3:def 8
.= rng[:f,g:] by A1,A2,A9,FUNCT_1:32
.= rng~[:f,g:] by A5,FUNCT_4:47;
now
let y,x be object;
hereby
assume that
A11: y in rng~[:f,g:] and
A12: x = (~([:g,f:]")).y;
y in rng[:f,g:] by A5,A11,FUNCT_4:47;
then y in [:rng f,rng g:] by FUNCT_3:67;
then consider y1,y2 being object such that
A13: y1 in rng f and
A14: y2 in rng g and
A15: y = [y1,y2] by ZFMISC_1:84;
set x1 = f".y1, x2 = g".y2;
A16: y2 in dom(g") by A2,A14,FUNCT_1:32;
A17: y1 in dom(f") by A1,A13,FUNCT_1:32;
then [y2,y1] in dom([:g,f:]") by A4,A16,ZFMISC_1:87;
then
A18: (~([:g,f:]")).(y1,y2) = [:g",f":].(y2,y1) by A3,FUNCT_4:def 2
.= [x2,x1] by A16,A17,FUNCT_3:def 8;
A19: y1 in dom(f") by A1,A13,FUNCT_1:32;
A20: y2 in dom(g") by A2,A14,FUNCT_1:32;
A21: x1 in rng(f") by A19,FUNCT_1:def 3;
A22: x2 in rng(g") by A20,FUNCT_1:def 3;
A23: x1 in dom f by A1,A21,FUNCT_1:33;
A24: x2 in dom g by A2,A22,FUNCT_1:33;
then
A25: [x2,x1] in dom[:g,f:] by A6,A23,ZFMISC_1:87;
then
A26: [x2,x1] in dom~[:f,g:] by A5,A6,FUNCT_4:46;
thus
x in dom~[:f,g:] by A5,A6,A12,A15,A18,A25,FUNCT_4:46;
A27: f.x1 = y1 by A1,A13,FUNCT_1:32;
A28: g.x2 = y2 by A2,A14,FUNCT_1:32;
thus (~[:f,g:]).x = ~[:f,g:].(x2,x1) by A12,A15,A18
.= [:f,g:].(x1,x2) by A26,FUNCT_4:43
.= y by A15,A23,A24,A27,A28,FUNCT_3:def 8;
end;
assume that
A29: x in dom~[:f,g:] and
A30: (~[:f,g:]).x = y;
thus y in rng~[:f,g:] by A29,A30,FUNCT_1:def 3;
x in dom[:g,f:] by A5,A6,A29,FUNCT_4:46;
then consider x1,x2 being object such that
A31: x1 in dom g and
A32: x2 in dom f and
A33: x = [x1,x2] by A6,ZFMISC_1:84;
A34: (~[:f,g:]).(x1,x2) = [:f,g:].(x2,x1) by A29,A33,FUNCT_4:43
.= [f.x2,g.x1] by A31,A32,FUNCT_3:def 8;
A35: g.x1 in rng g by A31,FUNCT_1:def 3;
f.x2 in rng f by A32,FUNCT_1:def 3;
then [g.x1,f.x2] in [:rng g, rng f:] by A35,ZFMISC_1:87;
then [g.x1,f.x2] in rng[:g,f:] by FUNCT_3:67;
then
A36: [g.x1,f.x2] in dom([:g,f:]") by A7,FUNCT_1:33;
[x1,x2] in dom[:g,f:] by A6,A31,A32,ZFMISC_1:87;
hence x = ([:g,f:]").([:g,f:].(x1,x2)) by A1,A2,A33,FUNCT_1:34
.= ([:g,f:]").(g.x1,f.x2) by A31,A32,FUNCT_3:def 8
.= (~([:g,f:]")).(f.x2,g.x1) by A36,FUNCT_4:def 2
.= (~([:g,f:]")).y by A30,A33,A34;
end;
hence thesis by A8,A10,FUNCT_1:32;
end;
theorem Th11:
for A,B be set, f being Function of A,B st f is onto
holds id B c= [:f,f:].:id A
proof
let A,B be set, f be Function of A,B;
assume f is onto;
then
A1: rng f = B;
let xx be object;
assume
A2: xx in id B;
then consider x,x9 being object such that
A3: xx = [x,x9] by RELAT_1:def 1;
A4: x = x9 by A2,A3,RELAT_1:def 10;
A5: x in B by A2,A3,RELAT_1:def 10;
then consider y being object such that
A6: y in A and
A7: f.y = x by A1,FUNCT_2:11;
A8: dom f = A by A5,FUNCT_2:def 1;
A9: [y,y] in id A by A6,RELAT_1:def 10;
[:f,f:].(y,y) = xx by A3,A4,A6,A7,A8,FUNCT_3:def 8;
hence thesis by A2,A9,FUNCT_2:35;
end;
theorem Th12:
for F,G being Function-yielding Function, f be Function
holds (G**F)*f = (G*f)**(F*f)
proof
let F,G be Function-yielding Function, f be Function;
A1: dom((G**F)*f) = f"dom(G**F) by RELAT_1:147
.= f"(dom G /\ dom F) by PBOOLE:def 19
.= (f"dom F) /\ (f"dom G) by FUNCT_1:68
.= (f"dom F) /\ dom(G*f) by RELAT_1:147
.= dom(F*f) /\ dom(G*f) by RELAT_1:147;
now
let i be object;
assume
A2: i in dom((G**F)*f);
then
A3: i in dom f by FUNCT_1:11;
A4: f.i in dom(G**F) by A2,FUNCT_1:11;
thus ((G**F)*f).i = (G**F).(f.i) by A2,FUNCT_1:12
.= (G.(f.i))*(F.(f.i)) by A4,PBOOLE:def 19
.= ((G*f).i)*(F.(f.i)) by A3,FUNCT_1:13
.= ((G*f).i)*((F*f).i) by A3,FUNCT_1:13;
end;
hence thesis by A1,PBOOLE:def 19;
end;
theorem Th13:
for A,B,C being set, f being Function of [:A,B:],C st ~f is onto
holds f is onto
proof
let A,B,C be set, f be Function of [:A,B:],C;
A1: rng~f c= rng f by FUNCT_4:41;
assume ~f is onto;
then rng~f = C;
hence rng f = C by A1;
end;
theorem Th14:
for A be set, B being non empty set, f being Function of A,B
holds [:f,f:].:id A c= id B
proof
let A be set, B be non empty set, f be Function of A,B;
let x be object;
assume x in [:f,f:].:id A;
then consider yy being object such that
A1: yy in [:A,A:] and
A2: yy in id A and
A3: [:f,f:].yy = x by FUNCT_2:64;
consider y,y9 being object such that
A4: y in A and y9 in A and
A5: yy = [y,y9] by A1,ZFMISC_1:84;
A6: y = y9 by A2,A5,RELAT_1:def 10;
reconsider y as Element of A by A4;
A7: f.y in B by A4,FUNCT_2:5;
A8: y in dom f by A4,FUNCT_2:def 1;
x = [:f,f:].(y,y9) by A3,A5
.= [f.y,f.y] by A6,A8,FUNCT_3:def 8;
hence thesis by A7,RELAT_1:def 10;
end;
begin :: Functions bewteen Cartesian products
definition
let A,B be set;
mode bifunction of A,B is Function of [:A,A:],[:B,B:];
end;
definition
let A,B be set, f be bifunction of A,B;
attr f is Covariant means
:Def1:
ex g being Function of A,B st f = [:g,g:];
attr f is Contravariant means
:Def2:
ex g being Function of A,B st f = ~[:g,g:];
end;
theorem Th15:
for A be set, B be non empty set,
b being Element of B, f being bifunction of A,B st f = [:A,A:] --> [b,b]
holds f is Covariant Contravariant
proof
let A be set, B be non empty set,
b be Element of B, f be bifunction of A,B such that
A1: f = [:A,A:] --> [b,b];
reconsider g = A --> b as Function of A,B;
thus f is Covariant
proof
take g;
thus thesis by A1,ALTCAT_2:1;
end;
take g;
[:A,A:] --> [b,b] = ~([:A,A:] --> [b,b]) by Th5;
hence thesis by A1,ALTCAT_2:1;
end;
registration
let A,B be set;
cluster Covariant Contravariant for bifunction of A,B;
existence
proof
per cases;
suppose
A1: B = {};
then [:B,B:] = {} by ZFMISC_1:90;
then reconsider f = {} as bifunction of A,B by Th1;
take f;
reconsider g = {} as Function of A,B by A1,Th1;
reconsider h = g as empty Function;
thus f is Covariant
proof
take g;
thus f = [:h,h:] .= [:g,g:];
end;
take g;
thus f = ~[:h,h:] .= ~[:g,g:];
end;
suppose
A2: B <> {};
set b = the Element of B;
set f = [:A,A:] --> [b,b];
[b,b] in [:B,B:] by A2,ZFMISC_1:87;
then reconsider f as bifunction of A,B by FUNCOP_1:45;
take f;
thus thesis by A2,Th15;
end;
end;
end;
theorem
for A,B being non empty set
for f being Covariant Contravariant bifunction of A,B
ex b being Element of B st f = [:A,A:] --> [b,b]
proof
let A,B be non empty set;
let f be Covariant Contravariant bifunction of A,B;
consider g1 being Function of A,B such that
A1: f = [:g1,g1:] by Def1;
consider g2 being Function of A,B such that
A2: f = ~[:g2,g2:] by Def2;
set a = the Element of A;
take b = g1.a;
A3: dom f = [:A,A:] by FUNCT_2:def 1;
now
let z be object;
assume z in dom f;
then consider a1,a2 being Element of A such that
A4: z = [a1,a2] by DOMAIN_1:1;
A5: dom g2 = A by FUNCT_2:def 1;
A6: dom g1 = A by FUNCT_2:def 1;
A7: dom[:g2,g2:] = [:dom g2, dom g2:] by FUNCT_3:def 8;
then
A8: [a1,a] in dom[:g2,g2:] by A5,ZFMISC_1:87;
A9: dom g2 = A by FUNCT_2:def 1;
[b,g1.a1] = f.(a,a1) by A1,A6,FUNCT_3:def 8
.= [:g2,g2:].(a1,a) by A2,A8,FUNCT_4:def 2
.= [g2.a1,g2.a] by A9,FUNCT_3:def 8;
then
A10: g2.a1 = b by XTUPLE_0:1;
A11: [a2,a] in dom[:g2,g2:] by A5,A7,ZFMISC_1:87;
[b,g1.a2] = f.(a,a2) by A1,A6,FUNCT_3:def 8
.= [:g2,g2:].(a2,a) by A2,A11,FUNCT_4:def 2
.= [g2.a2,g2.a] by A9,FUNCT_3:def 8;
then
A12: g2.a2 = b by XTUPLE_0:1;
A13: [a2,a1] in dom[:g2,g2:] by A5,A7,ZFMISC_1:87;
thus f.z = [:g1,g1:].(a1,a2) by A1,A4
.= [:g2,g2:].(a2,a1) by A1,A2,A13,FUNCT_4:def 2
.= [b,b] by A9,A10,A12,FUNCT_3:def 8;
end;
hence thesis by A3,FUNCOP_1:11;
end;
begin :: Unary transformatiom
definition
let I1,I2 be set, f be Function of I1,I2;
let A be ManySortedSet of I1, B be ManySortedSet of I2;
mode MSUnTrans of f,A,B -> ManySortedSet of I1 means
:Def3:
ex I29 being non empty set, B9 being ManySortedSet of I29,
f9 being Function of I1,I29 st f = f9 & B = B9 &
it is ManySortedFunction of A,B9*f9 if I2 <> {} otherwise it = EmptyMS I1;
existence
proof
hereby
assume I2 <> {};
then reconsider I29 = I2 as non empty set;
reconsider f9 = f as Function of I1,I29;
reconsider B9 = B as ManySortedSet of I29;
set IT = the ManySortedFunction of A,B9*f9;
reconsider IT9 = IT as ManySortedSet of I1;
take IT9,I29;
reconsider f9 = f as Function of I1,I29;
reconsider B9 = B as ManySortedSet of I29;
take B9,f9;
thus f = f9 & B = B9;
thus IT9 is ManySortedFunction of A,B9*f9;
end;
thus thesis;
end;
consistency;
end;
definition
let I1 be set, I2 be non empty set, f be Function of I1,I2;
let A be ManySortedSet of I1, B be ManySortedSet of I2;
redefine mode MSUnTrans of f,A,B means
:Def4:
it is ManySortedFunction of A,B*f;
compatibility
proof
let M be ManySortedSet of I1;
hereby
assume M is MSUnTrans of f,A,B;
then ex I29 being non empty set, B9 being ManySortedSet of I29,
f9 being Function of I1,I29 st f = f9 & B = B9 &
M is ManySortedFunction of A,B9*f9 by Def3;
hence M is ManySortedFunction of A,B*f;
end;
thus thesis by Def3;
end;
end;
registration
let I1,I2 be set;
let f be Function of I1,I2;
let A be ManySortedSet of I1, B be ManySortedSet of I2;
cluster -> Function-yielding for MSUnTrans of f,A,B;
coherence
proof
let M be MSUnTrans of f,A,B;
per cases;
suppose I2 <> {};
then ex I29 being non empty set, B9 being ManySortedSet of I29,
f9 being Function of I1,I29 st f = f9 & B = B9 &
M is ManySortedFunction of A,B9*f9 by Def3;
hence thesis;
end;
suppose I2 = {};
then M = EmptyMS I1 by Def3;
hence thesis;
end;
end;
end;
theorem Th17:
for I1 being set, I2,I3 being non empty set,
f being Function of I1,I2, g being Function of I2,I3,
B being ManySortedSet of I2, C being ManySortedSet of I3,
G being MSUnTrans of g,B,C holds G*f is MSUnTrans of g*f,B*f,C
proof
let I1 be set, I2,I3 be non empty set,
f be Function of I1,I2, g be Function of I2,I3,
B be ManySortedSet of I2, C be ManySortedSet of I3, G be MSUnTrans of g,B,C;
A1: C*(g*f) = C*g*f by RELAT_1:36;
G is ManySortedFunction of B,C*g by Def4;
hence G*f is ManySortedFunction of B*f,C*(g*f) by A1,ALTCAT_2:5;
end;
definition
let I1 be set, I2 be non empty set, f be Function of I1,I2,
A be ManySortedSet of [:I1,I1:], B be ManySortedSet of [:I2,I2:],
F be MSUnTrans of [:f,f:],A,B;
redefine func ~F -> MSUnTrans of [:f,f:],~A,~B;
coherence
proof
reconsider G = F as ManySortedFunction of A,B*[:f,f:] by Def4;
~G is ManySortedFunction of ~A,~B*[:f,f:] by ALTCAT_2:3;
hence ~F is MSUnTrans of [:f,f:],~A,~B by Def4;
end;
end;
theorem Th18:
for I1,I2 being non empty set,
A being ManySortedSet of I1, B being ManySortedSet of I2,
o being Element of I2 st B.o <> {}
for m being Element of B.o, f being Function of I1,I2 st f = I1 --> o holds
the set of all [o9,A.o9 --> m] where o9 is Element of I1
is MSUnTrans of f,A,B
proof
let I1,I2 be non empty set,
A be ManySortedSet of I1, B be ManySortedSet of I2,
o be Element of I2 such that
A1: B.o <> {};
let m be Element of B.o, f be Function of I1,I2 such that
A2: f = I1 --> o;
defpred P[set] means not contradiction;
deffunc F(set) = A.$1 --> m;
reconsider Xm = { [o9,F(o9)] where o9 is Element of I1:
P[o9] } as Function from ALTCAT_2:sch 1;
A3: Xm = { [o9,F(o9)] where o9 is Element of I1: P[o9] };
dom Xm = { o9 where o9 is Element of I1: P[o9] } from ALTCAT_2:sch 2(
A3)
.= I1 by DOMAIN_1:18;
then reconsider Xm as ManySortedSet of I1 by PARTFUN1:def 2,RELAT_1:def 18;
deffunc F(set) = A.$1 --> m;
A4: Xm = { [o9,F(o9)] where o9 is Element of I1: P[o9] };
now
let i be object;
assume
A5: i in I1;
then reconsider o9 = i as Element of I1;
A6: P[o9];
A7: i in dom f by A2,A5;
f.i = o by A2,A5,FUNCOP_1:7;
then m in B.(f.i) by A1;
then
A8: m in (B*f).i by A7,FUNCT_1:13;
Xm.o9 = F(o9) from ALTCAT_2:sch 3(A4,A6);
hence Xm.i is Function of A.i, (B*f).i by A8,FUNCOP_1:45;
end;
then Xm is ManySortedFunction of A,B*f by PBOOLE:def 15;
hence thesis by Def4;
end;
theorem Th19:
for I1 being set, I2,I3 being non empty set,
f being Function of I1,I2, g being Function of I2,I3,
A being ManySortedSet of I1, B being ManySortedSet of I2,
C being ManySortedSet of I3, F being MSUnTrans of f,A,B,
G being MSUnTrans of g*f,B*f,C
st for ii being set st ii in I1 & (B*f).ii = {}
holds A.ii = {} or (C*(g*f)).ii = {}
holds G**(F qua Function-yielding Function) is MSUnTrans of g*f,A,C
proof
let I1 be set, I2,I3 be non empty set,
f be Function of I1,I2, g be Function of I2,I3,
A be ManySortedSet of I1, B be ManySortedSet of I2,
C be ManySortedSet of I3, F be MSUnTrans of f,A,B,
G be MSUnTrans of g*f,B*f,C such that
A1: for ii being set st ii in I1 & (B*f).ii = {}
holds A.ii = {} or (C*(g*f)).ii = {};
reconsider G as ManySortedFunction of B*f,C*(g*f) by Def4;
reconsider F as ManySortedFunction of A,B*f by Def4;
A2: dom G = I1 by PARTFUN1:def 2;
A3: dom F = I1 by PARTFUN1:def 2;
A4: dom(G**F) = dom G /\ dom F by PBOOLE:def 19
.= I1 by A2,A3;
reconsider GF = G**F as ManySortedSet of I1;
GF is ManySortedFunction of A,C*(g*f)
proof
let ii be object;
assume
A5: ii in I1;
then reconsider Fi = F.ii as Function of A.ii, (B*f).ii by PBOOLE:def 15;
reconsider Gi = G.ii as Function of (B*f).ii, (C*(g*f)).ii
by A5,PBOOLE:def 15;
(B*f).ii = {} implies A.ii = {} or (C*(g*f)).ii = {} by A1,A5;
then Gi*Fi is Function of A.ii, (C*(g*f)).ii by FUNCT_2:13;
hence thesis by A4,A5,PBOOLE:def 19;
end;
hence thesis by Def4;
end;
begin :: Functors
definition
let C1,C2 be 1-sorted;
struct BimapStr over C1,C2
(#ObjectMap -> bifunction of the carrier of C1, the carrier of C2 #);
end;
definition
let C1,C2 be non empty AltGraph;
let F be BimapStr over C1,C2;
let o be Object of C1;
func F.o -> Object of C2 equals
((the ObjectMap of F).(o,o))`1;
coherence by MCART_1:10;
end;
definition
let A,B be 1-sorted, F be BimapStr over A,B;
attr F is one-to-one means
the ObjectMap of F is one-to-one;
attr F is onto means
the ObjectMap of F is onto;
attr F is reflexive means
(the ObjectMap of F).:id the carrier of A c= id the carrier of B;
attr F is coreflexive means
id the carrier of B c= (the ObjectMap of F).:id the carrier of A;
end;
definition
let A,B be non empty AltGraph, F be BimapStr over A,B;
redefine attr F is reflexive means
:Def10:
for o being Object of A holds (the ObjectMap of F).(o,o) = [F.o,F.o];
compatibility
proof
hereby
assume F is reflexive;
then
A1: (
the ObjectMap of F).:id the carrier of A c= id the carrier of B;
let o be Object of A;
[o,o] in id the carrier of A by RELAT_1:def 10;
then
A2: (the ObjectMap of F).(o,o) in
(the ObjectMap of F).:id the carrier of A by FUNCT_2:35;
consider p,p9 being object such that
A3: (the ObjectMap of F).(o,o) = [p,p9] by RELAT_1:def 1;
thus (the ObjectMap of F).(o,o) = [F.o,F.o] by A1,A2,A3,RELAT_1:def 10;
end;
assume
A4: for o being Object of A holds (the ObjectMap of F).(o,o) = [F.o,F.o];
let x be object;
assume x in (the ObjectMap of F).:id the carrier of A;
then consider y being object such that
A5: y in [:the carrier of A,the carrier of A:] and
A6: y in id the carrier of A and
A7: x = (the ObjectMap of F).y by FUNCT_2:64;
consider o,o9 being Element of A such that
A8: y = [o,o9] by A5,DOMAIN_1:1;
reconsider o as Object of A;
o = o9 by A6,A8,RELAT_1:def 10;
then x = [F.o,F.o] by A4,A7,A8;
hence thesis by RELAT_1:def 10;
end;
end;
theorem Th20:
for A,B being reflexive non empty AltGraph,
F being BimapStr over A,B st F is coreflexive for o being Object of B
ex o9 being Object of A st F.o9 = o
proof
let A,B be reflexive non empty AltGraph, F be BimapStr over A,B;
assume F is coreflexive;
then
A1: id the carrier of B c= (the ObjectMap of F).:id the carrier of A;
let o be Object of B;
reconsider oo = [o,o] as
Element of [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
[o,o] in id the carrier of B by RELAT_1:def 10;
then consider pp being Element of [:the carrier of A,the carrier of A:]
such that
A2: pp in id the carrier of A and
A3: (the ObjectMap of F).pp = oo by A1,FUNCT_2:65;
consider p,p9 being object such that
A4: pp = [p,p9] by RELAT_1:def 1;
A5: p = p9 by A2,A4,RELAT_1:def 10;
reconsider p as Object of A by A2,A4,RELAT_1:def 10;
take p;
thus thesis by A3,A4,A5;
end;
definition
let C1, C2 be non empty AltGraph;
let F be BimapStr over C1,C2;
attr F is feasible means
:Def11:
for o1,o2 being Object of C1 st <^o1,o2^> <> {} holds
(the Arrows of C2).((the ObjectMap of F).(o1,o2)) <> {};
end;
definition
let C1,C2 be AltGraph;
struct(BimapStr over C1,C2) FunctorStr over C1,C2
(#ObjectMap -> bifunction of the carrier of C1,the carrier of C2,
MorphMap ->
MSUnTrans of the ObjectMap, the Arrows of C1, the Arrows of C2 #);
end;
definition
let C1,C2 be 1-sorted;
let IT be BimapStr over C1,C2;
attr IT is Covariant means
:Def12:
the ObjectMap of IT is Covariant;
attr IT is Contravariant means
:Def13:
the ObjectMap of IT is Contravariant;
end;
registration
let C1,C2 be AltGraph;
cluster Covariant for FunctorStr over C1,C2;
existence
proof
set f = the Covariant bifunction of the carrier of C1, the carrier of C2;
set M = the MSUnTrans of f, the Arrows of C1, the Arrows of C2;
take F = FunctorStr(#f,M#);
thus the ObjectMap of F is Covariant;
end;
cluster Contravariant for FunctorStr over C1,C2;
existence
proof
set f = the Contravariant bifunction of the carrier of C1, the carrier of C2;
set M = the MSUnTrans of f, the Arrows of C1, the Arrows of C2;
take F = FunctorStr(#f,M#);
thus the ObjectMap of F is Contravariant;
end;
end;
definition
let C1,C2 be AltGraph;
let F be FunctorStr over C1,C2;
let o1,o2 be Object of C1;
func Morph-Map(F,o1,o2) -> set equals
(the MorphMap of F).(o1,o2);
correctness;
end;
registration
let C1,C2 be AltGraph;
let F be FunctorStr over C1,C2;
let o1,o2 be Object of C1;
cluster Morph-Map(F,o1,o2) -> Relation-like Function-like;
coherence;
end;
definition
let C1,C2 be non empty AltGraph;
let F be Covariant FunctorStr over C1,C2;
let o1,o2 be Object of C1;
redefine func Morph-Map(F,o1,o2) -> Function of <^o1,o2^>, <^F.o1,F.o2^>;
coherence
proof
consider I29 being non empty set, B9 being ManySortedSet of I29,
f9 being Function of [:the carrier of C1,the carrier of C1:],I29 such that
A1: the ObjectMap of F = f9 and
A2: the Arrows of C2 = B9 and
A3: the MorphMap of F is ManySortedFunction of the Arrows of C1,B9*f9 by Def3;
A4: (the Arrows of C1).[o1,o2] = (the Arrows of C1).(o1,o2)
.= <^o1,o2^> by ALTCAT_1:def 1;
A5: [o1,o2] in [:the carrier of C1, the carrier of C1:] by ZFMISC_1:87;
the ObjectMap of F is Covariant by Def12;
then consider g being Function of the carrier of C1, the carrier of C2
such that
A6: the ObjectMap of F = [:g,g:];
A7: F.o1 = [g.o1,g.o1]`1 by A6,FUNCT_3:75
.= g.o1;
A8: F.o2 = [g.o2,g.o2]`1 by A6,FUNCT_3:75
.= g.o2;
dom f9 = [:the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;
then (B9*f9).[o1,o2] = B9.(f9.(o1,o2)) by A5,FUNCT_1:13
.= (the Arrows of C2).(F.o1,F.o2) by A1,A2,A6,A7,A8,FUNCT_3:75
.= <^F.o1,F.o2^> by ALTCAT_1:def 1;
hence thesis by A3,A4,A5,PBOOLE:def 15;
end;
end;
definition
let C1,C2 be non empty AltGraph;
let F be Covariant FunctorStr over C1,C2;
let o1,o2 be Object of C1 such that
A1: <^o1,o2^> <> {} and
A2: <^F.o1,F.o2^> <> {};
let m be Morphism of o1,o2;
func F.m -> Morphism of F.o1, F.o2 equals
:Def15:
Morph-Map(F,o1,o2).m;
coherence
proof
reconsider A = <^o1,o2^>, B = <^F.o1,F.o2^> as non empty set by A1,A2;
reconsider M = Morph-Map(F,o1,o2) as Function of A,B;
reconsider m as Element of A;
M.m is Element of B;
hence thesis;
end;
end;
definition
let C1,C2 be non empty AltGraph;
let F be Contravariant FunctorStr over C1,C2;
let o1,o2 be Object of C1;
redefine func Morph-Map(F,o1,o2) -> Function of <^o1,o2^>, <^F.o2,F.o1^>;
coherence
proof
consider I29 being non empty set, B9 being ManySortedSet of I29,
f9 being Function of [:the carrier of C1,the carrier of C1:],I29 such that
A1: the ObjectMap of F = f9 and
A2: the Arrows of C2 = B9 and
A3: the MorphMap of F is ManySortedFunction of the Arrows of C1,B9*f9 by Def3;
A4: (the Arrows of C1).[o1,o2] = (the Arrows of C1).(o1,o2)
.= <^o1,o2^> by ALTCAT_1:def 1;
A5: [o1,o2] in [:the carrier of C1, the carrier of C1:] by ZFMISC_1:87;
the ObjectMap of F is Contravariant by Def13;
then consider g being Function of the carrier of C1, the carrier of C2
such that
A6: the ObjectMap of F = ~[:g,g:];
A7: dom f9 = [:the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;
then [o1,o1] in dom~[:g,g:] by A1,A6,ZFMISC_1:87;
then [o1,o1] in dom[:g,g:] by FUNCT_4:42;
then
A8: F.o1 = ([:g,g:].(o1,o1))`1 by A6,FUNCT_4:def 2
.= [g.o1,g.o1]`1 by FUNCT_3:75
.= g.o1;
[o2,o2] in dom~[:g,g:] by A1,A6,A7,ZFMISC_1:87;
then [o2,o2] in dom[:g,g:] by FUNCT_4:42;
then
A9: F.o2 = ([:g,g:].(o2,o2))`1 by A6,FUNCT_4:def 2
.= [g.o2,g.o2]`1 by FUNCT_3:75
.= g.o2;
[o1,o2] in dom~[:g,g:] by A1,A6,A7,ZFMISC_1:87;
then
A10: [o2,o1] in dom[:g,g:] by FUNCT_4:42;
(B9*f9).[o1,o2] = B9.(f9.(o1,o2)) by A5,A7,FUNCT_1:13
.= B9.([:g,g:].(o2,o1)) by A1,A6,A10,FUNCT_4:def 2
.= (the Arrows of C2).(F.o2,F.o1) by A2,A8,A9,FUNCT_3:75
.= <^F.o2,F.o1^> by ALTCAT_1:def 1;
hence thesis by A3,A4,A5,PBOOLE:def 15;
end;
end;
definition
let C1,C2 be non empty AltGraph;
let F be Contravariant FunctorStr over C1,C2;
let o1,o2 be Object of C1 such that
A1: <^o1,o2^> <> {} and
A2: <^F.o2,F.o1^> <> {};
let m be Morphism of o1,o2;
func F.m -> Morphism of F.o2, F.o1 equals
:Def16:
Morph-Map(F,o1,o2).m;
coherence
proof
reconsider A = <^o1,o2^>, B = <^F.o2,F.o1^> as non empty set by A1,A2;
reconsider M = Morph-Map(F,o1,o2) as Function of A,B;
reconsider m as Element of A;
M.m is Element of B;
hence thesis;
end;
end;
definition
let C1,C2 be non empty AltGraph;
let o be Object of C2 such that
A1: <^o,o^> <> {};
let m be Morphism of o,o;
func C1 --> m -> strict FunctorStr over C1,C2 means
:Def17:
the ObjectMap of it = [:the carrier of C1,the carrier of C1:] --> [o,o] &
the MorphMap of it =
the set of all
[[o1,o2],<^o1,o2^> --> m] where o1 is Object of C1, o2 is Object of C1;
existence
proof
set I1 = [:the carrier of C1,the carrier of C1:],
I2 = [:the carrier of C2,the carrier of C2:],
A = the Arrows of C1, B = the Arrows of C2;
reconsider oo = [o,o] as Element of I2 by ZFMISC_1:87;
B.oo = B.(o,o) .= <^o,o^> by ALTCAT_1:def 1;
then reconsider m as Element of B.oo;
reconsider f = I1 --> oo as Function of I1, I2;
reconsider f as bifunction of the carrier of C1,the carrier of C2;
set M = the set of all [[o1,o2],<^o1,o2^> --> m]
where o1 is Object of C1, o2 is Object of C1;
A2: M = the set of all [o9,A.o9 --> m] where o9 is Element of I1
proof
thus M c=
the set of all [o9,A.o9 --> m] where o9 is Element of I1
proof
let x be object;
assume x in M;
then consider o3,o4 being Object of C1 such that
A3: x = [[o3,o4],<^o3,o4^> --> m];
reconsider oo = [o3,o4] as Element of I1 by ZFMISC_1:87;
x = [oo,A.(o3,o4) --> m] by A3,ALTCAT_1:def 1
.= [oo,A.oo --> m];
hence thesis;
end;
let x be object;
assume x in the set of all [o9,A.o9 --> m] where o9 is Element of I1;
then consider o9 being Element of I1 such that
A4: x = [o9,A.o9 --> m];
reconsider o1 = o9`1, o2 = o9`2 as Element of C1 by MCART_1:10;
reconsider o1, o2 as Object of C1;
o9 = [o1,o2] by MCART_1:21;
then x = [[o1,o2],A.(o1,o2) --> m] by A4
.= [[o1,o2],<^o1,o2^> --> m] by ALTCAT_1:def 1;
hence thesis;
end;
B.(o,o) <> {} by A1,ALTCAT_1:def 1;
then reconsider M as MSUnTrans of f, A, B by A2,Th18;
take FunctorStr(#f,M#);
thus thesis;
end;
uniqueness;
end;
theorem Th21:
for C1,C2 being non empty AltGraph, o2 being Object of C2 st <^o2,o2^> <> {}
for m be Morphism of o2,o2, o1 being Object of C1 holds (C1 --> m).o1 = o2
proof
let C1,C2 be non empty AltGraph, o2 be Object of C2 such that
A1: <^o2,o2^> <> {};
let m be Morphism of o2,o2, o1 be Object of C1;
A2: [o1,o1] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:87;
thus (C1 --> m).o1 =
(([:the carrier of C1,the carrier of C1:] --> [o2,o2]).(o1,o1))`1
by A1,Def17
.= [o2,o2]`1 by A2,FUNCOP_1:7
.= o2;
end;
registration
let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph;
let o be Object of C2, m be Morphism of o,o;
cluster C1 --> m -> Covariant Contravariant feasible;
coherence
proof
<^o,o^> <> {} by ALTCAT_2:def 7;
then
A1: the ObjectMap of C1 --> m
= [:the carrier of C1,the carrier of C1:] --> [o,o] by Def17;
hence the ObjectMap of C1 --> m is Covariant Contravariant by Th15;
let o1,o2 be Object of C1 such that <^o1,o2^> <> {};
[o1,o2] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:87;
then (the Arrows of C2).((the ObjectMap of C1 --> m).(o1,o2))
= (the Arrows of C2).(o,o) by A1,FUNCOP_1:7;
hence thesis by ALTCAT_2:def 6;
end;
end;
registration
let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph;
cluster feasible Covariant Contravariant for FunctorStr over C1,C2;
existence
proof set o = the Object of C2;
set m = the Morphism of o,o;
take C1 --> m;
thus thesis;
end;
end;
theorem Th22:
for C1, C2 being non empty AltGraph,
F being Covariant FunctorStr over C1,C2, o1,o2 being Object of C1
holds (the ObjectMap of F).(o1,o2) = [F.o1,F.o2]
proof
let C1, C2 be non empty AltGraph, F be Covariant FunctorStr over C1,C2,
o1,o2 be Object of C1;
the ObjectMap of F is Covariant by Def12;
then consider f being Function of the carrier of C1, the carrier of C2 such
that
A1: the ObjectMap of F = [:f,f:];
A2: F.o1 = ([f.o1,f.o1])`1 by A1,FUNCT_3:75
.= f.o1;
F.o2 = ([f.o2,f.o2])`1 by A1,FUNCT_3:75
.= f.o2;
hence thesis by A1,A2,FUNCT_3:75;
end;
definition
let C1, C2 be non empty AltGraph;
let F be Covariant FunctorStr over C1,C2;
redefine attr F is feasible means
:Def18:
for o1,o2 being Object of C1 st <^o1,o2^> <> {} holds <^F.o1,F.o2^> <> {};
compatibility
proof
hereby
assume
A1: F is feasible;
let o1,o2 be Object of C1;
assume
A2: <^o1,o2^> <> {};
<^F.o1,F.o2^> = (the Arrows of C2).(F.o1,F.o2) by ALTCAT_1:def 1
.= (the Arrows of C2).((the ObjectMap of F).(o1,o2)) by Th22;
hence <^F.o1,F.o2^> <> {} by A1,A2;
end;
assume
A3: for
o1,o2 being Object of C1 st <^o1,o2^> <> {} holds <^F.o1,F.o2^> <> {};
let o1,o2 be Object of C1;
assume
A4: <^o1,o2^> <> {};
<^F.o1,F.o2^> = (the Arrows of C2).(F.o1,F.o2) by ALTCAT_1:def 1
.= (the Arrows of C2).((the ObjectMap of F).(o1,o2)) by Th22;
hence thesis by A3,A4;
end;
end;
theorem Th23:
for C1, C2 being non empty AltGraph,
F being Contravariant FunctorStr over C1,C2, o1,o2 being Object of C1
holds (the ObjectMap of F).(o1,o2) = [F.o2,F.o1]
proof
let C1, C2 be non empty AltGraph, F be Contravariant FunctorStr over C1,C2,
o1,o2 be Object of C1;
the ObjectMap of F is Contravariant by Def13;
then consider f being Function of the carrier of C1, the carrier of C2 such
that
A1: the ObjectMap of F = ~[:f,f:];
A2: dom[:f,f:] = [:the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;
then [o1,o1] in dom[:f,f:] by ZFMISC_1:87;
then
A3: F.o1 = ([:f,f:].(o1,o1))`1 by A1,FUNCT_4:def 2
.= ([f.o1,f.o1])`1 by FUNCT_3:75
.= f.o1;
[o2,o2] in dom[:f,f:] by A2,ZFMISC_1:87;
then
A4: F.o2 = ([:f,f:].(o2,o2))`1 by A1,FUNCT_4:def 2
.= ([f.o2,f.o2])`1 by FUNCT_3:75
.= f.o2;
[o2,o1] in dom[:f,f:] by A2,ZFMISC_1:87;
hence (the ObjectMap of F).(o1,o2) = [:f,f:].(o2,o1) by A1,FUNCT_4:def 2
.= [F.o2,F.o1] by A3,A4,FUNCT_3:75;
end;
definition
let C1, C2 be non empty AltGraph;
let F be Contravariant FunctorStr over C1,C2;
redefine attr F is feasible means
:Def19:
for o1,o2 being Object of C1 st <^o1,o2^> <> {} holds <^F.o2,F.o1^> <> {};
compatibility
proof
hereby
assume
A1: F is feasible;
let o1,o2 be Object of C1;
assume
A2: <^o1,o2^> <> {};
<^F.o2,F.o1^> = (the Arrows of C2).(F.o2,F.o1) by ALTCAT_1:def 1
.= (the Arrows of C2).((the ObjectMap of F).(o1,o2)) by Th23;
hence <^F.o2,F.o1^> <> {} by A1,A2;
end;
assume
A3: for
o1,o2 being Object of C1 st <^o1,o2^> <> {} holds <^F.o2,F.o1^> <> {};
let o1,o2 be Object of C1;
assume
A4: <^o1,o2^> <> {};
<^F.o2,F.o1^> = (the Arrows of C2).(F.o2,F.o1) by ALTCAT_1:def 1
.= (the Arrows of C2).((the ObjectMap of F).(o1,o2)) by Th23;
hence thesis by A3,A4;
end;
end;
registration
let C1,C2 be AltGraph;
let F be FunctorStr over C1,C2;
cluster the MorphMap of F -> Function-yielding;
coherence;
end;
registration
cluster non empty reflexive for AltCatStr;
existence
proof set C = the category;
take C;
thus thesis;
end;
end;
:: Wlasnosci funktorow, Semadeni-Wiweger str. 32
definition
let C1,C2 be with_units non empty AltCatStr;
let F be FunctorStr over C1,C2;
attr F is id-preserving means
:Def20:
for o being Object of C1 holds Morph-Map(F,o,o).idm o = idm F.o;
end;
theorem Th24:
for C1,C2 being non empty AltGraph, o2 being Object of C2 st <^o2,o2^> <> {}
for m be Morphism of o2,o2, o,o9 being Object of C1, f being Morphism of o,o9
st <^o,o9^> <> {} holds Morph-Map(C1 --> m,o,o9).f = m
proof
let C1,C2 be non empty AltGraph, o2 be Object of C2 such that
A1: <^o2,o2^> <> {};
let m be Morphism of o2,o2, o,o9 be Object of C1, f be Morphism of o,o9
such that
A2: <^o,o9^> <> {};
set X =
the set of all
[[o1,o19],<^o1,o19^> --> m] where o1 is Object of C1, o19 is Object of C1;
set Y = the set of all [[o1,o19],(the Arrows of C1).(o1,o19) --> m]
where o1 is Element of C1, o19 is Element of C1;
A3: X c= Y
proof
let e be object;
assume e in X;
then consider o1,o19 being Object of C1 such that
A4: e = [[o1,o19],<^o1,o19^> --> m];
e = [[o1,o19],(the Arrows of C1).(o1,o19) --> m] by A4,ALTCAT_1:def 1;
hence thesis;
end;
A5: Y c= X
proof
let e be object;
assume e in Y;
then consider o1,o19 being Element of C1 such that
A6: e = [[o1,o19],(the Arrows of C1).(o1,o19) --> m];
reconsider o1,o19 as Object of C1;
e = [[o1,o19],<^o1,o19^> --> m] by A6,ALTCAT_1:def 1;
hence thesis;
end;
defpred P[set,set] means not contradiction;
deffunc F(Element of C1,Element of C1) = (the Arrows of C1).($1,$2) --> m;
the MorphMap of C1 --> m = X by A1,Def17;
then
A7: the MorphMap of C1 --> m = { [[o1,o19],F(o1,o19)]
where o1 is Element of C1, o19 is Element of C1: P[o1,o19] }
by A3,A5;
A8: P[o,o9];
Morph-Map(C1 --> m,o,o9) = (the MorphMap of C1 --> m).(o,o9)
.= F(o,o9) from ValOnPair(A7,A8);
hence Morph-Map(C1 --> m,o,o9).f = (<^o,o9^> --> m).f by ALTCAT_1:def 1
.= m by A2,FUNCOP_1:7;
end;
registration
cluster with_units -> reflexive for non empty AltCatStr;
coherence;
end;
registration
let C1,C2 be with_units non empty AltCatStr;
let o2 be Object of C2;
cluster C1 --> idm o2 -> id-preserving;
coherence
proof
let o1 be Object of C1;
A1: <^o2,o2^> <> {} by ALTCAT_2:def 7;
<^o1,o1^> <> {} by ALTCAT_2:def 7;
hence Morph-Map(C1 --> idm o2,o1,o1).idm o1 = idm o2 by A1,Th24
.= idm(C1 --> idm o2).o1 by A1,Th21;
end;
end;
registration
let C1 be non empty AltGraph;
let C2 be non empty reflexive AltGraph;
let o2 be Object of C2;
let m be Morphism of o2,o2;
cluster C1 --> m -> reflexive;
coherence
proof
let o be Object of C1;
A1: [o,o] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:87;
<^o2,o2^> <> {} by ALTCAT_2:def 7;
then
A2: (the ObjectMap of C1 --> m).(o,o)
= ([:the carrier of C1,the carrier of C1:] --> [o2,o2]).[o,o] by Def17
.= [o2,o2] by A1,FUNCOP_1:7;
thus thesis by A2;
end;
end;
registration
let C1 be non empty AltGraph;
let C2 be non empty reflexive AltGraph;
cluster feasible reflexive for FunctorStr over C1,C2;
existence
proof set o2 = the Object of C2,m = the Morphism of o2,o2;
take C1 --> m;
thus thesis;
end;
end;
registration
let C1,C2 be with_units non empty AltCatStr;
cluster id-preserving feasible reflexive strict for FunctorStr over C1,C2;
existence
proof set o2 = the Object of C2;
take C1 --> idm o2;
thus thesis;
end;
end;
definition
let C1,C2 be non empty AltCatStr;
let F be FunctorStr over C1,C2;
attr F is comp-preserving means
for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for f being Morphism of o1,o2, g being Morphism of o2,o3
ex f9 being Morphism of F.o1,F.o2, g9 being Morphism of F.o2,F.o3 st
f9 = Morph-Map(F,o1,o2).f & g9 = Morph-Map(F,o2,o3).g &
Morph-Map(F,o1,o3).(g*f) = g9*f9;
end;
definition
let C1,C2 be non empty AltCatStr;
let F be FunctorStr over C1,C2;
attr F is comp-reversing means
for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for f being Morphism of o1,o2, g being Morphism of o2,o3
ex f9 being Morphism of F.o2,F.o1, g9 being Morphism of F.o3,F.o2 st
f9 = Morph-Map(F,o1,o2).f & g9 = Morph-Map(F,o2,o3).g &
Morph-Map(F,o1,o3).(g*f) = f9*g9;
end;
definition
let C1 be non empty transitive AltCatStr;
let C2 be non empty reflexive AltCatStr;
let F be Covariant feasible FunctorStr over C1,C2;
redefine attr F is comp-preserving means
for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for f being Morphism of o1,o2, g being Morphism of o2,o3
holds F.(g*f) = (F.g)*(F.f);
compatibility
proof
hereby
assume
A1: F is comp-preserving;
let o1,o2,o3 be Object of C1 such that
A2: <^o1,o2^> <> {} and
A3: <^o2,o3^> <> {};
let f be Morphism of o1,o2, g be Morphism of o2,o3;
consider f9 being Morphism of F.o1,F.o2, g9 being Morphism of F.o2,F.o3
such that
A4: f9 = Morph-Map(F,o1,o2).f and
A5: g9 = Morph-Map(F,o2,o3).g and
A6: Morph-Map(F,o1,o3).(g*f) = g9*f9 by A1,A2,A3;
A7: <^F.o1,F.o2^> <> {} by A2,Def18;
A8: <^F.o2,F.o3^> <> {} by A3,Def18;
A9: f9 = F.f by A2,A4,A7,Def15;
A10: g9 = F.g by A3,A5,A8,Def15;
A11: <^o1,o3^> <> {} by A2,A3,ALTCAT_1:def 2;
then <^F.o1,F.o3^> <> {} by Def18;
hence F.(g*f) = (F.g)*(F.f) by A6,A9,A10,A11,Def15;
end;
assume
A12: for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for f being Morphism of o1,o2, g being Morphism of o2,o3
holds F.(g*f) = (F.g)*(F.f);
let o1,o2,o3 be Object of C1 such that
A13: <^o1,o2^> <> {} and
A14: <^o2,o3^> <> {};
let f be Morphism of o1,o2, g be Morphism of o2,o3;
A15: <^F.o1,F.o2^> <> {} by A13,Def18;
then reconsider f9 = Morph-Map(F,o1,o2).f as Morphism of F.o1,F.o2
by A13,FUNCT_2:5;
A16: <^F.o2,F.o3^> <> {} by A14,Def18;
then reconsider g9 = Morph-Map(F,o2,o3).g as Morphism of F.o2,F.o3
by A14,FUNCT_2:5;
take f9, g9;
thus f9 = Morph-Map(F,o1,o2).f & g9 = Morph-Map(F,o2,o3).g;
A17: f9 = F.f by A13,A15,Def15;
A18: g9 = F.g by A14,A16,Def15;
A19: <^o1,o3^> <> {} by A13,A14,ALTCAT_1:def 2;
then <^F.o1,F.o3^> <> {} by Def18;
hence Morph-Map(F,o1,o3).(g*f) = F.(g*f) by A19,Def15
.= g9*f9 by A12,A13,A14,A17,A18;
end;
end;
definition
let C1 be non empty transitive AltCatStr;
let C2 be non empty reflexive AltCatStr;
let F be Contravariant feasible FunctorStr over C1,C2;
redefine attr F is comp-reversing means
for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for f being Morphism of o1,o2, g being Morphism of o2,o3
holds F.(g*f) = (F.f)*(F.g);
compatibility
proof
hereby
assume
A1: F is comp-reversing;
let o1,o2,o3 be Object of C1 such that
A2: <^o1,o2^> <> {} and
A3: <^o2,o3^> <> {};
let f be Morphism of o1,o2, g be Morphism of o2,o3;
consider f9 being Morphism of F.o2,F.o1, g9 being Morphism of F.o3,F.o2
such that
A4: f9 = Morph-Map(F,o1,o2).f and
A5: g9 = Morph-Map(F,o2,o3).g and
A6: Morph-Map(F,o1,o3).(g*f) = f9*g9 by A1,A2,A3;
A7: <^F.o2,F.o1^> <> {} by A2,Def19;
A8: <^F.o3,F.o2^> <> {} by A3,Def19;
A9: f9 = F.f by A2,A4,A7,Def16;
A10: g9 = F.g by A3,A5,A8,Def16;
A11: <^o1,o3^> <> {} by A2,A3,ALTCAT_1:def 2;
then <^F.o3,F.o1^> <> {} by Def19;
hence F.(g*f) = (F.f)*(F.g) by A6,A9,A10,A11,Def16;
end;
assume
A12: for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for f being Morphism of o1,o2, g being Morphism of o2,o3
holds F.(g*f) = (F.f)*(F.g);
let o1,o2,o3 be Object of C1 such that
A13: <^o1,o2^> <> {} and
A14: <^o2,o3^> <> {};
let f be Morphism of o1,o2, g be Morphism of o2,o3;
A15: <^F.o2,F.o1^> <> {} by A13,Def19;
then reconsider f9 = Morph-Map(F,o1,o2).f as Morphism of F.o2,F.o1
by A13,FUNCT_2:5;
A16: <^F.o3,F.o2^> <> {} by A14,Def19;
then reconsider g9 = Morph-Map(F,o2,o3).g as Morphism of F.o3,F.o2
by A14,FUNCT_2:5;
take f9, g9;
thus f9 = Morph-Map(F,o1,o2).f & g9 = Morph-Map(F,o2,o3).g;
A17: f9 = F.f by A13,A15,Def16;
A18: g9 = F.g by A14,A16,Def16;
A19: <^o1,o3^> <> {} by A13,A14,ALTCAT_1:def 2;
then <^F.o3,F.o1^> <> {} by Def19;
hence Morph-Map(F,o1,o3).(g*f) = F.(g*f) by A19,Def16
.= f9*g9 by A12,A13,A14,A17,A18;
end;
end;
theorem Th25:
for C1 being non empty AltGraph, C2 being non empty reflexive AltGraph,
o2 being Object of C2, m be Morphism of o2,o2,
F being Covariant feasible FunctorStr over C1,C2 st F = C1 --> m
for o,o9 being Object of C1, f being Morphism of o,o9 st <^o,o9^> <> {}
holds F.f = m
proof
let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph,
o2 be Object of C2;
A1: <^o2,o2^> <> {} by ALTCAT_2:def 7;
let m be Morphism of o2,o2,
F be Covariant feasible FunctorStr over C1,C2 such that
A2: F = C1 --> m;
let o,o9 be Object of C1, f be Morphism of o,o9;
assume
A3: <^o,o9^> <> {};
then <^F.o,F.o9^> <> {} by Def18;
hence F.f = Morph-Map(F,o,o9).f by A3,Def15
.= m by A1,A2,A3,Th24;
end;
theorem Th26:
for C1 being non empty AltGraph, C2 being non empty reflexive AltGraph,
o2 being Object of C2, m be Morphism of o2,o2,
o,o9 being Object of C1, f being Morphism of o,o9 st <^o,o9^> <> {}
holds (C1 --> m).f = m
proof
let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph,
o2 be Object of C2;
A1: <^o2,o2^> <> {} by ALTCAT_2:def 7;
let m be Morphism of o2,o2;
set F = C1 --> m;
let o,o9 be Object of C1, f be Morphism of o,o9;
assume
A2: <^o,o9^> <> {};
then <^F.o9,F.o^> <> {} by Def19;
hence F.f = Morph-Map(F,o,o9).f by A2,Def16
.= m by A1,A2,Th24;
end;
registration
let C1 be non empty transitive AltCatStr,
C2 be with_units non empty AltCatStr;
let o be Object of C2;
cluster C1 --> idm o -> comp-preserving comp-reversing;
coherence
proof
set F = C1 --> idm o;
reconsider G = F as Covariant feasible FunctorStr over C1,C2;
A1: <^o,o^> <> {} by ALTCAT_2:def 7;
G is comp-preserving
proof
let o1,o2,o3 be Object of C1;
assume that
A2: <^o1,o2^> <> {} and
A3: <^o2,o3^> <> {};
A4: <^o1,o3^> <> {} by A2,A3,ALTCAT_1:def 2;
let f be Morphism of o1,o2, g be Morphism of o2,o3;
A5: G.g = idm o by A3,Th25;
A6: G.f = idm o by A2,Th25;
A7: G.o1 = o by A1,Th21;
A8: G.o2 = o by A1,Th21;
A9: G.o3 = o by A1,Th21;
thus G.(g*f) = idm o by A4,Th25
.= (G.g)*(G.f) by A1,A5,A6,A7,A8,A9,ALTCAT_1:20;
end;
hence F is comp-preserving;
let o1,o2,o3 be Object of C1;
assume that
A10: <^o1,o2^> <> {} and
A11: <^o2,o3^> <> {};
A12: <^o1,o3^> <> {} by A10,A11,ALTCAT_1:def 2;
let f be Morphism of o1,o2, g be Morphism of o2,o3;
A13: F.g = idm o by A11,Th26;
A14: F.f = idm o by A10,Th26;
A15: F.o1 = o by A1,Th21;
A16: F.o2 = o by A1,Th21;
A17: F.o3 = o by A1,Th21;
thus F.(g*f) = idm o by A12,Th26
.= (F.f)*(F.g) by A1,A13,A14,A15,A16,A17,ALTCAT_1:20;
end;
end;
definition
let C1 be transitive with_units non empty AltCatStr,
C2 be with_units non empty AltCatStr;
mode Functor of C1,C2 -> FunctorStr over C1,C2 means
:Def25:
it is feasible id-preserving &
(it is Covariant comp-preserving or it is Contravariant comp-reversing);
existence
proof set o = the Object of C2;
take C1 --> idm o;
thus thesis;
end;
end;
definition
let C1 be transitive with_units non empty AltCatStr,
C2 be with_units non empty AltCatStr, F be Functor of C1,C2;
attr F is covariant means
:Def26:
F is Covariant comp-preserving;
attr F is contravariant means
:Def27:
F is Contravariant comp-reversing;
end;
definition
let A be AltCatStr, B be SubCatStr of A;
func incl B -> strict FunctorStr over B,A means
:Def28:
the ObjectMap of it = id [:the carrier of B, the carrier of B:] &
the MorphMap of it = id the Arrows of B;
existence
proof
the carrier of B c= the carrier of A by ALTCAT_2:def 11;
then reconsider CC = [:the carrier of B, the carrier of B:]
as Subset of [:the carrier of A, the carrier of A:] by ZFMISC_1:96;
set OM = id [:the carrier of B, the carrier of B:];
OM = incl CC;
then reconsider OM as bifunction of the carrier of B, the carrier of A;
set MM = id the Arrows of B;
MM is MSUnTrans of OM, the Arrows of B, the Arrows of A
proof
per cases;
case [:the carrier of A,the carrier of A:] <> {};
then reconsider I29 = [:the carrier of A,the carrier of A:]
as non empty set;
reconsider B9 = the Arrows of A as ManySortedSet of I29;
reconsider f9 = OM as
Function of [:the carrier of B,the carrier of B:],I29;
take I29, B9, f9;
thus OM = f9 & the Arrows of A = B9;
thus MM is ManySortedFunction of the Arrows of B,B9*f9
proof
let i be object;
assume
A1: i in [:the carrier of B,the carrier of B:];
then
A2: MM
.i is Function of (the Arrows of B).i, (the Arrows of B).i
by PBOOLE:def 15;
A3: the Arrows of B cc= the Arrows of A by ALTCAT_2:def 11;
(B9*f9).i = B9.(f9.i) by A1,FUNCT_2:15
.= (the Arrows of A).i by A1,FUNCT_1:18;
then (the Arrows of B).i c= (B9*f9).i by A1,A3,ALTCAT_2:def 2;
hence thesis by A2,FUNCT_2:7;
end;
end;
case [:the carrier of A,the carrier of A:] = {};
then CC = {};
hence thesis;
end;
end;
then reconsider MM as MSUnTrans of OM, the Arrows of B, the Arrows of A;
take FunctorStr(#OM,MM#);
thus thesis;
end;
correctness;
end;
definition
let A be AltGraph;
func id A -> strict FunctorStr over A,A means
:Def29:
the ObjectMap of it = id [:the carrier of A, the carrier of A:] &
the MorphMap of it = id the Arrows of A;
existence
proof
reconsider OM = id [:the carrier of A, the carrier of A:]
as bifunction of the carrier of A, the carrier of A;
set MM = id the Arrows of A;
MM is MSUnTrans of OM, the Arrows of A, the Arrows of A
proof
per cases;
case [:the carrier of A,the carrier of A:] <> {};
then reconsider I29 = [:the carrier of A,the carrier of A:]
as non empty set;
reconsider A9 = the Arrows of A as ManySortedSet of I29;
reconsider f9 = OM as
Function of [:the carrier of A,the carrier of A:],I29;
take I29, A9, f9;
thus OM = f9 & the Arrows of A = A9;
thus MM is ManySortedFunction of the Arrows of A,A9*f9
proof
let i be object;
assume
A1: i in [:the carrier of A,the carrier of A:];
then (A9*f9).i = A9.(f9.i) by FUNCT_2:15
.= (the Arrows of A).i by A1,FUNCT_1:18;
hence thesis by A1,PBOOLE:def 15;
end;
end;
case
[:the carrier of A,the carrier of A:] = {};
hence thesis;
end;
end;
then reconsider MM as MSUnTrans of OM, the Arrows of A, the Arrows of A;
take FunctorStr(#OM,MM#);
thus thesis;
end;
correctness;
end;
registration
let A be AltCatStr, B be SubCatStr of A;
cluster incl B -> Covariant;
coherence
proof
reconsider b = the carrier of B as Subset of A by ALTCAT_2:def 11;
incl b = id b;
then reconsider f = id the carrier of B as
Function of the carrier of B, the carrier of A;
take f;
thus
the ObjectMap of incl B = id[:the carrier of B,the carrier of B:] by Def28
.= [:f,f:] by FUNCT_3:69;
end;
end;
theorem Th27:
for A being non empty AltCatStr, B being non empty SubCatStr of A,
o being Object of B holds (incl B).o = o
proof
let A be non empty AltCatStr, B be non empty SubCatStr of A,
o be Object of B;
A1: [o,o] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
thus
(incl B).o = ((id[:the carrier of B,the carrier of B:]).[o,o])`1 by Def28
.= [o,o]`1 by A1,FUNCT_1:18
.= o;
end;
theorem Th28:
for A being non empty AltCatStr, B being non empty SubCatStr of A,
o1,o2 being Object of B holds <^o1,o2^> c= <^(incl B).o1,(incl B).o2^>
proof
let A be non empty AltCatStr, B be non empty SubCatStr of A,
o1,o2 be Object of B;
A1: [o1,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
A2: <^o1,o2^> = (the Arrows of B).(o1,o2) by ALTCAT_1:def 1
.= (the Arrows of B).[o1,o2];
A3: (incl B).o1 = o1 by Th27;
(incl B).o2 = o2 by Th27;
then
A4: <^(incl B).o1,(incl B).o2^> = (the Arrows of A).(o1,o2) by A3,
ALTCAT_1:def 1
.= (the Arrows of A).[o1,o2];
the Arrows of B cc= the Arrows of A by ALTCAT_2:def 11;
hence thesis by A1,A2,A4,ALTCAT_2:def 2;
end;
registration
let A be non empty AltCatStr, B be non empty SubCatStr of A;
cluster incl B -> feasible;
coherence
by Th28,XBOOLE_1:3;
end;
definition
let A,B be AltGraph, F be FunctorStr over A,B;
attr F is faithful means
the MorphMap of F is "1-1";
end;
definition
let A,B be AltGraph, F be FunctorStr over A,B;
attr F is full means
ex B9 being ManySortedSet of [:the carrier of A, the carrier of A:],
f being ManySortedFunction of (the Arrows of A),B9 st
B9 = (the Arrows of B)*the ObjectMap of F & f = the MorphMap of F
& f is "onto";
end;
definition
let A be AltGraph, B be non empty AltGraph, F be FunctorStr over A,B;
redefine attr F is full means
ex f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F st f = the MorphMap of F & f is "onto";
compatibility;
end;
definition
let A,B be AltGraph, F be FunctorStr over A,B;
attr F is injective means
F is one-to-one faithful;
attr F is surjective means
F is full onto;
end;
definition
let A,B be AltGraph, F be FunctorStr over A,B;
attr F is bijective means
F is injective surjective;
end;
registration
let A,B be transitive with_units non empty AltCatStr;
cluster strict covariant contravariant feasible for Functor of A,B;
existence
proof set o = the Object of B;
reconsider F = A --> idm o as Functor of A,B by Def25;
take F;
thus thesis;
end;
end;
theorem Th29:
for A being non empty AltGraph, o being Object of A holds (id A).o = o
proof
let A be non empty AltGraph, o be Object of A;
A1: [o,o] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
thus (id A).o = ((id[:the carrier of A,the carrier of A:]).[o,o])`1 by Def29
.= ([o,o])`1 by A1,FUNCT_1:18
.= o;
end;
theorem Th30:
for A being non empty AltGraph, o1,o2 being Object of A st <^o1,o2^> <> {}
for m being Morphism of o1,o2 holds Morph-Map(id A,o1,o2).m = m
proof
let A be non empty AltGraph, o1,o2 be Object of A such that
<^o1,o2^> <> {};
let m be Morphism of o1,o2;
A1: [o1,o2] in [:the carrier of A, the carrier of A:] by ZFMISC_1:87;
Morph-Map(id A,o1,o2) = (id the Arrows of A).[o1,o2] by Def29;
hence Morph-Map(id A,o1,o2).m
= (id((the Arrows of A).(o1,o2))).m by A1,MSUALG_3:def 1
.= (id<^o1,o2^>).m by ALTCAT_1:def 1
.= m;
end;
registration
let A be non empty AltGraph;
cluster id A -> feasible Covariant;
coherence
proof
thus id A is feasible
proof
let o1,o2 be Object of A;
A1: [o1,o2] in [:the carrier of A, the carrier of A:] by ZFMISC_1:87;
(the ObjectMap of id A).(o1,o2)
= (id[:the carrier of A, the carrier of A:]).[o1,o2] by Def29
.= [o1,o2] by A1,FUNCT_1:18;
then (the Arrows of A).((the ObjectMap of id A).(o1,o2))
= (the Arrows of A).(o1,o2)
.= <^o1,o2^> by ALTCAT_1:def 1;
hence thesis;
end;
thus id A is Covariant
proof
take I = id the carrier of A;
thus
the ObjectMap of id A = id[:the carrier of A,the carrier of A:] by Def29
.= [:I,I:] by FUNCT_3:69;
end;
end;
end;
registration
let A be non empty AltGraph;
cluster Covariant feasible for FunctorStr over A,A;
existence
proof
take id A;
thus thesis;
end;
end;
theorem Th31:
for A being non empty AltGraph, o1,o2 being Object of A st <^o1,o2^> <> {}
for F being Covariant feasible FunctorStr over A,A st F = id A
for m being Morphism of o1,o2 holds F.m = m
proof
let A be non empty AltGraph, o1,o2 be Object of A such that
A1: <^o1,o2^> <> {};
let F be Covariant feasible FunctorStr over A,A such that
A2: F = id A;
let m be Morphism of o1,o2;
<^F.o1,F.o2^> <> {} by A1,Def18;
hence F.m = Morph-Map(F,o1,o2).m by A1,Def15
.= m by A1,A2,Th30;
end;
registration
let A be transitive with_units non empty AltCatStr;
cluster id A -> id-preserving comp-preserving;
coherence
proof
thus id A is id-preserving
proof
let o be Object of A;
<^o,o^> <> {} by ALTCAT_2:def 7;
hence Morph-Map(id A,o,o).idm o = idm o by Th30
.= idm (id A).o by Th29;
end;
set F = id A;
F is comp-preserving
proof
let o1,o2,o3 be Object of A such that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {};
let f be Morphism of o1,o2, g be Morphism of o2,o3;
A3: <^o1,o3^> <> {} by A1,A2,ALTCAT_1:def 2;
A4: F.o1 = o1 by Th29;
A5: F.o2 = o2 by Th29;
A6: F.o3 = o3 by Th29;
A7: F.g = g by A2,Th31;
F.f = f by A1,Th31;
hence thesis by A3,A4,A5,A6,A7,Th31;
end;
hence thesis;
end;
end;
definition
let A be transitive with_units non empty AltCatStr;
redefine func id A -> strict covariant Functor of A,A;
coherence by Def25,Def26;
end;
registration
let A be AltGraph;
cluster id A -> bijective;
coherence
proof
set CC=[:the carrier of A,the carrier of A:];
A1: the ObjectMap of id A = id CC by Def29;
hence id A is one-to-one;
thus id A is faithful
proof
per cases;
suppose
A2: the carrier of A <> {};
let i be set, f be Function such that
A3: i in dom(the MorphMap of id A) and
A4: (the MorphMap of id A).i = f;
consider o1,o2 being Element of A such that
A5: i = [o1,o2] by A2,A3,DOMAIN_1:1;
reconsider o1,o2 as Object of A;
A6: [o1,o2] in [:the carrier of A, the carrier of A:] by A2,ZFMISC_1:87;
f = (id the Arrows of A).(o1,o2) by A4,A5,Def29
.= id((the Arrows of A).[o1,o2]) by A6,MSUALG_3:def 1;
hence thesis;
end;
suppose
A7: the carrier of A = {};
let i be set, f be Function such that
A8: i in dom(the MorphMap of id A) and
(the MorphMap of id A).i = f;
dom(the MorphMap of id A)
= [:the carrier of A, the carrier of A:] by PARTFUN1:def 2
.= {} by A7,ZFMISC_1:90;
hence thesis by A8;
end;
end;
thus id A is full proof per cases;
suppose A is non empty;
then reconsider A as non empty AltGraph;
id A is full
proof
reconsider f = the MorphMap of id A as
ManySortedFunction of (the Arrows of A),
(the Arrows of A)*the ObjectMap of id A by Def4;
take f;
thus f = the MorphMap of id A;
let i be set;
assume
A9: i in [:the carrier of A,the carrier of A:];
then consider o1,o2 being Element of A such that
A10: i = [o1,o2] by DOMAIN_1:1;
reconsider o1,o2 as Object of A;
A11: [o1,o2] in [:the carrier of A, the carrier of A:] by ZFMISC_1:87;
A12: dom(the ObjectMap of id A) = CC by A1;
f.i = (id the Arrows of A).(o1,o2) by A10,Def29
.= id((the Arrows of A).[o1,o2]) by A11,MSUALG_3:def 1;
hence rng(f.i) = (the Arrows of A).[o1,o2]
.= (the Arrows of A).((the ObjectMap of id A).i) by A1,A9,A10,FUNCT_1:18
.= ((the Arrows of A)*the ObjectMap of id A).i by A9,A12,FUNCT_1:13;
end;
hence thesis;
end;
suppose A is empty;
then
A13: the carrier of A = {};
the ObjectMap of id A = id [:the carrier of A, the carrier of A:] by Def29;
then reconsider B = (the Arrows of A)*the ObjectMap of id A as
ManySortedSet of [:the carrier of A, the carrier of A:] by Th2;
reconsider f = the MorphMap of id A as
ManySortedSet of [:the carrier of A, the carrier of A:];
f is ManySortedFunction of (the Arrows of A),B
proof
let i be object;
thus thesis by A13,ZFMISC_1:90;
end;
then reconsider f as ManySortedFunction of (the Arrows of A),B;
take B,f;
thus
B = (the Arrows of A)*the ObjectMap of id A & f = the MorphMap of id A;
let i be set;
thus thesis by A13,ZFMISC_1:90;
end;
end;
the ObjectMap of id A is onto by A1;
hence id A is onto;
end;
end;
begin :: The composition of functors
definition
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be feasible FunctorStr over C1,C2, G be FunctorStr over C2,C3;
func G*F -> strict FunctorStr over C1,C3 means
:Def36:
the ObjectMap of it = (the ObjectMap of G)*the ObjectMap of F &
the MorphMap of it =
((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F;
existence
proof
reconsider O = (the ObjectMap of G)*the ObjectMap of F
as bifunction of the carrier of C1, the carrier of C3;
set I1 = [:the carrier of C1,the carrier of C1:];
reconsider H = (the MorphMap of G)*the ObjectMap of F
as MSUnTrans of O,(the Arrows of C2)*the ObjectMap of F,the Arrows of C3
by Th17;
for ii being set st ii in I1 &
((the Arrows of C2)*the ObjectMap of F).ii = {}
holds (the Arrows of C1).ii = {} or ((the Arrows of C3)*O).ii = {}
proof
let ii be set such that
A1: ii in I1 and
A2: ((the Arrows of C2)*the ObjectMap of F).ii = {};
A3: dom the ObjectMap of F = I1 by FUNCT_2:def 1;
reconsider o1 = ii`1, o2 = ii`2 as Object of C1 by A1,MCART_1:10;
ii = [o1,o2] by A1,MCART_1:21;
then
A4: (the Arrows of C2).((the ObjectMap of F).(o1,o2))
= {} by A1,A2,A3,FUNCT_1:13;
(the Arrows of C1).ii = (the Arrows of C1).(o1,o2) by A1,MCART_1:21
.= <^o1,o2^> by ALTCAT_1:def 1
.= {} by A4,Def11;
hence thesis;
end;
then reconsider M = H**the MorphMap of F
as MSUnTrans of O, the Arrows of C1, the Arrows of C3 by Th19;
take FunctorStr(#O,M#);
thus thesis;
end;
correctness;
end;
registration
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be Covariant feasible FunctorStr over C1,C2,
G be Covariant FunctorStr over C2,C3;
cluster G*F -> Covariant;
correctness
proof
the ObjectMap of F is Covariant by Def12;
then consider f being Function of the carrier of C1, the carrier of C2
such that
A1: the ObjectMap of F = [:f,f:];
the ObjectMap of G is Covariant by Def12;
then consider g being Function of the carrier of C2, the carrier of C3
such that
A2: the ObjectMap of G = [:g,g:];
take g*f;
thus
the ObjectMap of G*F = (the ObjectMap of G)*the ObjectMap of F by Def36
.= [:g*f,g*f:] by A1,A2,FUNCT_3:71;
end;
end;
registration
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be Contravariant feasible FunctorStr over C1,C2,
G be Covariant FunctorStr over C2,C3;
cluster G*F -> Contravariant;
correctness
proof
the ObjectMap of F is Contravariant by Def13;
then consider f being Function of the carrier of C1, the carrier of C2
such that
A1: the ObjectMap of F = ~[:f,f:];
the ObjectMap of G is Covariant by Def12;
then consider g being Function of the carrier of C2, the carrier of C3
such that
A2: the ObjectMap of G = [:g,g:];
take g*f;
thus
the ObjectMap of G*F = (the ObjectMap of G)*the ObjectMap of F by Def36
.= ~([:g,g:]*[:f,f:]) by A1,A2,ALTCAT_2:2
.= ~[:g*f,g*f:] by FUNCT_3:71;
end;
end;
registration
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be Covariant feasible FunctorStr over C1,C2,
G be Contravariant FunctorStr over C2,C3;
cluster G*F -> Contravariant;
correctness
proof
the ObjectMap of F is Covariant by Def12;
then consider f being Function of the carrier of C1, the carrier of C2
such that
A1: the ObjectMap of F = [:f,f:];
the ObjectMap of G is Contravariant by Def13;
then consider g being Function of the carrier of C2, the carrier of C3
such that
A2: the ObjectMap of G = ~[:g,g:];
take g*f;
thus
the ObjectMap of G*F = (the ObjectMap of G)*the ObjectMap of F by Def36
.= ~([:g,g:]*[:f,f:]) by A1,A2,ALTCAT_2:3
.= ~[:g*f,g*f:] by FUNCT_3:71;
end;
end;
registration
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be Contravariant feasible FunctorStr over C1,C2,
G be Contravariant FunctorStr over C2,C3;
cluster G*F -> Covariant;
correctness
proof
the ObjectMap of F is Contravariant by Def13;
then consider f being Function of the carrier of C1, the carrier of C2
such that
A1: the ObjectMap of F = ~[:f,f:];
the ObjectMap of G is Contravariant by Def13;
then consider g being Function of the carrier of C2, the carrier of C3
such that
A2: the ObjectMap of G = ~[:g,g:];
take g*f;
thus
the ObjectMap of G*F = (the ObjectMap of G)*the ObjectMap of F by Def36
.= ~(~[:g,g:]*[:f,f:]) by A1,A2,ALTCAT_2:2
.= ~~([:g,g:]*[:f,f:]) by ALTCAT_2:3
.= [:g,g:]*[:f,f:] by FUNCT_4:53
.= [:g*f,g*f:] by FUNCT_3:71;
end;
end;
registration
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be feasible FunctorStr over C1,C2,
G be feasible FunctorStr over C2,C3;
cluster G*F -> feasible;
coherence
proof
let o1,o2 be Object of C1 such that
A1: <^o1,o2^> <> {};
reconsider p1 = ((the ObjectMap of F).(o1,o2))`1,
p2 = ((the ObjectMap of F).(o1,o2))`2 as Element of C2 by MCART_1:10;
reconsider p1,p2 as Object of C2;
[o1,o2] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:87;
then
A2: [o1,o2] in dom the ObjectMap of F by FUNCT_2:def 1;
A3: ((the ObjectMap of F).(o1,o2)) = [p1,p2] by MCART_1:21;
A4: ((the ObjectMap of(G*F)).(o1,o2))
= ((the ObjectMap of G)*the ObjectMap of F).[o1,o2] by Def36
.= (the ObjectMap of G).(p1,p2) by A2,A3,FUNCT_1:13;
<^p1,p2^> = (the Arrows of C2).(p1,p2) by ALTCAT_1:def 1
.= (the Arrows of C2).((the ObjectMap of F).(o1,o2)) by MCART_1:21;
then <^p1,p2^> <> {} by A1,Def11;
hence thesis by A4,Def11;
end;
end;
theorem
for C1 being non empty AltGraph, C2,C3,C4 being non empty reflexive AltGraph,
F being feasible FunctorStr over C1,C2,
G being feasible FunctorStr over C2,C3, H being FunctorStr over C3,C4
holds H*G*F = H*(G*F)
proof
let C1 be non empty AltGraph, C2,C3,C4 be non empty reflexive AltGraph,
F be feasible FunctorStr over C1,C2,
G be feasible FunctorStr over C2,C3, H be FunctorStr over C3,C4;
A1: the ObjectMap of H*G*F = (the ObjectMap of H*G)*the ObjectMap of F by Def36
.= (the ObjectMap of H)*(the ObjectMap of G)*the ObjectMap of F by Def36
.= (the ObjectMap of H)*((the ObjectMap of G)*the ObjectMap of F)
by RELAT_1:36
.= (the ObjectMap of H)*the ObjectMap of(G*F) by Def36
.= the ObjectMap of H*(G*F) by Def36;
the MorphMap of H*G*F
= ((the MorphMap of H*G)*the ObjectMap of F)**the MorphMap of F by Def36
.= ((the MorphMap of H)*(the ObjectMap of G)**the MorphMap of G)
*(the ObjectMap of F)**the MorphMap of F by Def36
.= (the MorphMap of H)*(the ObjectMap of G)*(the ObjectMap of F)
**((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F by Th12
.= (the MorphMap of H)*((the ObjectMap of G)*the ObjectMap of F)
**((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F by RELAT_1:36
.= ((the MorphMap of H)*the ObjectMap of G*F)**
((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F by Def36
.= ((the MorphMap of H)*the ObjectMap of G*F)**
(((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F) by PBOOLE:140
.= ((the MorphMap of H)*the ObjectMap of G*F)**the MorphMap of G*F by Def36
.= the MorphMap of H*(G*F) by Def36;
hence thesis by A1;
end;
theorem Th33:
for C1 being non empty AltCatStr, C2,C3 being non empty reflexive AltCatStr,
F be feasible reflexive FunctorStr over C1,C2, G be FunctorStr over C2,C3,
o be Object of C1 holds (G*F).o = G.(F.o)
proof
let C1 be non empty AltCatStr, C2,C3 be non empty reflexive AltCatStr,
F be feasible reflexive FunctorStr over C1,C2, G be FunctorStr over C2,C3,
o be Object of C1;
dom the ObjectMap of F = [:the carrier of C1,the carrier of C1:]
by FUNCT_2:def 1;
then
A1: [o,o] in dom the ObjectMap of F by ZFMISC_1:87;
thus (G*F).o = (((the ObjectMap of G)*the ObjectMap of F).(o,o))`1 by Def36
.= ((the ObjectMap of G).((the ObjectMap of F).[o,o]))`1 by A1,FUNCT_1:13
.= G.(F.o) by Def10;
end;
theorem Th34:
for C1 being non empty AltGraph, C2,C3 being non empty reflexive AltGraph,
F be feasible reflexive FunctorStr over C1,C2, G be FunctorStr over C2,C3,
o be Object of C1
holds Morph-Map(G*F,o,o) = Morph-Map(G,F.o,F.o)*Morph-Map(F,o,o)
proof
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph,
F be feasible reflexive FunctorStr over C1,C2,
G be FunctorStr over C2,C3, o be Object of C1;
A1: dom(the MorphMap of G) = [:the carrier of C2,the carrier of C2:]
by PARTFUN1:def 2;
rng(the ObjectMap of F) c= [:the carrier of C2,the carrier of C2:];
then dom((the MorphMap of G)*the ObjectMap of F)
= dom(the ObjectMap of F) by A1,RELAT_1:27
.= [:the carrier of C1,the carrier of C1:] by FUNCT_2:def 1;
then
A2: [o,o] in dom((the MorphMap of G)*the ObjectMap of F) by ZFMISC_1:87;
dom(the MorphMap of F) = [:the carrier of C1,the carrier of C1:]
by PARTFUN1:def 2;
then [o,o] in dom(the MorphMap of F) by ZFMISC_1:87;
then [o,o] in dom((the MorphMap of G)*the ObjectMap of F)
/\ dom(the MorphMap of F) by A2,XBOOLE_0:def 4;
then
A3: [o,o] in dom(((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F)
by PBOOLE:def 19;
A4: ((the MorphMap of G)*the ObjectMap of F).[o,o]
= (the MorphMap of G).((the ObjectMap of F).(o,o)) by A2,FUNCT_1:12
.= Morph-Map(G,F.o,F.o) by Def10;
thus Morph-Map(G*F,o,o)
= (((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F).(o,o)
by Def36
.= Morph-Map(G,F.o,F.o)*Morph-Map(F,o,o) by A3,A4,PBOOLE:def 19;
end;
registration
let C1,C2,C3 be with_units non empty AltCatStr;
let F be id-preserving feasible reflexive FunctorStr over C1,C2;
let G be id-preserving FunctorStr over C2,C3;
cluster G*F -> id-preserving;
coherence
proof
let o be Object of C1;
A1: [o,o] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:87;
then [o,o] in dom the ObjectMap of F by FUNCT_2:def 1;
then ((the Arrows of C2)*the ObjectMap of F).[o,o]
= (the Arrows of C2).((the ObjectMap of F).(o,o)) by FUNCT_1:13
.= (the Arrows of C2).(F.o,F.o) by Def10
.= <^F.o,F.o^> by ALTCAT_1:def 1;
then
A2: ((the Arrows of C2)*the ObjectMap of F).[o,o] <> {} by ALTCAT_2:def 7;
the MorphMap of F is ManySortedFunction of the Arrows of C1,
(the Arrows of C2)*the ObjectMap of F by Def4;
then Morph-Map(F,o,o) is Function of (the Arrows of C1).[o,o],
((the Arrows of C2)*the ObjectMap of F).[o,o] by A1,PBOOLE:def 15;
then
A3: dom Morph-Map(F,o,o) = (the Arrows of C1).(o,o) by A2,FUNCT_2:def 1
.= <^o,o^> by ALTCAT_1:def 1;
thus Morph-Map(G*F,o,o).idm o
= (Morph-Map(G,F.o,F.o)*Morph-Map(F,o,o)).idm o by Th34
.= Morph-Map(G,F.o,F.o).(Morph-Map(F,o,o).idm o) by A3,ALTCAT_1:19
,FUNCT_1:13
.= Morph-Map(G,F.o,F.o).idm F.o by Def20
.= idm G.(F.o) by Def20
.= idm (G*F).o by Th33;
end;
end;
definition
let A,C be non empty reflexive AltCatStr;
let B be non empty SubCatStr of A;
let F be FunctorStr over A,C;
func F|B -> FunctorStr over B,C equals
F*incl B;
correctness;
end;
begin :: The inverse functor
definition
let A,B be non empty AltGraph, F be FunctorStr over A,B;
assume
A1: F is bijective;
func F" -> strict FunctorStr over B,A means
:Def38:
the ObjectMap of it = (the ObjectMap of F)" &
ex f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F st
f = the MorphMap of F & the MorphMap of it = f""*(the ObjectMap of F)";
existence
proof
set OF = the ObjectMap of F;
F is injective by A1;
then F is one-to-one;
then
A2: OF is one-to-one;
F is surjective by A1;
then F is onto;
then OF is onto;
then
A3: rng OF = [:the carrier of B,the carrier of B:];
then reconsider OM = (the ObjectMap of F)" as
bifunction of the carrier of B, the carrier of A by A2,FUNCT_2:25;
reconsider f = the MorphMap of F as
ManySortedFunction of (the Arrows of A), (the Arrows of B)*OF by Def4;
(the Arrows of B)*OF*OM = (the Arrows of B)*(OF*OM) by RELAT_1:36
.= (the Arrows of B)*id[:the carrier of B,the carrier of B:]
by A2,A3,FUNCT_2:29
.= the Arrows of B by Th2;
then f""*OM is ManySortedFunction of the Arrows of B, (the Arrows of A)*OM
by ALTCAT_2:5;
then reconsider MM = f""*OM
as MSUnTrans of OM, the Arrows of B, the Arrows of A by Def4;
take G = FunctorStr(#OM,MM#);
thus the ObjectMap of G = OF";
take f;
thus thesis;
end;
uniqueness;
end;
theorem Th35:
for A,B being transitive with_units non empty AltCatStr,
F being feasible FunctorStr over A,B st F is bijective
holds F" is bijective feasible
proof
let A,B be transitive with_units non empty AltCatStr;
let F be feasible FunctorStr over A,B such that
A1: F is bijective;
set G = F";
A2: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
A3: F is injective by A1;
then F is one-to-one;
then
A4: the ObjectMap of F is one-to-one;
hence the ObjectMap of G is one-to-one by A2;
F is faithful by A3;
then
A5: the MorphMap of F is "1-1";
A6: F is surjective by A1;
then F is onto;
then
A7: the ObjectMap of F is onto;
consider h being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F such that
A8: h = the MorphMap of F and
A9: the MorphMap of G = h""*(the ObjectMap of F)" by A1,Def38;
F is full by A6;
then
A10: ex f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F st
f = the MorphMap of F & f is "onto";
set AA = [:the carrier of A,the carrier of A:],
BB = [:the carrier of B,the carrier of B:];
A11: rng the ObjectMap of F = BB by A7;
reconsider f = the MorphMap of G as ManySortedFunction of
(the Arrows of B),(the Arrows of A)*the ObjectMap of G by Def4;
f is "1-1"
proof
let i be set, g be Function such that
A12: i in dom f and
A13: f.i = g;
i in BB by A12;
then
A14: i in dom((the ObjectMap of F)") by A4,A11,FUNCT_1:33;
then (the ObjectMap of F)".i in rng((the ObjectMap of F)") by FUNCT_1:def 3
;
then
A15: (the ObjectMap of F)".i in dom the ObjectMap of F by A4,FUNCT_1:33;
then (the ObjectMap of F)".i in AA;
then (the ObjectMap of F)".i in dom h by PARTFUN1:def 2;
then
A16: h.((the ObjectMap of F)".i) is one-to-one by A5,A8;
g = h"".((the ObjectMap of F)".i) by A9,A13,A14,FUNCT_1:13
.= (h.((the ObjectMap of F)".i))" by A5,A8,A10,A15,MSUALG_3:def 4;
hence thesis by A16;
end;
hence the MorphMap of G is "1-1";
thus G is full
proof
take f;
thus f = the MorphMap of G;
let i be set;
assume
A17: i in BB;
then
A18: i in dom the ObjectMap of G by FUNCT_2:def 1;
A19: i in dom((the ObjectMap of F)") by A4,A11,A17,FUNCT_1:33;
then (the ObjectMap of F)".i in rng((the ObjectMap of F)") by FUNCT_1:def 3
;
then
A20: (the ObjectMap of F)".i in dom the ObjectMap of F by A4,FUNCT_1:33;
then (the ObjectMap of F)".i in AA;
then ((the ObjectMap of G).i) in dom h by A2,PARTFUN1:def 2;
then
A21: h.((the ObjectMap of G).i) is one-to-one by A5,A8;
set j = (the ObjectMap of G).i;
A22: h.j is Function of (the Arrows of A).j,
((the Arrows of B)*the ObjectMap of F).j by A2,A20,PBOOLE:def 15;
consider o1,o2 being Element of A such that
A23: j = [o1,o2] by A2,A20,DOMAIN_1:1;
reconsider o1,o2 as Object of A;
A24: now
assume (the Arrows of A).j <> {};
then (the Arrows of A).(o1,o2) <> {} by A23;
then <^o1,o2^> <> {} by ALTCAT_1:def 1;
then (the Arrows of B).((the ObjectMap of F).(o1,o2)) <> {} by Def11;
hence ((the Arrows of B)*the ObjectMap of F).j <> {} by A2,A20,A23,
FUNCT_1:13;
end;
f.i = h"".((the ObjectMap of F)".i) by A9,A19,FUNCT_1:13
.= (h.((the ObjectMap of F)".i))" by A5,A8,A10,A20,MSUALG_3:def 4;
hence rng(f.i) = dom(h.((the ObjectMap of G).i)) by A2,A21,FUNCT_1:33
.= (the Arrows of A).((the ObjectMap of G).i) by A22,A24,FUNCT_2:def 1
.= ((the Arrows of A)*the ObjectMap of G).i by A18,FUNCT_1:13;
end;
thus rng the ObjectMap of G = dom the ObjectMap of F by A2,A4,FUNCT_1:33
.= AA by FUNCT_2:def 1;
let o1,o2 be Object of B;
assume <^o1,o2^> <> {};
then
A25: (the Arrows of B).(o1,o2) <> {} by ALTCAT_1:def 1;
A26: [o1,o2] in BB by ZFMISC_1:87;
then consider p1,p2 being Element of A such that
A27: (the ObjectMap of G).[o1,o2] = [p1,p2] by DOMAIN_1:1,FUNCT_2:5;
reconsider p1,p2 as Object of A;
[o1,o2] in dom the ObjectMap of G by A26,FUNCT_2:def 1;
then
A28: (the ObjectMap of F).(p1,p2)
= ((the ObjectMap of F)*(the ObjectMap of G)).[o1,o2] by A27,FUNCT_1:13
.= (id BB).[o1,o2] by A2,A4,A11,FUNCT_1:39
.= [o1,o2] by A26,FUNCT_1:18;
assume
A29: (the Arrows of A).((the ObjectMap of G).(o1,o2)) = {};
A30: [p1,p2] in AA by ZFMISC_1:87;
then
A31: [p1,p2] in dom the ObjectMap of F by FUNCT_2:def 1;
h.[p1,p2] is Function of (the Arrows of A).[p1,p2],
((the Arrows of B)*the ObjectMap of F).[p1,p2] by A30,PBOOLE:def 15;
then {} = rng(h.[p1,p2]) by A27,A29
.= ((the Arrows of B)*the ObjectMap of F).[p1,p2] by A8,A10,A30
.= (the Arrows of B).[o1,o2] by A28,A31,FUNCT_1:13;
hence contradiction by A25;
end;
theorem Th36:
for A,B being transitive with_units non empty AltCatStr,
F being feasible reflexive FunctorStr over A,B st F is bijective coreflexive
holds F" is reflexive
proof
let A,B be transitive with_units non empty AltCatStr,
F be feasible reflexive FunctorStr over A,B such that
A1: F is bijective and
A2: F is coreflexive;
set G = F";
A3: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
let o be Object of B;
A4: dom the ObjectMap of F = [:the carrier of A,the carrier of A:]
by FUNCT_2:def 1;
consider p being Object of A such that
A5: o = F.p by A2,Th20;
F is injective by A1;
then F is one-to-one;
then
A6: the ObjectMap of F is one-to-one;
A7: [p,p] in dom the ObjectMap of F by A4,ZFMISC_1:87;
A8: G.(F.p) = (G*F).p by Th33
.= (((the ObjectMap of G)*the ObjectMap of F).(p,p))`1 by Def36
.= ((id dom the ObjectMap of F).[p,p])`1 by A3,A6,FUNCT_1:39
.= [p,p]`1 by A7,FUNCT_1:18
.= p;
thus (the ObjectMap of G).(o,o)
= (the ObjectMap of G).((the ObjectMap of F).(p,p)) by A5,Def10
.= ((the ObjectMap of G)*(the ObjectMap of F)).[p,p] by A7,FUNCT_1:13
.= (id dom the ObjectMap of F).[p,p] by A3,A6,FUNCT_1:39
.= [G.o,G.o] by A5,A7,A8,FUNCT_1:18;
end;
theorem Th37:
for A,B being transitive with_units non empty AltCatStr,
F being feasible reflexive id-preserving FunctorStr over A,B
st F is bijective coreflexive holds F" is id-preserving
proof
let A,B be transitive with_units non empty AltCatStr,
F be feasible reflexive id-preserving FunctorStr over A,B such that
A1: F is bijective coreflexive;
set G = F";
reconsider H = G as feasible reflexive FunctorStr over B,A by A1,Th35,Th36;
A2: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
consider f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F such that
A3: f = the MorphMap of F and
A4: the MorphMap of G = f""*(the ObjectMap of F)" by A1,Def38;
let o be Object of B;
A5: F is injective by A1;
then F is one-to-one;
then
A6: the ObjectMap of F is one-to-one;
F is faithful by A5;
then
A7: the MorphMap of F is "1-1";
F is surjective by A1;
then F is full;
then
A8: ex f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F st
f = the MorphMap of F & f is "onto";
A9: [G.o,G.o] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
A10: [o,o] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
then
A11: [o,o] in dom the ObjectMap of G by FUNCT_2:def 1;
A12: (the ObjectMap of F*H).(o,o)
= ((the ObjectMap of F)*the ObjectMap of H).[o,o] by Def36
.= ((the ObjectMap of F)*(the ObjectMap of F)").[o,o] by A1,Def38
.= (id rng the ObjectMap of F).[o,o] by A6,FUNCT_1:39
.= (id dom(the ObjectMap of G)).[o,o] by A2,A6,FUNCT_1:33
.= (id[:the carrier of B,the carrier of B:]).[o,o] by FUNCT_2:def 1
.= [o,o] by A10,FUNCT_1:18;
A13: F.(G.o) = (F*H).o by Th33
.= o by A12;
dom the MorphMap of F = [:the carrier of A,the carrier of A:]
by PARTFUN1:def 2;
then [G.o,G.o] in dom the MorphMap of F by ZFMISC_1:87;
then
A14: Morph-Map(F,G.o,G.o) is one-to-one by A7;
[G.o,G.o] in dom the ObjectMap of F by A9,FUNCT_2:def 1;
then ((the Arrows of B)*the ObjectMap of F).[G.o,G.o]
= (the Arrows of B).((the ObjectMap of F).(G.o,G.o)) by FUNCT_1:13
.= (the Arrows of B).(F.(G.o),F.(G.o)) by Def10;
then
A15: ((the Arrows of B)*the ObjectMap of F).[G.o,G.o] <> {} by ALTCAT_2:def 6;
Morph-Map(F,G.o,G.o) is Function of (the Arrows of A).[G.o,G.o],
((the Arrows of B)*the ObjectMap of F).[G.o,G.o] by A3,A9,PBOOLE:def 15;
then
A16: dom Morph-Map(F,G.o,G.o)
= (the Arrows of A).(G.o,G.o) by A15,FUNCT_2:def 1
.= <^G.o,G.o^> by ALTCAT_1:def 1;
((the Arrows of A)*the ObjectMap of G).[o,o]
= (the Arrows of A).((the ObjectMap of H).(o,o)) by A11,FUNCT_1:13
.= (the Arrows of A).(G.o,G.o) by Def10;
then
A17: ((the Arrows of A)*the ObjectMap of G).[o,o] <> {} by ALTCAT_2:def 6;
the MorphMap of G is ManySortedFunction of
the Arrows of B,(the Arrows of A)*the ObjectMap of G by Def4;
then Morph-Map(G,o,o) is Function of (the Arrows of B).[o,o],
((the Arrows of A)*the ObjectMap of G).[o,o] by A10,PBOOLE:def 15;
then
A18: dom Morph-Map(G,o,o) = (the Arrows of B).(o,o) by A17,FUNCT_2:def 1
.= <^o,o^> by ALTCAT_1:def 1;
then
A19: idm o in dom Morph-Map(G,o,o) by ALTCAT_1:19;
A20: Morph-Map(G,o,o)
= f"".((the ObjectMap of G).(o,o)) by A2,A4,A11,FUNCT_1:13
.= f"".[H.o,H.o] by Def10
.= Morph-Map(F,G.o,G.o)" by A3,A7,A8,A9,MSUALG_3:def 4;
Morph-Map(G,o,o).idm o in rng Morph-Map(G,o,o) by A19,FUNCT_1:def 3;
then
A21: Morph-Map(G,o,o).idm o in dom Morph-Map(F,G.o,G.o) by A14,A20,FUNCT_1:33;
Morph-Map(F,G.o,G.o).(Morph-Map(G,o,o).idm o)
= (Morph-Map(F,G.o,G.o)*Morph-Map(G,o,o)).idm o by A18,ALTCAT_1:19,FUNCT_1:13
.= (id rng Morph-Map(F,G.o,G.o)).idm o by A14,A20,FUNCT_1:39
.= (id dom Morph-Map(G,o,o)).idm o by A14,A20,FUNCT_1:33
.= idm F.(G.o) by A13,A18
.= Morph-Map(F,G.o,G.o).idm G.o by Def20;
hence thesis by A14,A16,A21;
end;
theorem Th38:
for A,B being transitive with_units non empty AltCatStr,
F being feasible FunctorStr over A,B st F is bijective Covariant
holds F" is Covariant
proof
let A,B be transitive with_units non empty AltCatStr,
F be feasible FunctorStr over A,B;
assume
A1: F is bijective Covariant;
then F is injective;
then F is one-to-one;
then
A2: the ObjectMap of F is one-to-one;
F is surjective by A1;
then F is onto;
then
A3: the ObjectMap of F is onto;
the ObjectMap of F is Covariant by A1;
then consider f being Function of the carrier of A, the carrier of B
such that
A4: the ObjectMap of F = [:f,f:];
A5: f is one-to-one by A2,A4,Th7;
then
A6: dom(f") = rng f by FUNCT_1:33;
A7: rng(f") = dom f by A5,FUNCT_1:33;
A8: rng[:f,f:] = [:the carrier of B,the carrier of B:] by A3,A4;
rng[:f,f:] = [:rng f,rng f:] by FUNCT_3:67;
then rng f = the carrier of B by A8,ZFMISC_1:92;
then reconsider g = f" as Function of the carrier of B, the carrier of A
by A6,A7,FUNCT_2:def 1,RELSET_1:4;
take g;
[:f,f:]" = [:g,g:] by A5,Th6;
hence thesis by A1,A4,Def38;
end;
theorem Th39:
for A,B being transitive with_units non empty AltCatStr,
F being feasible FunctorStr over A,B st F is bijective Contravariant
holds F" is Contravariant
proof
let A,B be transitive with_units non empty AltCatStr,
F be feasible FunctorStr over A,B;
assume
A1: F is bijective Contravariant;
then F is injective;
then F is one-to-one;
then
A2: the ObjectMap of F is one-to-one;
F is surjective by A1;
then F is onto;
then
A3: the ObjectMap of F is onto;
the ObjectMap of F is Contravariant by A1;
then consider f being Function of the carrier of A, the carrier of B
such that
A4: the ObjectMap of F = ~[:f,f:];
[:f,f:] is one-to-one by A2,A4,Th9;
then
A5: f is one-to-one by Th7;
then
A6: dom(f") = rng f by FUNCT_1:33;
A7: rng(f") = dom f by A5,FUNCT_1:33;
[:f,f:] is onto by A3,A4,Th13;
then
A8: rng[:f,f:] = [:the carrier of B,the carrier of B:];
rng[:f,f:] = [:rng f,rng f:] by FUNCT_3:67;
then rng f = the carrier of B by A8,ZFMISC_1:92;
then reconsider g = f" as Function of the carrier of B, the carrier of A
by A6,A7,FUNCT_2:def 1,RELSET_1:4;
take g;
A9: [:f,f:]" = [:g,g:] by A5,Th6;
thus the ObjectMap of F" = (the ObjectMap of F)" by A1,Def38
.= ~[:g,g:] by A4,A5,A9,Th10;
end;
theorem Th40:
for A,B being transitive with_units non empty AltCatStr,
F being feasible reflexive FunctorStr over A,B
st F is bijective coreflexive Covariant
for o1,o2 being Object of B, m being Morphism of o1,o2 st <^o1,o2^> <> {}
holds Morph-Map(F,F".o1,F".o2).(Morph-Map(F",o1,o2).m) = m
proof
let A,B be transitive with_units non empty AltCatStr,
F be feasible reflexive FunctorStr over A,B such that
A1: F is bijective coreflexive Covariant;
set G = F";
A2: G is Covariant by A1,Th38;
reconsider H = G as feasible reflexive FunctorStr over B,A by A1,Th35,Th36;
A3: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
consider f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F such that
A4: f = the MorphMap of F and
A5: the MorphMap of G = f""*(the ObjectMap of F)" by A1,Def38;
F is injective by A1;
then F is faithful;
then
A6: the MorphMap of F is "1-1";
F is surjective by A1;
then F is full;
then
A7: ex f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F st
f = the MorphMap of F & f is "onto";
let o1,o2 be Object of B, m be Morphism of o1,o2 such that
A8: <^o1,o2^> <> {};
A9: [G.o1,G.o2] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
A10: [o1,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
then
A11: [o1,o2] in dom the ObjectMap of G by FUNCT_2:def 1;
dom the MorphMap of F = [:the carrier of A,the carrier of A:]
by PARTFUN1:def 2;
then [G.o1,G.o2] in dom the MorphMap of F by ZFMISC_1:87;
then
A12: Morph-Map(F,G.o1,G.o2) is one-to-one by A6;
((the Arrows of A)*the ObjectMap of G).[o1,o2]
= (the Arrows of A).((the ObjectMap of H).(o1,o2)) by A11,FUNCT_1:13
.= (the Arrows of A).(H.o1,H.o2) by A2,Th22
.= <^H.o1,H.o2^> by ALTCAT_1:def 1;
then
A13: ((the Arrows of A)*the ObjectMap of G).[o1,o2] <> {} by A2,A8,Def18;
the MorphMap of G is ManySortedFunction of
the Arrows of B,(the Arrows of A)*the ObjectMap of G by Def4;
then Morph-Map(G,o1,o2) is Function of (the Arrows of B).[o1,o2],
((the Arrows of A)*the ObjectMap of G).[o1,o2] by A10,PBOOLE:def 15;
then
A14: dom Morph-Map(G,o1,o2) = (the Arrows of B).(o1,o2) by A13,FUNCT_2:def 1
.= <^o1,o2^> by ALTCAT_1:def 1;
A15: Morph-Map(G,o1,o2)
= f"".((the ObjectMap of G).(o1,o2)) by A3,A5,A11,FUNCT_1:13
.= f"".[H.o1,H.o2] by A2,Th22
.= Morph-Map(F,G.o1,G.o2)" by A4,A6,A7,A9,MSUALG_3:def 4;
thus Morph-Map(F,G.o1,G.o2).(Morph-Map(G,o1,o2).m)
= (Morph-Map(F,G.o1,G.o2)*Morph-Map(G,o1,o2)).m by A8,A14,FUNCT_1:13
.= (id rng Morph-Map(F,G.o1,G.o2)).m by A12,A15,FUNCT_1:39
.= (id dom Morph-Map(G,o1,o2)).m by A12,A15,FUNCT_1:33
.= m by A14;
end;
theorem Th41:
for A,B being transitive with_units non empty AltCatStr,
F being feasible reflexive FunctorStr over A,B
st F is bijective coreflexive Contravariant
for o1,o2 being Object of B, m being Morphism of o1,o2 st <^o1,o2^> <> {}
holds Morph-Map(F,F".o2,F".o1).(Morph-Map(F",o1,o2).m) = m
proof
let A,B be transitive with_units non empty AltCatStr,
F be feasible reflexive FunctorStr over A,B such that
A1: F is bijective coreflexive Contravariant;
set G = F";
A2: G is Contravariant by A1,Th39;
reconsider H = G as feasible reflexive FunctorStr over B,A by A1,Th35,Th36;
A3: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
consider f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F such that
A4: f = the MorphMap of F and
A5: the MorphMap of G = f""*(the ObjectMap of F)" by A1,Def38;
F is injective by A1;
then F is faithful;
then
A6: the MorphMap of F is "1-1";
F is surjective by A1;
then F is full;
then
A7: ex f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F st
f = the MorphMap of F & f is "onto";
let o1,o2 be Object of B, m be Morphism of o1,o2 such that
A8: <^o1,o2^> <> {};
A9: [G.o2,G.o1] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
A10: [o1,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
then
A11: [o1,o2] in dom the ObjectMap of G by FUNCT_2:def 1;
dom the MorphMap of F = [:the carrier of A,the carrier of A:]
by PARTFUN1:def 2;
then [G.o2,G.o1] in dom the MorphMap of F by ZFMISC_1:87;
then
A12: Morph-Map(F,G.o2,G.o1) is one-to-one by A6;
((the Arrows of A)*the ObjectMap of G).[o1,o2]
= (the Arrows of A).((the ObjectMap of H).(o1,o2)) by A11,FUNCT_1:13
.= (the Arrows of A).(H.o2,H.o1) by A2,Th23
.= <^H.o2,H.o1^> by ALTCAT_1:def 1;
then
A13: ((the Arrows of A)*the ObjectMap of G).[o1,o2] <> {} by A2,A8,Def19;
the MorphMap of G is ManySortedFunction of
the Arrows of B,(the Arrows of A)*the ObjectMap of G by Def4;
then Morph-Map(G,o1,o2) is Function of (the Arrows of B).[o1,o2],
((the Arrows of A)*the ObjectMap of G).[o1,o2] by A10,PBOOLE:def 15;
then
A14: dom Morph-Map(G,o1,o2) = (the Arrows of B).(o1,o2) by A13,FUNCT_2:def 1
.= <^o1,o2^> by ALTCAT_1:def 1;
A15: Morph-Map(G,o1,o2)
= f"".((the ObjectMap of G).(o1,o2)) by A3,A5,A11,FUNCT_1:13
.= f"".[H.o2,H.o1] by A2,Th23
.= Morph-Map(F,G.o2,G.o1)" by A4,A6,A7,A9,MSUALG_3:def 4;
thus Morph-Map(F,F".o2,F".o1).(Morph-Map(F",o1,o2).m)
= (Morph-Map(F,G.o2,G.o1)*Morph-Map(G,o1,o2)).m by A8,A14,FUNCT_1:13
.= (id rng Morph-Map(F,G.o2,G.o1)).m by A12,A15,FUNCT_1:39
.= (id dom Morph-Map(G,o1,o2)).m by A12,A15,FUNCT_1:33
.= m by A14;
end;
theorem Th42:
for A,B being transitive with_units non empty AltCatStr,
F being feasible reflexive FunctorStr over A,B st
F is bijective comp-preserving Covariant coreflexive
holds F" is comp-preserving
proof
let A,B be transitive with_units non empty AltCatStr,
F be feasible reflexive FunctorStr over A,B such that
A1: F is bijective comp-preserving Covariant coreflexive;
set G = F";
A2: G is Covariant by A1,Th38;
reconsider H = G as feasible reflexive FunctorStr over B,A by A1,Th35,Th36;
A3: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
consider ff being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F such that
A4: ff = the MorphMap of F and
A5: the MorphMap of G = ff""*(the ObjectMap of F)" by A1,Def38;
A6: F is injective by A1;
then F is one-to-one;
then
A7: the ObjectMap of F is one-to-one;
F is faithful by A6;
then
A8: the MorphMap of F is "1-1";
F is surjective by A1;
then F is full;
then
A9: ex f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F st
f = the MorphMap of F & f is "onto";
let o1,o2,o3 be Object of B;
assume
A10: <^o1,o2^> <> {};
then
A11: <^H.o1,H.o2^> <> {} by A2,Def18;
assume
A12: <^o2,o3^> <> {};
then
A13: <^H.o2,H.o3^> <> {} by A2,Def18;
A14: <^o1,o3^> <> {} by A10,A12,ALTCAT_1:def 2;
then
A15: <^H.o1,H.o3^> <> {} by A2,Def18;
then
A16: <^F.(G.o1),F.(G.o3)^> <> {} by A1,Def18;
let f be Morphism of o1,o2, g be Morphism of o2,o3;
reconsider K = G as Covariant FunctorStr over B,A by A1,Th38;
K.f = Morph-Map(K,o1,o2).f by A10,A11,Def15;
then reconsider f9 = Morph-Map(K,o1,o2).f as Morphism of G.o1,G.o2;
K.g = Morph-Map(K,o2,o3).g by A12,A13,Def15;
then reconsider g9 = Morph-Map(K,o2,o3).g as Morphism of G.o2,G.o3;
take f9,g9;
thus f9 = Morph-Map(G,o1,o2).f;
thus g9 = Morph-Map(G,o2,o3).g;
consider f99 being Morphism of F.(G.o1),F.(G.o2),
g99 being Morphism of F.(G.o2),F.(G.o3) such that
A17: f99 = Morph-Map(F,G.o1,G.o2).f9 and
A18: g99 = Morph-Map(F,G.o2,G.o3).g9 and
A19: Morph-Map(F,G.o1,G.o3).(g9*f9) = g99*f99 by A1,A11,A13;
A20: g = g99 by A1,A12,A18,Th40;
A21: f = f99 by A1,A10,A17,Th40;
A22: [G.o1,G.o3] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
A23: [o1,o3] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
then
A24: [o1,o3] in dom the ObjectMap of G by FUNCT_2:def 1;
dom the MorphMap of F = [:the carrier of A,the carrier of A:]
by PARTFUN1:def 2;
then [G.o1,G.o3] in dom the MorphMap of F by ZFMISC_1:87;
then
A25: Morph-Map(F,G.o1,G.o3) is one-to-one by A8;
[G.o1,G.o3] in dom the ObjectMap of F by A22,FUNCT_2:def 1;
then
A26: ((the Arrows of B)*the ObjectMap of F).[G.o1,G.o3]
= (the Arrows of B).((the ObjectMap of F).(G.o1,G.o3)) by FUNCT_1:13
.= (the Arrows of B).(F.(G.o1),F.(G.o3)) by A1,Th22
.= <^F.(G.o1),F.(G.o3)^> by ALTCAT_1:def 1;
Morph-Map(F,G.o1,G.o3) is Function of (the Arrows of A).[G.o1,G.o3],
((the Arrows of B)*the ObjectMap of F).[G.o1,G.o3] by A4,A22,PBOOLE:def 15;
then
A27: dom Morph-Map(F,G.o1,G.o3)
= (the Arrows of A).(G.o1,G.o3) by A16,A26,FUNCT_2:def 1
.= <^G.o1,G.o3^> by ALTCAT_1:def 1;
A28: ((the Arrows of A)*the ObjectMap of G).[o1,o3]
= (the Arrows of A).((the ObjectMap of H).(o1,o3)) by A24,FUNCT_1:13
.= (the Arrows of A).(G.o1,G.o3) by A2,Th22
.= <^G.o1,G.o3^> by ALTCAT_1:def 1;
the MorphMap of G is ManySortedFunction of
the Arrows of B,(the Arrows of A)*the ObjectMap of G by Def4;
then Morph-Map(G,o1,o3) is Function of (the Arrows of B).[o1,o3],
((the Arrows of A)*the ObjectMap of G).[o1,o3] by A23,PBOOLE:def 15;
then
A29: dom Morph-Map(G,o1,o3)
= (the Arrows of B).(o1,o3) by A15,A28,FUNCT_2:def 1
.= <^o1,o3^> by ALTCAT_1:def 1;
A30: Morph-Map(G,o1,o3)
= ff"".((the ObjectMap of G).(o1,o3)) by A3,A5,A24,FUNCT_1:13
.= ff"".[H.o1,H.o3] by A2,Th22
.= Morph-Map(F,G.o1,G.o3)" by A4,A8,A9,A22,MSUALG_3:def 4;
A31: the ObjectMap of F*H = (the ObjectMap of F)*the ObjectMap of H by Def36
.= (the ObjectMap of F)*(the ObjectMap of F)" by A1,Def38
.= id rng the ObjectMap of F by A7,FUNCT_1:39
.= id dom the ObjectMap of G by A3,A7,FUNCT_1:33
.= id[:the carrier of B,the carrier of B:] by FUNCT_2:def 1;
[o1,o1] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
then
A32: (the ObjectMap of F*H).(o1,o1) = [o1,o1] by A31,FUNCT_1:18;
A33: F.(G.o1) = (F*H).o1 by Th33
.= o1 by A32;
[o2,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
then
A34: (the ObjectMap of F*H).(o2,o2) = [o2,o2] by A31,FUNCT_1:18;
A35: F.(G.o2) = (F*H).o2 by Th33
.= o2 by A34;
[o3,o3] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
then
A36: (the ObjectMap of F*H).(o3,o3) = [o3,o3] by A31,FUNCT_1:18;
A37: F.(G.o3) = (F*H).o3 by Th33
.= o3 by A36;
Morph-Map(G,o1,o3).(g*f) in rng Morph-Map(G,o1,o3) by A14,A29,FUNCT_1:def 3;
then
A38: Morph-Map(G,o1,o3).(g*f) in dom Morph-Map(F,G.o1,G.o3) by A25,A30,
FUNCT_1:33;
Morph-Map(F,G.o1,G.o3).(Morph-Map(G,o1,o3).(g*f))
= Morph-Map(F,G.o1,G.o3).(g9*f9) by A1,A14,A19,A20,A21,A33,A35,A37,Th40;
hence thesis by A25,A27,A38;
end;
theorem Th43:
for A,B being transitive with_units non empty AltCatStr,
F being feasible reflexive FunctorStr over A,B st
F is bijective comp-reversing Contravariant coreflexive
holds F" is comp-reversing
proof
let A,B be transitive with_units non empty AltCatStr,
F be feasible reflexive FunctorStr over A,B such that
A1: F is bijective comp-reversing Contravariant coreflexive;
set G = F";
A2: G is Contravariant by A1,Th39;
reconsider H = G as feasible reflexive FunctorStr over B,A by A1,Th35,Th36;
A3: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
consider ff being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F such that
A4: ff = the MorphMap of F and
A5: the MorphMap of G = ff""*(the ObjectMap of F)" by A1,Def38;
A6: F is injective by A1;
then F is one-to-one;
then
A7: the ObjectMap of F is one-to-one;
F is faithful by A6;
then
A8: the MorphMap of F is "1-1";
F is surjective by A1;
then F is full;
then
A9: ex f being ManySortedFunction of (the Arrows of A),
(the Arrows of B)*the ObjectMap of F st
f = the MorphMap of F & f is "onto";
let o1,o2,o3 be Object of B;
assume
A10: <^o1,o2^> <> {};
then
A11: <^H.o2,H.o1^> <> {} by A2,Def19;
assume
A12: <^o2,o3^> <> {};
then
A13: <^H.o3,H.o2^> <> {} by A2,Def19;
A14: <^o1,o3^> <> {} by A10,A12,ALTCAT_1:def 2;
then
A15: <^H.o3,H.o1^> <> {} by A2,Def19;
then
A16: <^F.(G.o1),F.(G.o3)^> <> {} by A1,Def19;
let f be Morphism of o1,o2, g be Morphism of o2,o3;
reconsider K = G as Contravariant FunctorStr over B,A by A1,Th39;
K.f = Morph-Map(K,o1,o2).f by A10,A11,Def16;
then reconsider f9 = Morph-Map(K,o1,o2).f as Morphism of G.o2,G.o1;
K.g = Morph-Map(K,o2,o3).g by A12,A13,Def16;
then reconsider g9 = Morph-Map(K,o2,o3).g as Morphism of G.o3,G.o2;
take f9,g9;
thus f9 = Morph-Map(G,o1,o2).f;
thus g9 = Morph-Map(G,o2,o3).g;
consider g99 being Morphism of F.(G.o2),F.(G.o3),
f99 being Morphism of F.(G.o1),F.(G.o2) such that
A17: g99 = Morph-Map(F,G.o3,G.o2).g9 and
A18: f99 = Morph-Map(F,G.o2,G.o1).f9 and
A19: Morph-Map(F,G.o3,G.o1).(f9*g9) = g99*f99 by A1,A11,A13;
A20: g = g99 by A1,A12,A17,Th41;
A21: f = f99 by A1,A10,A18,Th41;
A22: [G.o3,G.o1] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
A23: [o1,o3] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
then
A24: [o1,o3] in dom the ObjectMap of G by FUNCT_2:def 1;
dom the MorphMap of F = [:the carrier of A,the carrier of A:]
by PARTFUN1:def 2;
then [G.o3,G.o1] in dom the MorphMap of F by ZFMISC_1:87;
then
A25: Morph-Map(F,G.o3,G.o1) is one-to-one by A8;
[G.o3,G.o1] in dom the ObjectMap of F by A22,FUNCT_2:def 1;
then
A26: ((the Arrows of B)*the ObjectMap of F).[G.o3,G.o1]
= (the Arrows of B).((the ObjectMap of F).(G.o3,G.o1)) by FUNCT_1:13
.= (the Arrows of B).(F.(G.o1),F.(G.o3)) by A1,Th23
.= <^F.(G.o1),F.(G.o3)^> by ALTCAT_1:def 1;
Morph-Map(F,G.o3,G.o1) is Function of (the Arrows of A).[G.o3,G.o1],
((the Arrows of B)*the ObjectMap of F).[G.o3,G.o1] by A4,A22,PBOOLE:def 15;
then
A27: dom Morph-Map(F,G.o3,G.o1)
= (the Arrows of A).(G.o3,G.o1) by A16,A26,FUNCT_2:def 1
.= <^G.o3,G.o1^> by ALTCAT_1:def 1;
A28: ((the Arrows of A)*the ObjectMap of G).[o1,o3]
= (the Arrows of A).((the ObjectMap of H).(o1,o3)) by A24,FUNCT_1:13
.= (the Arrows of A).(G.o3,G.o1) by A2,Th23
.= <^G.o3,G.o1^> by ALTCAT_1:def 1;
the MorphMap of G is ManySortedFunction of
the Arrows of B,(the Arrows of A)*the ObjectMap of G by Def4;
then Morph-Map(G,o1,o3) is Function of (the Arrows of B).[o1,o3],
((the Arrows of A)*the ObjectMap of G).[o1,o3] by A23,PBOOLE:def 15;
then
A29: dom Morph-Map(G,o1,o3)
= (the Arrows of B).(o1,o3) by A15,A28,FUNCT_2:def 1
.= <^o1,o3^> by ALTCAT_1:def 1;
A30: Morph-Map(G,o1,o3)
= ff"".((the ObjectMap of G).(o1,o3)) by A3,A5,A24,FUNCT_1:13
.= ff"".[H.o3,H.o1] by A2,Th23
.= Morph-Map(F,G.o3,G.o1)" by A4,A8,A9,A22,MSUALG_3:def 4;
A31: the ObjectMap of F*H = (the ObjectMap of F)*the ObjectMap of H by Def36
.= (the ObjectMap of F)*(the ObjectMap of F)" by A1,Def38
.= id rng the ObjectMap of F by A7,FUNCT_1:39
.= id dom the ObjectMap of G by A3,A7,FUNCT_1:33
.= id[:the carrier of B,the carrier of B:] by FUNCT_2:def 1;
[o1,o1] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
then
A32: (the ObjectMap of F*H).(o1,o1) = [o1,o1] by A31,FUNCT_1:18;
A33: F.(G.o1) = (F*H).o1 by Th33
.= o1 by A32;
[o2,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
then
A34: (the ObjectMap of F*H).(o2,o2) = [o2,o2] by A31,FUNCT_1:18;
A35: F.(G.o2) = (F*H).o2 by Th33
.= o2 by A34;
[o3,o3] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
then
A36: (the ObjectMap of F*H).(o3,o3) = [o3,o3] by A31,FUNCT_1:18;
A37: F.(G.o3) = (F*H).o3 by Th33
.= o3 by A36;
Morph-Map(G,o1,o3).(g*f) in rng Morph-Map(G,o1,o3) by A14,A29,FUNCT_1:def 3;
then
A38: Morph-Map(G,o1,o3).(g*f) in dom Morph-Map(F,G.o3,G.o1) by A25,A30,
FUNCT_1:33;
Morph-Map(F,G.o3,G.o1).(Morph-Map(G,o1,o3).(g*f))
= Morph-Map(F,G.o3,G.o1).(f9*g9) by A1,A14,A19,A20,A21,A33,A35,A37,Th41;
hence thesis by A25,A27,A38;
end;
registration
let C1 be 1-sorted, C2 be non empty 1-sorted;
cluster Covariant -> reflexive for BimapStr over C1,C2;
coherence
proof
let M be BimapStr over C1,C2;
assume M is Covariant;
then the ObjectMap of M is Covariant;
then ex f being Function of the carrier of C1, the carrier of C2
st the ObjectMap of M = [:f,f:];
hence
(the ObjectMap of M).:id the carrier of C1 c= id the carrier of C2 by Th14;
end;
end;
registration
let C1 be 1-sorted, C2 be non empty 1-sorted;
cluster Contravariant -> reflexive for BimapStr over C1,C2;
coherence
proof
let M be BimapStr over C1,C2;
assume M is Contravariant;
then the ObjectMap of M is Contravariant;
then consider f being Function of the carrier of C1, the carrier of C2
such that
A1: the ObjectMap of M = ~[:f,f:];
(~[:f,f:]).:id the carrier of C1 = [:f,f:].:id the carrier of C1 by Th3;
hence
(the ObjectMap of M).:id the carrier of C1 c= id the carrier of C2
by A1,Th14;
end;
end;
theorem Th44:
for C1,C2 being 1-sorted, M being BimapStr over C1,C2
st M is Covariant onto holds M is coreflexive
proof
let C1,C2 be 1-sorted;
let M be BimapStr over C1,C2;
assume
A1: M is Covariant onto;
then the ObjectMap of M is Covariant;
then consider f being Function of the carrier of C1, the carrier of C2
such that
A2: the ObjectMap of M = [:f,f:];
the ObjectMap of M is onto by A1;
then f is onto by A2,Th4;
hence
id the carrier of C2 c= (the ObjectMap of M).:id the carrier of C1
by A2,Th11;
end;
theorem Th45:
for C1,C2 being 1-sorted, M being BimapStr over C1,C2
st M is Contravariant onto holds M is coreflexive
proof
let C1,C2 be 1-sorted;
let M be BimapStr over C1,C2;
assume
A1: M is Contravariant onto;
then the ObjectMap of M is Contravariant;
then consider f being Function of the carrier of C1, the carrier of C2
such that
A2: the ObjectMap of M = ~[:f,f:];
the ObjectMap of M is onto by A1;
then [:f,f:] is onto by A2,Th13;
then
A3: f is onto by Th4;
(the ObjectMap of M).:id the carrier of C1
= [:f,f:].:id the carrier of C1 by A2,Th3;
hence
id the carrier of C2 c= (the ObjectMap of M).:id the carrier of C1
by A3,Th11;
end;
registration
let C1 be transitive with_units non empty AltCatStr,
C2 be with_units non empty AltCatStr;
cluster covariant -> reflexive for Functor of C1,C2;
coherence;
end;
registration
let C1 be transitive with_units non empty AltCatStr,
C2 be with_units non empty AltCatStr;
cluster contravariant -> reflexive for Functor of C1,C2;
coherence;
end;
theorem Th46:
for C1 being transitive with_units non empty AltCatStr,
C2 being with_units non empty AltCatStr,
F being Functor of C1,C2 st F is covariant onto holds F is coreflexive
by Th44;
theorem Th47:
for C1 being transitive with_units non empty AltCatStr,
C2 being with_units non empty AltCatStr,
F being Functor of C1,C2 st F is contravariant onto holds F is coreflexive
by Th45;
theorem Th48:
for A,B being transitive with_units non empty AltCatStr,
F being covariant Functor of A,B st F is bijective
ex G being Functor of B,A st G = F" & G is bijective covariant
proof
let A,B be transitive with_units non empty AltCatStr,
F be covariant Functor of A,B;
assume
A1: F is bijective;
then F is injective;
then F is one-to-one;
then
A2: the ObjectMap of F is one-to-one;
A3: F is feasible by Def25;
then
A4: F" is bijective feasible by A1,Th35;
A5: F is id-preserving by Def25;
A6: F is comp-preserving by Def26;
F is surjective by A1;
then
A7: F is onto;
then
A8: the ObjectMap of F is onto;
A9: F is Covariant by Def26;
A10: F is coreflexive by A7,Th46;
A11: F" is Covariant proof F is Covariant by Def26;
then the ObjectMap of F is Covariant;
then consider f being Function of the carrier of A, the carrier of B
such that
A12: the ObjectMap of F = [:f,f:];
A13: f is one-to-one by A2,A12,Th7;
then
A14: dom(f") = rng f by FUNCT_1:33;
A15: rng(f") = dom f by A13,FUNCT_1:33;
A16: rng[:f,f:] = [:the carrier of B,the carrier of B:]
by A8,A12;
rng[:f,f:] = [:rng f,rng f:] by FUNCT_3:67;
then rng f = the carrier of B by A16,ZFMISC_1:92;
then reconsider g = f" as Function of the carrier of B, the carrier of A
by A14,A15,FUNCT_2:def 1,RELSET_1:4;
take g;
[:f,f:]" = [:g,g:] by A13,Th6;
hence thesis by A1,A12,Def38;
end;
A17: F" is id-preserving by A1,A3,A5,A10,Th37;
F" is comp-preserving by A1,A3,A6,A9,A10,Th42;
then reconsider G = F" as Functor of B,A by A4,A11,A17,Def25;
take G;
thus G = F";
thus G is bijective by A1,A3,Th35;
thus G is Covariant by A11;
thus thesis by A1,A3,A6,A9,A10,Th42;
end;
theorem Th49:
for A,B being transitive with_units non empty AltCatStr,
F being contravariant Functor of A,B st F is bijective
ex G being Functor of B,A st G = F" & G is bijective contravariant
proof
let A,B be transitive with_units non empty AltCatStr,
F be contravariant Functor of A,B;
assume
A1: F is bijective;
then F is injective;
then F is one-to-one;
then
A2: the ObjectMap of F is one-to-one;
A3: F is feasible by Def25;
then
A4: F" is bijective feasible by A1,Th35;
A5: F is id-preserving by Def25;
A6: F is comp-reversing by Def27;
F is surjective by A1;
then
A7: F is onto;
then
A8: the ObjectMap of F is onto;
A9: F is Contravariant by Def27;
A10: F is coreflexive by A7,Th47;
A11: F" is Contravariant proof F is Contravariant by Def27;
then the ObjectMap of F is Contravariant;
then consider f being Function of the carrier of A, the carrier of B
such that
A12: the ObjectMap of F = ~[:f,f:];
[:f,f:] is one-to-one by A2,A12,Th9;
then
A13: f is one-to-one by Th7;
then
A14: dom(f") = rng f by FUNCT_1:33;
A15: rng(f") = dom f by A13,FUNCT_1:33;
[:f,f:] is onto by A8,A12,Th13;
then
A16: rng[:f,f:] = [:the carrier of B,the carrier of B:];
rng[:f,f:] = [:rng f,rng f:] by FUNCT_3:67;
then rng f = the carrier of B by A16,ZFMISC_1:92;
then reconsider g = f" as Function of the carrier of B, the carrier of A
by A14,A15,FUNCT_2:def 1,RELSET_1:4;
take g;
A17: [:f,f:]" = [:g,g:] by A13,Th6;
thus the ObjectMap of F" = (the ObjectMap of F)" by A1,Def38
.= ~[:g,g:] by A12,A13,A17,Th10;
end;
A18: F" is id-preserving by A1,A3,A5,A10,Th37;
F" is comp-reversing by A1,A3,A6,A9,A10,Th43;
then reconsider G = F" as Functor of B,A by A4,A11,A18,Def25;
take G;
thus G = F";
thus G is bijective by A1,A3,Th35;
thus G is Contravariant by A11;
thus thesis by A1,A3,A6,A9,A10,Th43;
end;
definition
let A,B be transitive with_units non empty AltCatStr;
pred A,B are_isomorphic means
ex F being Functor of A,B st F is bijective covariant;
reflexivity
proof
let A be transitive with_units non empty AltCatStr;
take id A;
thus thesis;
end;
symmetry
proof
let A,B be transitive with_units non empty AltCatStr;
given F being Functor of A,B such that
A1: F is bijective covariant;
consider G being Functor of B,A such that G = F" and
A2: G is bijective covariant by A1,Th48;
take G;
thus thesis by A2;
end;
pred A,B are_anti-isomorphic means
ex F being Functor of A,B st F is bijective contravariant;
symmetry
proof
let A,B be transitive with_units non empty AltCatStr;
given F being Functor of A,B such that
A3: F is bijective contravariant;
consider G being Functor of B,A such that G = F" and
A4: G is bijective contravariant by A3,Th49;
take G;
thus thesis by A4;
end;
end;