The abstract of the Mizar article:

Basic Properties of Functor Structures

by

Claus Zinn, and

Wolfgang Jaksch

Received April 24, 1996

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