:: Object-Free Definition of Categories :: by Marco Riccardi :: :: Received October 7, 2013 :: Copyright (c) 2013-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 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, STRUCT_0, RELSET_1, FUNCT_2, PARTFUN1, CAT_1, CARD_2, NAT_1; requirements SUBSET, BOOLE, 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));