:: FUNCTOR1 semantic presentation

registration

cluster non empty transitive with_units reflexive AltCatStr ;
existence

proof end;

end;

registration

let A be non empty reflexive AltCatStr ;
cluster non empty reflexive SubCatStr of A;
existence

proof end;

end;

registration

let C1, C2 be non empty reflexive AltCatStr ;
let F be feasible FunctorStr of C1,C2;
let A be non empty reflexive SubCatStr of C1;
cluster F | A -> feasible ;
coherence ;

end;

theorem :: FUNCTOR1:1

for X being set holds id X is onto

proof end;

theorem :: FUNCTOR1:2

for A being non empty set
for B, C being non empty Subset of A
for D being non empty Subset of B st C = D holds
incl C = (incl B) * (incl D)

proof end;

theorem Th3: :: FUNCTOR1:3

for X, Y being set
for f being Function of X,Y st f is bijective holds
f " is Function of Y,X

proof end;

theorem :: FUNCTOR1:4

for X, Y being set
for Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is bijective & g is bijective holds
ex h being Function of X,Z st
( h = g * f & h is bijective )

proof end;

theorem Th5: :: FUNCTOR1:5

for A being non empty reflexive AltCatStr
for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
incl C = (incl B) * (incl D)

proof end;

theorem Th6: :: FUNCTOR1:6

for A, B being non empty AltCatStr
for F being FunctorStr of A,B st F is bijective holds
( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )

proof end;

theorem Th7: :: FUNCTOR1:7

for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is one-to-one & G is one-to-one holds
G * F is one-to-one

proof end;

theorem Th8: :: FUNCTOR1:8

for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is faithful & G is faithful holds
G * F is faithful

proof end;

theorem Th9: :: FUNCTOR1:9

for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is onto & G is onto holds
G * F is onto

proof end;

theorem Th10: :: FUNCTOR1:10

for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is full & G is full holds
G * F is full

proof end;

theorem Th11: :: FUNCTOR1:11

for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is injective & G is injective holds
G * F is injective

proof end;

theorem Th12: :: FUNCTOR1:12

for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is surjective & G is surjective holds
G * F is surjective

proof end;

theorem Th13: :: FUNCTOR1:13

for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is bijective & G is bijective holds
G * F is bijective

proof end;

theorem :: FUNCTOR1:14

for A, I being non empty reflexive AltCatStr
for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
for F being FunctorStr of A,I holds F | C = (F | B) | D

proof end;

theorem :: FUNCTOR1:15

for C1, C2, C3 being non empty reflexive AltCatStr
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3
for A being non empty reflexive SubCatStr of C1 holds (G * F) | A = G * (F | A) by FUNCTOR0:33;

theorem :: FUNCTOR1:16

canceled;

theorem :: FUNCTOR1:17

for A being non empty AltCatStr
for B being non empty SubCatStr of A holds
( B is full iff incl B is full )

proof end;

theorem :: FUNCTOR1:18

for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr of C1,C2 holds
( F is full iff for o1, o2 being object of C1 holds Morph-Map F,o1,o2 is onto )

proof end;

theorem :: FUNCTOR1:19

for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr of C1,C2 holds
( F is faithful iff for o1, o2 being object of C1 holds Morph-Map F,o1,o2 is one-to-one )

proof end;

theorem :: FUNCTOR1:20

for A being non empty transitive with_units AltCatStr holds (id A) " = id A

proof end;

theorem :: FUNCTOR1:21

for A, B being non empty transitive with_units reflexive AltCatStr
for F being feasible FunctorStr of A,B st F is bijective holds
for G being feasible FunctorStr of B,A st FunctorStr(# the ObjectMap of G,the MorphMap of G #) = F " holds
F * G = id B

proof end;

Lm1: for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )

proof end;

theorem :: FUNCTOR1:22

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

proof end;

theorem :: FUNCTOR1:23

for A, B being non empty transitive with_units reflexive AltCatStr
for F being feasible FunctorStr of A,B st F is bijective holds
(F " ) " = FunctorStr(# the ObjectMap of F,the MorphMap of F #)

proof end;

theorem :: FUNCTOR1:24

for A, B, C being non empty transitive with_units reflexive AltCatStr
for G being feasible FunctorStr of A,B
for F being feasible FunctorStr of B,C
for GI being feasible FunctorStr of B,A
for FI being feasible FunctorStr of C,B st F is bijective & G is bijective & FI is bijective & GI is bijective & FunctorStr(# the ObjectMap of GI,the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI,the MorphMap of FI #) = F " holds
(F * G) " = GI * FI

proof end;