:: Object-Free Definition of Categories
:: by Marco Riccardi
::
:: Received October 7, 2013
:: Copyright (c) 2013-2018 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 FUNCT_1, TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, SUBSET_1, WELLORD1,
CAT_1, ALTCAT_1, GRAPH_1, BINOP_1, STRUCT_0, PARTFUN1, FUNCOP_1,
MONOID_0, NATTRA_1, MSSUBFAM, ALTCAT_2, ARYTM_0, NUMBERS, ARYTM_3,
CARD_1, FUNCTOR0, MOD_4, CAT_6, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_3, FUNCT_4, RELAT_1,
FUNCT_1, FUNCT_2, ORDINAL1, PARTFUN1, FINSEQ_1, STRUCT_0, FUNCOP_1,
RELSET_1, BINOP_1, GRAPH_1, CAT_1, CAT_2, NUMBERS, NAT_1, XXREAL_0,
XTUPLE_0, ALG_1, XCMPLX_0, WELLORD2, CARD_1, INT_1, VALUED_0, ISOCAT_1;
constructors NUMBERS, FUNCT_2, CLASSES2, FINSEQ_1, STRUCT_0, FUNCOP_1,
RELAT_2, PARTFUN1, RELSET_1, BINOP_1, FUNCT_4, CAT_1, CAT_2, NAT_1,
XXREAL_0, WELLORD2, XREAL_0, CARD_1, XCMPLX_0, INT_1, VALUED_0, ISOCAT_1;
registrations XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, ORDINAL1,
XTUPLE_0, CARD_1, CLASSES2, STRUCT_0, RELSET_1, FUNCT_2, PARTFUN1,
GRFUNC_1, BINOP_1, CAT_1, CARD_2, NAT_LAT, FINSET_1, XXREAL_0, XREAL_0,
NAT_1, NUMBERS, VALUED_0, FINSEQ_1;
requirements SUBSET, BOOLE, REAL, NUMERALS, ARITHM;
begin :: Yet another definition of category
definition
struct (1-sorted) CategoryStr
(# carrier -> set,
composition -> PartFunc of [:the carrier, the carrier:], the carrier #);
end;
reserve C for CategoryStr;
definition
let C;
func Mor(C) -> set equals
:: CAT_6:def 1
the carrier of C;
end;
definition
let C;
mode morphism of C is Element of Mor(C);
end;
reserve f,f1,f2,f3 for morphism of C;
definition
let C,f1,f2;
pred f1,f2 are_composable means
:: CAT_6:def 2
[f1,f2] in dom the composition of C;
end;
notation
let C,f1,f2;
synonym f1 |> f2 for f1,f2 are_composable;
end;
definition
let C,f1,f2;
assume
f1 |> f2;
func f1 (*) f2 -> morphism of C equals
:: CAT_6:def 3
(the composition of C).(f1,f2);
end;
definition
let C,f;
attr f is left_identity means
:: CAT_6:def 4
for f1 being morphism of C st f |> f1 holds f (*) f1 = f1;
attr f is right_identity means
:: CAT_6:def 5
for f1 being morphism of C st f1 |> f holds f1 (*) f = f1;
end;
definition
let C;
attr C is with_left_identities means
:: CAT_6:def 6
for f1 being morphism of C st f1 in the carrier of C holds
ex f being morphism of C st f |> f1 & f is left_identity;
attr C is with_right_identities means
:: CAT_6:def 7
for f1 being morphism of C st f1 in the carrier of C holds
ex f being morphism of C st f1 |> f & f is right_identity;
attr C is left_composable means
:: CAT_6:def 8
for f,f1,f2 being morphism of C st f1 |> f2 holds f1(*)f2 |> f iff f2 |> f;
attr C is right_composable means
:: CAT_6:def 9
for f,f1,f2 being morphism of C st f1 |> f2 holds f |> f1(*)f2 iff f |> f1;
attr C is associative means
:: CAT_6:def 10
for f1,f2,f3 being morphism of C
st f1 |> f2 & f2 |> f3 & (f1(*)f2) |> f3 & f1 |> (f2(*)f3)
holds f1(*)(f2(*)f3) = (f1(*)f2)(*)f3;
end;
definition
let C;
attr C is composable means
:: CAT_6:def 11
C is left_composable right_composable;
attr C is with_identities means
:: CAT_6:def 12
C is with_left_identities with_right_identities;
end;
definition
let C;
func C opp -> strict CategoryStr equals
:: CAT_6:def 13
CategoryStr (#the carrier of C, ~the composition of C#);
end;
theorem :: CAT_6:1
C is empty implies not f1 |> f2;
reserve g1,g2 for morphism of C opp;
theorem :: CAT_6:2
f1 = g1 & f2 = g2 implies (f1 |> f2 iff g2 |> g1);
theorem :: CAT_6:3
f1 = g1 & f2 = g2 & f1 |> f2 implies f1 (*) f2 = g2 (*) g1;
theorem :: CAT_6:4
C is left_composable iff C opp is right_composable;
theorem :: CAT_6:5
C is right_composable iff C opp is left_composable;
theorem :: CAT_6:6
C is with_left_identities iff C opp is with_right_identities;
theorem :: CAT_6:7
C is with_right_identities iff C opp is with_left_identities;
theorem :: CAT_6:8
C is associative iff C opp is associative;
registration
cluster with_left_identities non with_right_identities
composable associative for CategoryStr;
end;
registration
cluster non with_left_identities with_right_identities
composable associative for CategoryStr;
end;
registration
cluster non left_composable right_composable
with_identities associative for CategoryStr;
end;
registration
cluster left_composable non right_composable
with_identities associative for CategoryStr;
end;
registration
cluster non associative composable with_identities for CategoryStr;
end;
registration
cluster empty for CategoryStr;
end;
registration
cluster empty -> left_composable right_composable with_left_identities
with_right_identities associative for CategoryStr;
end;
registration
cluster strict with_left_identities with_right_identities
left_composable right_composable associative for CategoryStr;
end;
registration
cluster strict with_identities composable associative for CategoryStr;
end;
definition
mode category is with_identities composable associative CategoryStr;
end;
definition
let C,f;
attr f is identity means
:: CAT_6:def 14
f is left_identity right_identity;
end;
theorem :: CAT_6:9
C is with_identities implies (f is left_identity iff f is right_identity);
theorem :: CAT_6:10
C is empty implies f is identity;
theorem :: CAT_6:11
for g1,g2 being morphism of the CategoryStr of C
st f1 = g1 & f2 = g2 & f1 |> f2 holds f1 (*) f2 = g1 (*) g2;
theorem :: CAT_6:12
C is left_composable iff the CategoryStr of C is left_composable;
theorem :: CAT_6:13
C is right_composable iff the CategoryStr of C is right_composable;
theorem :: CAT_6:14
C is composable iff the CategoryStr of C is composable;
theorem :: CAT_6:15
C is associative iff the CategoryStr of C is associative;
theorem :: CAT_6:16
for g being morphism of the CategoryStr of C st f = g
holds f is left_identity iff g is left_identity;
theorem :: CAT_6:17
C is with_left_identities iff the CategoryStr of C is with_left_identities;
theorem :: CAT_6:18
for g being morphism of the CategoryStr of C st f = g
holds f is right_identity iff g is right_identity;
theorem :: CAT_6:19
C is with_right_identities iff the CategoryStr of C is with_right_identities;
theorem :: CAT_6:20
C is with_identities iff the CategoryStr of C is with_identities;
definition
let C;
attr C is discrete means
:: CAT_6:def 15
for f being morphism of C holds f is identity;
end;
registration
cluster strict empty discrete with_identities composable associative
for CategoryStr;
end;
theorem :: CAT_6:21
for C being discrete CategoryStr, f1,f2 being morphism of C
st f1 |> f2 holds f1 = f2 & f1 (*) f2 = f2;
registration
cluster discrete -> composable associative for CategoryStr;
end;
definition
let X be set;
func DiscreteCat(X) -> strict discrete category means
:: CAT_6:def 16
the carrier of it = X;
end;
registration
cluster strict for category;
cluster strict empty for category;
cluster strict non empty for category;
end;
definition
let C;
func Ob(C) -> Subset of Mor(C) equals
:: CAT_6:def 17
{f where f is morphism of C: f is identity & f in Mor(C)};
end;
definition
let C;
mode Object of C is Element of Ob(C);
end;
registration
let C be non empty with_identities CategoryStr;
cluster Ob(C) -> non empty;
end;
theorem :: CAT_6:22
for C being non empty with_identities CategoryStr, f being morphism of C
holds f is identity iff f is Object of C;
theorem :: CAT_6:23
for C being non empty with_identities CategoryStr, f,f1 being morphism of C,
o being Object of C st f = o holds
(f |> f1 implies f (*) f1 = f1) &
(f1 |> f implies f1 (*) f = f1) & f |> f;
theorem :: CAT_6:24
for C being non empty with_identities CategoryStr, f being morphism of C
st f is identity holds f |> f;
theorem :: CAT_6:25
for C1,C2 being with_identities CategoryStr
st the CategoryStr of C1 = the CategoryStr of C2
holds for f1 being morphism of C1, f2 being morphism of C2 st f1 = f2 holds
f1 is identity iff f2 is identity;
definition
let C be composable with_identities CategoryStr;
let f be morphism of C;
func dom f -> Object of C means
:: CAT_6:def 18
ex f1 being morphism of C st it = f1 & f |> f1 & f1 is identity
if C is non empty otherwise it = the Object of C;
func cod f -> Object of C means
:: CAT_6:def 19
ex f1 being morphism of C st it = f1 & f1 |> f & f1 is identity
if C is non empty otherwise it = the Object of C;
end;
theorem :: CAT_6:26
for C being composable with_identities CategoryStr, f,f1 being morphism of C
st f |> f1 & f1 is identity holds dom f = f1;
theorem :: CAT_6:27
for C being composable with_identities CategoryStr, f,f1 being morphism of C
st f1 |> f & f1 is identity holds cod f = f1;
definition
let C be with_identities CategoryStr;
let o be Object of C;
func id- o -> morphism of C equals
:: CAT_6:def 20
o;
end;
definition
let C,D be CategoryStr;
mode Functor of C,D is Function of C,D;
end;
reserve C,D,E for with_identities CategoryStr;
reserve F for Functor of C,D;
reserve G for Functor of D,E;
reserve f for morphism of C;
definition
let C,D,F,f;
func F.f -> morphism of D equals
:: CAT_6:def 21
F.f if C is non empty otherwise the Object of D;
end;
definition
let C,D,F;
attr F is identity-preserving means
:: CAT_6:def 22
for f being morphism of C st f is identity holds F.f is identity;
attr F is multiplicative means
:: CAT_6:def 23
for f1,f2 being morphism of C st f1 |> f2 holds F.f1 |> F.f2 &
F.(f1(*)f2) = (F.f1) (*) (F.f2);
attr F is antimultiplicative means
:: CAT_6:def 24
for f1,f2 being morphism of C st f1 |> f2 holds F.f2 |> F.f1 &
F.(f1(*)f2) = (F.f2) (*) (F.f1);
end;
registration
let C,D;
cluster identity-preserving for Functor of C,D;
end;
registration
let C be empty with_identities CategoryStr;
let D be with_identities CategoryStr;
cluster identity-preserving multiplicative antimultiplicative
for Functor of C,D;
end;
registration
let C be with_identities CategoryStr;
let D be non empty with_identities CategoryStr;
cluster identity-preserving multiplicative antimultiplicative
for Functor of C,D;
end;
theorem :: CAT_6:28
ex C,D being category, F being Functor of C,D st
F is multiplicative & F is non identity-preserving;
theorem :: CAT_6:29
C is non empty & D is empty implies not ex F being Functor of C,D st
F is multiplicative or F is antimultiplicative;
theorem :: CAT_6:30
ex C,D being category, F being Functor of C,D st
F is non multiplicative & F is identity-preserving;
definition
let C,D,F;
attr F is covariant means
:: CAT_6:def 25
F is identity-preserving & F is multiplicative;
attr F is contravariant means
:: CAT_6:def 26
F is identity-preserving & F is antimultiplicative;
end;
registration
let C be empty with_identities CategoryStr;
let D be with_identities CategoryStr;
cluster covariant contravariant for Functor of C,D;
end;
registration
let C be with_identities CategoryStr;
let D be non empty with_identities CategoryStr;
cluster covariant contravariant for Functor of C,D;
end;
theorem :: CAT_6:31
C is non empty & D is empty implies not ex F being Functor of C,D
st F is covariant or F is contravariant;
definition
let C,D be non empty with_identities CategoryStr;
let F be covariant Functor of C,D;
let f be Object of C;
redefine func F.f -> Object of D;
end;
theorem :: CAT_6:32
for C,D being non empty composable with_identities CategoryStr,
F being covariant Functor of C,D,
f being morphism of C
holds F.(dom f) = dom(F.f) & F.(cod f) = cod(F.f);
theorem :: CAT_6:33
for C,D being non empty composable with_identities CategoryStr,
F being covariant Functor of C,D,
o being Object of C holds F.(id- o) = id-(F.o);
definition
let C,D,E;
let F,G;
assume
(F is covariant or F is contravariant) &
(G is covariant or G is contravariant);
func G (*) F -> Functor of C,E equals
:: CAT_6:def 27
F * G;
end;
theorem :: CAT_6:34
F is covariant & G is covariant & C is non empty implies (G(*)F).f = G.(F.f);
theorem :: CAT_6:35
F is covariant & G is covariant implies G (*) F is covariant;
definition
let C;
redefine func id C -> Functor of C,C;
end;
registration
let C;
cluster id C -> covariant;
end;
definition
let C,D;
pred C,D are_isomorphic means
:: CAT_6:def 28
ex F being Functor of C,D, G being Functor of D,C
st F is covariant & G is covariant & G (*) F = id C & F (*) G = id D;
reflexivity;
symmetry;
end;
notation
let C,D;
synonym C ~= D for C,D are_isomorphic;
end;
begin
definition
let C be CategoryStr;
func CompMap(C) ->
PartFunc of [:Mor(C), Mor(C):], Mor(C) equals
:: CAT_6:def 29
the composition of C;
end;
definition
let C be composable with_identities CategoryStr;
func SourceMap(C) -> Function of Mor(C), Ob(C) means
:: CAT_6:def 30
for f being Element of Mor(C) holds it.f = dom f if C is non empty
otherwise it = {};
func TargetMap(C) -> Function of Mor(C), Ob(C) means
:: CAT_6:def 31
for f being Element of Mor(C) holds it.f = cod f if C is non empty
otherwise it = {};
end;
definition
let C be with_identities CategoryStr;
func IdMap(C) -> Function of Ob(C), Mor(C) means
:: CAT_6:def 32
for o being Element of Ob(C) holds it.o = id-o if C is non empty
otherwise it = {};
end;
theorem :: CAT_6:36
for C being non empty composable with_identities CategoryStr
for f,g being Element of Mor(C) holds
[g,f] in dom(CompMap(C)) iff (SourceMap(C)).g = (TargetMap(C)).f;
theorem :: CAT_6:37
for C being composable with_identities CategoryStr
for f,g being Element of Mor(C)
st (SourceMap(C)).g = (TargetMap(C)).f holds
(SourceMap(C)).((CompMap(C)).(g,f)) = (SourceMap(C)).f &
(TargetMap(C)).((CompMap(C)).(g,f)) = (TargetMap(C)).g;
theorem :: CAT_6:38
for C being composable associative with_identities CategoryStr
for f,g,h being Element of Mor(C)
st (SourceMap(C)).h = (TargetMap(C)).g &
(SourceMap(C)).g = (TargetMap(C)).f
holds (CompMap(C)).(h,(CompMap(C)).(g,f)) =
(CompMap(C)).((CompMap(C)).(h,g),f);
theorem :: CAT_6:39
for C being composable with_identities CategoryStr
for b being Element of Ob(C) holds
(SourceMap(C)).((IdMap(C)).b) = b & (TargetMap(C)).((IdMap(C)).b) = b &
(for f being Element of Mor(C) st (TargetMap(C)).f = b
holds (CompMap(C)).((IdMap(C)).b,f) = f ) &
for g being Element of Mor(C) st (SourceMap(C)).g = b
holds (CompMap(C)).(g,(IdMap(C)).b) = g;
definition
let C be non empty category;
func Alter(C) -> strict Category equals
:: CAT_6:def 33
CatStr(#Ob(C), Mor(C), SourceMap(C), TargetMap(C), CompMap(C)#);
end;
definition
let A be Category;
func alter(A) -> strict category equals
:: CAT_6:def 34
CategoryStr(# the carrier' of A, the Comp of A #);
end;
registration
let A be Category;
cluster alter(A) -> non empty;
end;
theorem :: CAT_6:40
for A being Category, a1,a2 being (Morphism of A),
f1,f2 being morphism of alter(A) st a1 = f1 & a2 = f2 &
[a1,a2] in dom the Comp of A holds a1(*)a2 = f1(*)f2;
theorem :: CAT_6:41
for A being Category, f being morphism of alter(A)
holds f is identity iff ex o being Object of A st f = id o;
theorem :: CAT_6:42
for A,B being Category, F being Functor of A,B
holds F is covariant Functor of alter(A), alter(B);
theorem :: CAT_6:43
for C being non empty category, a1,a2 being (Morphism of Alter(C)),
f1,f2 being morphism of C st a1 = f1 & a2 = f2 & f1 |> f2
holds a1(*)a2 = f1(*)f2;
theorem :: CAT_6:44
for C being non empty category, f1 being morphism of C,
a1 being Morphism of Alter(C) st a1 = f1
holds dom f1 = dom a1 & cod f1 = cod a1;
theorem :: CAT_6:45
for C being non empty category, o1 being Object of C,
o2 being Object of Alter(C) st o1 = o2 holds id- o1 = id o2;
theorem :: CAT_6:46
for C being non empty category, f being morphism of C
holds f is identity iff ex o being Object of Alter(C) st f = id o;
theorem :: CAT_6:47
for C,D being non empty category, F being covariant Functor of C,D
holds F is Functor of Alter(C), Alter(D);
theorem :: CAT_6:48
for C,D being Category, F being covariant Functor of alter(C), alter(D)
holds F is Functor of C, D;
theorem :: CAT_6:49
for C1,C2 being Category st alter(C1) ~= alter(C2) holds C1 ~= C2;
theorem :: CAT_6:50
for C1,C2 being Category st the carrier' of C1 = the carrier' of C2
& the Comp of C1 = the Comp of C2 holds C1 ~= C2;
theorem :: CAT_6:51
for C being Category holds C ~= Alter(alter(C));
theorem :: CAT_6:52
for C being non empty category holds C ~= alter(Alter(C));