Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

### Basic Properties of Functor Structures

by
Claus Zinn, and
Wolfgang Jaksch

MML identifier: FUNCTOR1
[ Mizar article, MML identifier index ]

```environ

vocabulary RELAT_2, ALTCAT_1, ALTCAT_2, MSUALG_6, FUNCTOR0, RELAT_1, FUNCT_3,
FUNCT_1, SGRAPH1, BOOLE, MSUALG_3, CAT_1, ENS_1, PRALG_1, PBOOLE,
NATTRA_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, BINOP_1, STRUCT_0, PBOOLE, MSUALG_1, PRALG_1, MSUALG_3,
ALTCAT_1, ALTCAT_2, FUNCT_3, FUNCTOR0, AUTALG_1;
constructors FUNCTOR0, MCART_1, AUTALG_1;
clusters RELAT_1, FUNCT_1, ALTCAT_2, MSUALG_1, STRUCT_0, PRALG_1, FUNCTOR0,
RELSET_1, SUBSET_1, FUNCT_2;
requirements SUBSET, BOOLE;

begin

reserve X,Y for set;
reserve Z for non empty set;

:: ===================================================================
:: Definitions of some clusters
:: ===================================================================

definition
cluster transitive with_units reflexive (non empty AltCatStr);
end;

definition
let A be non empty reflexive AltCatStr;
cluster non empty reflexive SubCatStr of A;
end;

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

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

begin

theorem :: FUNCTOR1:1
for X being set holds
id X is onto;

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

theorem :: FUNCTOR1:2
for A being non empty set,
B,C being non empty Subset of A,
D being non empty Subset of B st C=D holds
incl C = incl B * incl D;

theorem :: FUNCTOR1:3
for f being Function of X,Y
st f is bijective
holds
f" is Function of Y,X;

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

theorem :: FUNCTOR1:4
for f being Function of X,Y,
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;

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

begin

theorem :: FUNCTOR1:5
for A being non empty reflexive AltCatStr,
B being non empty reflexive SubCatStr of A,
C being non empty SubCatStr of A,
D being non empty SubCatStr of B st C = D holds
incl C = incl B * incl D;

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

theorem :: FUNCTOR1:6
for A,B being non empty AltCatStr,
F being FunctorStr over A,B st F is bijective holds
the ObjectMap of F is bijective &
the MorphMap of F is "1-1";

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

theorem :: FUNCTOR1:7
for C1 being non empty AltGraph, C2,C3 being non empty reflexive AltGraph,
F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3 st
F is one-to-one & G is one-to-one holds
G*F is one-to-one;

theorem :: FUNCTOR1:8
for C1 being non empty AltGraph, C2,C3 being non empty reflexive AltGraph,
F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3 st
F is faithful & G is faithful holds
G*F is faithful;

theorem :: FUNCTOR1:9
for C1 being non empty AltGraph, C2,C3 being non empty reflexive AltGraph,
F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3 st
F is onto & G is onto holds
G*F is onto;

theorem :: FUNCTOR1:10
for C1 being non empty AltGraph, C2,C3 being non empty reflexive AltGraph,
F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3 st
F is full & G is full holds
G*F is full;

theorem :: FUNCTOR1:11
for C1 being non empty AltGraph, C2,C3 being non empty reflexive AltGraph,
F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3 st
F is injective & G is injective holds
G*F is injective;

theorem :: FUNCTOR1:12
for C1 being non empty AltGraph, C2,C3 being non empty reflexive AltGraph,
F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3 st
F is surjective & G is surjective holds
G*F is surjective;

theorem :: FUNCTOR1:13
for C1 being non empty AltGraph, C2,C3 being non empty reflexive AltGraph,
F being feasible FunctorStr over C1,C2, G being FunctorStr over C2,C3 st
F is bijective & G is bijective holds
G*F is bijective;

begin :: Theorems about the restriction ans inclusion operator

theorem :: FUNCTOR1:14
for A,I being non empty reflexive AltCatStr,
B being non empty reflexive SubCatStr of A,
C being non empty SubCatStr of A,
D being non empty SubCatStr of B st C = D
for F being FunctorStr over A,I holds
F|C = F|B|D;

theorem :: FUNCTOR1:15
for C1,C2,C3 being non empty reflexive AltCatStr,
F being feasible FunctorStr over C1,C2,
G being FunctorStr over C2,C3
for A being non empty reflexive SubCatStr of C1 holds
(G*F)|A = G*(F|A);

:: ===================== trivial Corollary ============================

canceled;

theorem :: FUNCTOR1:17
for A being non empty AltCatStr,
B being non empty SubCatStr of A holds
B is full iff incl B is full;

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

begin :: Theorems about 'full' and 'faithful' of Functor Structures

theorem :: FUNCTOR1:18
for C1, C2 being non empty AltCatStr,
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;

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

theorem :: FUNCTOR1:19
for C1, C2 being non empty AltCatStr,
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;

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

begin :: Theorems about the inversion of Functor Structures

theorem :: FUNCTOR1:20
for A being transitive with_units (non empty AltCatStr)
holds
(id A)" = id A;

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

theorem :: FUNCTOR1:21
for A, B being transitive with_units reflexive (non empty AltCatStr)
for F being feasible FunctorStr over A,B st F is bijective
for G being feasible FunctorStr over B,A st the FunctorStr of G=F" holds
F * G = id B;

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

theorem :: FUNCTOR1:22
for A, B being transitive with_units reflexive (non empty AltCatStr)
for F being feasible FunctorStr over A,B st F is bijective holds

(F") * F = id A;

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

theorem :: FUNCTOR1:23
for A, B being transitive with_units reflexive (non empty AltCatStr)
for F being feasible FunctorStr over A,B st F is bijective holds
(F")" = the FunctorStr of F;

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

theorem :: FUNCTOR1:24
for A, B, C being transitive with_units reflexive (non empty AltCatStr),
G being feasible FunctorStr over A,B,
F being feasible FunctorStr over B,C,
GI being feasible FunctorStr over B,A,
FI being feasible FunctorStr over C,B
st F is bijective & G is bijective &
FI is bijective & GI is bijective &
the FunctorStr of GI=G" & the FunctorStr of FI=F" holds
(F*G)" = (GI*FI);
```