:: Basic Properties of Functor Structures :: by Claus Zinn and Wolfgang Jaksch :: :: Received April 24, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, RELAT_2, ALTCAT_1, ALTCAT_2, MSUALG_6, FUNCTOR0, RELAT_1, FUNCT_2, FUNCT_1, SUBSET_1, FUNCT_3, ZFMISC_1, STRUCT_0, TARSKI, MEMBER_1, MSUALG_3, ENS_1, CAT_1, PBOOLE, REALSET1, PZFMISC1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE, PARTFUN1, FUNCT_2, BINOP_1, REALSET1, PZFMISC1, STRUCT_0, MSUALG_3, ALTCAT_1, ALTCAT_2, FUNCT_3, FUNCTOR0; constructors REALSET1, PZFMISC1, MSUALG_3, FUNCTOR0, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE, STRUCT_0, ALTCAT_2, FUNCTOR0, RELSET_1; requirements SUBSET, BOOLE; begin reserve X,Y for set; reserve Z for non empty set; registration cluster transitive with_units reflexive for non empty AltCatStr; end; registration let A be non empty reflexive AltCatStr; cluster non empty reflexive for SubCatStr of A; end; registration 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 registration let X be set; cluster id X -> onto; end; theorem :: FUNCTOR1:1 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:2 for f being Function of X,Y st f is bijective holds f" is Function of Y,X; theorem :: FUNCTOR1:3 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:4 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:5 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:6 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: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 faithful & G is faithful holds G*F is faithful; 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 onto & G is onto holds G*F is onto; 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 full & G is full holds G*F is full; 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 injective & G is injective holds G*F is injective; 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 surjective & G is surjective holds G*F is surjective; 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 bijective & G is bijective holds G*F is bijective; begin :: Theorems about the restriction ans inclusion operator theorem :: FUNCTOR1:13 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:14 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:15 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:16 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:17 for A being transitive with_units non empty AltCatStr holds (id A)" = id A; :: =================================================================== theorem :: FUNCTOR1:18 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:19 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:20 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:21 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 & the FunctorStr of GI=G" & the FunctorStr of FI=F" holds (F*G)" = (GI*FI);