:: Basic Properties of Functor Structures
:: by Claus Zinn and Wolfgang Jaksch
::
:: Received April 24, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

registration

cluster non empty transitive with_units reflexive for AltCatStr ;

existence
ex b₁ being non empty AltCatStr st
( b₁ is transitive & b₁ is with_units & b₁ is reflexive )

proof end;

end;

registration

let A be non empty reflexive AltCatStr ;

cluster non empty reflexive for SubCatStr of A;

existence
ex b₁ being SubCatStr of A st
( not b₁ is empty & b₁ is reflexive )

proof end;

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;

cluster F | A -> feasible ;

coherence
F | A is feasible ;

end;

registration

let X be set ;

cluster id X -> onto ;

coherence
id X is onto

proof end;

end;

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)

proof end;

theorem Th2: :: FUNCTOR1:2

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

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)

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

proof end;

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

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

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

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

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

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 over C1,C2
for G being FunctorStr over C2,C3 st F is injective & G is injective holds
G * F is injective by Th7, Th6;

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;

theorem Th12: :: FUNCTOR1:12

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 bijective & G is bijective holds
G * F is bijective by Th11, Th10;

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

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 )

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 )

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 )

proof end;

theorem :: FUNCTOR1:17

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

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

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

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

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

proof end;