Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### The abstract of the Mizar article:

### Concrete Categories

**by****Grzegorz Bancerek**- Received January 12, 2001
- MML identifier: YELLOW18

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_2, ALTCAT_1, BOOLE, CAT_1, PBOOLE, FUNCT_1, RELAT_1, PRALG_1, BINOP_1, MCART_1, ALTCAT_2, FUNCTOR0, MSUALG_6, SGRAPH1, MSUALG_3, WELLORD1, ISOCAT_1, NATTRA_1, QC_LANG1, ALTCAT_3, OPPCAT_1, CAT_3, FUNCT_2, FUNCT_5, SEQ_1, COMMACAT, PROB_1, CARD_3, YELLOW18; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, PROB_1, MCART_1, ZF_FUND1, BINOP_1, MULTOP_1, CARD_3, STRUCT_0, FUNCT_5, PBOOLE, PRALG_1, MSUALG_1, MSUALG_3, FUNCT_3, COMMACAT, ALTCAT_1, ALTCAT_2, FUNCTOR0, ALTCAT_3, FUNCTOR2, FUNCTOR3; constructors ZF_FUND1, WAYBEL_1, CAT_5, ALTCAT_3, FUNCTOR3, PROB_1, MEMBERED; clusters SUBSET_1, RELSET_1, RELAT_1, FUNCT_1, PRALG_1, STRUCT_0, MSUALG_1, ALTCAT_1, ALTCAT_2, FUNCTOR0, FUNCTOR2, ALTCAT_4, MEMBERED, ZFMISC_1, FUNCT_2, NUMBERS, ORDINAL2; requirements SUBSET, BOOLE; begin :: <section1>Definability of categories and functors</section1> scheme AltCatStrLambda { A() -> non empty set, B(set,set) -> set, C(set,set,set,set,set) -> set }: ex C being strict non empty transitive AltCatStr st the carrier of C = A() & (for a,b being object of C holds <^a,b^> = B(a,b)) & (for a,b,c being object of C st <^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of b,c holds g*f = C(a,b,c,f,g)) provided for a,b,c being Element of A(), f,g being set st f in B(a,b) & g in B(b,c) holds C(a,b,c,f,g) in B(a,c); scheme CatAssocSch { A() -> non empty transitive AltCatStr, C(set,set,set,set,set) -> set }: A() is associative provided for a,b,c being object of A() st <^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of b,c holds g*f = C(a,b,c,f,g) and for a,b,c,d being object of A(), f,g,h being set st f in <^a,b^> & g in <^b,c^> & h in <^c,d^> holds C(a,c,d,C(a,b,c,f,g),h) = C(a,b,d,f,C(b,c,d,g,h)); scheme CatUnitsSch { A() -> non empty transitive AltCatStr, C(set,set,set,set,set) -> set }: A() is with_units provided for a,b,c being object of A() st <^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of b,c holds g*f = C(a,b,c,f,g) and for a being object of A() ex f being set st f in <^a,a^> & for b being object of A(), g being set st g in <^a,b^> holds C(a,a,b,f,g) = g and for a being object of A() ex f being set st f in <^a,a^> & for b being object of A(), g being set st g in <^b,a^> holds C(b,a,a,g,f) = g; scheme CategoryLambda { A() -> non empty set, B(set,set) -> set, C(set,set,set,set,set) -> set }: ex C being strict category st the carrier of C = A() & (for a,b being object of C holds <^a,b^> = B(a,b)) & (for a,b,c being object of C st <^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of b,c holds g*f = C(a,b,c,f,g)) provided for a,b,c being Element of A(), f,g being set st f in B(a,b) & g in B(b,c) holds C(a,b,c,f,g) in B(a,c) and for a,b,c,d being Element of A(), f,g,h being set st f in B(a,b) & g in B(b,c) & h in B(c,d) holds C(a,c,d,C(a,b,c,f,g),h) = C(a,b,d,f,C(b,c,d,g,h)) and for a being Element of A() ex f being set st f in B(a,a) & for b being Element of A(), g being set st g in B(a,b) holds C(a,a,b,f,g) = g and for a being Element of A() ex f being set st f in B(a,a) & for b being Element of A(), g being set st g in B(b,a) holds C(b,a,a,g,f) = g; scheme CategoryLambdaUniq { A() -> non empty set, B(set,set) -> set, C(set,set,set,set,set) -> set }: for C1,C2 being non empty transitive AltCatStr st the carrier of C1 = A() & (for a,b being object of C1 holds <^a,b^> = B(a,b)) & (for a,b,c being object of C1 st <^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of b,c holds g*f = C(a,b,c,f,g)) & the carrier of C2 = A() & (for a,b being object of C2 holds <^a,b^> = B(a,b)) & (for a,b,c being object of C2 st <^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of b,c holds g*f = C(a,b,c,f,g)) holds the AltCatStr of C1 = the AltCatStr of C2; scheme CategoryQuasiLambda { A() -> non empty set, P[set,set,set], B(set,set) -> set, C(set,set,set,set,set) -> set }: ex C being strict category st the carrier of C = A() & (for a,b being object of C for f being set holds f in <^a,b^> iff f in B(a,b) & P[a,b,f]) & (for a,b,c being object of C st <^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of b,c holds g*f = C(a,b,c,f,g)) provided for a,b,c being Element of A(), f,g being set st f in B(a,b) & P[a,b,f] & g in B(b,c) & P[b,c,g] holds C(a,b,c,f,g) in B(a,c) & P[a,c, C(a,b,c,f,g)] and for a,b,c,d being Element of A(), f,g,h being set st f in B(a,b) & P[a,b,f] & g in B(b,c) & P[b,c,g] & h in B(c,d) & P[c,d,h] holds C(a,c,d,C(a,b,c,f,g),h) = C(a,b,d,f,C(b,c,d,g,h)) and for a being Element of A() ex f being set st f in B(a,a) & P[a,a,f] & for b being Element of A(), g being set st g in B(a,b) & P[a,b,g] holds C(a,a,b,f,g) = g and for a being Element of A() ex f being set st f in B(a,a) & P[a,a,f] & for b being Element of A(), g being set st g in B(b,a) & P[b,a,g] holds C(b,a,a,g,f) = g; definition let f be Function-yielding Function; let a,b,c be set; cluster f.(a,b,c) -> Relation-like Function-like; end; scheme SubcategoryEx { A() -> category, P[set], Q[set,set,set]}: ex B being strict non empty subcategory of A() st (for a being object of A() holds a is object of B iff P[a]) & (for a,b being object of A(), a',b' being object of B st a' = a & b' = b & <^a,b^> <> {} for f being Morphism of a,b holds f in <^a',b'^> iff Q[a,b,f]) provided ex a being object of A() st P[a] and for a,b,c being object of A() st P[a] & P[b] & P[c] & <^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of b,c st Q[a,b,f] & Q[b,c,g] holds Q[a,c,g*f] and for a being object of A() st P[a] holds Q[a,a, idm a]; scheme CovariantFunctorLambda { A,B() -> category, O(set) -> set, F(set,set,set) -> set }: ex F being covariant strict Functor of A(),B() st (for a being object of A() holds F.a = O(a)) & for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b holds F.f = F(a,b,f) provided for a being object of A() holds O(a) is object of B() and for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b holds F(a,b,f) in (the Arrows of B()).(O(a), O(b)) and for a,b,c being object of A() st <^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of b,c for a',b',c' being object of B() st a' = O(a) & b' = O(b) & c' = O(c) for f' being Morphism of a',b', g' being Morphism of b',c' st f' = F(a,b,f) & g' = F(b,c,g) holds F(a,c,g*f) = g'*f' and for a being object of A(), a' being object of B() st a' = O(a) holds F(a,a,idm a) = idm a'; theorem :: YELLOW18:1 for A,B being category, F,G being covariant Functor of A,B st (for a being object of A holds F.a = G.a) & (for a,b being object of A st <^a,b^> <> {} for f being Morphism of a,b holds F.f = G.f) holds the FunctorStr of F = the FunctorStr of G; scheme ContravariantFunctorLambda { A,B() -> category, O(set) -> set, F(set,set,set) -> set }: ex F being contravariant strict Functor of A(),B() st (for a being object of A() holds F.a = O(a)) & for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b holds F.f = F(a,b,f) provided for a being object of A() holds O(a) is object of B() and for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b holds F(a,b,f) in (the Arrows of B()).(O(b), O(a)) and for a,b,c being object of A() st <^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of b,c for a',b',c' being object of B() st a' = O(a) & b' = O(b) & c' = O(c) for f' being Morphism of b',a', g' being Morphism of c',b' st f' = F(a,b,f) & g' = F(b,c,g) holds F(a,c,g*f) = f'*g' and for a being object of A(), a' being object of B() st a' = O(a) holds F(a,a,idm a) = idm a'; theorem :: YELLOW18:2 for A,B being category, F,G being contravariant Functor of A,B st (for a being object of A holds F.a = G.a) & (for a,b being object of A st <^a,b^> <> {} for f being Morphism of a,b holds F.f = G.f) holds the FunctorStr of F = the FunctorStr of G; begin :: <section2>Isomorphism and equivalence of categories</section2> definition let A,B,C be non empty set; let f be Function of [:A,B:], C; redefine attr f is one-to-one means :: YELLOW18:def 1 for a1,a2 being Element of A, b1,b2 being Element of B st f.(a1,b1) = f.(a2,b2) holds a1 = a2 & b1 = b2; end; scheme CoBijectiveSch { A,B() -> category, F() -> covariant Functor of A(), B(), O(set) -> set, F(set,set,set) -> set }: F() is bijective provided for a being object of A() holds F().a = O(a) and for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b holds F().f = F(a,b,f) and for a,b being object of A() st O(a) = O(b) holds a = b and for a,b being object of A() st <^a,b^> <> {} for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g and for a,b being object of B() st <^a,b^> <> {} for f being Morphism of a,b ex c,d being object of A(), g being Morphism of c,d st a = O(c) & b = O(d) & <^c,d^> <> {} & f = F(c,d,g); scheme CatIsomorphism { A,B() -> category, O(set) -> set, F(set,set,set) -> set }: A(), B() are_isomorphic provided ex F being covariant Functor of A(),B() st (for a being object of A() holds F.a = O(a)) & for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b holds F.f = F(a,b,f) and for a,b being object of A() st O(a) = O(b) holds a = b and for a,b being object of A() st <^a,b^> <> {} for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g and for a,b being object of B() st <^a,b^> <> {} for f being Morphism of a,b ex c,d being object of A(), g being Morphism of c,d st a = O(c) & b = O(d) & <^c,d^> <> {} & f = F(c,d,g); scheme ContraBijectiveSch { A,B() -> category, F() -> contravariant Functor of A(), B(), O(set) -> set, F(set,set,set) -> set }: F() is bijective provided for a being object of A() holds F().a = O(a) and for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b holds F().f = F(a,b,f) and for a,b being object of A() st O(a) = O(b) holds a = b and for a,b being object of A() st <^a,b^> <> {} for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g and for a,b being object of B() st <^a,b^> <> {} for f being Morphism of a,b ex c,d being object of A(), g being Morphism of c,d st b = O(c) & a = O(d) & <^c,d^> <> {} & f = F(c,d,g); scheme CatAntiIsomorphism { A,B() -> category, O(set) -> set, F(set,set,set) -> set }: A(), B() are_anti-isomorphic provided ex F being contravariant Functor of A(),B() st (for a being object of A() holds F.a = O(a)) & for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b holds F.f = F(a,b,f) and for a,b being object of A() st O(a) = O(b) holds a = b and for a,b being object of A() st <^a,b^> <> {} for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g and for a,b being object of B() st <^a,b^> <> {} for f being Morphism of a,b ex c,d being object of A(), g being Morphism of c,d st b = O(c) & a = O(d) & <^c,d^> <> {} & f = F(c,d,g); definition let A,B be category; pred A,B are_equivalent means :: YELLOW18:def 2 ex F being covariant Functor of A,B, G being covariant Functor of B,A st G*F, id A are_naturally_equivalent & F*G, id B are_naturally_equivalent; reflexivity; symmetry; end; theorem :: YELLOW18:3 for A,B,C being non empty reflexive AltGraph for F1,F2 being feasible FunctorStr over A,B for G1,G2 being FunctorStr over B,C st the FunctorStr of F1 = the FunctorStr of F2 & the FunctorStr of G1 = the FunctorStr of G2 holds G1*F1 = G2*F2; theorem :: YELLOW18:4 for A,B,C being category st A,B are_equivalent & B,C are_equivalent holds A,C are_equivalent; theorem :: YELLOW18:5 for A,B being category st A,B are_isomorphic holds A,B are_equivalent; scheme NatTransLambda { A, B() -> category, F, G() -> covariant Functor of A(), B(), T(set) -> set }: ex t being natural_transformation of F(), G() st F() is_naturally_transformable_to G() & for a being object of A() holds t!a = T(a) provided for a being object of A() holds T(a) in <^F().a, G().a^> and for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b for g1 being Morphism of F().a, G().a st g1 = T(a) for g2 being Morphism of F().b, G().b st g2 = T(b) holds g2*F().f = G().f*g1; scheme NatEquivalenceLambda { A, B() -> category, F, G() -> covariant Functor of A(), B(), T(set) -> set }: ex t being natural_equivalence of F(), G() st F(), G() are_naturally_equivalent & for a being object of A() holds t!a = T(a) provided for a being object of A() holds T(a) in <^F().a, G().a^> & <^G().a, F().a^> <> {} & for f being Morphism of F().a, G().a st f = T(a) holds f is iso and for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b for g1 being Morphism of F().a, G().a st g1 = T(a) for g2 being Morphism of F().b, G().b st g2 = T(b) holds g2*F().f = G().f*g1; begin :: <section3>Dual categories</section3> definition let C1,C2 be non empty AltCatStr; pred C1, C2 are_opposite means :: YELLOW18:def 3 the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~the Arrows of C1 & for a,b,c being object of C1 for a',b',c' being object of C2 st a' = a & b' = b & c' = c holds (the Comp of C2).(a',b',c') = ~((the Comp of C1).(c,b,a)); symmetry; end; theorem :: YELLOW18:6 for A,B being non empty AltCatStr st A, B are_opposite for a being object of A holds a is object of B; theorem :: YELLOW18:7 for A,B being non empty AltCatStr st A, B are_opposite for a,b being object of A, a',b' being object of B st a' = a & b' = b holds <^a,b^> = <^b',a'^>; theorem :: YELLOW18:8 for A,B being non empty AltCatStr st A, B are_opposite for a,b being object of A, a',b' being object of B st a' = a & b' = b for f being Morphism of a,b holds f is Morphism of b', a'; theorem :: YELLOW18:9 for C1,C2 being non empty transitive AltCatStr holds C1, C2 are_opposite iff the carrier of C2 = the carrier of C1 & for a,b,c being object of C1 for a',b',c' being object of C2 st a' = a & b' = b & c' = c holds <^a,b^> = <^b',a'^> & (<^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b, g being Morphism of b,c for f' being Morphism of b',a', g' being Morphism of c',b' st f' = f & g' = g holds f'*g' = g*f); theorem :: YELLOW18:10 for A,B being category st A, B are_opposite for a being object of A, b being object of B st a = b holds idm a = idm b; theorem :: YELLOW18:11 for C being transitive non empty AltCatStr ex C' being strict transitive non empty AltCatStr st C, C' are_opposite; theorem :: YELLOW18:12 for A,B being transitive non empty AltCatStr st A,B are_opposite holds A is associative implies B is associative; theorem :: YELLOW18:13 for A,B being transitive non empty AltCatStr st A,B are_opposite holds A is with_units implies B is with_units; theorem :: YELLOW18:14 for C,C1,C2 being non empty AltCatStr st C, C1 are_opposite holds C, C2 are_opposite iff the AltCatStr of C1 = the AltCatStr of C2; definition let C be transitive non empty AltCatStr; func C opp -> strict transitive non empty AltCatStr means :: YELLOW18:def 4 C, it are_opposite; end; definition let C be associative (transitive non empty AltCatStr); cluster C opp -> associative; end; definition let C be with_units (transitive non empty AltCatStr); cluster C opp -> with_units; end; definition let A,B be category such that A, B are_opposite; func dualizing-func(A,B) -> contravariant strict Functor of A,B means :: YELLOW18:def 5 (for a being object of A holds it.a = a) & for a,b being object of A st <^a,b^> <> {} for f being Morphism of a,b holds it.f = f; end; theorem :: YELLOW18:15 for A,B being category st A,B are_opposite holds dualizing-func(A,B)*dualizing-func(B,A) = id B; theorem :: YELLOW18:16 for A, B being category st A, B are_opposite holds dualizing-func(A,B) is bijective; definition let A be category; cluster dualizing-func(A, A opp) -> bijective; cluster dualizing-func(A opp, A) -> bijective; end; theorem :: YELLOW18:17 for A, B being category st A, B are_opposite holds A, B are_anti-isomorphic; theorem :: YELLOW18:18 for A, B, C being category st A, B are_opposite holds A, C are_isomorphic iff B, C are_anti-isomorphic; theorem :: YELLOW18:19 for A, B, C, D being category st A, B are_opposite & C, D are_opposite holds A, C are_isomorphic implies B, D are_isomorphic; theorem :: YELLOW18:20 for A, B, C, D being category st A, B are_opposite & C, D are_opposite holds A, C are_anti-isomorphic implies B, D are_anti-isomorphic; theorem :: YELLOW18:21 for A, B being category st A, B are_opposite for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} for a', b' being object of B st a' = a & b' = b for f being Morphism of a,b, f' being Morphism of b',a' st f' = f holds f is retraction iff f' is coretraction; theorem :: YELLOW18:22 for A, B being category st A, B are_opposite for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} for a', b' being object of B st a' = a & b' = b for f being Morphism of a,b, f' being Morphism of b',a' st f' = f holds f is coretraction iff f' is retraction; theorem :: YELLOW18:23 for A, B being category st A, B are_opposite for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} for a', b' being object of B st a' = a & b' = b for f being Morphism of a,b, f' being Morphism of b',a' st f' = f & f is retraction coretraction holds f'" = f"; theorem :: YELLOW18:24 for A, B being category st A, B are_opposite for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} for a', b' being object of B st a' = a & b' = b for f being Morphism of a,b, f' being Morphism of b',a' st f' = f holds f is iso iff f' is iso; theorem :: YELLOW18:25 for A, B, C, D being category st A, B are_opposite & C, D are_opposite for F, G being covariant Functor of B, C st F, G are_naturally_equivalent holds dualizing-func(C,D)*G*dualizing-func(A,B), dualizing-func(C,D)*F*dualizing-func(A,B) are_naturally_equivalent; theorem :: YELLOW18:26 for A, B, C, D being category st A, B are_opposite & C, D are_opposite holds A, C are_equivalent implies B, D are_equivalent; definition let A,B be category; pred A,B are_dual means :: YELLOW18:def 6 A, B opp are_equivalent; symmetry; end; theorem :: YELLOW18:27 for A, B being category st A, B are_anti-isomorphic holds A, B are_dual; theorem :: YELLOW18:28 for A, B, C being category st A, B are_opposite holds A, C are_equivalent iff B, C are_dual; theorem :: YELLOW18:29 for A, B, C being category st A, B are_dual & B, C are_equivalent holds A, C are_dual; theorem :: YELLOW18:30 for A, B, C being category st A, B are_dual & B, C are_dual holds A, C are_equivalent; begin :: <section4>Concrete categories</section4> theorem :: YELLOW18:31 for X,Y,x being set holds x in Funcs(X,Y) iff x is Function & proj1 x = X & proj2 x c= Y; definition let C be 1-sorted; mode ManySortedSet of C is ManySortedSet of the carrier of C; end; definition let C be category; attr C is para-functional means :: YELLOW18:def 7 ex F being ManySortedSet of C st for a1,a2 being object of C holds <^a1,a2^> c= Funcs(F.a1,F.a2); end; definition cluster quasi-functional -> para-functional category; end; definition let C be category; let a be set; func C-carrier_of a means :: YELLOW18:def 8 ex b being object of C st b = a & it = proj1 idm b if a is object of C otherwise it = {}; end; definition let C be category; let a be object of C; redefine func C-carrier_of a equals :: YELLOW18:def 9 proj1 idm a; synonym the_carrier_of a; end; theorem :: YELLOW18:32 for A being non empty set, a being object of EnsCat A holds idm a = id a; theorem :: YELLOW18:33 for A being non empty set for a being object of EnsCat A holds the_carrier_of a = a; definition let C be category; attr C is set-id-inheriting means :: YELLOW18:def 10 for a being object of C holds idm a = id the_carrier_of a; end; definition let A be non empty set; cluster EnsCat A -> set-id-inheriting; end; definition let C be category; attr C is concrete means :: YELLOW18:def 11 C is para-functional semi-functional set-id-inheriting; end; definition cluster concrete -> para-functional semi-functional set-id-inheriting category; cluster para-functional semi-functional set-id-inheriting -> concrete category; end; definition cluster concrete quasi-functional strict category; end; theorem :: YELLOW18:34 for C being category holds C is para-functional iff for a1,a2 being object of C holds <^a1,a2^> c= Funcs(the_carrier_of a1, the_carrier_of a2); theorem :: YELLOW18:35 for C being para-functional category for a,b being object of C st <^a,b^> <> {} for f being Morphism of a,b holds f is Function of the_carrier_of a, the_carrier_of b; definition let A be para-functional category; let a,b be object of A; cluster -> Function-like Relation-like Morphism of a,b; end; theorem :: YELLOW18:36 for C being para-functional category for a,b being object of C st <^a,b^> <> {} for f being Morphism of a,b holds dom f = the_carrier_of a & rng f c= the_carrier_of b; theorem :: YELLOW18:37 for C being para-functional semi-functional category for a being object of C holds the_carrier_of a = dom idm a; theorem :: YELLOW18:38 for C being para-functional semi-functional category for a,b,c being object of C st <^a,b^> <> {} & <^b,c^> <> {} for f being Morphism of a,b, g being Morphism of b,c holds g*f = (g qua Function)*(f qua Function); theorem :: YELLOW18:39 for C being para-functional semi-functional category for a being object of C st id the_carrier_of a in <^a,a^> holds idm a = id the_carrier_of a; scheme ConcreteCategoryLambda { A() -> non empty set, B(set,set) -> set, D(set) -> set }: ex C being concrete strict category st the carrier of C = A() & (for a being object of C holds the_carrier_of a = D(a)) & for a,b being object of C holds <^a,b^> = B(a,b) provided for a,b,c being Element of A(), f,g being Function st f in B(a,b) & g in B(b,c) holds g*f in B(a,c) and for a,b being Element of A() holds B(a,b) c= Funcs(D(a), D(b)) and for a being Element of A() holds id D(a) in B(a,a); scheme ConcreteCategoryQuasiLambda { A() -> non empty set, P[set,set,set], D(set) -> set }: ex C being concrete strict category st the carrier of C = A() & (for a being object of C holds the_carrier_of a = D(a)) & for a,b being Element of A(), f being Function holds f in (the Arrows of C).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f] provided for a,b,c being Element of A(), f,g being Function st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] and for a being Element of A() holds P[a,a,id D(a)]; scheme ConcreteCategoryEx { A() -> non empty set, B(set) -> set, D[set, set], P[set,set,set] }: ex C being concrete strict category st the carrier of C = A() & (for a being object of C for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x]) & for a,b being Element of A(), f being Function holds f in (the Arrows of C).(a,b) iff f in Funcs(C-carrier_of a, C-carrier_of b) & P[a,b,f] provided for a,b,c being Element of A(), f,g being Function st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] and for a being Element of A(), X being set st for x being set holds x in X iff x in B(a) & D[a,x] holds P[a,a,id X]; scheme ConcreteCategoryUniq1 { A() -> non empty set, B(set,set) -> set }: for C1, C2 being para-functional semi-functional category st the carrier of C1 = A() & (for a,b being object of C1 holds <^a,b^> = B(a,b)) & the carrier of C2 = A() & (for a,b being object of C2 holds <^a,b^> = B(a,b)) holds the AltCatStr of C1 = the AltCatStr of C2; scheme ConcreteCategoryUniq2 { A() -> non empty set, P[set,set,set], D(set) -> set }: for C1,C2 being para-functional semi-functional category st the carrier of C1 = A() & (for a,b being Element of A(), f being Function holds f in (the Arrows of C1).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f]) & the carrier of C2 = A() & (for a,b being Element of A(), f being Function holds f in (the Arrows of C2).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f]) holds the AltCatStr of C1 = the AltCatStr of C2; scheme ConcreteCategoryUniq3 { A() -> non empty set, B(set) -> set, D[set, set], P[set,set,set] }: for C1,C2 being para-functional semi-functional category st the carrier of C1 = A() & (for a being object of C1 for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x]) & (for a,b being Element of A(), f being Function holds f in (the Arrows of C1).(a,b) iff f in Funcs(C1-carrier_of a, C1-carrier_of b) & P[a,b,f]) & the carrier of C2 = A() & (for a being object of C2 for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x]) & (for a,b being Element of A(), f being Function holds f in (the Arrows of C2).(a,b) iff f in Funcs(C2-carrier_of a, C2-carrier_of b) & P[a,b,f]) holds the AltCatStr of C1 = the AltCatStr of C2; begin :: <section5>Equivalence between concrete categories</section5> theorem :: YELLOW18:40 for C being concrete category for a,b being object of C st <^a,b^> <> {} & <^b,a^> <> {} for f being Morphism of a,b st f is retraction holds rng f = the_carrier_of b; theorem :: YELLOW18:41 for C being concrete category for a,b being object of C st <^a,b^> <> {} & <^b,a^> <> {} for f being Morphism of a,b st f is coretraction holds f is one-to-one; theorem :: YELLOW18:42 for C being concrete category for a,b being object of C st <^a,b^> <> {} & <^b,a^> <> {} for f being Morphism of a,b st f is iso holds f is one-to-one & rng f = the_carrier_of b; theorem :: YELLOW18:43 for C being para-functional semi-functional category for a,b being object of C st <^a,b^> <> {} for f being Morphism of a,b st f is one-to-one & (f qua Function)" in <^b,a^> holds f is iso; theorem :: YELLOW18:44 for C being concrete category for a,b being object of C st <^a,b^> <> {} & <^b,a^> <> {} for f being Morphism of a,b st f is iso holds f" = (f qua Function)"; scheme ConcreteCatEquivalence { A,B() -> para-functional semi-functional category, O1, O2(set) -> set, F1, F2(set,set,set) -> Function, A, B(set) -> Function }: A(), B() are_equivalent provided ex F being covariant Functor of A(),B() st (for a being object of A() holds F.a = O1(a)) & for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b holds F.f = F1(a,b,f) and ex G being covariant Functor of B(),A() st (for a being object of B() holds G.a = O2(a)) & for a,b being object of B() st <^a,b^> <> {} for f being Morphism of a,b holds G.f = F2(a,b,f) and for a, b being object of A() st a = O2(O1(b)) holds A(b) in <^a, b^> & A(b)" in <^b,a^> & A(b) is one-to-one and for a, b being object of B() st b = O1(O2(a)) holds B(a) in <^a, b^> & B(a)" in <^b,a^> & B(a) is one-to-one and for a,b being object of A() st <^a,b^> <> {} for f being Morphism of a,b holds A(b)*F2(O1(a),O1(b),F1(a,b,f)) = f*A(a) and for a,b being object of B() st <^a,b^> <> {} for f being Morphism of a,b holds F1(O2(a),O2(b),F2(a,b,f))*B(a) = B(b)*f; begin :: <section6>Concretization of categories</section6> definition let C be category; func Concretized C -> concrete strict category means :: YELLOW18:def 12 the carrier of it = the carrier of C & (for a being object of it for x being set holds x in the_carrier_of a iff x in Union disjoin the Arrows of C & a = x`22) & for a,b being Element of C, f being Function holds f in (the Arrows of it).(a,b) iff f in Funcs(it-carrier_of a, it-carrier_of b) & ex fa,fb being object of C, g being Morphism of fa, fb st fa = a & fb = b & <^fa, fb^> <> {} & for o being object of C st <^o, fa^> <> {} for h being Morphism of o,fa holds f.[h,[o,fa]] = [g*h,[o,fb]]; end; theorem :: YELLOW18:45 for A being category, a being object of A, x being set holds x in (Concretized A)-carrier_of a iff ex b being object of A, f being Morphism of b,a st <^b,a^> <> {} & x = [f,[b,a]]; definition let A be category; let a be object of A; cluster (Concretized A)-carrier_of a -> non empty; end; theorem :: YELLOW18:46 for A being category, a, b being object of A st <^a,b^> <> {} for f being Morphism of a,b ex F being Function of (Concretized A)-carrier_of a, (Concretized A)-carrier_of b st F in (the Arrows of Concretized A).(a,b) & :: F.[idm a, [a,a]] = [f, [a,b]] & for c being object of A, g being Morphism of c,a st <^c,a^> <> {} holds F.[g, [c,a]] = [f*g, [c,b]]; theorem :: YELLOW18:47 for A being category, a, b being object of A st <^a,b^> <> {} for F1,F2 being Function st F1 in (the Arrows of Concretized A).(a,b) & F2 in (the Arrows of Concretized A).(a,b) & F1.[idm a, [a,a]] = F2.[idm a, [a,a]] holds F1 = F2; scheme NonUniqMSFunctionEx {I() -> set, A, B() -> ManySortedSet of I(), P[set,set,set]}: ex F being ManySortedFunction of A(), B() st for i,x being set st i in I() & x in A().i holds F.i.x in B().i & P[i,x,F.i.x] provided for i,x being set st i in I() & x in A().i ex y being set st y in B().i & P[i,x,y]; definition let A be category; func Concretization A -> covariant strict Functor of A, Concretized A means :: YELLOW18:def 13 (for a being object of A holds it.a = a) & (for a, b being object of A st <^a,b^> <> {} for f being Morphism of a,b holds it.f.[idm a, [a,a]] = [f, [a,b]]); end; definition let A be category; cluster Concretization A -> bijective; end; theorem :: YELLOW18:48 for A being category holds A, Concretized A are_isomorphic;

Back to top