:: FUNCTOR0 semantic presentation

scheme :: FUNCTOR0:sch 1
ValOnPair{ F₁() -> non empty set , F₂() -> Function, F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅( set , set ) -> set , P₁[ set , set ] } :

F₂() . F₃(),F₄() = F₅(F₃(),F₄())

provided

A1: F₂() = { [[o,o'],F₅(o,o')] where o, o' is Element of F₁() : P₁[o,o'] } and
A2: P₁[F₃(),F₄()]

proof end;

theorem Th1: :: FUNCTOR0:1

for A being set holds {} is Function of A, {}

proof end;

theorem :: FUNCTOR0:2

canceled;

theorem Th3: :: FUNCTOR0:3

for I being set
for M being ManySortedSet of I holds M * (id I) = M

proof end;

registration

let f be empty Function;
cluster ~ f -> empty ;
coherence

proof end;

let g be Function;
cluster [:f,g:] -> empty ;
coherence

proof end;

cluster [:g,f:] -> empty ;
coherence

proof end;

end;

theorem Th4: :: FUNCTOR0:4

for A being set
for f being Function holds f .: (id A) = (~ f) .: (id A)

proof end;

theorem Th5: :: FUNCTOR0:5

for X, Y being set
for f being Function of X,Y holds
( f is onto iff [:f,f:] is onto )

proof end;

registration

let f be Function-yielding Function;
cluster ~ f -> Function-yielding ;
coherence ;

end;

theorem Th6: :: FUNCTOR0:6

for A, B, a being set holds ~ ([:A,B:] --> a) = [:B,A:] --> a

proof end;

theorem Th7: :: FUNCTOR0:7

for f, g being Function st f is one-to-one & g is one-to-one holds
[:f,g:] " = [:(f " ),(g " ):]

proof end;

theorem Th8: :: FUNCTOR0:8

for f being Function st [:f,f:] is one-to-one holds
f is one-to-one

proof end;

theorem Th9: :: FUNCTOR0:9

for f being Function st f is one-to-one holds
~ f is one-to-one

proof end;

theorem Th10: :: FUNCTOR0:10

for f, g being Function st ~ [:f,g:] is one-to-one holds
[:g,f:] is one-to-one

proof end;

theorem Th11: :: FUNCTOR0:11

for f, g being Function st f is one-to-one & g is one-to-one holds
(~ [:f,g:]) " = ~ ([:g,f:] " )

proof end;

theorem Th12: :: FUNCTOR0:12

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 end;

theorem Th13: :: FUNCTOR0:13

for F, G being Function-yielding Function
for f being Function holds (G ** F) * f = (G * f) ** (F * f)

proof 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

proof end;

end;

theorem Th14: :: FUNCTOR0:14

for A, B, C being set
for f being Function of [:A,B:],C st ~ f is onto holds
f is onto

proof end;

theorem Th15: :: FUNCTOR0:15

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 end;

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;
canceled;
attr f is Covariant means :Def2: :: FUNCTOR0:def 2
ex g being Function of A,B st f = [:g,g:];
attr f is Contravariant means :Def3: :: FUNCTOR0:def 3
ex g being Function of A,B st f = ~ [:g,g:];

end;

:: deftheorem FUNCTOR0:def 1 :

:: deftheorem Def2 defines Covariant FUNCTOR0:def 2 :

:: deftheorem Def3 defines Contravariant FUNCTOR0:def 3 :

theorem Th16: :: FUNCTOR0:16

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 end;

registration

let A, B be set ;
cluster Covariant Contravariant Relation of [:A,A:],[:B,B:];
existence

proof end;

end;

theorem :: FUNCTOR0:17

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 end;

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 :Def4: :: FUNCTOR0:def 4
ex I2' being non empty set ex B' being ManySortedSet of I2' ex f' being Function of I1,I2' st
( f = f' & B = B' & it is ManySortedFunction of A,B' * f' ) if I2 <> {}
otherwise it = [0] I1;
existence

proof end;

consistency ;

end;

:: deftheorem Def4 defines MSUnTrans FUNCTOR0:def 4 :

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 :Def5: :: FUNCTOR0:def 5
it is ManySortedFunction of A,B * f;
compatibility

proof end;

end;

:: deftheorem Def5 defines MSUnTrans FUNCTOR0:def 5 :

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 MSUnTrans of f,A,B;
coherence

proof end;

end;

theorem Th18: :: FUNCTOR0:18

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 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

proof end;

end;

theorem Th19: :: FUNCTOR0:19

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
{ [o',((A . o') --> m)] where o' is Element of I1 : verum } is MSUnTrans of f,A,B

proof end;

theorem Th20: :: FUNCTOR0:20

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 end;

definition

let C1, C2 be 1-sorted ;
attr c₃ is strict;
struct BimapStr of C1,C2 -> ;
aggr BimapStr(# ObjectMap #) -> BimapStr of C1,C2;
sel ObjectMap c₃ -> bifunction of the carrier of C1,the carrier of C2;

end;

definition

let C1, C2 be non empty AltGraph ;
let F be BimapStr of C1,C2;
let o be object of C1;
func F . o -> object of C2 equals :: FUNCTOR0:def 6
(the ObjectMap of F . o,o) `1 ;
coherence by MCART_1:10;

end;

:: deftheorem defines . FUNCTOR0:def 6 :

definition

let A, B be 1-sorted ;
let F be BimapStr of A,B;
attr F is one-to-one means :Def7: :: FUNCTOR0:def 7
the ObjectMap of F is one-to-one;
attr F is onto means :Def8: :: FUNCTOR0:def 8
the ObjectMap of F is onto;
attr F is reflexive means :Def9: :: FUNCTOR0:def 9
the ObjectMap of F .: (id the carrier of A) c= id the carrier of B;
attr F is coreflexive means :Def10: :: FUNCTOR0:def 10
id the carrier of B c= the ObjectMap of F .: (id the carrier of A);

end;

:: 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 :

definition

let A, B be non empty AltGraph ;
let F be BimapStr of A,B;
redefine attr F is reflexive means :Def11: :: FUNCTOR0:def 11
for o being object of A holds the ObjectMap of F . o,o = [(F . o),(F . o)];
compatibility

proof end;

end;

:: deftheorem Def11 defines reflexive FUNCTOR0:def 11 :

theorem Th21: :: FUNCTOR0:21

for A, B being non empty reflexive AltGraph
for F being BimapStr of A,B st F is coreflexive holds
for o being object of B ex o' being object of A st F . o' = o

proof end;

definition

let C1, C2 be non empty AltGraph ;
let F be BimapStr of C1,C2;
attr F is feasible means :Def12: :: FUNCTOR0:def 12
for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
the Arrows of C2 . (the ObjectMap of F . o1,o2) <> {} ;

end;

:: deftheorem Def12 defines feasible FUNCTOR0:def 12 :

definition

let C1, C2 be AltGraph ;
attr c₃ is strict;
struct FunctorStr of C1,C2 -> BimapStr of C1,C2;
aggr FunctorStr(# ObjectMap, MorphMap #) -> FunctorStr of C1,C2;
sel MorphMap c₃ -> MSUnTrans of the ObjectMap of c₃,the Arrows of C1,the Arrows of C2;

end;

definition

let C1, C2 be 1-sorted ;
let IT be BimapStr of C1,C2;
attr IT is Covariant means :Def13: :: FUNCTOR0:def 13
the ObjectMap of IT is Covariant;
attr IT is Contravariant means :Def14: :: FUNCTOR0:def 14
the ObjectMap of IT is Contravariant;

end;

:: deftheorem Def13 defines Covariant FUNCTOR0:def 13 :

:: deftheorem Def14 defines Contravariant FUNCTOR0:def 14 :

registration

let C1, C2 be AltGraph ;
cluster Covariant FunctorStr of C1,C2;
existence

proof end;

cluster Contravariant FunctorStr of C1,C2;
existence

proof end;

end;

definition

let C1, C2 be AltGraph ;
let F be FunctorStr of C1,C2;
let o1, o2 be object of C1;
func Morph-Map F,o1,o2 -> set equals :: FUNCTOR0:def 15
the MorphMap of F . o1,o2;
correctness ;

end;

:: deftheorem defines Morph-Map FUNCTOR0:def 15 :

registration

let C1, C2 be AltGraph ;
let F be FunctorStr of C1,C2;
let o1, o2 be object of C1;
cluster Morph-Map F,o1,o2 -> Relation-like Function-like ;
coherence

proof end;

end;

definition

let C1, C2 be non empty AltGraph ;
let F be Covariant FunctorStr of 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

proof end;

end;

definition

let C1, C2 be non empty AltGraph ;
let F be Covariant FunctorStr of C1,C2;
let o1, o2 be object of C1;
assume A1: ( <^o1,o2^> <> {} & <^(F . o1),(F . o2)^> <> {} ) ;
let m be Morphism of o1,o2;
func F . m -> Morphism of (F . o1),(F . o2) equals :Def16: :: FUNCTOR0:def 16
(Morph-Map F,o1,o2) . m;
coherence

proof end;

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 C1;
:: original: Morph-Map
redefine func Morph-Map F,o1,o2 -> Function of <^o1,o2^>,<^(F . o2),(F . o1)^>;
coherence

proof end;

end;

definition

let C1, C2 be non empty AltGraph ;
let F be Contravariant FunctorStr of C1,C2;
let o1, o2 be object of C1;
assume A1: ( <^o1,o2^> <> {} & <^(F . o2),(F . o1)^> <> {} ) ;
let m be Morphism of o1,o2;
func F . m -> Morphism of (F . o2),(F . o1) equals :Def17: :: FUNCTOR0:def 17
(Morph-Map F,o1,o2) . m;
coherence

proof end;

end;

:: deftheorem Def17 defines . FUNCTOR0:def 17 :

definition

let C1, C2 be non empty AltGraph ;
let o be object of C2;
assume A1: <^o,o^> <> {} ;
let m be Morphism of o,o;
func C1 --> m -> strict FunctorStr of C1,C2 means :Def18: :: FUNCTOR0:def 18
( 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

proof end;

uniqueness ;

end;

:: deftheorem Def18 defines --> FUNCTOR0:def 18 :

theorem Th22: :: FUNCTOR0:22

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 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;
cluster C1 --> m -> feasible strict Covariant Contravariant ;
coherence

proof end;

end;

registration

let C1 be non empty AltGraph ;
let C2 be non empty reflexive AltGraph ;
cluster feasible Covariant Contravariant FunctorStr of C1,C2;
existence

proof end;

end;

theorem Th23: :: FUNCTOR0:23

for C1, C2 being non empty AltGraph
for F being Covariant FunctorStr of C1,C2
for o1, o2 being object of C1 holds the ObjectMap of F . o1,o2 = [(F . o1),(F . o2)]

proof end;

definition

let C1, C2 be non empty AltGraph ;
let F be Covariant FunctorStr of C1,C2;
redefine attr F is feasible means :Def19: :: FUNCTOR0:def 19
for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {} ;
compatibility

proof end;

end;

:: deftheorem Def19 defines feasible FUNCTOR0:def 19 :

theorem Th24: :: FUNCTOR0:24

for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr of C1,C2
for o1, o2 being object of C1 holds the ObjectMap of F . o1,o2 = [(F . o2),(F . o1)]

proof end;

definition

let C1, C2 be non empty AltGraph ;
let F be Contravariant FunctorStr of C1,C2;
redefine attr F is feasible means :Def20: :: FUNCTOR0:def 20
for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {} ;
compatibility

proof end;

end;

:: deftheorem Def20 defines feasible FUNCTOR0:def 20 :

registration

let C1, C2 be AltGraph ;
let F be FunctorStr of C1,C2;
cluster the MorphMap of F -> Function-yielding ;
coherence ;

end;

registration

cluster non empty reflexive AltCatStr ;
existence

proof end;

end;

definition

let C1, C2 be non empty with_units AltCatStr ;
let F be FunctorStr of C1,C2;
attr F is id-preserving means :Def21: :: FUNCTOR0:def 21
for o being object of C1 holds (Morph-Map F,o,o) . (idm o) = idm (F . o);

end;

:: deftheorem Def21 defines id-preserving FUNCTOR0:def 21 :

theorem Th25: :: FUNCTOR0:25

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, o' being object of C1
for f being Morphism of o,o' st <^o,o'^> <> {} holds
(Morph-Map (C1 --> m),o,o') . f = m

proof end;

registration

cluster non empty with_units -> non empty reflexive AltCatStr ;
coherence

proof end;

end;

registration

let C1, C2 be non empty with_units AltCatStr ;
let o2 be object of C2;
cluster C1 --> (idm o2) -> feasible strict Covariant Contravariant id-preserving ;
coherence

proof end;

end;

registration

let C1 be non empty AltGraph ;
let C2 be non empty reflexive AltGraph ;
let o2 be object of C2;
let m be Morphism of o2,o2;
cluster C1 --> m -> reflexive feasible strict Covariant Contravariant ;
coherence

proof end;

end;

registration

let C1 be non empty AltGraph ;
let C2 be non empty reflexive AltGraph ;
cluster reflexive feasible FunctorStr of C1,C2;
existence

proof end;

end;

registration

let C1, C2 be non empty with_units AltCatStr ;
cluster reflexive feasible strict id-preserving FunctorStr of C1,C2;
existence

proof end;

end;

definition

let C1, C2 be non empty AltCatStr ;
let F be FunctorStr of C1,C2;
attr F is comp-preserving 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 f' being Morphism of (F . o1),(F . o2) ex g' being Morphism of (F . o2),(F . o3) 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 :

definition

let C1, C2 be non empty AltCatStr ;
let F be FunctorStr of C1,C2;
attr F is comp-reversing means :Def23: :: 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 ex f' being Morphism of (F . o2),(F . o1) ex g' being Morphism of (F . o3),(F . o2) 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 :

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 :: 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 . g) * (F . f);
compatibility

proof end;

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 :: FUNCTOR0:def 25
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

proof end;

end;

:: deftheorem defines comp-reversing FUNCTOR0:def 25 :

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 F being feasible Covariant FunctorStr of C1,C2 st F = C1 --> m holds
for o, o' being object of C1
for f being Morphism of o,o' st <^o,o'^> <> {} holds
F . f = m

proof end;

theorem Th27: :: FUNCTOR0:27

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, o' being object of C1
for f being Morphism of o,o' st <^o,o'^> <> {} holds
(C1 --> m) . f = m

proof end;

registration

let C1 be non empty transitive AltCatStr ;
let C2 be non empty with_units AltCatStr ;
let o be object of C2;
cluster C1 --> (idm o) -> reflexive feasible strict Covariant Contravariant comp-preserving comp-reversing ;
coherence

proof 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 of C1,C2 means :Def26: :: FUNCTOR0:def 26
( it is feasible & it is id-preserving & ( ( it is Covariant & it is comp-preserving ) or ( it is Contravariant & it is comp-reversing ) ) );
existence

proof end;

end;

:: deftheorem Def26 defines Functor FUNCTOR0:def 26 :

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;
attr F is covariant means :Def27: :: FUNCTOR0:def 27
( F is Covariant & F is comp-preserving );
attr F is contravariant means :Def28: :: FUNCTOR0:def 28
( F is Contravariant & F is comp-reversing );

end;

:: deftheorem Def27 defines covariant FUNCTOR0:def 27 :

:: deftheorem Def28 defines contravariant FUNCTOR0:def 28 :

definition

let A be AltCatStr ;
let B be SubCatStr of A;
func incl B -> strict FunctorStr of B,A means :Def29: :: FUNCTOR0:def 29
( the ObjectMap of it = id [:the carrier of B,the carrier of B:] & the MorphMap of it = id the Arrows of B );
existence

proof end;

correctness ;

end;

:: deftheorem Def29 defines incl FUNCTOR0:def 29 :

definition

let A be AltGraph ;
func id A -> strict FunctorStr of A,A means :Def30: :: FUNCTOR0:def 30
( the ObjectMap of it = id [:the carrier of A,the carrier of A:] & the MorphMap of it = id the Arrows of A );
existence

proof end;

correctness ;

end;

:: deftheorem Def30 defines id FUNCTOR0:def 30 :

registration

let A be AltCatStr ;
let B be SubCatStr of A;
cluster incl B -> strict Covariant ;
coherence

proof end;

end;

theorem Th28: :: FUNCTOR0:28

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 end;

theorem Th29: :: FUNCTOR0:29

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 end;

registration

let A be non empty AltCatStr ;
let B be non empty SubCatStr of A;
cluster incl B -> feasible strict Covariant ;
coherence

proof end;

end;

definition

let A, B be AltGraph ;
let F be FunctorStr of A,B;
attr F is faithful means :Def31: :: FUNCTOR0:def 31
the MorphMap of F is "1-1";

end;

:: deftheorem Def31 defines faithful FUNCTOR0:def 31 :

definition

let A, B be AltGraph ;
let F be FunctorStr of A,B;
attr F is full means :Def32: :: FUNCTOR0:def 32
ex B' being ManySortedSet of [:the carrier of A,the carrier of A:] ex f being ManySortedFunction of the Arrows of A,B' st
( B' = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" );

end;

:: deftheorem Def32 defines full FUNCTOR0:def 32 :

definition

let A be AltGraph ;
let B be non empty AltGraph ;
let F be FunctorStr of A,B;
redefine attr F is full means :Def33: :: FUNCTOR0:def 33
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

proof end;

end;

:: deftheorem Def33 defines full FUNCTOR0:def 33 :

definition

let A, B be AltGraph ;
let F be FunctorStr of A,B;
attr F is injective means :Def34: :: FUNCTOR0:def 34
( F is one-to-one & F is faithful );
attr F is surjective means :Def35: :: FUNCTOR0:def 35
( F is full & F is onto );

end;

:: deftheorem Def34 defines injective FUNCTOR0:def 34 :

:: deftheorem Def35 defines surjective FUNCTOR0:def 35 :

definition

let A, B be AltGraph ;
let F be FunctorStr of A,B;
attr F is bijective means :Def36: :: FUNCTOR0:def 36
( F is injective & F is surjective );

end;

:: deftheorem Def36 defines bijective FUNCTOR0:def 36 :

registration

let A, B be non empty transitive with_units AltCatStr ;
cluster feasible strict covariant contravariant Functor of A,B;
existence

proof end;

end;

theorem Th30: :: FUNCTOR0:30

for A being non empty AltGraph
for o being object of A holds (id A) . o = o

proof end;

theorem Th31: :: FUNCTOR0:31

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 end;

registration

let A be non empty AltGraph ;
cluster id A -> feasible strict Covariant ;
coherence

proof end;

end;

registration

let A be non empty AltGraph ;
cluster feasible Covariant FunctorStr of A,A;
existence

proof end;

end;

theorem Th32: :: FUNCTOR0:32

for A being non empty AltGraph
for o1, o2 being object of A st <^o1,o2^> <> {} holds
for F being feasible Covariant FunctorStr of A,A st F = id A holds
for m being Morphism of o1,o2 holds F . m = m

proof end;

registration

let A be non empty transitive with_units AltCatStr ;
cluster id A -> feasible strict Covariant id-preserving comp-preserving ;
coherence

proof 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 by Def26, Def27;

end;

registration

let A be AltGraph ;
cluster id A -> strict bijective ;
coherence

proof end;

end;

definition

let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible FunctorStr of C1,C2;
let G be FunctorStr of C2,C3;
func G * F -> strict FunctorStr of C1,C3 means :Def37: :: FUNCTOR0:def 37
( the ObjectMap of it = the ObjectMap of G * the ObjectMap of F & the MorphMap of it = (the MorphMap of G * the ObjectMap of F) ** the MorphMap of F );
existence

proof end;

correctness ;

end;

:: deftheorem Def37 defines * FUNCTOR0:def 37 :

registration

let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Covariant FunctorStr of C1,C2;
let G be Covariant FunctorStr of C2,C3;
cluster G * F -> strict Covariant ;
correctness

proof end;

end;

registration

let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Contravariant FunctorStr of C1,C2;
let G be Covariant FunctorStr of C2,C3;
cluster G * F -> strict Contravariant ;
correctness

proof end;

end;

registration

let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Covariant FunctorStr of C1,C2;
let G be Contravariant FunctorStr of C2,C3;
cluster G * F -> strict Contravariant ;
correctness

proof end;

end;

registration

let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Contravariant FunctorStr of C1,C2;
let G be Contravariant FunctorStr of C2,C3;
cluster G * F -> strict Covariant ;
correctness

proof end;

end;

registration

let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible FunctorStr of C1,C2;
let G be feasible FunctorStr of C2,C3;
cluster G * F -> feasible strict ;
coherence

proof end;

end;

theorem :: FUNCTOR0:33

for C1 being non empty AltGraph
for C2, C3, C4 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being feasible FunctorStr of C2,C3
for H being FunctorStr of C3,C4 holds (H * G) * F = H * (G * F)

proof end;

theorem Th34: :: FUNCTOR0:34

for C1 being non empty AltCatStr
for C2, C3 being non empty reflexive AltCatStr
for F being reflexive feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3
for o being object of C1 holds (G * F) . o = G . (F . o)

proof end;

theorem Th35: :: FUNCTOR0:35

for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being reflexive feasible FunctorStr of C1,C2
for G being FunctorStr of 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 end;

registration

let C1, C2, C3 be non empty with_units AltCatStr ;
let F be reflexive feasible id-preserving FunctorStr of C1,C2;
let G be id-preserving FunctorStr of C2,C3;
cluster G * F -> strict id-preserving ;
coherence

proof end;

end;

definition

let A, C be non empty reflexive AltCatStr ;
let B be non empty SubCatStr of A;
let F be FunctorStr of A,C;
func F | B -> FunctorStr of B,C equals :: FUNCTOR0:def 38
F * (incl B);
correctness ;

end;

:: deftheorem defines | FUNCTOR0:def 38 :

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: :: FUNCTOR0:def 39
( the ObjectMap of it = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & the MorphMap of it = (f "" ) * (the ObjectMap of F " ) ) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def39 defines " FUNCTOR0:def 39 :

theorem Th36: :: FUNCTOR0:36

for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr of A,B st F is bijective holds
( F " is bijective & F " is feasible )

proof end;

theorem Th37: :: FUNCTOR0:37

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of A,B st F is bijective & F is coreflexive holds
F " is reflexive

proof end;

theorem Th38: :: FUNCTOR0:38

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible id-preserving FunctorStr of A,B st F is bijective & F is coreflexive holds
F " is id-preserving

proof end;

theorem Th39: :: FUNCTOR0:39

for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr of A,B st F is bijective & F is Covariant holds
F " is Covariant

proof end;

theorem Th40: :: FUNCTOR0:40

for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr of A,B st F is bijective & F is Contravariant holds
F " is Contravariant

proof end;

theorem Th41: :: FUNCTOR0:41

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of 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 end;

theorem Th42: :: FUNCTOR0:42

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of 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 end;

theorem Th43: :: FUNCTOR0:43

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of A,B st F is bijective & F is comp-preserving & F is Covariant & F is coreflexive holds
F " is comp-preserving

proof end;

theorem Th44: :: FUNCTOR0:44

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of A,B st F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive holds
F " is comp-reversing

proof end;

registration

let C1 be 1-sorted ;
let C2 be non empty 1-sorted ;
cluster Covariant -> reflexive BimapStr of C1,C2;
coherence

proof end;

end;

registration

let C1 be 1-sorted ;
let C2 be non empty 1-sorted ;
cluster Contravariant -> reflexive BimapStr of C1,C2;
coherence

proof end;

end;

theorem Th45: :: FUNCTOR0:45

for C1, C2 being 1-sorted
for M being BimapStr of C1,C2 st M is Covariant & M is onto holds
M is coreflexive

proof end;

theorem Th46: :: FUNCTOR0:46

for C1, C2 being 1-sorted
for M being BimapStr of C1,C2 st M is Contravariant & M is onto holds
M is coreflexive

proof end;

registration

let C1 be non empty transitive with_units AltCatStr ;
let C2 be non empty with_units AltCatStr ;
cluster covariant -> reflexive Functor of C1,C2;
coherence

proof end;

end;

registration

let C1 be non empty transitive with_units AltCatStr ;
let C2 be non empty with_units AltCatStr ;
cluster contravariant -> reflexive Functor of C1,C2;
coherence

proof end;

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 covariant & F is onto holds
F is coreflexive

proof end;

theorem Th48: :: FUNCTOR0:48

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 end;

theorem Th49: :: FUNCTOR0:49

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 end;

theorem Th50: :: FUNCTOR0:50

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 end;

definition

let A, B be non empty transitive with_units AltCatStr ;
pred A,B are_isomorphic means :: FUNCTOR0:def 40
ex F being Functor of A,B st
( F is bijective & F is covariant );
reflexivity

proof end;

symmetry

proof end;

pred A,B are_anti-isomorphic means :: FUNCTOR0:def 41
ex F being Functor of A,B st
( F is bijective & F is contravariant );
symmetry

proof end;

end;

:: deftheorem defines are_isomorphic FUNCTOR0:def 40 :

:: deftheorem defines are_anti-isomorphic FUNCTOR0:def 41 :