:: FUNCTOR0 semantic presentation
begin
scheme :: FUNCTOR0:sch 1
ValOnPair{ F1() -> non empty set , F2() -> Function, F3() -> Element of F1(), F4() -> Element of F1(), F5( set , set ) -> set , P1[ set , set ] } :
F2() . (F3(),F4()) = F5(F3(),F4())
provided
A1: F2() = { [[o,o9],F5(o,o9)] where o, o9 is Element of F1() : P1[o,o9] } and
A2: P1[F3(),F4()]
proof
defpred S1[ set ] means P1[$1 `1 ,$1 `2 ];
deffunc H1( set ) -> set = F5(($1 `1),($1 `2));
A3: F2() = { [o,H1(o)] where o is Element of [:F1(),F1():] : S1[o] }
proof
thus F2() c= { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] } :: according to XBOOLE_0:def_10 ::_thesis: { [o,H1(o)] where o is Element of [:F1(),F1():] : S1[o] } c= F2()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F2() or y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] } )
assume y in F2() ; ::_thesis: y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] }
then consider o1, o2 being Element of F1() such that
A4: y = [[o1,o2],F5(o1,o2)] and
A5: P1[o1,o2] by A1;
reconsider p = [o1,o2] as Element of [:F1(),F1():] by ZFMISC_1:87;
A6: p `1 = o1 by MCART_1:7;
p `2 = o2 by MCART_1:7;
hence y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] } by A4, A5, A6; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { [o,H1(o)] where o is Element of [:F1(),F1():] : S1[o] } or y in F2() )
assume y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] } ; ::_thesis: y in F2()
then consider o being Element of [:F1(),F1():] such that
A7: y = [o,F5((o `1),(o `2))] and
A8: P1[o `1 ,o `2 ] ;
reconsider o1 = o `1 , o2 = o `2 as Element of F1() by MCART_1:10;
o = [o1,o2] by MCART_1:21;
hence y in F2() by A1, A7, A8; ::_thesis: verum
end;
reconsider x = [F3(),F4()] as Element of [:F1(),F1():] by ZFMISC_1:87;
A9: x `1 = F3() by MCART_1:7;
then A10: S1[x] by A2, MCART_1:7;
thus F2() . (F3(),F4()) = F2() . x
.= H1(x) from ALTCAT_2:sch_3(A3, A10)
.= F5(F3(),F4()) by A9, MCART_1:7 ; ::_thesis: verum
end;
theorem Th1: :: FUNCTOR0:1
for A being set holds {} is Function of A,{}
proof
let A be set ; ::_thesis: {} is Function of A,{}
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: {} is Function of A,{}
hence {} is Function of A,{} by RELSET_1:12; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: {} is Function of A,{}
thus {} is Function of A,{} by FUNCT_2:def_1, RELSET_1:12; ::_thesis: verum
end;
end;
end;
theorem Th2: :: FUNCTOR0:2
for I being set
for M being ManySortedSet of I holds M * (id I) = M
proof
let I be set ; ::_thesis: for M being ManySortedSet of I holds M * (id I) = M
let M be ManySortedSet of I; ::_thesis: M * (id I) = M
I = dom M by PARTFUN1:def_2;
hence M * (id I) = M by RELAT_1:52; ::_thesis: verum
end;
registration
let f be empty Function;
cluster ~ f -> empty ;
coherence
~ f is empty
proof
rng f = {} ;
then rng (~ f) = {} by FUNCT_4:41, XBOOLE_1:3;
hence ~ f is empty ; ::_thesis: verum
end;
let g be Function;
cluster[:f,g:] -> empty ;
coherence
[:f,g:] is empty
proof
dom f = {} ;
then dom [:f,g:] = [:{},(dom g):] by FUNCT_3:def_8;
hence [:f,g:] is empty by ZFMISC_1:90; ::_thesis: verum
end;
cluster[:g,f:] -> empty ;
coherence
[:g,f:] is empty
proof
dom f = {} ;
then dom [:g,f:] = [:(dom g),{}:] by FUNCT_3:def_8;
hence [:g,f:] is empty by ZFMISC_1:90; ::_thesis: verum
end;
end;
theorem Th3: :: FUNCTOR0:3
for A being set
for f being Function holds f .: (id A) = (~ f) .: (id A)
proof
let A be set ; ::_thesis: for f being Function holds f .: (id A) = (~ f) .: (id A)
let f be Function; ::_thesis: f .: (id A) = (~ f) .: (id A)
thus f .: (id A) c= (~ f) .: (id A) :: according to XBOOLE_0:def_10 ::_thesis: (~ f) .: (id A) c= f .: (id A)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (id A) or y in (~ f) .: (id A) )
assume y in f .: (id A) ; ::_thesis: y in (~ f) .: (id A)
then consider x being set 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 set 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 y in (~ f) .: (id A) by A2, A3, A4, A6, FUNCT_1:def_6; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (~ f) .: (id A) or y in f .: (id A) )
assume y in (~ f) .: (id A) ; ::_thesis: y in f .: (id A)
then consider x being set 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 set 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 y in f .: (id A) by A8, A9, A10, A12, FUNCT_1:def_6; ::_thesis: verum
end;
theorem Th4: :: FUNCTOR0:4
for X, Y being set
for f being Function of X,Y holds
( f is onto iff [:f,f:] is onto )
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y holds
( f is onto iff [:f,f:] is onto )
let f be Function of X,Y; ::_thesis: ( f is onto iff [:f,f:] is onto )
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 ( f is onto iff [:f,f:] is onto ) by FUNCT_2:def_3; ::_thesis: verum
end;
registration
let f be Function-yielding Function;
cluster ~ f -> Function-yielding ;
coherence
~ f is Function-yielding ;
end;
theorem Th5: :: FUNCTOR0:5
for A, B, a being set holds ~ ([:A,B:] --> a) = [:B,A:] --> a
proof
let A, B be set ; ::_thesis: for a being set holds ~ ([:A,B:] --> a) = [:B,A:] --> a
let a be set ; ::_thesis: ~ ([:A,B:] --> a) = [:B,A:] --> a
A1: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_([:B,A:]_-->_a)_implies_ex_y,_z_being_set_st_
(_x_=_[z,y]_&_[y,z]_in_dom_([:A,B:]_-->_a)_)_)_&_(_ex_y,_z_being_set_st_
(_x_=_[z,y]_&_[y,z]_in_dom_([:A,B:]_-->_a)_)_implies_x_in_dom_([:B,A:]_-->_a)_)_)
let x be set ; ::_thesis: ( ( x in dom ([:B,A:] --> a) implies ex y, z being set st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) ) & ( ex y, z being set st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) implies x in dom ([:B,A:] --> a) ) )
hereby ::_thesis: ( ex y, z being set st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) ) implies x in dom ([:B,A:] --> a) )
assume x in dom ([:B,A:] --> a) ; ::_thesis: ex y, z being set st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) )
then consider z, y being set such that
A2: z in B and
A3: y in A and
A4: x = [z,y] by ZFMISC_1:def_2;
take y = y; ::_thesis: ex z being set st
( x = [z,y] & [y,z] in dom ([:A,B:] --> a) )
take z = z; ::_thesis: ( x = [z,y] & [y,z] in dom ([:A,B:] --> a) )
thus x = [z,y] by A4; ::_thesis: [y,z] in dom ([:A,B:] --> a)
[y,z] in [:A,B:] by A2, A3, ZFMISC_1:87;
hence [y,z] in dom ([:A,B:] --> a) by FUNCOP_1:13; ::_thesis: verum
end;
given y, z being set such that A5: x = [z,y] and
A6: [y,z] in dom ([:A,B:] --> a) ; ::_thesis: x in dom ([:B,A:] --> 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) by FUNCOP_1:13; ::_thesis: verum
end;
now__::_thesis:_for_y,_z_being_set_st_[y,z]_in_dom_([:A,B:]_-->_a)_holds_
([:B,A:]_-->_a)_._(z,y)_=_([:A,B:]_-->_a)_._(y,z)
let y, z be set ; ::_thesis: ( [y,z] in dom ([:A,B:] --> a) implies ([:B,A:] --> a) . (z,y) = ([:A,B:] --> a) . (y,z) )
assume A8: [y,z] in dom ([:A,B:] --> a) ; ::_thesis: ([:B,A:] --> a) . (z,y) = ([:A,B:] --> a) . (y,z)
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 ;
::_thesis: verum
end;
hence ~ ([:A,B:] --> a) = [:B,A:] --> a by A1, FUNCT_4:def_2; ::_thesis: verum
end;
theorem Th6: :: FUNCTOR0:6
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; ::_thesis: ( f is one-to-one & g is one-to-one implies [:f,g:] " = [:(f "),(g "):] )
assume that
A1: f is one-to-one and
A2: g is one-to-one ; ::_thesis: [:f,g:] " = [:(f "),(g "):]
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 set st x in dom (f ") & y in dom (g ") holds
([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)]
proof
let x, y be set ; ::_thesis: ( x in dom (f ") & y in dom (g ") implies ([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)] )
assume that
A7: x in dom (f ") and
A8: y in dom (g ") ; ::_thesis: ([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)]
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 ([:f,g:] ") . (x,y) = [((f ") . x),((g ") . y)] by A1, A2, A13, FUNCT_1:32; ::_thesis: verum
end;
hence [:f,g:] " = [:(f "),(g "):] by A6, FUNCT_3:def_8; ::_thesis: verum
end;
theorem Th7: :: FUNCTOR0:7
for f being Function st [:f,f:] is one-to-one holds
f is one-to-one
proof
let f be Function; ::_thesis: ( [:f,f:] is one-to-one implies f is one-to-one )
assume A1: [:f,f:] is one-to-one ; ::_thesis: f is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A2: x1 in dom f and
A3: x2 in dom f and
A4: f . x1 = f . x2 ; ::_thesis: x1 = 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, FUNCT_1:def_4;
hence x1 = x2 by XTUPLE_0:1; ::_thesis: verum
end;
theorem Th8: :: FUNCTOR0:8
for f being Function st f is one-to-one holds
~ f is one-to-one
proof
let f be Function; ::_thesis: ( f is one-to-one implies ~ f is one-to-one )
assume A1: f is one-to-one ; ::_thesis: ~ f is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 (~ f) or not x2 in proj1 (~ f) or not (~ f) . x1 = (~ f) . x2 or x1 = x2 )
consider X, Y being set such that
A2: dom (~ f) c= [:X,Y:] by FUNCT_4:44;
assume A3: x1 in dom (~ f) ; ::_thesis: ( not x2 in proj1 (~ f) or not (~ f) . x1 = (~ f) . x2 or x1 = x2 )
then consider x11, x12 being set 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) ; ::_thesis: ( not (~ f) . x1 = (~ f) . x2 or x1 = x2 )
then consider x21, x22 being set 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 ; ::_thesis: x1 = 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, FUNCT_1:def_4;
then x12 = x22 by XTUPLE_0:1;
hence x1 = x2 by A4, A6, A10, XTUPLE_0:1; ::_thesis: verum
end;
theorem Th9: :: FUNCTOR0:9
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; ::_thesis: ( ~ [:f,g:] is one-to-one implies [:g,f:] is one-to-one )
assume A1: ~ [:f,g:] is one-to-one ; ::_thesis: [:g,f:] is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 [:g,f:] or not x2 in proj1 [:g,f:] or not [:g,f:] . x1 = [:g,f:] . x2 or x1 = x2 )
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:] ; ::_thesis: ( not x2 in proj1 [:g,f:] or not [:g,f:] . x1 = [:g,f:] . x2 or x1 = x2 )
then consider x11, x12 being set 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:] ; ::_thesis: ( not [:g,f:] . x1 = [:g,f:] . x2 or x1 = x2 )
then consider x21, x22 being set 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 ; ::_thesis: x1 = 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 x1 = x2 by A1, A6, A9, A10, A11, FUNCT_1:def_4; ::_thesis: verum
end;
theorem Th10: :: FUNCTOR0:10
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; ::_thesis: ( f is one-to-one & g is one-to-one implies (~ [:f,g:]) " = ~ ([:g,f:] ") )
assume that
A1: f is one-to-one and
A2: g is one-to-one ; ::_thesis: (~ [:f,g:]) " = ~ ([:g,f:] ")
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__::_thesis:_for_y,_x_being_set_holds_
(_(_y_in_rng_(~_[:f,g:])_&_x_=_(~_([:g,f:]_"))_._y_implies_(_x_in_dom_(~_[:f,g:])_&_(~_[:f,g:])_._x_=_y_)_)_&_(_x_in_dom_(~_[:f,g:])_&_(~_[:f,g:])_._x_=_y_implies_(_y_in_rng_(~_[:f,g:])_&_x_=_(~_([:g,f:]_"))_._y_)_)_)
let y, x be set ; ::_thesis: ( ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y implies ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y ) ) & ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y implies ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y ) ) )
hereby ::_thesis: ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y implies ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y ) )
assume that
A11: y in rng (~ [:f,g:]) and
A12: x = (~ ([:g,f:] ")) . y ; ::_thesis: ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = 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 set 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;
set 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
.= [((g ") . y2),((f ") . y1)] 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: (f ") . y1 in rng (f ") by A19, FUNCT_1:def_3;
A22: (g ") . y2 in rng (g ") by A20, FUNCT_1:def_3;
A23: (f ") . y1 in dom f by A1, A21, FUNCT_1:33;
A24: (g ") . y2 in dom g by A2, A22, FUNCT_1:33;
then A25: [((g ") . y2),((f ") . y1)] in dom [:g,f:] by A6, A23, ZFMISC_1:87;
then A26: [((g ") . y2),((f ") . y1)] 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; ::_thesis: (~ [:f,g:]) . x = y
A27: f . ((f ") . y1) = y1 by A1, A13, FUNCT_1:32;
A28: g . ((g ") . y2) = y2 by A2, A14, FUNCT_1:32;
thus (~ [:f,g:]) . x = (~ [:f,g:]) . (((g ") . y2),((f ") . y1)) by A12, A15, A18
.= [:f,g:] . (((f ") . y1),((g ") . y2)) by A26, FUNCT_4:43
.= y by A15, A23, A24, A27, A28, FUNCT_3:def_8 ; ::_thesis: verum
end;
assume that
A29: x in dom (~ [:f,g:]) and
A30: (~ [:f,g:]) . x = y ; ::_thesis: ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y )
thus y in rng (~ [:f,g:]) by A29, A30, FUNCT_1:def_3; ::_thesis: x = (~ ([:g,f:] ")) . y
x in dom [:g,f:] by A5, A6, A29, FUNCT_4:46;
then consider x1, x2 being set 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 ;
::_thesis: verum
end;
hence (~ [:f,g:]) " = ~ ([:g,f:] ") by A8, A10, FUNCT_1:32; ::_thesis: verum
end;
theorem Th11: :: FUNCTOR0:11
for A, B being set
for f being Function of A,B st f is onto holds
id B c= [:f,f:] .: (id A)
proof
let A, B be set ; ::_thesis: for f being Function of A,B st f is onto holds
id B c= [:f,f:] .: (id A)
let f be Function of A,B; ::_thesis: ( f is onto implies id B c= [:f,f:] .: (id A) )
assume f is onto ; ::_thesis: id B c= [:f,f:] .: (id A)
then A1: rng f = B by FUNCT_2:def_3;
let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in id B or xx in [:f,f:] .: (id A) )
assume A2: xx in id B ; ::_thesis: xx in [:f,f:] .: (id A)
then consider x, x9 being set 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 set 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 xx in [:f,f:] .: (id A) by A2, A9, FUNCT_2:35; ::_thesis: verum
end;
theorem Th12: :: FUNCTOR0:12
for F, G being Function-yielding Function
for f being Function holds (G ** F) * f = (G * f) ** (F * f)
proof
let F, G be Function-yielding Function; ::_thesis: for f being Function holds (G ** F) * f = (G * f) ** (F * f)
let f be Function; ::_thesis: (G ** F) * f = (G * f) ** (F * f)
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__::_thesis:_for_i_being_set_st_i_in_dom_((G_**_F)_*_f)_holds_
((G_**_F)_*_f)_._i_=_((G_*_f)_._i)_*_((F_*_f)_._i)
let i be set ; ::_thesis: ( i in dom ((G ** F) * f) implies ((G ** F) * f) . i = ((G * f) . i) * ((F * f) . i) )
assume A2: i in dom ((G ** F) * f) ; ::_thesis: ((G ** F) * f) . i = ((G * f) . i) * ((F * f) . i)
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 ; ::_thesis: verum
end;
hence (G ** F) * f = (G * f) ** (F * f) by A1, PBOOLE:def_19; ::_thesis: verum
end;
definition
let A, B, C be set ;
let f be Function of [:A,B:],C;
:: original: ~
redefine func ~ f -> Function of [:B,A:],C;
coherence
~ f is Function of [:B,A:],C
proof
percases ( C = {} or C <> {} ) ;
supposeA1: C = {} ; ::_thesis: ~ f is Function of [:B,A:],C
then reconsider f = f as empty set ;
~ f = {} ;
hence ~ f is Function of [:B,A:],C by A1, Th1; ::_thesis: verum
end;
suppose C <> {} ; ::_thesis: ~ f is Function of [:B,A:],C
hence ~ f is Function of [:B,A:],C by FUNCT_4:49; ::_thesis: verum
end;
end;
end;
end;
theorem Th13: :: FUNCTOR0:13
for A, B, C being set
for f being Function of [:A,B:],C st ~ f is onto holds
f is onto
proof
let A, B, C be set ; ::_thesis: for f being Function of [:A,B:],C st ~ f is onto holds
f is onto
let f be Function of [:A,B:],C; ::_thesis: ( ~ f is onto implies f is onto )
A1: rng (~ f) c= rng f by FUNCT_4:41;
assume ~ f is onto ; ::_thesis: f is onto
then rng (~ f) = C by FUNCT_2:def_3;
hence rng f = C by A1, XBOOLE_0:def_10; :: according to FUNCT_2:def_3 ::_thesis: verum
end;
theorem Th14: :: FUNCTOR0:14
for A being set
for B being non empty set
for f being Function of A,B holds [:f,f:] .: (id A) c= id B
proof
let A be set ; ::_thesis: for B being non empty set
for f being Function of A,B holds [:f,f:] .: (id A) c= id B
let B be non empty set ; ::_thesis: for f being Function of A,B holds [:f,f:] .: (id A) c= id B
let f be Function of A,B; ::_thesis: [:f,f:] .: (id A) c= id B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:f,f:] .: (id A) or x in id B )
assume x in [:f,f:] .: (id A) ; ::_thesis: x in id B
then consider yy being set 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 set 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 = 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 x in id B by A7, RELAT_1:def_10; ::_thesis: verum
end;
begin
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 ;
let f be bifunction of A,B;
attrf is Covariant means :Def1: :: FUNCTOR0:def 1
ex g being Function of A,B st f = [:g,g:];
attrf is Contravariant means :Def2: :: FUNCTOR0:def 2
ex g being Function of A,B st f = ~ [:g,g:];
end;
:: deftheorem Def1 defines Covariant FUNCTOR0:def_1_:_
for A, B being set
for f being bifunction of A,B holds
( f is Covariant iff ex g being Function of A,B st f = [:g,g:] );
:: deftheorem Def2 defines Contravariant FUNCTOR0:def_2_:_
for A, B being set
for f being bifunction of A,B holds
( f is Contravariant iff ex g being Function of A,B st f = ~ [:g,g:] );
theorem Th15: :: FUNCTOR0:15
for A being set
for B being non empty set
for b being Element of B
for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds
( f is Covariant & f is Contravariant )
proof
let A be set ; ::_thesis: for B being non empty set
for b being Element of B
for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds
( f is Covariant & f is Contravariant )
let B be non empty set ; ::_thesis: for b being Element of B
for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds
( f is Covariant & f is Contravariant )
let b be Element of B; ::_thesis: for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds
( f is Covariant & f is Contravariant )
let f be bifunction of A,B; ::_thesis: ( f = [:A,A:] --> [b,b] implies ( f is Covariant & f is Contravariant ) )
assume A1: f = [:A,A:] --> [b,b] ; ::_thesis: ( f is Covariant & f is Contravariant )
reconsider g = A --> b as Function of A,B ;
thus f is Covariant ::_thesis: f is Contravariant
proof
take g ; :: according to FUNCTOR0:def_1 ::_thesis: f = [:g,g:]
thus f = [:g,g:] by A1, ALTCAT_2:1; ::_thesis: verum
end;
take g ; :: according to FUNCTOR0:def_2 ::_thesis: f = ~ [:g,g:]
[:A,A:] --> [b,b] = ~ ([:A,A:] --> [b,b]) by Th5;
hence f = ~ [:g,g:] by A1, ALTCAT_2:1; ::_thesis: verum
end;
registration
let A, B be set ;
cluster Relation-like [:A,A:] -defined [:B,B:] -valued Function-like quasi_total Covariant Contravariant for Element of bool [:[:A,A:],[:B,B:]:];
existence
ex b1 being bifunction of A,B st
( b1 is Covariant & b1 is Contravariant )
proof
percases ( B = {} or B <> {} ) ;
supposeA1: B = {} ; ::_thesis: ex b1 being bifunction of A,B st
( b1 is Covariant & b1 is Contravariant )
then [:B,B:] = {} by ZFMISC_1:90;
then reconsider f = {} as bifunction of A,B by Th1;
take f ; ::_thesis: ( f is Covariant & f is Contravariant )
reconsider g = {} as Function of A,B by A1, Th1;
reconsider h = g as empty Function ;
thus f is Covariant ::_thesis: f is Contravariant
proof
take g ; :: according to FUNCTOR0:def_1 ::_thesis: f = [:g,g:]
thus f = [:h,h:]
.= [:g,g:] ; ::_thesis: verum
end;
take g ; :: according to FUNCTOR0:def_2 ::_thesis: f = ~ [:g,g:]
thus f = ~ [:h,h:]
.= ~ [:g,g:] ; ::_thesis: verum
end;
supposeA2: B <> {} ; ::_thesis: ex b1 being bifunction of A,B st
( b1 is Covariant & b1 is Contravariant )
set b = the Element of B;
set f = [:A,A:] --> [ the Element of B, the Element of B];
[ the Element of B, the Element of B] in [:B,B:] by A2, ZFMISC_1:87;
then reconsider f = [:A,A:] --> [ the Element of B, the Element of B] as bifunction of A,B by FUNCOP_1:45;
take f ; ::_thesis: ( f is Covariant & f is Contravariant )
thus ( f is Covariant & f is Contravariant ) by A2, Th15; ::_thesis: verum
end;
end;
end;
end;
theorem :: FUNCTOR0:16
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 ; ::_thesis: for f being Covariant Contravariant bifunction of A,B ex b being Element of B st f = [:A,A:] --> [b,b]
let f be Covariant Contravariant bifunction of A,B; ::_thesis: ex b being Element of B st f = [:A,A:] --> [b,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 . the Element of A; ::_thesis: f = [:A,A:] --> [b,b]
A3: dom f = [:A,A:] by FUNCT_2:def_1;
now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_
f_._z_=_[b,b]
let z be set ; ::_thesis: ( z in dom f implies f . z = [b,b] )
assume z in dom f ; ::_thesis: f . z = [b,b]
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, the Element of A] in dom [:g2,g2:] by A5, ZFMISC_1:87;
A9: dom g2 = A by FUNCT_2:def_1;
[b,(g1 . a1)] = f . ( the Element of A,a1) by A1, A6, FUNCT_3:def_8
.= [:g2,g2:] . (a1, the Element of A) by A2, A8, FUNCT_4:def_2
.= [(g2 . a1),(g2 . the Element of A)] by A9, FUNCT_3:def_8 ;
then A10: g2 . a1 = b by XTUPLE_0:1;
A11: [a2, the Element of A] in dom [:g2,g2:] by A5, A7, ZFMISC_1:87;
[b,(g1 . a2)] = f . ( the Element of A,a2) by A1, A6, FUNCT_3:def_8
.= [:g2,g2:] . (a2, the Element of A) by A2, A11, FUNCT_4:def_2
.= [(g2 . a2),(g2 . the Element of 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 ; ::_thesis: verum
end;
hence f = [:A,A:] --> [b,b] by A3, FUNCOP_1:11; ::_thesis: verum
end;
begin
definition
let I1, I2 be set ;
let f be Function of I1,I2;
let A be ManySortedSet of I1;
let B be ManySortedSet of I2;
mode MSUnTrans of f,A,B -> ManySortedSet of I1 means :Def3: :: FUNCTOR0:def 3
ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & it is ManySortedFunction of A,B9 * f9 ) if I2 <> {}
otherwise it = [[0]] I1;
existence
( ( I2 <> {} implies ex b1 being ManySortedSet of I1 ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & b1 is ManySortedFunction of A,B9 * f9 ) ) & ( not I2 <> {} implies ex b1 being ManySortedSet of I1 st b1 = [[0]] I1 ) )
proof
hereby ::_thesis: ( not I2 <> {} implies ex b1 being ManySortedSet of I1 st b1 = [[0]] I1 )
assume I2 <> {} ; ::_thesis: ex IT9 being ManySortedSet of I1 ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )
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 = the ManySortedFunction of A,B9 * f9 as ManySortedSet of I1 ;
take IT9 = IT9; ::_thesis: ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )
take I29 = I29; ::_thesis: ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )
reconsider f9 = f as Function of I1,I29 ;
reconsider B9 = B as ManySortedSet of I29 ;
take B9 = B9; ::_thesis: ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )
take f9 = f9; ::_thesis: ( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )
thus ( f = f9 & B = B9 ) ; ::_thesis: IT9 is ManySortedFunction of A,B9 * f9
thus IT9 is ManySortedFunction of A,B9 * f9 ; ::_thesis: verum
end;
thus ( not I2 <> {} implies ex b1 being ManySortedSet of I1 st b1 = [[0]] I1 ) ; ::_thesis: verum
end;
consistency
for b1 being ManySortedSet of I1 holds verum ;
end;
:: deftheorem Def3 defines MSUnTrans FUNCTOR0:def_3_:_
for I1, I2 being set
for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for b6 being ManySortedSet of I1 holds
( ( I2 <> {} implies ( b6 is MSUnTrans of f,A,B iff ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & b6 is ManySortedFunction of A,B9 * f9 ) ) ) & ( not I2 <> {} implies ( b6 is MSUnTrans of f,A,B iff b6 = [[0]] I1 ) ) );
definition
let I1 be set ;
let I2 be non empty set ;
let f be Function of I1,I2;
let A be ManySortedSet of I1;
let B be ManySortedSet of I2;
redefine mode MSUnTrans of f,A,B means :Def4: :: FUNCTOR0:def 4
it is ManySortedFunction of A,B * f;
compatibility
for b1 being ManySortedSet of I1 holds
( b1 is MSUnTrans of f,A,B iff b1 is ManySortedFunction of A,B * f )
proof
let M be ManySortedSet of I1; ::_thesis: ( M is MSUnTrans of f,A,B iff M is ManySortedFunction of A,B * f )
hereby ::_thesis: ( M is ManySortedFunction of A,B * f implies M is MSUnTrans of f,A,B )
assume M is MSUnTrans of f,A,B ; ::_thesis: M is ManySortedFunction of A,B * f
then ex I29 being non empty set ex B9 being ManySortedSet of I29 ex 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 ; ::_thesis: verum
end;
thus ( M is ManySortedFunction of A,B * f implies M is MSUnTrans of f,A,B ) by Def3; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines MSUnTrans FUNCTOR0:def_4_:_
for I1 being set
for I2 being non empty set
for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for b6 being ManySortedSet of I1 holds
( b6 is MSUnTrans of f,A,B iff b6 is ManySortedFunction of A,B * f );
registration
let I1, I2 be set ;
let f be Function of I1,I2;
let A be ManySortedSet of I1;
let B be ManySortedSet of I2;
cluster -> Function-yielding for MSUnTrans of f,A,B;
coherence
for b1 being MSUnTrans of f,A,B holds b1 is Function-yielding
proof
let M be MSUnTrans of f,A,B; ::_thesis: M is Function-yielding
percases ( I2 <> {} or I2 = {} ) ;
suppose I2 <> {} ; ::_thesis: M is Function-yielding
then ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & M is ManySortedFunction of A,B9 * f9 ) by Def3;
hence M is Function-yielding ; ::_thesis: verum
end;
suppose I2 = {} ; ::_thesis: M is Function-yielding
then M = [[0]] I1 by Def3;
hence M is Function-yielding ; ::_thesis: verum
end;
end;
end;
end;
theorem Th17: :: FUNCTOR0:17
for I1 being set
for I2, I3 being non empty set
for f being Function of I1,I2
for g being Function of I2,I3
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C
proof
let I1 be set ; ::_thesis: for I2, I3 being non empty set
for f being Function of I1,I2
for g being Function of I2,I3
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C
let I2, I3 be non empty set ; ::_thesis: for f being Function of I1,I2
for g being Function of I2,I3
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C
let f be Function of I1,I2; ::_thesis: for g being Function of I2,I3
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C
let g be Function of I2,I3; ::_thesis: for B being ManySortedSet of I2
for C being ManySortedSet of I3
for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C
let B be ManySortedSet of I2; ::_thesis: for C being ManySortedSet of I3
for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C
let C be ManySortedSet of I3; ::_thesis: for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C
let G be MSUnTrans of g,B,C; ::_thesis: G * f is MSUnTrans of g * f,B * f,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; :: according to FUNCTOR0:def_4 ::_thesis: verum
end;
definition
let I1 be set ;
let I2 be non empty set ;
let f be Function of I1,I2;
let A be ManySortedSet of [:I1,I1:];
let B be ManySortedSet of [:I2,I2:];
let F be MSUnTrans of [:f,f:],A,B;
:: original: ~
redefine func ~ F -> MSUnTrans of [:f,f:], ~ A, ~ B;
coherence
~ F is MSUnTrans of [:f,f:], ~ A, ~ B
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; ::_thesis: verum
end;
end;
theorem Th18: :: FUNCTOR0:18
for I1, I2 being non empty set
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for o being Element of I2 st B . o <> {} holds
for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
proof
let I1, I2 be non empty set ; ::_thesis: for A being ManySortedSet of I1
for B being ManySortedSet of I2
for o being Element of I2 st B . o <> {} holds
for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
let A be ManySortedSet of I1; ::_thesis: for B being ManySortedSet of I2
for o being Element of I2 st B . o <> {} holds
for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
let B be ManySortedSet of I2; ::_thesis: for o being Element of I2 st B . o <> {} holds
for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
let o be Element of I2; ::_thesis: ( B . o <> {} implies for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B )
assume A1: B . o <> {} ; ::_thesis: for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
let m be Element of B . o; ::_thesis: for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
let f be Function of I1,I2; ::_thesis: ( f = I1 --> o implies { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B )
assume A2: f = I1 --> o ; ::_thesis: { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
defpred S1[ set ] means verum;
deffunc H1( set ) -> Element of bool [:(A . $1),{m}:] = (A . $1) --> m;
reconsider Xm = { [o9,H1(o9)] where o9 is Element of I1 : S1[o9] } as Function from ALTCAT_2:sch_1();
A3: Xm = { [o9,H1(o9)] where o9 is Element of I1 : S1[o9] } ;
dom Xm = { o9 where o9 is Element of I1 : S1[o9] } from ALTCAT_2:sch_2(A3)
.= I1 by DOMAIN_1:18 ;
then reconsider Xm = Xm as ManySortedSet of I1 by PARTFUN1:def_2, RELAT_1:def_18;
deffunc H2( set ) -> Element of bool [:(A . $1),{m}:] = (A . $1) --> m;
A4: Xm = { [o9,H2(o9)] where o9 is Element of I1 : S1[o9] } ;
now__::_thesis:_for_i_being_set_st_i_in_I1_holds_
Xm_._i_is_Function_of_(A_._i),((B_*_f)_._i)
let i be set ; ::_thesis: ( i in I1 implies Xm . i is Function of (A . i),((B * f) . i) )
assume A5: i in I1 ; ::_thesis: Xm . i is Function of (A . i),((B * f) . i)
then reconsider o9 = i as Element of I1 ;
A6: S1[o9] ;
A7: i in dom f by A2, A5, FUNCOP_1:13;
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 = H2(o9) from ALTCAT_2:sch_3(A4, A6);
hence Xm . i is Function of (A . i),((B * f) . i) by A8, FUNCOP_1:45; ::_thesis: verum
end;
then Xm is ManySortedFunction of A,B * f by PBOOLE:def_15;
hence { [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B by Def4; ::_thesis: verum
end;
theorem Th19: :: FUNCTOR0:19
for I1 being set
for I2, I3 being non empty set
for f being Function of I1,I2
for g being Function of I2,I3
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
proof
let I1 be set ; ::_thesis: for I2, I3 being non empty set
for f being Function of I1,I2
for g being Function of I2,I3
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let I2, I3 be non empty set ; ::_thesis: for f being Function of I1,I2
for g being Function of I2,I3
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let f be Function of I1,I2; ::_thesis: for g being Function of I2,I3
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let g be Function of I2,I3; ::_thesis: for A being ManySortedSet of I1
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let A be ManySortedSet of I1; ::_thesis: for B being ManySortedSet of I2
for C being ManySortedSet of I3
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let B be ManySortedSet of I2; ::_thesis: for C being ManySortedSet of I3
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let C be ManySortedSet of I3; ::_thesis: for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let F be MSUnTrans of f,A,B; ::_thesis: for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
let G be MSUnTrans of g * f,B * f,C; ::_thesis: ( ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) implies G ** F is MSUnTrans of g * f,A,C )
assume A1: for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ; ::_thesis: G ** F is MSUnTrans of g * f,A,C
reconsider G = G as ManySortedFunction of B * f,C * (g * f) by Def4;
reconsider F = 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 set ; :: according to PBOOLE:def_15 ::_thesis: ( not ii in I1 or GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):] )
assume A5: ii in I1 ; ::_thesis: GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):]
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;
( not (B * f) . ii = {} or 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 GF . ii is Element of bool [:(A . ii),((C * (g * f)) . ii):] by A4, A5, PBOOLE:def_19; ::_thesis: verum
end;
hence G ** F is MSUnTrans of g * f,A,C by Def4; ::_thesis: verum
end;
begin
definition
let C1, C2 be 1-sorted ;
attrc3 is strict ;
struct BimapStr over C1,C2 -> ;
aggrBimapStr(# ObjectMap #) -> BimapStr over C1,C2;
sel ObjectMap c3 -> 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;
funcF . o -> object of C2 equals :: FUNCTOR0:def 5
( the ObjectMap of F . (o,o)) `1 ;
coherence
( the ObjectMap of F . (o,o)) `1 is object of C2 by MCART_1:10;
end;
:: deftheorem defines . FUNCTOR0:def_5_:_
for C1, C2 being non empty AltGraph
for F being BimapStr over C1,C2
for o being object of C1 holds F . o = ( the ObjectMap of F . (o,o)) `1 ;
definition
let A, B be 1-sorted ;
let F be BimapStr over A,B;
attrF is one-to-one means :Def6: :: FUNCTOR0:def 6
the ObjectMap of F is one-to-one ;
attrF is onto means :Def7: :: FUNCTOR0:def 7
the ObjectMap of F is onto ;
attrF is reflexive means :Def8: :: FUNCTOR0:def 8
the ObjectMap of F .: (id the carrier of A) c= id the carrier of B;
attrF is coreflexive means :Def9: :: FUNCTOR0:def 9
id the carrier of B c= the ObjectMap of F .: (id the carrier of A);
end;
:: deftheorem Def6 defines one-to-one FUNCTOR0:def_6_:_
for A, B being 1-sorted
for F being BimapStr over A,B holds
( F is one-to-one iff the ObjectMap of F is one-to-one );
:: deftheorem Def7 defines onto FUNCTOR0:def_7_:_
for A, B being 1-sorted
for F being BimapStr over A,B holds
( F is onto iff the ObjectMap of F is onto );
:: deftheorem Def8 defines reflexive FUNCTOR0:def_8_:_
for A, B being 1-sorted
for F being BimapStr over A,B holds
( F is reflexive iff the ObjectMap of F .: (id the carrier of A) c= id the carrier of B );
:: deftheorem Def9 defines coreflexive FUNCTOR0:def_9_:_
for A, B being 1-sorted
for F being BimapStr over A,B holds
( F is coreflexive iff id the carrier of B c= the ObjectMap of F .: (id the carrier of A) );
definition
let A, B be non empty AltGraph ;
let F be BimapStr over A,B;
redefine attr F is reflexive means :Def10: :: FUNCTOR0:def 10
for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)];
compatibility
( F is reflexive iff for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] )
proof
hereby ::_thesis: ( ( for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] ) implies F is reflexive )
assume F is reflexive ; ::_thesis: for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)]
then A1: the ObjectMap of F .: (id the carrier of A) c= id the carrier of B by Def8;
let o be object of A; ::_thesis: the ObjectMap of F . (o,o) = [(F . o),(F . o)]
[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 set such that
A3: the ObjectMap of F . (o,o) = [p,p9] by RELAT_1:def_1;
F . o = p by A3, MCART_1:7;
hence the ObjectMap of F . (o,o) = [(F . o),(F . o)] by A1, A2, A3, RELAT_1:def_10; ::_thesis: verum
end;
assume A4: for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] ; ::_thesis: F is reflexive
let x be set ; :: according to TARSKI:def_3,FUNCTOR0:def_8 ::_thesis: ( not x in the ObjectMap of F .: (id the carrier of A) or x in id the carrier of B )
assume x in the ObjectMap of F .: (id the carrier of A) ; ::_thesis: x in id the carrier of B
then consider y being set 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 = 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 x in id the carrier of B by RELAT_1:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines reflexive FUNCTOR0:def_10_:_
for A, B being non empty AltGraph
for F being BimapStr over A,B holds
( F is reflexive iff for o being object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] );
theorem Th20: :: FUNCTOR0:20
for A, B being non empty reflexive AltGraph
for F being BimapStr over A,B st F is coreflexive holds
for o being object of B ex o9 being object of A st F . o9 = o
proof
let A, B be non empty reflexive AltGraph ; ::_thesis: for F being BimapStr over A,B st F is coreflexive holds
for o being object of B ex o9 being object of A st F . o9 = o
let F be BimapStr over A,B; ::_thesis: ( F is coreflexive implies for o being object of B ex o9 being object of A st F . o9 = o )
assume F is coreflexive ; ::_thesis: for o being object of B ex o9 being object of A st F . o9 = o
then A1: id the carrier of B c= the ObjectMap of F .: (id the carrier of A) by Def9;
let o be object of B; ::_thesis: ex o9 being object of A st F . o9 = o
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 set such that
A4: pp = [p,p9] by RELAT_1:def_1;
A5: p = p9 by A2, A4, RELAT_1:def_10;
reconsider p = p as object of A by A2, A4, RELAT_1:def_10;
take p ; ::_thesis: F . p = o
thus F . p = o by A3, A4, A5, MCART_1:7; ::_thesis: verum
end;
definition
let C1, C2 be non empty AltGraph ;
let F be BimapStr over C1,C2;
attrF is feasible means :Def11: :: FUNCTOR0:def 11
for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} ;
end;
:: deftheorem Def11 defines feasible FUNCTOR0:def_11_:_
for C1, C2 being non empty AltGraph
for F being BimapStr over C1,C2 holds
( F is feasible iff for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} );
definition
let C1, C2 be AltGraph ;
attrc3 is strict ;
struct FunctorStr over C1,C2 -> BimapStr over C1,C2;
aggrFunctorStr(# ObjectMap, MorphMap #) -> FunctorStr over C1,C2;
sel MorphMap c3 -> MSUnTrans of the ObjectMap of c3, the Arrows of C1, the Arrows of C2;
end;
definition
let C1, C2 be 1-sorted ;
let IT be BimapStr over C1,C2;
attrIT is Covariant means :Def12: :: FUNCTOR0:def 12
the ObjectMap of IT is Covariant ;
attrIT is Contravariant means :Def13: :: FUNCTOR0:def 13
the ObjectMap of IT is Contravariant ;
end;
:: deftheorem Def12 defines Covariant FUNCTOR0:def_12_:_
for C1, C2 being 1-sorted
for IT being BimapStr over C1,C2 holds
( IT is Covariant iff the ObjectMap of IT is Covariant );
:: deftheorem Def13 defines Contravariant FUNCTOR0:def_13_:_
for C1, C2 being 1-sorted
for IT being BimapStr over C1,C2 holds
( IT is Contravariant iff the ObjectMap of IT is Contravariant );
registration
let C1, C2 be AltGraph ;
cluster Covariant for FunctorStr over C1,C2;
existence
ex b1 being FunctorStr over C1,C2 st b1 is Covariant
proof
set f = the Covariant bifunction of the carrier of C1, the carrier of C2;
set M = the MSUnTrans of the Covariant bifunction of the carrier of C1, the carrier of C2, the Arrows of C1, the Arrows of C2;
take F = FunctorStr(# the Covariant bifunction of the carrier of C1, the carrier of C2, the MSUnTrans of the Covariant bifunction of the carrier of C1, the carrier of C2, the Arrows of C1, the Arrows of C2 #); ::_thesis: F is Covariant
thus the ObjectMap of F is Covariant ; :: according to FUNCTOR0:def_12 ::_thesis: verum
end;
cluster Contravariant for FunctorStr over C1,C2;
existence
ex b1 being FunctorStr over C1,C2 st b1 is Contravariant
proof
set f = the Contravariant bifunction of the carrier of C1, the carrier of C2;
set M = the MSUnTrans of the Contravariant bifunction of the carrier of C1, the carrier of C2, the Arrows of C1, the Arrows of C2;
take F = FunctorStr(# the Contravariant bifunction of the carrier of C1, the carrier of C2, the MSUnTrans of the Contravariant bifunction of the carrier of C1, the carrier of C2, the Arrows of C1, the Arrows of C2 #); ::_thesis: F is Contravariant
thus the ObjectMap of F is Contravariant ; :: according to FUNCTOR0:def_13 ::_thesis: verum
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 :: FUNCTOR0:def 14
the MorphMap of F . (o1,o2);
correctness
coherence
the MorphMap of F . (o1,o2) is set ;
;
end;
:: deftheorem defines Morph-Map FUNCTOR0:def_14_:_
for C1, C2 being AltGraph
for F being FunctorStr over C1,C2
for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) = the MorphMap of F . (o1,o2);
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
( Morph-Map (F,o1,o2) is Relation-like & Morph-Map (F,o1,o2) is Function-like ) ;
end;
definition
let C1, C2 be non empty AltGraph ;
let F be Covariant FunctorStr over C1,C2;
let o1, o2 be object of C1;
:: original: Morph-Map
redefine func Morph-Map (F,o1,o2) -> Function of <^o1,o2^>,<^(F . o1),(F . o2)^>;
coherence
Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o1),(F . o2)^>
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:] by Def1;
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 Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o1),(F . o2)^> by A3, A4, A5, PBOOLE:def_15; ::_thesis: verum
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;
assume that
A1: <^o1,o2^> <> {} and
A2: <^(F . o1),(F . o2)^> <> {} ;
let m be Morphism of o1,o2;
funcF . m -> Morphism of (F . o1),(F . o2) equals :Def15: :: FUNCTOR0:def 15
(Morph-Map (F,o1,o2)) . m;
coherence
(Morph-Map (F,o1,o2)) . m is Morphism of (F . o1),(F . o2)
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 = m as Element of A ;
M . m is Element of B ;
hence (Morph-Map (F,o1,o2)) . m is Morphism of (F . o1),(F . o2) ; ::_thesis: verum
end;
end;
:: deftheorem Def15 defines . FUNCTOR0:def_15_:_
for C1, C2 being non empty AltGraph
for F being Covariant FunctorStr over C1,C2
for o1, o2 being object of C1 st <^o1,o2^> <> {} & <^(F . o1),(F . o2)^> <> {} holds
for m being Morphism of o1,o2 holds F . m = (Morph-Map (F,o1,o2)) . m;
definition
let C1, C2 be non empty AltGraph ;
let F be Contravariant FunctorStr over C1,C2;
let o1, o2 be object of C1;
:: original: Morph-Map
redefine func Morph-Map (F,o1,o2) -> Function of <^o1,o2^>,<^(F . o2),(F . o1)^>;
coherence
Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o2),(F . o1)^>
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:] by Def2;
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 Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o2),(F . o1)^> by A3, A4, A5, PBOOLE:def_15; ::_thesis: verum
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;
assume that
A1: <^o1,o2^> <> {} and
A2: <^(F . o2),(F . o1)^> <> {} ;
let m be Morphism of o1,o2;
funcF . m -> Morphism of (F . o2),(F . o1) equals :Def16: :: FUNCTOR0:def 16
(Morph-Map (F,o1,o2)) . m;
coherence
(Morph-Map (F,o1,o2)) . m is Morphism of (F . o2),(F . o1)
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 = m as Element of A ;
M . m is Element of B ;
hence (Morph-Map (F,o1,o2)) . m is Morphism of (F . o2),(F . o1) ; ::_thesis: verum
end;
end;
:: deftheorem Def16 defines . FUNCTOR0:def_16_:_
for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr over C1,C2
for o1, o2 being object of C1 st <^o1,o2^> <> {} & <^(F . o2),(F . o1)^> <> {} holds
for m being Morphism of o1,o2 holds F . m = (Morph-Map (F,o1,o2)) . m;
definition
let C1, C2 be non empty AltGraph ;
let o be object of C2;
assume B1: <^o,o^> <> {} ;
let m be Morphism of o,o;
funcC1 --> m -> strict FunctorStr over C1,C2 means :Def17: :: FUNCTOR0:def 17
( the ObjectMap of it = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of it = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } );
existence
ex b1 being strict FunctorStr over C1,C2 st
( the ObjectMap of b1 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b1 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } )
proof
set I1 = [: the carrier of C1, the carrier of C1:];
set I2 = [: the carrier of C2, the carrier of C2:];
set A = the Arrows of C1;
set B = the Arrows of C2;
reconsider oo = [o,o] as Element of [: the carrier of C2, the carrier of C2:] by ZFMISC_1:87;
the Arrows of C2 . oo = the Arrows of C2 . (o,o)
.= <^o,o^> by ALTCAT_1:def_1 ;
then reconsider m = m as Element of the Arrows of C2 . oo ;
reconsider f = [: the carrier of C1, the carrier of C1:] --> oo as Function of [: the carrier of C1, the carrier of C1:],[: the carrier of C2, the carrier of C2:] ;
reconsider f = f as bifunction of the carrier of C1, the carrier of C2 ;
set M = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ;
A1: { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } = { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum }
proof
thus { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } c= { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } :: according to XBOOLE_0:def_10 ::_thesis: { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } c= { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } or x in { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } )
assume x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ; ::_thesis: x in { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum }
then consider o3, o4 being object of C1 such that
A2: x = [[o3,o4],(<^o3,o4^> --> m)] ;
reconsider oo = [o3,o4] as Element of [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87;
x = [oo,(( the Arrows of C1 . (o3,o4)) --> m)] by A2, ALTCAT_1:def_1
.= [oo,(( the Arrows of C1 . oo) --> m)] ;
hence x in { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } or x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } )
assume x in { [o9,(( the Arrows of C1 . o9) --> m)] where o9 is Element of [: the carrier of C1, the carrier of C1:] : verum } ; ::_thesis: x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum }
then consider o9 being Element of [: the carrier of C1, the carrier of C1:] such that
A3: x = [o9,(( the Arrows of C1 . o9) --> m)] ;
reconsider o1 = o9 `1 , o2 = o9 `2 as Element of C1 by MCART_1:10;
reconsider o1 = o1, o2 = o2 as object of C1 ;
o9 = [o1,o2] by MCART_1:21;
then x = [[o1,o2],(( the Arrows of C1 . (o1,o2)) --> m)] by A3
.= [[o1,o2],(<^o1,o2^> --> m)] by ALTCAT_1:def_1 ;
hence x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ; ::_thesis: verum
end;
the Arrows of C2 . (o,o) <> {} by B1, ALTCAT_1:def_1;
then reconsider M = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } as MSUnTrans of f, the Arrows of C1, the Arrows of C2 by A1, Th18;
take FunctorStr(# f,M #) ; ::_thesis: ( the ObjectMap of FunctorStr(# f,M #) = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of FunctorStr(# f,M #) = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } )
thus ( the ObjectMap of FunctorStr(# f,M #) = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of FunctorStr(# f,M #) = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict FunctorStr over C1,C2 st the ObjectMap of b1 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b1 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } & the ObjectMap of b2 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b2 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } holds
b1 = b2 ;
end;
:: deftheorem Def17 defines --> FUNCTOR0:def_17_:_
for C1, C2 being non empty AltGraph
for o being object of C2 st <^o,o^> <> {} holds
for m being Morphism of o,o
for b5 being strict FunctorStr over C1,C2 holds
( b5 = C1 --> m iff ( the ObjectMap of b5 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b5 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ) );
theorem Th21: :: FUNCTOR0:21
for C1, C2 being non empty AltGraph
for o2 being object of C2 st <^o2,o2^> <> {} holds
for m being Morphism of o2,o2
for o1 being object of C1 holds (C1 --> m) . o1 = o2
proof
let C1, C2 be non empty AltGraph ; ::_thesis: for o2 being object of C2 st <^o2,o2^> <> {} holds
for m being Morphism of o2,o2
for o1 being object of C1 holds (C1 --> m) . o1 = o2
let o2 be object of C2; ::_thesis: ( <^o2,o2^> <> {} implies for m being Morphism of o2,o2
for o1 being object of C1 holds (C1 --> m) . o1 = o2 )
assume A1: <^o2,o2^> <> {} ; ::_thesis: for m being Morphism of o2,o2
for o1 being object of C1 holds (C1 --> m) . o1 = o2
let m be Morphism of o2,o2; ::_thesis: for o1 being object of C1 holds (C1 --> m) . o1 = o2
let o1 be object of C1; ::_thesis: (C1 --> m) . o1 = o2
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 ; ::_thesis: verum
end;
registration
let C1 be non empty AltGraph ;
let C2 be non empty reflexive AltGraph ;
let o be object of C2;
let m be Morphism of o,o;
clusterC1 --> m -> feasible strict Covariant Contravariant ;
coherence
( C1 --> m is Covariant & C1 --> m is Contravariant & C1 --> m is feasible )
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 & the ObjectMap of (C1 --> m) is Contravariant ) by Th15; :: according to FUNCTOR0:def_12,FUNCTOR0:def_13 ::_thesis: C1 --> m is feasible
let o1, o2 be object of C1; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of C2 . ( the ObjectMap of (C1 --> m) . (o1,o2)) <> {} )
assume <^o1,o2^> <> {} ; ::_thesis: the Arrows of C2 . ( the ObjectMap of (C1 --> m) . (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 the Arrows of C2 . ( the ObjectMap of (C1 --> m) . (o1,o2)) <> {} by ALTCAT_2:def_6; ::_thesis: verum
end;
end;
registration
let C1 be non empty AltGraph ;
let C2 be non empty reflexive AltGraph ;
cluster feasible Covariant Contravariant for FunctorStr over C1,C2;
existence
ex b1 being FunctorStr over C1,C2 st
( b1 is feasible & b1 is Covariant & b1 is Contravariant )
proof
set o = the object of C2;
set m = the Morphism of the object of C2, the object of C2;
take C1 --> the Morphism of the object of C2, the object of C2 ; ::_thesis: ( C1 --> the Morphism of the object of C2, the object of C2 is feasible & C1 --> the Morphism of the object of C2, the object of C2 is Covariant & C1 --> the Morphism of the object of C2, the object of C2 is Contravariant )
thus ( C1 --> the Morphism of the object of C2, the object of C2 is feasible & C1 --> the Morphism of the object of C2, the object of C2 is Covariant & C1 --> the Morphism of the object of C2, the object of C2 is Contravariant ) ; ::_thesis: verum
end;
end;
theorem Th22: :: FUNCTOR0:22
for C1, C2 being non empty AltGraph
for F being Covariant FunctorStr over C1,C2
for 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 ; ::_thesis: for F being Covariant FunctorStr over C1,C2
for o1, o2 being object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)]
let F be Covariant FunctorStr over C1,C2; ::_thesis: for o1, o2 being object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)]
let o1, o2 be object of C1; ::_thesis: the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)]
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:] by Def1;
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 the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)] by A1, A2, FUNCT_3:75; ::_thesis: verum
end;
definition
let C1, C2 be non empty AltGraph ;
let F be Covariant FunctorStr over C1,C2;
redefine attr F is feasible means :Def18: :: FUNCTOR0:def 18
for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {} ;
compatibility
( F is feasible iff for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {} )
proof
hereby ::_thesis: ( ( for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {} ) implies F is feasible )
assume A1: F is feasible ; ::_thesis: for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {}
let o1, o2 be object of C1; ::_thesis: ( <^o1,o2^> <> {} implies <^(F . o1),(F . o2)^> <> {} )
assume A2: <^o1,o2^> <> {} ; ::_thesis: <^(F . o1),(F . 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, Def11; ::_thesis: verum
end;
assume A3: for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {} ; ::_thesis: F is feasible
let o1, o2 be object of C1; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} )
assume A4: <^o1,o2^> <> {} ; ::_thesis: the Arrows of C2 . ( the ObjectMap of F . (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 the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} by A3, A4; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines feasible FUNCTOR0:def_18_:_
for C1, C2 being non empty AltGraph
for F being Covariant FunctorStr over C1,C2 holds
( F is feasible iff for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {} );
theorem Th23: :: FUNCTOR0:23
for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr over C1,C2
for 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 ; ::_thesis: for F being Contravariant FunctorStr over C1,C2
for o1, o2 being object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)]
let F be Contravariant FunctorStr over C1,C2; ::_thesis: for o1, o2 being object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)]
let o1, o2 be object of C1; ::_thesis: the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)]
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:] by Def2;
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 ;
::_thesis: verum
end;
definition
let C1, C2 be non empty AltGraph ;
let F be Contravariant FunctorStr over C1,C2;
redefine attr F is feasible means :Def19: :: FUNCTOR0:def 19
for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {} ;
compatibility
( F is feasible iff for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {} )
proof
hereby ::_thesis: ( ( for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {} ) implies F is feasible )
assume A1: F is feasible ; ::_thesis: for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {}
let o1, o2 be object of C1; ::_thesis: ( <^o1,o2^> <> {} implies <^(F . o2),(F . o1)^> <> {} )
assume A2: <^o1,o2^> <> {} ; ::_thesis: <^(F . o2),(F . o1)^> <> {}
<^(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, Def11; ::_thesis: verum
end;
assume A3: for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {} ; ::_thesis: F is feasible
let o1, o2 be object of C1; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} )
assume A4: <^o1,o2^> <> {} ; ::_thesis: the Arrows of C2 . ( the ObjectMap of F . (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 the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} by A3, A4; ::_thesis: verum
end;
end;
:: deftheorem Def19 defines feasible FUNCTOR0:def_19_:_
for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr over C1,C2 holds
( F is feasible iff for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {} );
registration
let C1, C2 be AltGraph ;
let F be FunctorStr over C1,C2;
cluster the MorphMap of F -> Function-yielding ;
coherence
the MorphMap of F is Function-yielding ;
end;
registration
cluster non empty reflexive for AltCatStr ;
existence
ex b1 being AltCatStr st
( not b1 is empty & b1 is reflexive )
proof
set C = the category;
take the category ; ::_thesis: ( not the category is empty & the category is reflexive )
thus ( not the category is empty & the category is reflexive ) ; ::_thesis: verum
end;
end;
definition
let C1, C2 be non empty with_units AltCatStr ;
let F be FunctorStr over C1,C2;
attrF is id-preserving means :Def20: :: FUNCTOR0:def 20
for o being object of C1 holds (Morph-Map (F,o,o)) . (idm o) = idm (F . o);
end;
:: deftheorem Def20 defines id-preserving FUNCTOR0:def_20_:_
for C1, C2 being non empty with_units AltCatStr
for F being FunctorStr over C1,C2 holds
( F is id-preserving iff for o being object of C1 holds (Morph-Map (F,o,o)) . (idm o) = idm (F . o) );
theorem Th24: :: FUNCTOR0:24
for C1, C2 being non empty AltGraph
for o2 being object of C2 st <^o2,o2^> <> {} holds
for m being Morphism of o2,o2
for o, o9 being object of C1
for 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 ; ::_thesis: for o2 being object of C2 st <^o2,o2^> <> {} holds
for m being Morphism of o2,o2
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(Morph-Map ((C1 --> m),o,o9)) . f = m
let o2 be object of C2; ::_thesis: ( <^o2,o2^> <> {} implies for m being Morphism of o2,o2
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(Morph-Map ((C1 --> m),o,o9)) . f = m )
assume A1: <^o2,o2^> <> {} ; ::_thesis: for m being Morphism of o2,o2
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(Morph-Map ((C1 --> m),o,o9)) . f = m
let m be Morphism of o2,o2; ::_thesis: for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(Morph-Map ((C1 --> m),o,o9)) . f = m
let o, o9 be object of C1; ::_thesis: for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(Morph-Map ((C1 --> m),o,o9)) . f = m
let f be Morphism of o,o9; ::_thesis: ( <^o,o9^> <> {} implies (Morph-Map ((C1 --> m),o,o9)) . f = m )
assume A2: <^o,o9^> <> {} ; ::_thesis: (Morph-Map ((C1 --> m),o,o9)) . f = m
set X = { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } ;
set Y = { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } ;
A3: { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } c= { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } or e in { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } )
assume e in { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } ; ::_thesis: e in { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum }
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 e in { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } ; ::_thesis: verum
end;
A5: { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } c= { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } or e in { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } )
assume e in { [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] where o1, o19 is Element of C1 : verum } ; ::_thesis: e in { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum }
then consider o1, o19 being Element of C1 such that
A6: e = [[o1,o19],(( the Arrows of C1 . (o1,o19)) --> m)] ;
reconsider o1 = o1, o19 = o19 as object of C1 ;
e = [[o1,o19],(<^o1,o19^> --> m)] by A6, ALTCAT_1:def_1;
hence e in { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } ; ::_thesis: verum
end;
defpred S1[ set , set ] means verum;
deffunc H1( Element of C1, Element of C1) -> Element of bool [:( the Arrows of C1 . ($1,$2)),{m}:] = ( the Arrows of C1 . ($1,$2)) --> m;
the MorphMap of (C1 --> m) = { [[o1,o19],(<^o1,o19^> --> m)] where o1, o19 is object of C1 : verum } by A1, Def17;
then A7: the MorphMap of (C1 --> m) = { [[o1,o19],H1(o1,o19)] where o1, o19 is Element of C1 : S1[o1,o19] } by A3, A5, XBOOLE_0:def_10;
A8: S1[o,o9] ;
Morph-Map ((C1 --> m),o,o9) = the MorphMap of (C1 --> m) . (o,o9)
.= H1(o,o9) from FUNCTOR0:sch_1(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 ;
::_thesis: verum
end;
registration
cluster non empty with_units -> non empty reflexive for AltCatStr ;
coherence
for b1 being non empty AltCatStr st b1 is with_units holds
b1 is reflexive ;
end;
registration
let C1, C2 be non empty with_units AltCatStr ;
let o2 be object of C2;
clusterC1 --> (idm o2) -> strict id-preserving ;
coherence
C1 --> (idm o2) is id-preserving
proof
let o1 be object of C1; :: according to FUNCTOR0:def_20 ::_thesis: (Morph-Map ((C1 --> (idm o2)),o1,o1)) . (idm o1) = idm ((C1 --> (idm o2)) . o1)
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 ;
::_thesis: verum
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;
clusterC1 --> m -> reflexive strict ;
coherence
C1 --> m is reflexive
proof
let o be object of C1; :: according to FUNCTOR0:def_10 ::_thesis: the ObjectMap of (C1 --> m) . (o,o) = [((C1 --> m) . o),((C1 --> m) . o)]
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 ;
then (C1 --> m) . o = o2 by MCART_1:7;
hence the ObjectMap of (C1 --> m) . (o,o) = [((C1 --> m) . o),((C1 --> m) . o)] by A2; ::_thesis: verum
end;
end;
registration
let C1 be non empty AltGraph ;
let C2 be non empty reflexive AltGraph ;
cluster reflexive feasible for FunctorStr over C1,C2;
existence
ex b1 being FunctorStr over C1,C2 st
( b1 is feasible & b1 is reflexive )
proof
set o2 = the object of C2;
set m = the Morphism of the object of C2, the object of C2;
take C1 --> the Morphism of the object of C2, the object of C2 ; ::_thesis: ( C1 --> the Morphism of the object of C2, the object of C2 is feasible & C1 --> the Morphism of the object of C2, the object of C2 is reflexive )
thus ( C1 --> the Morphism of the object of C2, the object of C2 is feasible & C1 --> the Morphism of the object of C2, the object of C2 is reflexive ) ; ::_thesis: verum
end;
end;
registration
let C1, C2 be non empty with_units AltCatStr ;
cluster reflexive feasible strict id-preserving for FunctorStr over C1,C2;
existence
ex b1 being FunctorStr over C1,C2 st
( b1 is id-preserving & b1 is feasible & b1 is reflexive & b1 is strict )
proof
set o2 = the object of C2;
take C1 --> (idm the object of C2) ; ::_thesis: ( C1 --> (idm the object of C2) is id-preserving & C1 --> (idm the object of C2) is feasible & C1 --> (idm the object of C2) is reflexive & C1 --> (idm the object of C2) is strict )
thus ( C1 --> (idm the object of C2) is id-preserving & C1 --> (idm the object of C2) is feasible & C1 --> (idm the object of C2) is reflexive & C1 --> (idm the object of C2) is strict ) ; ::_thesis: verum
end;
end;
definition
let C1, C2 be non empty AltCatStr ;
let F be FunctorStr over C1,C2;
attrF is comp-preserving means :Def21: :: FUNCTOR0:def 21
for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex 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;
:: deftheorem Def21 defines comp-preserving FUNCTOR0:def_21_:_
for C1, C2 being non empty AltCatStr
for F being FunctorStr over C1,C2 holds
( F is comp-preserving iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex 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 ) );
definition
let C1, C2 be non empty AltCatStr ;
let F be FunctorStr over C1,C2;
attrF is comp-reversing means :Def22: :: FUNCTOR0:def 22
for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex 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;
:: deftheorem Def22 defines comp-reversing FUNCTOR0:def_22_:_
for C1, C2 being non empty AltCatStr
for F being FunctorStr over C1,C2 holds
( F is comp-reversing iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex 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 ) );
definition
let C1 be non empty transitive AltCatStr ;
let C2 be non empty reflexive AltCatStr ;
let F be feasible Covariant FunctorStr over C1,C2;
redefine attr F is comp-preserving means :: FUNCTOR0:def 23
for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f);
compatibility
( F is comp-preserving iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) )
proof
hereby ::_thesis: ( ( for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) ) implies F is comp-preserving )
assume A1: F is comp-preserving ; ::_thesis: for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f)
let o1, o2, o3 be object of C1; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) )
assume that
A2: <^o1,o2^> <> {} and
A3: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f)
let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f)
let g be Morphism of o2,o3; ::_thesis: F . (g * f) = (F . g) * (F . f)
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, Def21;
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; ::_thesis: verum
end;
assume A12: for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) ; ::_thesis: F is comp-preserving
let o1, o2, o3 be object of C1; :: according to FUNCTOR0:def_21 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex 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 ) )
assume that
A13: <^o1,o2^> <> {} and
A14: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex 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 )
let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex 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 )
let g be Morphism of o2,o3; ::_thesis: ex f9 being Morphism of (F . o1),(F . o2) ex 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 )
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 ; ::_thesis: ex 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 )
take g9 ; ::_thesis: ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 )
thus ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g ) ; ::_thesis: (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9
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 ;
::_thesis: verum
end;
end;
:: deftheorem defines comp-preserving FUNCTOR0:def_23_:_
for C1 being non empty transitive AltCatStr
for C2 being non empty reflexive AltCatStr
for F being feasible Covariant FunctorStr over C1,C2 holds
( F is comp-preserving iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) );
definition
let C1 be non empty transitive AltCatStr ;
let C2 be non empty reflexive AltCatStr ;
let F be feasible Contravariant FunctorStr over C1,C2;
redefine attr F is comp-reversing means :: FUNCTOR0:def 24
for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g);
compatibility
( F is comp-reversing iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) )
proof
hereby ::_thesis: ( ( for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) ) implies F is comp-reversing )
assume A1: F is comp-reversing ; ::_thesis: for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g)
let o1, o2, o3 be object of C1; ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) )
assume that
A2: <^o1,o2^> <> {} and
A3: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g)
let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g)
let g be Morphism of o2,o3; ::_thesis: F . (g * f) = (F . f) * (F . g)
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, Def22;
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; ::_thesis: verum
end;
assume A12: for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) ; ::_thesis: F is comp-reversing
let o1, o2, o3 be object of C1; :: according to FUNCTOR0:def_22 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex 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 ) )
assume that
A13: <^o1,o2^> <> {} and
A14: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex 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 )
let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex 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 )
let g be Morphism of o2,o3; ::_thesis: ex f9 being Morphism of (F . o2),(F . o1) ex 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 )
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 ; ::_thesis: ex 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 )
take g9 ; ::_thesis: ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 )
thus ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g ) ; ::_thesis: (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9
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 ;
::_thesis: verum
end;
end;
:: deftheorem defines comp-reversing FUNCTOR0:def_24_:_
for C1 being non empty transitive AltCatStr
for C2 being non empty reflexive AltCatStr
for F being feasible Contravariant FunctorStr over C1,C2 holds
( F is comp-reversing iff for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) );
theorem Th25: :: FUNCTOR0:25
for C1 being non empty AltGraph
for C2 being non empty reflexive AltGraph
for o2 being object of C2
for m being Morphism of o2,o2
for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
proof
let C1 be non empty AltGraph ; ::_thesis: for C2 being non empty reflexive AltGraph
for o2 being object of C2
for m being Morphism of o2,o2
for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
let C2 be non empty reflexive AltGraph ; ::_thesis: for o2 being object of C2
for m being Morphism of o2,o2
for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
let o2 be object of C2; ::_thesis: for m being Morphism of o2,o2
for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
A1: <^o2,o2^> <> {} by ALTCAT_2:def_7;
let m be Morphism of o2,o2; ::_thesis: for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
let F be feasible Covariant FunctorStr over C1,C2; ::_thesis: ( F = C1 --> m implies for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m )
assume A2: F = C1 --> m ; ::_thesis: for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
let o, o9 be object of C1; ::_thesis: for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
let f be Morphism of o,o9; ::_thesis: ( <^o,o9^> <> {} implies F . f = m )
assume A3: <^o,o9^> <> {} ; ::_thesis: F . f = m
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 ;
::_thesis: verum
end;
theorem Th26: :: FUNCTOR0:26
for C1 being non empty AltGraph
for C2 being non empty reflexive AltGraph
for o2 being object of C2
for m being Morphism of o2,o2
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(C1 --> m) . f = m
proof
let C1 be non empty AltGraph ; ::_thesis: for C2 being non empty reflexive AltGraph
for o2 being object of C2
for m being Morphism of o2,o2
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(C1 --> m) . f = m
let C2 be non empty reflexive AltGraph ; ::_thesis: for o2 being object of C2
for m being Morphism of o2,o2
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(C1 --> m) . f = m
let o2 be object of C2; ::_thesis: for m being Morphism of o2,o2
for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(C1 --> m) . f = m
A1: <^o2,o2^> <> {} by ALTCAT_2:def_7;
let m be Morphism of o2,o2; ::_thesis: for o, o9 being object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(C1 --> m) . f = m
set F = C1 --> m;
let o, o9 be object of C1; ::_thesis: for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(C1 --> m) . f = m
let f be Morphism of o,o9; ::_thesis: ( <^o,o9^> <> {} implies (C1 --> m) . f = m )
assume A2: <^o,o9^> <> {} ; ::_thesis: (C1 --> m) . f = m
then <^((C1 --> m) . o9),((C1 --> m) . o)^> <> {} by Def19;
hence (C1 --> m) . f = (Morph-Map ((C1 --> m),o,o9)) . f by A2, Def16
.= m by A1, A2, Th24 ;
::_thesis: verum
end;
registration
let C1 be non empty transitive AltCatStr ;
let C2 be non empty with_units AltCatStr ;
let o be object of C2;
clusterC1 --> (idm o) -> strict comp-preserving comp-reversing ;
coherence
( C1 --> (idm o) is comp-preserving & C1 --> (idm o) is comp-reversing )
proof
set F = C1 --> (idm o);
reconsider G = C1 --> (idm o) as feasible Covariant 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; :: according to FUNCTOR0:def_23 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds G . (g * f) = (G . g) * (G . f) )
assume that
A2: <^o1,o2^> <> {} and
A3: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds G . (g * f) = (G . g) * (G . f)
A4: <^o1,o3^> <> {} by A2, A3, ALTCAT_1:def_2;
let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 holds G . (g * f) = (G . g) * (G . f)
let g be Morphism of o2,o3; ::_thesis: G . (g * f) = (G . g) * (G . f)
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 ; ::_thesis: verum
end;
hence C1 --> (idm o) is comp-preserving ; ::_thesis: C1 --> (idm o) is comp-reversing
let o1, o2, o3 be object of C1; :: according to FUNCTOR0:def_24 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g) )
assume that
A10: <^o1,o2^> <> {} and
A11: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g)
A12: <^o1,o3^> <> {} by A10, A11, ALTCAT_1:def_2;
let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 holds (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g)
let g be Morphism of o2,o3; ::_thesis: (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g)
A13: (C1 --> (idm o)) . g = idm o by A11, Th26;
A14: (C1 --> (idm o)) . f = idm o by A10, Th26;
A15: (C1 --> (idm o)) . o1 = o by A1, Th21;
A16: (C1 --> (idm o)) . o2 = o by A1, Th21;
A17: (C1 --> (idm o)) . o3 = o by A1, Th21;
thus (C1 --> (idm o)) . (g * f) = idm o by A12, Th26
.= ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g) by A1, A13, A14, A15, A16, A17, ALTCAT_1:20 ; ::_thesis: verum
end;
end;
definition
let C1 be non empty transitive with_units AltCatStr ;
let C2 be non empty with_units AltCatStr ;
mode Functor of C1,C2 -> FunctorStr over C1,C2 means :Def25: :: FUNCTOR0:def 25
( it is feasible & it is id-preserving & ( ( it is Covariant & it is comp-preserving ) or ( it is Contravariant & it is comp-reversing ) ) );
existence
ex b1 being FunctorStr over C1,C2 st
( b1 is feasible & b1 is id-preserving & ( ( b1 is Covariant & b1 is comp-preserving ) or ( b1 is Contravariant & b1 is comp-reversing ) ) )
proof
set o = the object of C2;
take C1 --> (idm the object of C2) ; ::_thesis: ( C1 --> (idm the object of C2) is feasible & C1 --> (idm the object of C2) is id-preserving & ( ( C1 --> (idm the object of C2) is Covariant & C1 --> (idm the object of C2) is comp-preserving ) or ( C1 --> (idm the object of C2) is Contravariant & C1 --> (idm the object of C2) is comp-reversing ) ) )
thus ( C1 --> (idm the object of C2) is feasible & C1 --> (idm the object of C2) is id-preserving & ( ( C1 --> (idm the object of C2) is Covariant & C1 --> (idm the object of C2) is comp-preserving ) or ( C1 --> (idm the object of C2) is Contravariant & C1 --> (idm the object of C2) is comp-reversing ) ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def25 defines Functor FUNCTOR0:def_25_:_
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for b3 being FunctorStr over C1,C2 holds
( b3 is Functor of C1,C2 iff ( b3 is feasible & b3 is id-preserving & ( ( b3 is Covariant & b3 is comp-preserving ) or ( b3 is Contravariant & b3 is comp-reversing ) ) ) );
definition
let C1 be non empty transitive with_units AltCatStr ;
let C2 be non empty with_units AltCatStr ;
let F be Functor of C1,C2;
attrF is covariant means :Def26: :: FUNCTOR0:def 26
( F is Covariant & F is comp-preserving );
attrF is contravariant means :Def27: :: FUNCTOR0:def 27
( F is Contravariant & F is comp-reversing );
end;
:: deftheorem Def26 defines covariant FUNCTOR0:def_26_:_
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 holds
( F is covariant iff ( F is Covariant & F is comp-preserving ) );
:: deftheorem Def27 defines contravariant FUNCTOR0:def_27_:_
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 holds
( F is contravariant iff ( F is Contravariant & F is comp-reversing ) );
definition
let A be AltCatStr ;
let B be SubCatStr of A;
func incl B -> strict FunctorStr over B,A means :Def28: :: FUNCTOR0:def 28
( the ObjectMap of it = id [: the carrier of B, the carrier of B:] & the MorphMap of it = id the Arrows of B );
existence
ex b1 being strict FunctorStr over B,A st
( the ObjectMap of b1 = id [: the carrier of B, the carrier of B:] & the MorphMap of b1 = id the Arrows of B )
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:];
id [: the carrier of B, the carrier of B:] = incl CC ;
then reconsider OM = id [: the carrier of B, the carrier of B:] as bifunction of the carrier of B, the carrier of A ;
set MM = id the Arrows of B;
id the Arrows of B is MSUnTrans of OM, the Arrows of B, the Arrows of A
proof
percases ( [: the carrier of A, the carrier of A:] <> {} or [: the carrier of A, the carrier of A:] = {} ) ;
:: according to FUNCTOR0:def_3
case [: the carrier of A, the carrier of A:] <> {} ; ::_thesis: ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of B, the carrier of B:],I29 st
( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 )
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 ; ::_thesis: ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of B, the carrier of B:],I29 st
( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 )
take B9 ; ::_thesis: ex f9 being Function of [: the carrier of B, the carrier of B:],I29 st
( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 )
take f9 ; ::_thesis: ( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 )
thus ( OM = f9 & the Arrows of A = B9 ) ; ::_thesis: id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9
thus id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 ::_thesis: verum
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in [: the carrier of B, the carrier of B:] or (id the Arrows of B) . i is Element of bool [:( the Arrows of B . i),((B9 * f9) . i):] )
assume A1: i in [: the carrier of B, the carrier of B:] ; ::_thesis: (id the Arrows of B) . i is Element of bool [:( the Arrows of B . i),((B9 * f9) . i):]
then A2: (id the Arrows of B) . 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 (id the Arrows of B) . i is Element of bool [:( the Arrows of B . i),((B9 * f9) . i):] by A2, FUNCT_2:7; ::_thesis: verum
end;
end;
case [: the carrier of A, the carrier of A:] = {} ; ::_thesis: id the Arrows of B = [[0]] [: the carrier of B, the carrier of B:]
then CC = {} ;
hence id the Arrows of B = [[0]] [: the carrier of B, the carrier of B:] ; ::_thesis: verum
end;
end;
end;
then reconsider MM = id the Arrows of B as MSUnTrans of OM, the Arrows of B, the Arrows of A ;
take FunctorStr(# OM,MM #) ; ::_thesis: ( the ObjectMap of FunctorStr(# OM,MM #) = id [: the carrier of B, the carrier of B:] & the MorphMap of FunctorStr(# OM,MM #) = id the Arrows of B )
thus ( the ObjectMap of FunctorStr(# OM,MM #) = id [: the carrier of B, the carrier of B:] & the MorphMap of FunctorStr(# OM,MM #) = id the Arrows of B ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being strict FunctorStr over B,A st the ObjectMap of b1 = id [: the carrier of B, the carrier of B:] & the MorphMap of b1 = id the Arrows of B & the ObjectMap of b2 = id [: the carrier of B, the carrier of B:] & the MorphMap of b2 = id the Arrows of B holds
b1 = b2;
;
end;
:: deftheorem Def28 defines incl FUNCTOR0:def_28_:_
for A being AltCatStr
for B being SubCatStr of A
for b3 being strict FunctorStr over B,A holds
( b3 = incl B iff ( the ObjectMap of b3 = id [: the carrier of B, the carrier of B:] & the MorphMap of b3 = id the Arrows of B ) );
definition
let A be AltGraph ;
func id A -> strict FunctorStr over A,A means :Def29: :: FUNCTOR0:def 29
( the ObjectMap of it = id [: the carrier of A, the carrier of A:] & the MorphMap of it = id the Arrows of A );
existence
ex b1 being strict FunctorStr over A,A st
( the ObjectMap of b1 = id [: the carrier of A, the carrier of A:] & the MorphMap of b1 = id the Arrows of A )
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;
id the Arrows of A is MSUnTrans of OM, the Arrows of A, the Arrows of A
proof
percases ( [: the carrier of A, the carrier of A:] <> {} or [: the carrier of A, the carrier of A:] = {} ) ;
:: according to FUNCTOR0:def_3
case [: the carrier of A, the carrier of A:] <> {} ; ::_thesis: ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of A, the carrier of A:],I29 st
( OM = f9 & the Arrows of A = B9 & id the Arrows of A is ManySortedFunction of the Arrows of A,B9 * f9 )
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 ; ::_thesis: ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of A, the carrier of A:],I29 st
( OM = f9 & the Arrows of A = B9 & id the Arrows of A is ManySortedFunction of the Arrows of A,B9 * f9 )
take A9 ; ::_thesis: ex f9 being Function of [: the carrier of A, the carrier of A:],I29 st
( OM = f9 & the Arrows of A = A9 & id the Arrows of A is ManySortedFunction of the Arrows of A,A9 * f9 )
take f9 ; ::_thesis: ( OM = f9 & the Arrows of A = A9 & id the Arrows of A is ManySortedFunction of the Arrows of A,A9 * f9 )
thus ( OM = f9 & the Arrows of A = A9 ) ; ::_thesis: id the Arrows of A is ManySortedFunction of the Arrows of A,A9 * f9
thus id the Arrows of A is ManySortedFunction of the Arrows of A,A9 * f9 ::_thesis: verum
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in [: the carrier of A, the carrier of A:] or (id the Arrows of A) . i is Element of bool [:( the Arrows of A . i),((A9 * f9) . i):] )
assume A1: i in [: the carrier of A, the carrier of A:] ; ::_thesis: (id the Arrows of A) . i is Element of bool [:( the Arrows of A . i),((A9 * f9) . i):]
then (A9 * f9) . i = A9 . (f9 . i) by FUNCT_2:15
.= the Arrows of A . i by A1, FUNCT_1:18 ;
hence (id the Arrows of A) . i is Element of bool [:( the Arrows of A . i),((A9 * f9) . i):] by A1, PBOOLE:def_15; ::_thesis: verum
end;
end;
case [: the carrier of A, the carrier of A:] = {} ; ::_thesis: id the Arrows of A = [[0]] [: the carrier of A, the carrier of A:]
hence id the Arrows of A = [[0]] [: the carrier of A, the carrier of A:] ; ::_thesis: verum
end;
end;
end;
then reconsider MM = id the Arrows of A as MSUnTrans of OM, the Arrows of A, the Arrows of A ;
take FunctorStr(# OM,MM #) ; ::_thesis: ( the ObjectMap of FunctorStr(# OM,MM #) = id [: the carrier of A, the carrier of A:] & the MorphMap of FunctorStr(# OM,MM #) = id the Arrows of A )
thus ( the ObjectMap of FunctorStr(# OM,MM #) = id [: the carrier of A, the carrier of A:] & the MorphMap of FunctorStr(# OM,MM #) = id the Arrows of A ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being strict FunctorStr over A,A st the ObjectMap of b1 = id [: the carrier of A, the carrier of A:] & the MorphMap of b1 = id the Arrows of A & the ObjectMap of b2 = id [: the carrier of A, the carrier of A:] & the MorphMap of b2 = id the Arrows of A holds
b1 = b2;
;
end;
:: deftheorem Def29 defines id FUNCTOR0:def_29_:_
for A being AltGraph
for b2 being strict FunctorStr over A,A holds
( b2 = id A iff ( the ObjectMap of b2 = id [: the carrier of A, the carrier of A:] & the MorphMap of b2 = id the Arrows of A ) );
registration
let A be AltCatStr ;
let B be SubCatStr of A;
cluster incl B -> strict Covariant ;
coherence
incl B is Covariant
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 ; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (incl B) = [:f,f:]
thus the ObjectMap of (incl B) = id [: the carrier of B, the carrier of B:] by Def28
.= [:f,f:] by FUNCT_3:69 ; ::_thesis: verum
end;
end;
theorem Th27: :: FUNCTOR0:27
for A being non empty AltCatStr
for B being non empty SubCatStr of A
for o being object of B holds (incl B) . o = o
proof
let A be non empty AltCatStr ; ::_thesis: for B being non empty SubCatStr of A
for o being object of B holds (incl B) . o = o
let B be non empty SubCatStr of A; ::_thesis: for o being object of B holds (incl B) . o = o
let o be object of B; ::_thesis: (incl B) . o = o
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 ; ::_thesis: verum
end;
theorem Th28: :: FUNCTOR0:28
for A being non empty AltCatStr
for B being non empty SubCatStr of A
for o1, o2 being object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>
proof
let A be non empty AltCatStr ; ::_thesis: for B being non empty SubCatStr of A
for o1, o2 being object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>
let B be non empty SubCatStr of A; ::_thesis: for o1, o2 being object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>
let o1, o2 be object of B; ::_thesis: <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>
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 <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^> by A1, A2, A4, ALTCAT_2:def_2; ::_thesis: verum
end;
registration
let A be non empty AltCatStr ;
let B be non empty SubCatStr of A;
cluster incl B -> feasible strict ;
coherence
incl B is feasible
proof
let o1, o2 be object of B; :: according to FUNCTOR0:def_18 ::_thesis: ( <^o1,o2^> <> {} implies <^((incl B) . o1),((incl B) . o2)^> <> {} )
thus ( <^o1,o2^> <> {} implies <^((incl B) . o1),((incl B) . o2)^> <> {} ) by Th28, XBOOLE_1:3; ::_thesis: verum
end;
end;
definition
let A, B be AltGraph ;
let F be FunctorStr over A,B;
attrF is faithful means :Def30: :: FUNCTOR0:def 30
the MorphMap of F is "1-1" ;
end;
:: deftheorem Def30 defines faithful FUNCTOR0:def_30_:_
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is faithful iff the MorphMap of F is "1-1" );
definition
let A, B be AltGraph ;
let F be FunctorStr over A,B;
attrF is full means :Def31: :: FUNCTOR0:def 31
ex B9 being ManySortedSet of [: the carrier of A, the carrier of A:] ex 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;
:: deftheorem Def31 defines full FUNCTOR0:def_31_:_
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is full iff ex B9 being ManySortedSet of [: the carrier of A, the carrier of A:] ex 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" ) );
definition
let A be AltGraph ;
let B be non empty AltGraph ;
let F be FunctorStr over A,B;
redefine attr F is full means :Def32: :: FUNCTOR0:def 32
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
( F is full iff 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" ) )
proof
hereby ::_thesis: ( 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" ) implies F is full )
assume F is full ; ::_thesis: 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" )
then consider B9 being ManySortedSet of [: the carrier of A, the carrier of A:], f being ManySortedFunction of the Arrows of A,B9 such that
A1: B9 = the Arrows of B * the ObjectMap of F and
A2: f = the MorphMap of F and
A3: f is "onto" by Def31;
reconsider f = f as ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F by A1;
take f = f; ::_thesis: ( f = the MorphMap of F & f is "onto" )
thus f = the MorphMap of F by A2; ::_thesis: f is "onto"
thus f is "onto" by A1, A3; ::_thesis: verum
end;
given 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: f is "onto" ; ::_thesis: F is full
take the Arrows of B * the ObjectMap of F ; :: according to FUNCTOR0:def_31 ::_thesis: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( the Arrows of B * the ObjectMap of F = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" )
thus ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( the Arrows of B * the ObjectMap of F = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" ) by A4, A5; ::_thesis: verum
end;
end;
:: deftheorem Def32 defines full FUNCTOR0:def_32_:_
for A being AltGraph
for B being non empty AltGraph
for F being FunctorStr over A,B holds
( F is full iff 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" ) );
definition
let A, B be AltGraph ;
let F be FunctorStr over A,B;
attrF is injective means :Def33: :: FUNCTOR0:def 33
( F is one-to-one & F is faithful );
attrF is surjective means :Def34: :: FUNCTOR0:def 34
( F is full & F is onto );
end;
:: deftheorem Def33 defines injective FUNCTOR0:def_33_:_
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is injective iff ( F is one-to-one & F is faithful ) );
:: deftheorem Def34 defines surjective FUNCTOR0:def_34_:_
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is surjective iff ( F is full & F is onto ) );
definition
let A, B be AltGraph ;
let F be FunctorStr over A,B;
attrF is bijective means :Def35: :: FUNCTOR0:def 35
( F is injective & F is surjective );
end;
:: deftheorem Def35 defines bijective FUNCTOR0:def_35_:_
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is bijective iff ( F is injective & F is surjective ) );
registration
let A, B be non empty transitive with_units AltCatStr ;
cluster feasible strict covariant contravariant for Functor of A,B;
existence
ex b1 being Functor of A,B st
( b1 is strict & b1 is covariant & b1 is contravariant & b1 is feasible )
proof
set o = the object of B;
reconsider F = A --> (idm the object of B) as Functor of A,B by Def25;
take F ; ::_thesis: ( F is strict & F is covariant & F is contravariant & F is feasible )
thus ( F is strict & F is covariant & F is contravariant & F is feasible ) by Def26, Def27; ::_thesis: verum
end;
end;
theorem Th29: :: FUNCTOR0:29
for A being non empty AltGraph
for o being object of A holds (id A) . o = o
proof
let A be non empty AltGraph ; ::_thesis: for o being object of A holds (id A) . o = o
let o be object of A; ::_thesis: (id A) . o = o
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 ; ::_thesis: verum
end;
theorem Th30: :: FUNCTOR0:30
for A being non empty AltGraph
for o1, o2 being object of A st <^o1,o2^> <> {} holds
for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m
proof
let A be non empty AltGraph ; ::_thesis: for o1, o2 being object of A st <^o1,o2^> <> {} holds
for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m
let o1, o2 be object of A; ::_thesis: ( <^o1,o2^> <> {} implies for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m )
assume A1: <^o1,o2^> <> {} ; ::_thesis: for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m
let m be Morphism of o1,o2; ::_thesis: (Morph-Map ((id A),o1,o2)) . m = m
A2: [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 A2, MSUALG_3:def_1
.= (id <^o1,o2^>) . m by ALTCAT_1:def_1
.= m by A1, FUNCT_1:18 ;
::_thesis: verum
end;
registration
let A be non empty AltGraph ;
cluster id A -> feasible strict Covariant ;
coherence
( id A is feasible & id A is Covariant )
proof
thus id A is feasible ::_thesis: id A is Covariant
proof
let o1, o2 be object of A; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of A . ( the ObjectMap of (id A) . (o1,o2)) <> {} )
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 ( <^o1,o2^> <> {} implies the Arrows of A . ( the ObjectMap of (id A) . (o1,o2)) <> {} ) ; ::_thesis: verum
end;
thus id A is Covariant ::_thesis: verum
proof
take I = id the carrier of A; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (id A) = [:I,I:]
thus the ObjectMap of (id A) = id [: the carrier of A, the carrier of A:] by Def29
.= [:I,I:] by FUNCT_3:69 ; ::_thesis: verum
end;
end;
end;
registration
let A be non empty AltGraph ;
cluster feasible Covariant for FunctorStr over A,A;
existence
ex b1 being FunctorStr over A,A st
( b1 is Covariant & b1 is feasible )
proof
take id A ; ::_thesis: ( id A is Covariant & id A is feasible )
thus ( id A is Covariant & id A is feasible ) ; ::_thesis: verum
end;
end;
theorem Th31: :: FUNCTOR0:31
for A being non empty AltGraph
for o1, o2 being object of A st <^o1,o2^> <> {} holds
for F being feasible Covariant FunctorStr over A,A st F = id A holds
for m being Morphism of o1,o2 holds F . m = m
proof
let A be non empty AltGraph ; ::_thesis: for o1, o2 being object of A st <^o1,o2^> <> {} holds
for F being feasible Covariant FunctorStr over A,A st F = id A holds
for m being Morphism of o1,o2 holds F . m = m
let o1, o2 be object of A; ::_thesis: ( <^o1,o2^> <> {} implies for F being feasible Covariant FunctorStr over A,A st F = id A holds
for m being Morphism of o1,o2 holds F . m = m )
assume A1: <^o1,o2^> <> {} ; ::_thesis: for F being feasible Covariant FunctorStr over A,A st F = id A holds
for m being Morphism of o1,o2 holds F . m = m
let F be feasible Covariant FunctorStr over A,A; ::_thesis: ( F = id A implies for m being Morphism of o1,o2 holds F . m = m )
assume A2: F = id A ; ::_thesis: for m being Morphism of o1,o2 holds F . m = m
let m be Morphism of o1,o2; ::_thesis: F . m = m
<^(F . o1),(F . o2)^> <> {} by A1, Def18;
hence F . m = (Morph-Map (F,o1,o2)) . m by A1, Def15
.= m by A1, A2, Th30 ;
::_thesis: verum
end;
registration
let A be non empty transitive with_units AltCatStr ;
cluster id A -> strict id-preserving comp-preserving ;
coherence
( id A is id-preserving & id A is comp-preserving )
proof
thus id A is id-preserving ::_thesis: id A is comp-preserving
proof
let o be object of A; :: according to FUNCTOR0:def_20 ::_thesis: (Morph-Map ((id A),o,o)) . (idm o) = idm ((id A) . o)
<^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 ;
::_thesis: verum
end;
set F = id A;
id A is comp-preserving
proof
let o1, o2, o3 be object of A; :: according to FUNCTOR0:def_23 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds (id A) . (g * f) = ((id A) . g) * ((id A) . f) )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds (id A) . (g * f) = ((id A) . g) * ((id A) . f)
let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 holds (id A) . (g * f) = ((id A) . g) * ((id A) . f)
let g be Morphism of o2,o3; ::_thesis: (id A) . (g * f) = ((id A) . g) * ((id A) . f)
A3: <^o1,o3^> <> {} by A1, A2, ALTCAT_1:def_2;
A4: (id A) . o1 = o1 by Th29;
A5: (id A) . o2 = o2 by Th29;
A6: (id A) . o3 = o3 by Th29;
A7: (id A) . g = g by A2, Th31;
(id A) . f = f by A1, Th31;
hence (id A) . (g * f) = ((id A) . g) * ((id A) . f) by A3, A4, A5, A6, A7, Th31; ::_thesis: verum
end;
hence id A is comp-preserving ; ::_thesis: verum
end;
end;
definition
let A be non empty transitive with_units AltCatStr ;
:: original: id
redefine func id A -> strict covariant Functor of A,A;
coherence
id A is strict covariant Functor of A,A by Def25, Def26;
end;
registration
let A be AltGraph ;
cluster id A -> strict bijective ;
coherence
id A is bijective
proof
set CC = [: the carrier of A, the carrier of A:];
A1: the ObjectMap of (id A) = id [: the carrier of A, the carrier of A:] by Def29;
hence id A is one-to-one by Def6; :: according to FUNCTOR0:def_33,FUNCTOR0:def_35 ::_thesis: ( id A is faithful & id A is surjective )
thus id A is faithful ::_thesis: id A is surjective
proof
percases ( the carrier of A <> {} or the carrier of A = {} ) ;
supposeA2: the carrier of A <> {} ; ::_thesis: id A is faithful
let i be set ; :: according to MSUALG_3:def_2,FUNCTOR0:def_30 ::_thesis: for b1 being set holds
( not i in proj1 the MorphMap of (id A) or not the MorphMap of (id A) . i = b1 or b1 is one-to-one )
let f be Function; ::_thesis: ( not i in proj1 the MorphMap of (id A) or not the MorphMap of (id A) . i = f or f is one-to-one )
assume that
A3: i in dom the MorphMap of (id A) and
A4: the MorphMap of (id A) . i = f ; ::_thesis: f is one-to-one
consider o1, o2 being Element of A such that
A5: i = [o1,o2] by A2, A3, DOMAIN_1:1;
reconsider o1 = o1, o2 = 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 f is one-to-one ; ::_thesis: verum
end;
supposeA7: the carrier of A = {} ; ::_thesis: id A is faithful
let i be set ; :: according to MSUALG_3:def_2,FUNCTOR0:def_30 ::_thesis: for b1 being set holds
( not i in proj1 the MorphMap of (id A) or not the MorphMap of (id A) . i = b1 or b1 is one-to-one )
let f be Function; ::_thesis: ( not i in proj1 the MorphMap of (id A) or not the MorphMap of (id A) . i = f or f is one-to-one )
assume that
A8: i in dom the MorphMap of (id A) and
the MorphMap of (id A) . i = f ; ::_thesis: f is one-to-one
dom the MorphMap of (id A) = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2
.= {} by A7, ZFMISC_1:90 ;
hence f is one-to-one by A8; ::_thesis: verum
end;
end;
end;
thus id A is full :: according to FUNCTOR0:def_34 ::_thesis: id A is onto
proof
percases ( not A is empty or A is empty ) ;
suppose not A is empty ; ::_thesis: id A is full
then reconsider A = 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 ; :: according to FUNCTOR0:def_32 ::_thesis: ( f = the MorphMap of (id A) & f is "onto" )
thus f = the MorphMap of (id A) ; ::_thesis: f is "onto"
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in [: the carrier of A, the carrier of A:] or proj2 (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i )
assume A9: i in [: the carrier of A, the carrier of A:] ; ::_thesis: proj2 (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i
then consider o1, o2 being Element of A such that
A10: i = [o1,o2] by DOMAIN_1:1;
reconsider o1 = o1, o2 = 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) = [: the carrier of A, the carrier of A:] by A1, RELAT_1:45;
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] by RELAT_1:45
.= 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 ;
::_thesis: verum
end;
hence id A is full ; ::_thesis: verum
end;
suppose A is empty ; ::_thesis: id A is full
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 set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in [: the carrier of A, the carrier of A:] or f . i is Element of bool [:( the Arrows of A . i),(B . i):] )
thus ( not i in [: the carrier of A, the carrier of A:] or f . i is Element of bool [:( the Arrows of A . i),(B . i):] ) by A13, ZFMISC_1:90; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the Arrows of A,B ;
take B ; :: according to FUNCTOR0:def_31 ::_thesis: ex f being ManySortedFunction of the Arrows of A,B st
( B = the Arrows of A * the ObjectMap of (id A) & f = the MorphMap of (id A) & f is "onto" )
take f ; ::_thesis: ( B = the Arrows of A * the ObjectMap of (id A) & f = the MorphMap of (id A) & f is "onto" )
thus ( B = the Arrows of A * the ObjectMap of (id A) & f = the MorphMap of (id A) ) ; ::_thesis: f is "onto"
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in [: the carrier of A, the carrier of A:] or proj2 (f . i) = B . i )
thus ( not i in [: the carrier of A, the carrier of A:] or proj2 (f . i) = B . i ) by A13, ZFMISC_1:90; ::_thesis: verum
end;
end;
end;
rng (id [: the carrier of A, the carrier of A:]) = [: the carrier of A, the carrier of A:] ;
then the ObjectMap of (id A) is onto by A1, FUNCT_2:def_3;
hence id A is onto by Def7; ::_thesis: verum
end;
end;
begin
definition
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible FunctorStr over C1,C2;
let G be FunctorStr over C2,C3;
funcG * F -> strict FunctorStr over C1,C3 means :Def36: :: FUNCTOR0:def 36
( 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
ex b1 being strict FunctorStr over C1,C3 st
( the ObjectMap of b1 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b1 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F )
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 [: the carrier of C1, the carrier of C1:] & ( the Arrows of C2 * the ObjectMap of F) . ii = {} & not the Arrows of C1 . ii = {} holds
( the Arrows of C3 * O) . ii = {}
proof
let ii be set ; ::_thesis: ( ii in [: the carrier of C1, the carrier of C1:] & ( the Arrows of C2 * the ObjectMap of F) . ii = {} & not the Arrows of C1 . ii = {} implies ( the Arrows of C3 * O) . ii = {} )
assume that
A1: ii in [: the carrier of C1, the carrier of C1:] and
A2: ( the Arrows of C2 * the ObjectMap of F) . ii = {} ; ::_thesis: ( the Arrows of C1 . ii = {} or ( the Arrows of C3 * O) . ii = {} )
A3: dom the ObjectMap of F = [: the carrier of C1, the carrier of C1:] 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 ( the Arrows of C1 . ii = {} or ( the Arrows of C3 * O) . ii = {} ) ; ::_thesis: verum
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 #) ; ::_thesis: ( the ObjectMap of FunctorStr(# O,M #) = the ObjectMap of G * the ObjectMap of F & the MorphMap of FunctorStr(# O,M #) = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F )
thus ( the ObjectMap of FunctorStr(# O,M #) = the ObjectMap of G * the ObjectMap of F & the MorphMap of FunctorStr(# O,M #) = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being strict FunctorStr over C1,C3 st the ObjectMap of b1 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b1 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F & the ObjectMap of b2 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b2 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F holds
b1 = b2;
;
end;
:: deftheorem Def36 defines * FUNCTOR0:def_36_:_
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for b6 being strict FunctorStr over C1,C3 holds
( b6 = G * F iff ( the ObjectMap of b6 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b6 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F ) );
registration
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Covariant FunctorStr over C1,C2;
let G be Covariant FunctorStr over C2,C3;
clusterG * F -> strict Covariant ;
correctness
coherence
G * F is Covariant ;
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:] by Def1;
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:] by Def1;
take g * f ; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (G * F) = [:(g * f),(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 ; ::_thesis: verum
end;
end;
registration
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Contravariant FunctorStr over C1,C2;
let G be Covariant FunctorStr over C2,C3;
clusterG * F -> strict Contravariant ;
correctness
coherence
G * F is Contravariant ;
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:] by Def2;
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:] by Def1;
take g * f ; :: according to FUNCTOR0:def_2,FUNCTOR0:def_13 ::_thesis: the ObjectMap of (G * F) = ~ [:(g * f),(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 ; ::_thesis: verum
end;
end;
registration
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Covariant FunctorStr over C1,C2;
let G be Contravariant FunctorStr over C2,C3;
clusterG * F -> strict Contravariant ;
correctness
coherence
G * F is Contravariant ;
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:] by Def1;
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:] by Def2;
take g * f ; :: according to FUNCTOR0:def_2,FUNCTOR0:def_13 ::_thesis: the ObjectMap of (G * F) = ~ [:(g * f),(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 ; ::_thesis: verum
end;
end;
registration
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Contravariant FunctorStr over C1,C2;
let G be Contravariant FunctorStr over C2,C3;
clusterG * F -> strict Covariant ;
correctness
coherence
G * F is Covariant ;
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:] by Def2;
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:] by Def2;
take g * f ; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (G * F) = [:(g * f),(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 ; ::_thesis: verum
end;
end;
registration
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible FunctorStr over C1,C2;
let G be feasible FunctorStr over C2,C3;
clusterG * F -> feasible strict ;
coherence
G * F is feasible
proof
let o1, o2 be object of C1; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of C3 . ( the ObjectMap of (G * F) . (o1,o2)) <> {} )
assume A1: <^o1,o2^> <> {} ; ::_thesis: the Arrows of C3 . ( the ObjectMap of (G * F) . (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 = p1, p2 = 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 the Arrows of C3 . ( the ObjectMap of (G * F) . (o1,o2)) <> {} by A4, Def11; ::_thesis: verum
end;
end;
theorem :: FUNCTOR0:32
for C1 being non empty AltGraph
for C2, C3, C4 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being feasible FunctorStr over C2,C3
for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)
proof
let C1 be non empty AltGraph ; ::_thesis: for C2, C3, C4 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being feasible FunctorStr over C2,C3
for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)
let C2, C3, C4 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2
for G being feasible FunctorStr over C2,C3
for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)
let F be feasible FunctorStr over C1,C2; ::_thesis: for G being feasible FunctorStr over C2,C3
for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)
let G be feasible FunctorStr over C2,C3; ::_thesis: for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)
let H be FunctorStr over C3,C4; ::_thesis: (H * G) * F = H * (G * F)
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 (H * G) * F = H * (G * F) by A1; ::_thesis: verum
end;
theorem Th33: :: FUNCTOR0:33
for C1 being non empty AltCatStr
for C2, C3 being non empty reflexive AltCatStr
for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being object of C1 holds (G * F) . o = G . (F . o)
proof
let C1 be non empty AltCatStr ; ::_thesis: for C2, C3 being non empty reflexive AltCatStr
for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being object of C1 holds (G * F) . o = G . (F . o)
let C2, C3 be non empty reflexive AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being object of C1 holds (G * F) . o = G . (F . o)
let F be reflexive feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3
for o being object of C1 holds (G * F) . o = G . (F . o)
let G be FunctorStr over C2,C3; ::_thesis: for o being object of C1 holds (G * F) . o = G . (F . o)
let o be object of C1; ::_thesis: (G * F) . o = G . (F . o)
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 ; ::_thesis: verum
end;
theorem Th34: :: FUNCTOR0:34
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being 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 ; ::_thesis: for C2, C3 being non empty reflexive AltGraph
for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
let F be reflexive feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3
for o being object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
let G be FunctorStr over C2,C3; ::_thesis: for o being object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
let o be object of C1; ::_thesis: Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
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 ; ::_thesis: verum
end;
registration
let C1, C2, C3 be non empty with_units AltCatStr ;
let F be reflexive feasible id-preserving FunctorStr over C1,C2;
let G be id-preserving FunctorStr over C2,C3;
clusterG * F -> strict id-preserving ;
coherence
G * F is id-preserving
proof
let o be object of C1; :: according to FUNCTOR0:def_20 ::_thesis: (Morph-Map ((G * F),o,o)) . (idm o) = idm ((G * F) . o)
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 ; ::_thesis: verum
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;
funcF | B -> FunctorStr over B,C equals :: FUNCTOR0:def 37
F * (incl B);
correctness
coherence
F * (incl B) is FunctorStr over B,C;
;
end;
:: deftheorem defines | FUNCTOR0:def_37_:_
for A, C being non empty reflexive AltCatStr
for B being non empty SubCatStr of A
for F being FunctorStr over A,C holds F | B = F * (incl B);
begin
definition
let A, B be non empty AltGraph ;
let F be FunctorStr over A,B;
assume A1: F is bijective ;
funcF " -> strict FunctorStr over B,A means :Def38: :: FUNCTOR0:def 38
( 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
ex b1 being strict FunctorStr over B,A st
( the ObjectMap of b1 = 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 b1 = (f "") * ( the ObjectMap of F ") ) )
proof
set OF = the ObjectMap of F;
F is injective by A1, Def35;
then F is one-to-one by Def33;
then A2: the ObjectMap of F is one-to-one by Def6;
F is surjective by A1, Def35;
then F is onto by Def34;
then the ObjectMap of F is onto by Def7;
then A3: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by FUNCT_2:def_3;
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 * the ObjectMap of F by Def4;
( the Arrows of B * the ObjectMap of F) * OM = the Arrows of B * ( the ObjectMap of F * 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 #); ::_thesis: ( the ObjectMap of G = 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 G = (f "") * ( the ObjectMap of F ") ) )
thus the ObjectMap of G = the ObjectMap of F " ; ::_thesis: 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 G = (f "") * ( the ObjectMap of F ") )
take f ; ::_thesis: ( f = the MorphMap of F & the MorphMap of G = (f "") * ( the ObjectMap of F ") )
thus ( f = the MorphMap of F & the MorphMap of G = (f "") * ( the ObjectMap of F ") ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict FunctorStr over B,A st the ObjectMap of b1 = 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 b1 = (f "") * ( the ObjectMap of F ") ) & the ObjectMap of b2 = 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 b2 = (f "") * ( the ObjectMap of F ") ) holds
b1 = b2 ;
end;
:: deftheorem Def38 defines " FUNCTOR0:def_38_:_
for A, B being non empty AltGraph
for F being FunctorStr over A,B st F is bijective holds
for b4 being strict FunctorStr over B,A holds
( b4 = F " iff ( the ObjectMap of b4 = 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 b4 = (f "") * ( the ObjectMap of F ") ) ) );
theorem Th35: :: FUNCTOR0:35
for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr over A,B st F is bijective holds
( F " is bijective & F " is feasible )
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B st F is bijective holds
( F " is bijective & F " is feasible )
let F be feasible FunctorStr over A,B; ::_thesis: ( F is bijective implies ( F " is bijective & F " is feasible ) )
assume A1: F is bijective ; ::_thesis: ( F " is bijective & F " is feasible )
set G = F " ;
A2: the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38;
A3: F is injective by A1, Def35;
then F is one-to-one by Def33;
then A4: the ObjectMap of F is one-to-one by Def6;
hence the ObjectMap of (F ") is one-to-one by A2; :: according to FUNCTOR0:def_6,FUNCTOR0:def_33,FUNCTOR0:def_35 ::_thesis: ( F " is faithful & F " is surjective & F " is feasible )
F is faithful by A3, Def33;
then A5: the MorphMap of F is "1-1" by Def30;
A6: F is surjective by A1, Def35;
then F is onto by Def34;
then A7: the ObjectMap of F is onto by Def7;
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 (F ") = (h "") * ( the ObjectMap of F ") by A1, Def38;
F is full by A6, Def34;
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" ) by Def32;
set AA = [: the carrier of A, the carrier of A:];
set BB = [: the carrier of B, the carrier of B:];
A11: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by A7, FUNCT_2:def_3;
reconsider f = the MorphMap of (F ") as ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4;
f is "1-1"
proof
let i be set ; :: according to MSUALG_3:def_2 ::_thesis: for b1 being set holds
( not i in proj1 f or not f . i = b1 or b1 is one-to-one )
let g be Function; ::_thesis: ( not i in proj1 f or not f . i = g or g is one-to-one )
assume that
A12: i in dom f and
A13: f . i = g ; ::_thesis: g is one-to-one
i in [: the carrier of B, the carrier of B:] 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 [: the carrier of A, the carrier of A:] ;
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, MSUALG_3:def_2;
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 g is one-to-one by A16; ::_thesis: verum
end;
hence the MorphMap of (F ") is "1-1" ; :: according to FUNCTOR0:def_30 ::_thesis: ( F " is surjective & F " is feasible )
thus F " is full :: according to FUNCTOR0:def_34 ::_thesis: ( F " is onto & F " is feasible )
proof
take f ; :: according to FUNCTOR0:def_32 ::_thesis: ( f = the MorphMap of (F ") & f is "onto" )
thus f = the MorphMap of (F ") ; ::_thesis: f is "onto"
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in [: the carrier of B, the carrier of B:] or proj2 (f . i) = ( the Arrows of A * the ObjectMap of (F ")) . i )
assume A17: i in [: the carrier of B, the carrier of B:] ; ::_thesis: proj2 (f . i) = ( the Arrows of A * the ObjectMap of (F ")) . i
then A18: i in dom the ObjectMap of (F ") 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 [: the carrier of A, the carrier of A:] ;
then the ObjectMap of (F ") . i in dom h by A2, PARTFUN1:def_2;
then A21: h . ( the ObjectMap of (F ") . i) is one-to-one by A5, A8, MSUALG_3:def_2;
set j = the ObjectMap of (F ") . i;
A22: h . ( the ObjectMap of (F ") . i) is Function of ( the Arrows of A . ( the ObjectMap of (F ") . i)),(( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of (F ") . i)) by A2, A20, PBOOLE:def_15;
consider o1, o2 being Element of A such that
A23: the ObjectMap of (F ") . i = [o1,o2] by A2, A20, DOMAIN_1:1;
reconsider o1 = o1, o2 = o2 as object of A ;
A24: now__::_thesis:_(_the_Arrows_of_A_._(_the_ObjectMap_of_(F_")_._i)_<>_{}_implies_(_the_Arrows_of_B_*_the_ObjectMap_of_F)_._(_the_ObjectMap_of_(F_")_._i)_<>_{}_)
assume the Arrows of A . ( the ObjectMap of (F ") . i) <> {} ; ::_thesis: ( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of (F ") . i) <> {}
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) . ( the ObjectMap of (F ") . i) <> {} by A2, A20, A23, FUNCT_1:13; ::_thesis: verum
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 (F ") . i)) by A2, A21, FUNCT_1:33
.= the Arrows of A . ( the ObjectMap of (F ") . i) by A22, A24, FUNCT_2:def_1
.= ( the Arrows of A * the ObjectMap of (F ")) . i by A18, FUNCT_1:13 ;
::_thesis: verum
end;
thus rng the ObjectMap of (F ") = dom the ObjectMap of F by A2, A4, FUNCT_1:33
.= [: the carrier of A, the carrier of A:] by FUNCT_2:def_1 ; :: according to FUNCT_2:def_3,FUNCTOR0:def_7 ::_thesis: F " is feasible
let o1, o2 be object of B; :: according to FUNCTOR0:def_11 ::_thesis: ( <^o1,o2^> <> {} implies the Arrows of A . ( the ObjectMap of (F ") . (o1,o2)) <> {} )
assume <^o1,o2^> <> {} ; ::_thesis: the Arrows of A . ( the ObjectMap of (F ") . (o1,o2)) <> {}
then A25: the Arrows of B . (o1,o2) <> {} by ALTCAT_1:def_1;
A26: [o1,o2] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87;
then consider p1, p2 being Element of A such that
A27: the ObjectMap of (F ") . [o1,o2] = [p1,p2] by DOMAIN_1:1, FUNCT_2:5;
reconsider p1 = p1, p2 = p2 as object of A ;
[o1,o2] in dom the ObjectMap of (F ") by A26, FUNCT_2:def_1;
then A28: the ObjectMap of F . (p1,p2) = ( the ObjectMap of F * the ObjectMap of (F ")) . [o1,o2] by A27, FUNCT_1:13
.= (id [: the carrier of B, the carrier of B:]) . [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 (F ") . (o1,o2)) = {} ; ::_thesis: contradiction
A30: [p1,p2] in [: the carrier of A, the carrier of A:] 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, MSUALG_3:def_3
.= the Arrows of B . [o1,o2] by A28, A31, FUNCT_1:13 ;
hence contradiction by A25; ::_thesis: verum
end;
theorem Th36: :: FUNCTOR0:36
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive holds
F " is reflexive
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive holds
F " is reflexive
let F be reflexive feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is coreflexive implies F " is reflexive )
assume that
A1: F is bijective and
A2: F is coreflexive ; ::_thesis: F " is reflexive
set G = F " ;
A3: the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38;
let o be object of B; :: according to FUNCTOR0:def_10 ::_thesis: the ObjectMap of (F ") . (o,o) = [((F ") . o),((F ") . o)]
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, Def35;
then F is one-to-one by Def33;
then A6: the ObjectMap of F is one-to-one by Def6;
A7: [p,p] in dom the ObjectMap of F by A4, ZFMISC_1:87;
A8: (F ") . (F . p) = ((F ") * F) . p by Th33
.= (( the ObjectMap of (F ") * 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 (F ") . (o,o) = the ObjectMap of (F ") . ( the ObjectMap of F . (p,p)) by A5, Def10
.= ( the ObjectMap of (F ") * 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
.= [((F ") . o),((F ") . o)] by A5, A7, A8, FUNCT_1:18 ; ::_thesis: verum
end;
theorem Th37: :: FUNCTOR0:37
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible id-preserving FunctorStr over A,B st F is bijective & F is coreflexive holds
F " is id-preserving
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible id-preserving FunctorStr over A,B st F is bijective & F is coreflexive holds
F " is id-preserving
let F be reflexive feasible id-preserving FunctorStr over A,B; ::_thesis: ( F is bijective & F is coreflexive implies F " is id-preserving )
assume A1: ( F is bijective & F is coreflexive ) ; ::_thesis: F " is id-preserving
set G = F " ;
reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36;
A2: the ObjectMap of (F ") = 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 (F ") = (f "") * ( the ObjectMap of F ") by A1, Def38;
let o be object of B; :: according to FUNCTOR0:def_20 ::_thesis: (Morph-Map ((F "),o,o)) . (idm o) = idm ((F ") . o)
A5: F is injective by A1, Def35;
then F is one-to-one by Def33;
then A6: the ObjectMap of F is one-to-one by Def6;
F is faithful by A5, Def33;
then A7: the MorphMap of F is "1-1" by Def30;
F is surjective by A1, Def35;
then F is full by Def34;
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" ) by Def32;
A9: [((F ") . o),((F ") . 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 (F ") 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 (F "))) . [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 . ((F ") . o) = (F * H) . o by Th33
.= o by A12, MCART_1:7 ;
dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2;
then [((F ") . o),((F ") . o)] in dom the MorphMap of F by ZFMISC_1:87;
then A14: Morph-Map (F,((F ") . o),((F ") . o)) is one-to-one by A7, MSUALG_3:def_2;
[((F ") . o),((F ") . o)] in dom the ObjectMap of F by A9, FUNCT_2:def_1;
then ( the Arrows of B * the ObjectMap of F) . [((F ") . o),((F ") . o)] = the Arrows of B . ( the ObjectMap of F . (((F ") . o),((F ") . o))) by FUNCT_1:13
.= the Arrows of B . ((F . ((F ") . o)),(F . ((F ") . o))) by Def10 ;
then A15: ( the Arrows of B * the ObjectMap of F) . [((F ") . o),((F ") . o)] <> {} by ALTCAT_2:def_6;
Morph-Map (F,((F ") . o),((F ") . o)) is Function of ( the Arrows of A . [((F ") . o),((F ") . o)]),(( the Arrows of B * the ObjectMap of F) . [((F ") . o),((F ") . o)]) by A3, A9, PBOOLE:def_15;
then A16: dom (Morph-Map (F,((F ") . o),((F ") . o))) = the Arrows of A . (((F ") . o),((F ") . o)) by A15, FUNCT_2:def_1
.= <^((F ") . o),((F ") . o)^> by ALTCAT_1:def_1 ;
( the Arrows of A * the ObjectMap of (F ")) . [o,o] = the Arrows of A . ( the ObjectMap of H . (o,o)) by A11, FUNCT_1:13
.= the Arrows of A . (((F ") . o),((F ") . o)) by Def10 ;
then A17: ( the Arrows of A * the ObjectMap of (F ")) . [o,o] <> {} by ALTCAT_2:def_6;
the MorphMap of (F ") is ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4;
then Morph-Map ((F "),o,o) is Function of ( the Arrows of B . [o,o]),(( the Arrows of A * the ObjectMap of (F ")) . [o,o]) by A10, PBOOLE:def_15;
then A18: dom (Morph-Map ((F "),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 ((F "),o,o)) by ALTCAT_1:19;
A20: Morph-Map ((F "),o,o) = (f "") . ( the ObjectMap of (F ") . (o,o)) by A2, A4, A11, FUNCT_1:13
.= (f "") . [(H . o),(H . o)] by Def10
.= (Morph-Map (F,((F ") . o),((F ") . o))) " by A3, A7, A8, A9, MSUALG_3:def_4 ;
(Morph-Map ((F "),o,o)) . (idm o) in rng (Morph-Map ((F "),o,o)) by A19, FUNCT_1:def_3;
then A21: (Morph-Map ((F "),o,o)) . (idm o) in dom (Morph-Map (F,((F ") . o),((F ") . o))) by A14, A20, FUNCT_1:33;
(Morph-Map (F,((F ") . o),((F ") . o))) . ((Morph-Map ((F "),o,o)) . (idm o)) = ((Morph-Map (F,((F ") . o),((F ") . o))) * (Morph-Map ((F "),o,o))) . (idm o) by A18, ALTCAT_1:19, FUNCT_1:13
.= (id (rng (Morph-Map (F,((F ") . o),((F ") . o))))) . (idm o) by A14, A20, FUNCT_1:39
.= (id (dom (Morph-Map ((F "),o,o)))) . (idm o) by A14, A20, FUNCT_1:33
.= idm (F . ((F ") . o)) by A13, A18, ALTCAT_1:19, FUNCT_1:18
.= (Morph-Map (F,((F ") . o),((F ") . o))) . (idm ((F ") . o)) by Def20 ;
hence (Morph-Map ((F "),o,o)) . (idm o) = idm ((F ") . o) by A14, A16, A21, FUNCT_1:def_4; ::_thesis: verum
end;
theorem Th38: :: FUNCTOR0:38
for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr over A,B st F is bijective & F is Covariant holds
F " is Covariant
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B st F is bijective & F is Covariant holds
F " is Covariant
let F be feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is Covariant implies F " is Covariant )
assume A1: ( F is bijective & F is Covariant ) ; ::_thesis: F " is Covariant
then F is injective by Def35;
then F is one-to-one by Def33;
then A2: the ObjectMap of F is one-to-one by Def6;
F is surjective by A1, Def35;
then F is onto by Def34;
then A3: the ObjectMap of F is onto by Def7;
the ObjectMap of F is Covariant by A1, Def12;
then consider f being Function of the carrier of A, the carrier of B such that
A4: the ObjectMap of F = [:f,f:] by Def1;
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, FUNCT_2:def_3;
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 ; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (F ") = [:g,g:]
[:f,f:] " = [:g,g:] by A5, Th6;
hence the ObjectMap of (F ") = [:g,g:] by A1, A4, Def38; ::_thesis: verum
end;
theorem Th39: :: FUNCTOR0:39
for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr over A,B st F is bijective & F is Contravariant holds
F " is Contravariant
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B st F is bijective & F is Contravariant holds
F " is Contravariant
let F be feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is Contravariant implies F " is Contravariant )
assume A1: ( F is bijective & F is Contravariant ) ; ::_thesis: F " is Contravariant
then F is injective by Def35;
then F is one-to-one by Def33;
then A2: the ObjectMap of F is one-to-one by Def6;
F is surjective by A1, Def35;
then F is onto by Def34;
then A3: the ObjectMap of F is onto by Def7;
the ObjectMap of F is Contravariant by A1, Def13;
then consider f being Function of the carrier of A, the carrier of B such that
A4: the ObjectMap of F = ~ [:f,f:] by Def2;
[: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:] by FUNCT_2:def_3;
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 ; :: according to FUNCTOR0:def_2,FUNCTOR0:def_13 ::_thesis: the ObjectMap of (F ") = ~ [:g,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 ; ::_thesis: verum
end;
theorem Th40: :: FUNCTOR0:40
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Covariant holds
for o1, o2 being object of B
for 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 non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Covariant holds
for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m
let F be reflexive feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is coreflexive & F is Covariant implies for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m )
assume A1: ( F is bijective & F is coreflexive & F is Covariant ) ; ::_thesis: for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m
set G = F " ;
A2: F " is Covariant by A1, Th38;
reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36;
A3: the ObjectMap of (F ") = 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 (F ") = (f "") * ( the ObjectMap of F ") by A1, Def38;
F is injective by A1, Def35;
then F is faithful by Def33;
then A6: the MorphMap of F is "1-1" by Def30;
F is surjective by A1, Def35;
then F is full by Def34;
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" ) by Def32;
let o1, o2 be object of B; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m
let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m )
assume A8: <^o1,o2^> <> {} ; ::_thesis: (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m
A9: [((F ") . o1),((F ") . 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 (F ") by FUNCT_2:def_1;
dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2;
then [((F ") . o1),((F ") . o2)] in dom the MorphMap of F by ZFMISC_1:87;
then A12: Morph-Map (F,((F ") . o1),((F ") . o2)) is one-to-one by A6, MSUALG_3:def_2;
( the Arrows of A * the ObjectMap of (F ")) . [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 (F ")) . [o1,o2] <> {} by A2, A8, Def18;
the MorphMap of (F ") is ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4;
then Morph-Map ((F "),o1,o2) is Function of ( the Arrows of B . [o1,o2]),(( the Arrows of A * the ObjectMap of (F ")) . [o1,o2]) by A10, PBOOLE:def_15;
then A14: dom (Morph-Map ((F "),o1,o2)) = the Arrows of B . (o1,o2) by A13, FUNCT_2:def_1
.= <^o1,o2^> by ALTCAT_1:def_1 ;
A15: Morph-Map ((F "),o1,o2) = (f "") . ( the ObjectMap of (F ") . (o1,o2)) by A3, A5, A11, FUNCT_1:13
.= (f "") . [(H . o1),(H . o2)] by A2, Th22
.= (Morph-Map (F,((F ") . o1),((F ") . o2))) " by A4, A6, A7, A9, MSUALG_3:def_4 ;
thus (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = ((Morph-Map (F,((F ") . o1),((F ") . o2))) * (Morph-Map ((F "),o1,o2))) . m by A8, A14, FUNCT_1:13
.= (id (rng (Morph-Map (F,((F ") . o1),((F ") . o2))))) . m by A12, A15, FUNCT_1:39
.= (id (dom (Morph-Map ((F "),o1,o2)))) . m by A12, A15, FUNCT_1:33
.= m by A8, A14, FUNCT_1:18 ; ::_thesis: verum
end;
theorem Th41: :: FUNCTOR0:41
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Contravariant holds
for o1, o2 being object of B
for 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 non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Contravariant holds
for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m
let F be reflexive feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is coreflexive & F is Contravariant implies for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m )
assume A1: ( F is bijective & F is coreflexive & F is Contravariant ) ; ::_thesis: for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m
set G = F " ;
A2: F " is Contravariant by A1, Th39;
reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36;
A3: the ObjectMap of (F ") = 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 (F ") = (f "") * ( the ObjectMap of F ") by A1, Def38;
F is injective by A1, Def35;
then F is faithful by Def33;
then A6: the MorphMap of F is "1-1" by Def30;
F is surjective by A1, Def35;
then F is full by Def34;
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" ) by Def32;
let o1, o2 be object of B; ::_thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m
let m be Morphism of o1,o2; ::_thesis: ( <^o1,o2^> <> {} implies (Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m )
assume A8: <^o1,o2^> <> {} ; ::_thesis: (Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m
A9: [((F ") . o2),((F ") . 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 (F ") by FUNCT_2:def_1;
dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2;
then [((F ") . o2),((F ") . o1)] in dom the MorphMap of F by ZFMISC_1:87;
then A12: Morph-Map (F,((F ") . o2),((F ") . o1)) is one-to-one by A6, MSUALG_3:def_2;
( the Arrows of A * the ObjectMap of (F ")) . [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 (F ")) . [o1,o2] <> {} by A2, A8, Def19;
the MorphMap of (F ") is ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4;
then Morph-Map ((F "),o1,o2) is Function of ( the Arrows of B . [o1,o2]),(( the Arrows of A * the ObjectMap of (F ")) . [o1,o2]) by A10, PBOOLE:def_15;
then A14: dom (Morph-Map ((F "),o1,o2)) = the Arrows of B . (o1,o2) by A13, FUNCT_2:def_1
.= <^o1,o2^> by ALTCAT_1:def_1 ;
A15: Morph-Map ((F "),o1,o2) = (f "") . ( the ObjectMap of (F ") . (o1,o2)) by A3, A5, A11, FUNCT_1:13
.= (f "") . [(H . o2),(H . o1)] by A2, Th23
.= (Morph-Map (F,((F ") . o2),((F ") . 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,((F ") . o2),((F ") . o1))) * (Morph-Map ((F "),o1,o2))) . m by A8, A14, FUNCT_1:13
.= (id (rng (Morph-Map (F,((F ") . o2),((F ") . o1))))) . m by A12, A15, FUNCT_1:39
.= (id (dom (Morph-Map ((F "),o1,o2)))) . m by A12, A15, FUNCT_1:33
.= m by A8, A14, FUNCT_1:18 ; ::_thesis: verum
end;
theorem Th42: :: FUNCTOR0:42
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-preserving & F is Covariant & F is coreflexive holds
F " is comp-preserving
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-preserving & F is Covariant & F is coreflexive holds
F " is comp-preserving
let F be reflexive feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is comp-preserving & F is Covariant & F is coreflexive implies F " is comp-preserving )
assume A1: ( F is bijective & F is comp-preserving & F is Covariant & F is coreflexive ) ; ::_thesis: F " is comp-preserving
set G = F " ;
A2: F " is Covariant by A1, Th38;
reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36;
A3: the ObjectMap of (F ") = 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 (F ") = (ff "") * ( the ObjectMap of F ") by A1, Def38;
A6: F is injective by A1, Def35;
then F is one-to-one by Def33;
then A7: the ObjectMap of F is one-to-one by Def6;
F is faithful by A6, Def33;
then A8: the MorphMap of F is "1-1" by Def30;
F is surjective by A1, Def35;
then F is full by Def34;
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" ) by Def32;
let o1, o2, o3 be object of B; :: according to FUNCTOR0:def_21 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex 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 ) )
assume A10: <^o1,o2^> <> {} ; ::_thesis: ( not <^o2,o3^> <> {} or for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex 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 ) )
then A11: <^(H . o1),(H . o2)^> <> {} by A2, Def18;
assume A12: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex 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 )
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 . ((F ") . o1)),(F . ((F ") . o3))^> <> {} by A1, Def18;
let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex 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 )
let g be Morphism of o2,o3; ::_thesis: ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex 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 )
reconsider K = F " 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 ((F ") . o1),((F ") . 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 ((F ") . o2),((F ") . o3) ;
take f9 ; ::_thesis: ex 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 )
take g9 ; ::_thesis: ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 )
thus f9 = (Morph-Map ((F "),o1,o2)) . f ; ::_thesis: ( g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 )
thus g9 = (Morph-Map ((F "),o2,o3)) . g ; ::_thesis: (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9
consider f99 being Morphism of (F . ((F ") . o1)),(F . ((F ") . o2)), g99 being Morphism of (F . ((F ") . o2)),(F . ((F ") . o3)) such that
A17: f99 = (Morph-Map (F,((F ") . o1),((F ") . o2))) . f9 and
A18: g99 = (Morph-Map (F,((F ") . o2),((F ") . o3))) . g9 and
A19: (Morph-Map (F,((F ") . o1),((F ") . o3))) . (g9 * f9) = g99 * f99 by A1, A11, A13, Def21;
A20: g = g99 by A1, A12, A18, Th40;
A21: f = f99 by A1, A10, A17, Th40;
A22: [((F ") . o1),((F ") . 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 (F ") by FUNCT_2:def_1;
dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2;
then [((F ") . o1),((F ") . o3)] in dom the MorphMap of F by ZFMISC_1:87;
then A25: Morph-Map (F,((F ") . o1),((F ") . o3)) is one-to-one by A8, MSUALG_3:def_2;
[((F ") . o1),((F ") . o3)] in dom the ObjectMap of F by A22, FUNCT_2:def_1;
then A26: ( the Arrows of B * the ObjectMap of F) . [((F ") . o1),((F ") . o3)] = the Arrows of B . ( the ObjectMap of F . (((F ") . o1),((F ") . o3))) by FUNCT_1:13
.= the Arrows of B . ((F . ((F ") . o1)),(F . ((F ") . o3))) by A1, Th22
.= <^(F . ((F ") . o1)),(F . ((F ") . o3))^> by ALTCAT_1:def_1 ;
Morph-Map (F,((F ") . o1),((F ") . o3)) is Function of ( the Arrows of A . [((F ") . o1),((F ") . o3)]),(( the Arrows of B * the ObjectMap of F) . [((F ") . o1),((F ") . o3)]) by A4, A22, PBOOLE:def_15;
then A27: dom (Morph-Map (F,((F ") . o1),((F ") . o3))) = the Arrows of A . (((F ") . o1),((F ") . o3)) by A16, A26, FUNCT_2:def_1
.= <^((F ") . o1),((F ") . o3)^> by ALTCAT_1:def_1 ;
A28: ( the Arrows of A * the ObjectMap of (F ")) . [o1,o3] = the Arrows of A . ( the ObjectMap of H . (o1,o3)) by A24, FUNCT_1:13
.= the Arrows of A . (((F ") . o1),((F ") . o3)) by A2, Th22
.= <^((F ") . o1),((F ") . o3)^> by ALTCAT_1:def_1 ;
the MorphMap of (F ") is ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4;
then Morph-Map ((F "),o1,o3) is Function of ( the Arrows of B . [o1,o3]),(( the Arrows of A * the ObjectMap of (F ")) . [o1,o3]) by A23, PBOOLE:def_15;
then A29: dom (Morph-Map ((F "),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 ((F "),o1,o3) = (ff "") . ( the ObjectMap of (F ") . (o1,o3)) by A3, A5, A24, FUNCT_1:13
.= (ff "") . [(H . o1),(H . o3)] by A2, Th22
.= (Morph-Map (F,((F ") . o1),((F ") . 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 (F ")) 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 . ((F ") . o1) = (F * H) . o1 by Th33
.= o1 by A32, MCART_1:7 ;
[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 . ((F ") . o2) = (F * H) . o2 by Th33
.= o2 by A34, MCART_1:7 ;
[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 . ((F ") . o3) = (F * H) . o3 by Th33
.= o3 by A36, MCART_1:7 ;
(Morph-Map ((F "),o1,o3)) . (g * f) in rng (Morph-Map ((F "),o1,o3)) by A14, A29, FUNCT_1:def_3;
then A38: (Morph-Map ((F "),o1,o3)) . (g * f) in dom (Morph-Map (F,((F ") . o1),((F ") . o3))) by A25, A30, FUNCT_1:33;
(Morph-Map (F,((F ") . o1),((F ") . o3))) . ((Morph-Map ((F "),o1,o3)) . (g * f)) = (Morph-Map (F,((F ") . o1),((F ") . o3))) . (g9 * f9) by A1, A14, A19, A20, A21, A33, A35, A37, Th40;
hence (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 by A25, A27, A38, FUNCT_1:def_4; ::_thesis: verum
end;
theorem Th43: :: FUNCTOR0:43
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive holds
F " is comp-reversing
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive holds
F " is comp-reversing
let F be reflexive feasible FunctorStr over A,B; ::_thesis: ( F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive implies F " is comp-reversing )
assume A1: ( F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive ) ; ::_thesis: F " is comp-reversing
set G = F " ;
A2: F " is Contravariant by A1, Th39;
reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36;
A3: the ObjectMap of (F ") = 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 (F ") = (ff "") * ( the ObjectMap of F ") by A1, Def38;
A6: F is injective by A1, Def35;
then F is one-to-one by Def33;
then A7: the ObjectMap of F is one-to-one by Def6;
F is faithful by A6, Def33;
then A8: the MorphMap of F is "1-1" by Def30;
F is surjective by A1, Def35;
then F is full by Def34;
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" ) by Def32;
let o1, o2, o3 be object of B; :: according to FUNCTOR0:def_22 ::_thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o2),((F ") . o1) ex 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 ) )
assume A10: <^o1,o2^> <> {} ; ::_thesis: ( not <^o2,o3^> <> {} or for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o2),((F ") . o1) ex 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 ) )
then A11: <^(H . o2),(H . o1)^> <> {} by A2, Def19;
assume A12: <^o2,o3^> <> {} ; ::_thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o2),((F ") . o1) ex 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 )
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 . ((F ") . o1)),(F . ((F ") . o3))^> <> {} by A1, Def19;
let f be Morphism of o1,o2; ::_thesis: for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o2),((F ") . o1) ex 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 )
let g be Morphism of o2,o3; ::_thesis: ex f9 being Morphism of ((F ") . o2),((F ") . o1) ex 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 )
reconsider K = F " 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 ((F ") . o2),((F ") . 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 ((F ") . o3),((F ") . o2) ;
take f9 ; ::_thesis: ex 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 )
take g9 ; ::_thesis: ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 )
thus f9 = (Morph-Map ((F "),o1,o2)) . f ; ::_thesis: ( g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 )
thus g9 = (Morph-Map ((F "),o2,o3)) . g ; ::_thesis: (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9
consider g99 being Morphism of (F . ((F ") . o2)),(F . ((F ") . o3)), f99 being Morphism of (F . ((F ") . o1)),(F . ((F ") . o2)) such that
A17: g99 = (Morph-Map (F,((F ") . o3),((F ") . o2))) . g9 and
A18: f99 = (Morph-Map (F,((F ") . o2),((F ") . o1))) . f9 and
A19: (Morph-Map (F,((F ") . o3),((F ") . o1))) . (f9 * g9) = g99 * f99 by A1, A11, A13, Def22;
A20: g = g99 by A1, A12, A17, Th41;
A21: f = f99 by A1, A10, A18, Th41;
A22: [((F ") . o3),((F ") . 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 (F ") by FUNCT_2:def_1;
dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2;
then [((F ") . o3),((F ") . o1)] in dom the MorphMap of F by ZFMISC_1:87;
then A25: Morph-Map (F,((F ") . o3),((F ") . o1)) is one-to-one by A8, MSUALG_3:def_2;
[((F ") . o3),((F ") . o1)] in dom the ObjectMap of F by A22, FUNCT_2:def_1;
then A26: ( the Arrows of B * the ObjectMap of F) . [((F ") . o3),((F ") . o1)] = the Arrows of B . ( the ObjectMap of F . (((F ") . o3),((F ") . o1))) by FUNCT_1:13
.= the Arrows of B . ((F . ((F ") . o1)),(F . ((F ") . o3))) by A1, Th23
.= <^(F . ((F ") . o1)),(F . ((F ") . o3))^> by ALTCAT_1:def_1 ;
Morph-Map (F,((F ") . o3),((F ") . o1)) is Function of ( the Arrows of A . [((F ") . o3),((F ") . o1)]),(( the Arrows of B * the ObjectMap of F) . [((F ") . o3),((F ") . o1)]) by A4, A22, PBOOLE:def_15;
then A27: dom (Morph-Map (F,((F ") . o3),((F ") . o1))) = the Arrows of A . (((F ") . o3),((F ") . o1)) by A16, A26, FUNCT_2:def_1
.= <^((F ") . o3),((F ") . o1)^> by ALTCAT_1:def_1 ;
A28: ( the Arrows of A * the ObjectMap of (F ")) . [o1,o3] = the Arrows of A . ( the ObjectMap of H . (o1,o3)) by A24, FUNCT_1:13
.= the Arrows of A . (((F ") . o3),((F ") . o1)) by A2, Th23
.= <^((F ") . o3),((F ") . o1)^> by ALTCAT_1:def_1 ;
the MorphMap of (F ") is ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4;
then Morph-Map ((F "),o1,o3) is Function of ( the Arrows of B . [o1,o3]),(( the Arrows of A * the ObjectMap of (F ")) . [o1,o3]) by A23, PBOOLE:def_15;
then A29: dom (Morph-Map ((F "),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 ((F "),o1,o3) = (ff "") . ( the ObjectMap of (F ") . (o1,o3)) by A3, A5, A24, FUNCT_1:13
.= (ff "") . [(H . o3),(H . o1)] by A2, Th23
.= (Morph-Map (F,((F ") . o3),((F ") . 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 (F ")) 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 . ((F ") . o1) = (F * H) . o1 by Th33
.= o1 by A32, MCART_1:7 ;
[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 . ((F ") . o2) = (F * H) . o2 by Th33
.= o2 by A34, MCART_1:7 ;
[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 . ((F ") . o3) = (F * H) . o3 by Th33
.= o3 by A36, MCART_1:7 ;
(Morph-Map ((F "),o1,o3)) . (g * f) in rng (Morph-Map ((F "),o1,o3)) by A14, A29, FUNCT_1:def_3;
then A38: (Morph-Map ((F "),o1,o3)) . (g * f) in dom (Morph-Map (F,((F ") . o3),((F ") . o1))) by A25, A30, FUNCT_1:33;
(Morph-Map (F,((F ") . o3),((F ") . o1))) . ((Morph-Map ((F "),o1,o3)) . (g * f)) = (Morph-Map (F,((F ") . o3),((F ") . o1))) . (f9 * g9) by A1, A14, A19, A20, A21, A33, A35, A37, Th41;
hence (Morph-Map ((F "),o1,o3)) . (g * f) = f9 * g9 by A25, A27, A38, FUNCT_1:def_4; ::_thesis: verum
end;
registration
let C1 be 1-sorted ;
let C2 be non empty 1-sorted ;
cluster Covariant -> reflexive for BimapStr over C1,C2;
coherence
for b1 being BimapStr over C1,C2 st b1 is Covariant holds
b1 is reflexive
proof
let M be BimapStr over C1,C2; ::_thesis: ( M is Covariant implies M is reflexive )
assume M is Covariant ; ::_thesis: M is reflexive
then the ObjectMap of M is Covariant by Def12;
then ex f being Function of the carrier of C1, the carrier of C2 st the ObjectMap of M = [:f,f:] by Def1;
hence the ObjectMap of M .: (id the carrier of C1) c= id the carrier of C2 by Th14; :: according to FUNCTOR0:def_8 ::_thesis: verum
end;
end;
registration
let C1 be 1-sorted ;
let C2 be non empty 1-sorted ;
cluster Contravariant -> reflexive for BimapStr over C1,C2;
coherence
for b1 being BimapStr over C1,C2 st b1 is Contravariant holds
b1 is reflexive
proof
let M be BimapStr over C1,C2; ::_thesis: ( M is Contravariant implies M is reflexive )
assume M is Contravariant ; ::_thesis: M is reflexive
then the ObjectMap of M is Contravariant by Def13;
then consider f being Function of the carrier of C1, the carrier of C2 such that
A1: the ObjectMap of M = ~ [:f,f:] by Def2;
(~ [: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; :: according to FUNCTOR0:def_8 ::_thesis: verum
end;
end;
theorem Th44: :: FUNCTOR0:44
for C1, C2 being 1-sorted
for M being BimapStr over C1,C2 st M is Covariant & M is onto holds
M is coreflexive
proof
let C1, C2 be 1-sorted ; ::_thesis: for M being BimapStr over C1,C2 st M is Covariant & M is onto holds
M is coreflexive
let M be BimapStr over C1,C2; ::_thesis: ( M is Covariant & M is onto implies M is coreflexive )
assume A1: ( M is Covariant & M is onto ) ; ::_thesis: M is coreflexive
then the ObjectMap of M is Covariant by Def12;
then consider f being Function of the carrier of C1, the carrier of C2 such that
A2: the ObjectMap of M = [:f,f:] by Def1;
the ObjectMap of M is onto by A1, Def7;
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; :: according to FUNCTOR0:def_9 ::_thesis: verum
end;
theorem Th45: :: FUNCTOR0:45
for C1, C2 being 1-sorted
for M being BimapStr over C1,C2 st M is Contravariant & M is onto holds
M is coreflexive
proof
let C1, C2 be 1-sorted ; ::_thesis: for M being BimapStr over C1,C2 st M is Contravariant & M is onto holds
M is coreflexive
let M be BimapStr over C1,C2; ::_thesis: ( M is Contravariant & M is onto implies M is coreflexive )
assume A1: ( M is Contravariant & M is onto ) ; ::_thesis: M is coreflexive
then the ObjectMap of M is Contravariant by Def13;
then consider f being Function of the carrier of C1, the carrier of C2 such that
A2: the ObjectMap of M = ~ [:f,f:] by Def2;
the ObjectMap of M is onto by A1, Def7;
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; :: according to FUNCTOR0:def_9 ::_thesis: verum
end;
registration
let C1 be non empty transitive with_units AltCatStr ;
let C2 be non empty with_units AltCatStr ;
cluster covariant -> reflexive for Functor of C1,C2;
coherence
for b1 being Functor of C1,C2 st b1 is covariant holds
b1 is reflexive
proof
let F be Functor of C1,C2; ::_thesis: ( F is covariant implies F is reflexive )
assume F is covariant ; ::_thesis: F is reflexive
then reconsider F = F as Covariant FunctorStr over C1,C2 by Def26;
F is reflexive ;
hence F is reflexive ; ::_thesis: verum
end;
end;
registration
let C1 be non empty transitive with_units AltCatStr ;
let C2 be non empty with_units AltCatStr ;
cluster contravariant -> reflexive for Functor of C1,C2;
coherence
for b1 being Functor of C1,C2 st b1 is contravariant holds
b1 is reflexive
proof
let F be Functor of C1,C2; ::_thesis: ( F is contravariant implies F is reflexive )
assume F is contravariant ; ::_thesis: F is reflexive
then reconsider F = F as Contravariant FunctorStr over C1,C2 by Def27;
F is reflexive ;
hence F is reflexive ; ::_thesis: verum
end;
end;
theorem Th46: :: FUNCTOR0:46
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 st F is covariant & F is onto holds
F is coreflexive
proof
let C1 be non empty transitive with_units AltCatStr ; ::_thesis: for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 st F is covariant & F is onto holds
F is coreflexive
let C2 be non empty with_units AltCatStr ; ::_thesis: for F being Functor of C1,C2 st F is covariant & F is onto holds
F is coreflexive
let F be Functor of C1,C2; ::_thesis: ( F is covariant & F is onto implies F is coreflexive )
assume A1: ( F is covariant & F is onto ) ; ::_thesis: F is coreflexive
then F is Covariant by Def26;
hence F is coreflexive by A1, Th44; ::_thesis: verum
end;
theorem Th47: :: FUNCTOR0:47
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 st F is contravariant & F is onto holds
F is coreflexive
proof
let C1 be non empty transitive with_units AltCatStr ; ::_thesis: for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 st F is contravariant & F is onto holds
F is coreflexive
let C2 be non empty with_units AltCatStr ; ::_thesis: for F being Functor of C1,C2 st F is contravariant & F is onto holds
F is coreflexive
let F be Functor of C1,C2; ::_thesis: ( F is contravariant & F is onto implies F is coreflexive )
assume A1: ( F is contravariant & F is onto ) ; ::_thesis: F is coreflexive
then F is Contravariant by Def27;
hence F is coreflexive by A1, Th45; ::_thesis: verum
end;
theorem Th48: :: FUNCTOR0:48
for A, B being non empty transitive with_units AltCatStr
for F being covariant Functor of A,B st F is bijective holds
ex G being Functor of B,A st
( G = F " & G is bijective & G is covariant )
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being covariant Functor of A,B st F is bijective holds
ex G being Functor of B,A st
( G = F " & G is bijective & G is covariant )
let F be covariant Functor of A,B; ::_thesis: ( F is bijective implies ex G being Functor of B,A st
( G = F " & G is bijective & G is covariant ) )
assume A1: F is bijective ; ::_thesis: ex G being Functor of B,A st
( G = F " & G is bijective & G is covariant )
then F is injective by Def35;
then F is one-to-one by Def33;
then A2: the ObjectMap of F is one-to-one by Def6;
A3: F is feasible by Def25;
then A4: ( F " is bijective & F " is feasible ) by A1, Th35;
A5: F is id-preserving by Def25;
A6: F is comp-preserving by Def26;
F is surjective by A1, Def35;
then A7: F is onto by Def34;
then A8: the ObjectMap of F is onto by Def7;
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 by Def12;
then consider f being Function of the carrier of A, the carrier of B such that
A12: the ObjectMap of F = [:f,f:] by Def1;
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, FUNCT_2:def_3;
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 ; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: the ObjectMap of (F ") = [:g,g:]
[:f,f:] " = [:g,g:] by A13, Th6;
hence the ObjectMap of (F ") = [:g,g:] by A1, A12, Def38; ::_thesis: verum
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 ; ::_thesis: ( G = F " & G is bijective & G is covariant )
thus G = F " ; ::_thesis: ( G is bijective & G is covariant )
thus G is bijective by A1, A3, Th35; ::_thesis: G is covariant
thus G is Covariant by A11; :: according to FUNCTOR0:def_26 ::_thesis: G is comp-preserving
thus G is comp-preserving by A1, A3, A6, A9, A10, Th42; ::_thesis: verum
end;
theorem Th49: :: FUNCTOR0:49
for A, B being non empty transitive with_units AltCatStr
for F being contravariant Functor of A,B st F is bijective holds
ex G being Functor of B,A st
( G = F " & G is bijective & G is contravariant )
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being contravariant Functor of A,B st F is bijective holds
ex G being Functor of B,A st
( G = F " & G is bijective & G is contravariant )
let F be contravariant Functor of A,B; ::_thesis: ( F is bijective implies ex G being Functor of B,A st
( G = F " & G is bijective & G is contravariant ) )
assume A1: F is bijective ; ::_thesis: ex G being Functor of B,A st
( G = F " & G is bijective & G is contravariant )
then F is injective by Def35;
then F is one-to-one by Def33;
then A2: the ObjectMap of F is one-to-one by Def6;
A3: F is feasible by Def25;
then A4: ( F " is bijective & F " is feasible ) by A1, Th35;
A5: F is id-preserving by Def25;
A6: F is comp-reversing by Def27;
F is surjective by A1, Def35;
then A7: F is onto by Def34;
then A8: the ObjectMap of F is onto by Def7;
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 by Def13;
then consider f being Function of the carrier of A, the carrier of B such that
A12: the ObjectMap of F = ~ [:f,f:] by Def2;
[: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:] by FUNCT_2:def_3;
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 ; :: according to FUNCTOR0:def_2,FUNCTOR0:def_13 ::_thesis: the ObjectMap of (F ") = ~ [:g,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 ; ::_thesis: verum
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 ; ::_thesis: ( G = F " & G is bijective & G is contravariant )
thus G = F " ; ::_thesis: ( G is bijective & G is contravariant )
thus G is bijective by A1, A3, Th35; ::_thesis: G is contravariant
thus G is Contravariant by A11; :: according to FUNCTOR0:def_27 ::_thesis: G is comp-reversing
thus G is comp-reversing by A1, A3, A6, A9, A10, Th43; ::_thesis: verum
end;
definition
let A, B be non empty transitive with_units AltCatStr ;
predA,B are_isomorphic means :: FUNCTOR0:def 39
ex F being Functor of A,B st
( F is bijective & F is covariant );
reflexivity
for A being non empty transitive with_units AltCatStr ex F being Functor of A,A st
( F is bijective & F is covariant )
proof
let A be non empty transitive with_units AltCatStr ; ::_thesis: ex F being Functor of A,A st
( F is bijective & F is covariant )
take id A ; ::_thesis: ( id A is bijective & id A is covariant )
thus ( id A is bijective & id A is covariant ) ; ::_thesis: verum
end;
symmetry
for A, B being non empty transitive with_units AltCatStr st ex F being Functor of A,B st
( F is bijective & F is covariant ) holds
ex F being Functor of B,A st
( F is bijective & F is covariant )
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: ( ex F being Functor of A,B st
( F is bijective & F is covariant ) implies ex F being Functor of B,A st
( F is bijective & F is covariant ) )
given F being Functor of A,B such that A1: ( F is bijective & F is covariant ) ; ::_thesis: ex F being Functor of B,A st
( F is bijective & F is covariant )
consider G being Functor of B,A such that
G = F " and
A2: ( G is bijective & G is covariant ) by A1, Th48;
take G ; ::_thesis: ( G is bijective & G is covariant )
thus ( G is bijective & G is covariant ) by A2; ::_thesis: verum
end;
predA,B are_anti-isomorphic means :: FUNCTOR0:def 40
ex F being Functor of A,B st
( F is bijective & F is contravariant );
symmetry
for A, B being non empty transitive with_units AltCatStr st ex F being Functor of A,B st
( F is bijective & F is contravariant ) holds
ex F being Functor of B,A st
( F is bijective & F is contravariant )
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: ( ex F being Functor of A,B st
( F is bijective & F is contravariant ) implies ex F being Functor of B,A st
( F is bijective & F is contravariant ) )
given F being Functor of A,B such that A3: ( F is bijective & F is contravariant ) ; ::_thesis: ex F being Functor of B,A st
( F is bijective & F is contravariant )
consider G being Functor of B,A such that
G = F " and
A4: ( G is bijective & G is contravariant ) by A3, Th49;
take G ; ::_thesis: ( G is bijective & G is contravariant )
thus ( G is bijective & G is contravariant ) by A4; ::_thesis: verum
end;
end;
:: deftheorem defines are_isomorphic FUNCTOR0:def_39_:_
for A, B being non empty transitive with_units AltCatStr holds
( A,B are_isomorphic iff ex F being Functor of A,B st
( F is bijective & F is covariant ) );
:: deftheorem defines are_anti-isomorphic FUNCTOR0:def_40_:_
for A, B being non empty transitive with_units AltCatStr holds
( A,B are_anti-isomorphic iff ex F being Functor of A,B st
( F is bijective & F is contravariant ) );