Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

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

Back to top