:: by Claus Zinn and Wolfgang Jaksch

::

:: Received April 24, 1996

:: Copyright (c) 1996-2019 Association of Mizar Users

registration

existence

ex b_{1} being non empty AltCatStr st

( b_{1} is transitive & b_{1} is with_units & b_{1} is reflexive )

end;
ex b

( b

proof end;

registration

let A be non empty reflexive AltCatStr ;

existence

ex b_{1} being SubCatStr of A st

( not b_{1} is empty & b_{1} is reflexive )

end;
existence

ex b

( not b

proof end;

registration

let C1, C2 be non empty reflexive AltCatStr ;

let F be feasible FunctorStr over C1,C2;

let A be non empty reflexive SubCatStr of C1;

coherence

F | A is feasible ;

end;
let F be feasible FunctorStr over C1,C2;

let A be non empty reflexive SubCatStr of C1;

coherence

F | A is feasible ;

theorem :: FUNCTOR1:1

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)

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

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 )

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 Th4: :: FUNCTOR1:4

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)

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 Th5: :: FUNCTOR1:5

for A, B being non empty AltCatStr

for F being FunctorStr over A,B st F is bijective holds

( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )

for F being FunctorStr over A,B st F is bijective holds

( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )

proof end;

theorem Th6: :: FUNCTOR1:6

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 st F is one-to-one & G is one-to-one holds

G * F is one-to-one

for C2, C3 being non empty reflexive AltGraph

for F being feasible FunctorStr over C1,C2

for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds

G * F is one-to-one

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 over C1,C2

for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds

G * F is faithful

for C2, C3 being non empty reflexive AltGraph

for F being feasible FunctorStr over C1,C2

for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds

G * F is faithful

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 over C1,C2

for G being FunctorStr over C2,C3 st F is onto & G is onto holds

G * F is onto

for C2, C3 being non empty reflexive AltGraph

for F being feasible FunctorStr over C1,C2

for G being FunctorStr over C2,C3 st F is onto & G is onto holds

G * F is onto

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 over C1,C2

for G being FunctorStr over C2,C3 st F is full & G is full holds

G * F is full

for C2, C3 being non empty reflexive AltGraph

for F being feasible FunctorStr over C1,C2

for G being FunctorStr over 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 over C1,C2

for G being FunctorStr over C2,C3 st F is surjective & G is surjective holds

G * F is surjective by Th8, Th9;

for C2, C3 being non empty reflexive AltGraph

for F being feasible FunctorStr over C1,C2

for G being FunctorStr over C2,C3 st F is surjective & G is surjective holds

G * F is surjective by Th8, Th9;

theorem :: FUNCTOR1:13

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 over A,I holds F | C = (F | B) | D

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 over A,I holds F | C = (F | B) | D

proof end;

theorem :: FUNCTOR1:14

for A being non empty AltCatStr

for B being non empty SubCatStr of A holds

( B is full iff incl B is full )

for B being non empty SubCatStr of A holds

( B is full iff incl B is full )

proof end;

theorem :: FUNCTOR1:15

for C1, C2 being non empty AltCatStr

for F being Covariant FunctorStr over C1,C2 holds

( F is full iff for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) is onto )

for F being Covariant FunctorStr over 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:16

for C1, C2 being non empty AltCatStr

for F being Covariant FunctorStr over C1,C2 holds

( F is faithful iff for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) is one-to-one )

for F being Covariant FunctorStr over 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:18

for A, B being non empty transitive with_units reflexive AltCatStr

for F being feasible FunctorStr over A,B st F is bijective holds

for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds

F * G = id B

for F being feasible FunctorStr over A,B st F is bijective holds

for G being feasible FunctorStr over 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:19

for A, B being non empty transitive with_units reflexive AltCatStr

for F being feasible FunctorStr over A,B st F is bijective holds

(F ") * F = id A

for F being feasible FunctorStr over A,B st F is bijective holds

(F ") * F = id A

proof end;

:: ===================================================================

theorem :: FUNCTOR1:20

for A, B being non empty transitive with_units reflexive AltCatStr

for F being feasible FunctorStr over A,B st F is bijective holds

(F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)

for F being feasible FunctorStr over A,B st F is bijective holds

(F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)

proof end;

theorem :: FUNCTOR1:21

for A, B, C being non empty transitive with_units reflexive AltCatStr

for G being feasible FunctorStr over A,B

for F being feasible FunctorStr over B,C

for GI being feasible FunctorStr over B,A

for FI being feasible FunctorStr over C,B st F is bijective & G 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

for G being feasible FunctorStr over A,B

for F being feasible FunctorStr over B,C

for GI being feasible FunctorStr over B,A

for FI being feasible FunctorStr over C,B st F is bijective & G 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;

:: Lemmata about properties of G*F, where G,F are FunctorStr

:: ===================================================================