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