begin
scheme
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,o'],F5(o,o')] where o, o' is Element of F1() : P1[o,o'] }
and A2:
P1[
F3(),
F4()]
theorem Th1:
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
begin
:: deftheorem FUNCTOR0:def 1 :
canceled;
:: deftheorem Def2 defines Covariant FUNCTOR0:def 2 :
:: deftheorem Def3 defines Contravariant FUNCTOR0:def 3 :
theorem Th16:
theorem
begin
:: deftheorem Def4 defines MSUnTrans FUNCTOR0:def 4 :
:: deftheorem Def5 defines MSUnTrans FUNCTOR0:def 5 :
theorem Th18:
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;
~redefine func ~ F -> MSUnTrans of
[:f,f:],
~ A,
~ B;
coherence
~ F is MSUnTrans of [:f,f:], ~ A, ~ B
end;
theorem Th19:
theorem Th20:
begin
:: deftheorem defines . FUNCTOR0:def 6 :
:: deftheorem Def7 defines one-to-one FUNCTOR0:def 7 :
:: deftheorem Def8 defines onto FUNCTOR0:def 8 :
:: deftheorem Def9 defines reflexive FUNCTOR0:def 9 :
:: deftheorem Def10 defines coreflexive FUNCTOR0:def 10 :
:: deftheorem Def11 defines reflexive FUNCTOR0:def 11 :
theorem Th21:
:: deftheorem Def12 defines feasible FUNCTOR0:def 12 :
:: deftheorem Def13 defines Covariant FUNCTOR0:def 13 :
:: deftheorem Def14 defines Contravariant FUNCTOR0:def 14 :
:: deftheorem defines Morph-Map FUNCTOR0:def 15 :
definition
let C1,
C2 be non
empty AltGraph ;
let F be
Covariant FunctorStr of
C1,
C2;
let o1,
o2 be
object of ;
Morph-Mapredefine 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)^>
end;
definition
let C1,
C2 be non
empty AltGraph ;
let F be
Covariant FunctorStr of
C1,
C2;
let o1,
o2 be
object of ;
assume that A1:
<^o1,o2^> <> {}
and A2:
<^(F . o1),(F . o2)^> <> {}
;
let m be
Morphism of ,;
func F . m -> Morphism of ,
equals :
Def16:
(Morph-Map F,o1,o2) . m;
coherence
(Morph-Map F,o1,o2) . m is Morphism of ,
end;
:: deftheorem Def16 defines . FUNCTOR0:def 16 :
definition
let C1,
C2 be non
empty AltGraph ;
let F be
Contravariant FunctorStr of
C1,
C2;
let o1,
o2 be
object of ;
Morph-Mapredefine 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)^>
end;
definition
let C1,
C2 be non
empty AltGraph ;
let F be
Contravariant FunctorStr of
C1,
C2;
let o1,
o2 be
object of ;
assume that A1:
<^o1,o2^> <> {}
and A2:
<^(F . o2),(F . o1)^> <> {}
;
let m be
Morphism of ,;
func F . m -> Morphism of ,
equals :
Def17:
(Morph-Map F,o1,o2) . m;
coherence
(Morph-Map F,o1,o2) . m is Morphism of ,
end;
:: deftheorem Def17 defines . FUNCTOR0:def 17 :
definition
let C1,
C2 be non
empty AltGraph ;
let o be
object of ;
assume A1:
<^o,o^> <> {}
;
let m be
Morphism of ,;
func C1 --> m -> strict FunctorStr of
C1,
C2 means :
Def18:
( 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 : verum } );
existence
ex b1 being strict FunctorStr of 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 : verum } )
uniqueness
for b1, b2 being strict FunctorStr of 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 : 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 : verum } holds
b1 = b2
;
end;
:: deftheorem Def18 defines --> FUNCTOR0:def 18 :
for
C1,
C2 being non
empty AltGraph for
o being
object of st
<^o,o^> <> {} holds
for
m being
Morphism of ,
for
b5 being
strict FunctorStr of
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 : verum } ) );
theorem Th22:
theorem Th23:
:: deftheorem Def19 defines feasible FUNCTOR0:def 19 :
theorem Th24:
:: deftheorem Def20 defines feasible FUNCTOR0:def 20 :
:: deftheorem Def21 defines id-preserving FUNCTOR0:def 21 :
theorem Th25:
definition
let C1,
C2 be non
empty AltCatStr ;
let F be
FunctorStr of
C1,
C2;
attr F is
comp-preserving means :
Def22:
for
o1,
o2,
o3 being
object of st
<^o1,o2^> <> {} &
<^o2,o3^> <> {} holds
for
f being
Morphism of ,
for
g being
Morphism of , ex
f' being
Morphism of , ex
g' being
Morphism of , st
(
f' = (Morph-Map F,o1,o2) . f &
g' = (Morph-Map F,o2,o3) . g &
(Morph-Map F,o1,o3) . (g * f) = g' * f' );
end;
:: deftheorem Def22 defines comp-preserving FUNCTOR0:def 22 :
for
C1,
C2 being non
empty AltCatStr for
F being
FunctorStr of
C1,
C2 holds
(
F is
comp-preserving iff for
o1,
o2,
o3 being
object of st
<^o1,o2^> <> {} &
<^o2,o3^> <> {} holds
for
f being
Morphism of ,
for
g being
Morphism of , ex
f' being
Morphism of , ex
g' being
Morphism of , st
(
f' = (Morph-Map F,o1,o2) . f &
g' = (Morph-Map F,o2,o3) . g &
(Morph-Map F,o1,o3) . (g * f) = g' * f' ) );
definition
let C1,
C2 be non
empty AltCatStr ;
let F be
FunctorStr of
C1,
C2;
attr F is
comp-reversing means :
Def23:
for
o1,
o2,
o3 being
object of st
<^o1,o2^> <> {} &
<^o2,o3^> <> {} holds
for
f being
Morphism of ,
for
g being
Morphism of , ex
f' being
Morphism of , ex
g' being
Morphism of , st
(
f' = (Morph-Map F,o1,o2) . f &
g' = (Morph-Map F,o2,o3) . g &
(Morph-Map F,o1,o3) . (g * f) = f' * g' );
end;
:: deftheorem Def23 defines comp-reversing FUNCTOR0:def 23 :
for
C1,
C2 being non
empty AltCatStr for
F being
FunctorStr of
C1,
C2 holds
(
F is
comp-reversing iff for
o1,
o2,
o3 being
object of st
<^o1,o2^> <> {} &
<^o2,o3^> <> {} holds
for
f being
Morphism of ,
for
g being
Morphism of , ex
f' being
Morphism of , ex
g' being
Morphism of , st
(
f' = (Morph-Map F,o1,o2) . f &
g' = (Morph-Map F,o2,o3) . g &
(Morph-Map F,o1,o3) . (g * f) = f' * g' ) );
definition
let C1 be non
empty transitive AltCatStr ;
let C2 be non
empty reflexive AltCatStr ;
let F be
feasible Covariant FunctorStr of
C1,
C2;
redefine attr F is
comp-preserving means
for
o1,
o2,
o3 being
object of st
<^o1,o2^> <> {} &
<^o2,o3^> <> {} holds
for
f being
Morphism of ,
for
g being
Morphism of , holds
F . (g * f) = (F . g) * (F . f);
compatibility
( F is comp-preserving iff for o1, o2, o3 being object of st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of ,
for g being Morphism of , holds F . (g * f) = (F . g) * (F . f) )
end;
:: deftheorem defines comp-preserving FUNCTOR0:def 24 :
definition
let C1 be non
empty transitive AltCatStr ;
let C2 be non
empty reflexive AltCatStr ;
let F be
feasible Contravariant FunctorStr of
C1,
C2;
redefine attr F is
comp-reversing means
for
o1,
o2,
o3 being
object of st
<^o1,o2^> <> {} &
<^o2,o3^> <> {} holds
for
f being
Morphism of ,
for
g being
Morphism of , holds
F . (g * f) = (F . f) * (F . g);
compatibility
( F is comp-reversing iff for o1, o2, o3 being object of st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of ,
for g being Morphism of , holds F . (g * f) = (F . f) * (F . g) )
end;
:: deftheorem defines comp-reversing FUNCTOR0:def 25 :
theorem Th26:
theorem Th27:
:: deftheorem Def26 defines Functor FUNCTOR0:def 26 :
:: deftheorem Def27 defines covariant FUNCTOR0:def 27 :
:: deftheorem Def28 defines contravariant FUNCTOR0:def 28 :
:: deftheorem Def29 defines incl FUNCTOR0:def 29 :
:: deftheorem Def30 defines id FUNCTOR0:def 30 :
theorem Th28:
theorem Th29:
:: deftheorem Def31 defines faithful FUNCTOR0:def 31 :
:: deftheorem Def32 defines full FUNCTOR0:def 32 :
:: deftheorem Def33 defines full FUNCTOR0:def 33 :
:: deftheorem Def34 defines injective FUNCTOR0:def 34 :
:: deftheorem Def35 defines surjective FUNCTOR0:def 35 :
:: deftheorem Def36 defines bijective FUNCTOR0:def 36 :
theorem Th30:
theorem Th31:
theorem Th32:
begin
:: deftheorem Def37 defines * FUNCTOR0:def 37 :
theorem
theorem Th34:
theorem Th35:
:: deftheorem defines | FUNCTOR0:def 38 :
begin
definition
let A,
B be non
empty AltGraph ;
let F be
FunctorStr of
A,
B;
assume A1:
F is
bijective
;
func F " -> strict FunctorStr of
B,
A means :
Def39:
( 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 of 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 " ) ) )
uniqueness
for b1, b2 being strict FunctorStr of 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 Def39 defines " FUNCTOR0:def 39 :
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
definition
let A,
B be non
empty transitive with_units AltCatStr ;
pred A,
B are_isomorphic means
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 )
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 )
pred A,
B are_anti-isomorphic means
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 )
end;
:: deftheorem defines are_isomorphic FUNCTOR0:def 40 :
:: deftheorem defines are_anti-isomorphic FUNCTOR0:def 41 :