:: Concrete Categories
:: by Grzegorz Bancerek
::
:: Received January 12, 2001
:: Copyright (c) 2001-2017 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, STRUCT_0, RELAT_2, ALTCAT_1, CAT_1, RELAT_1, SUBSET_1,
PBOOLE, ZFMISC_1, FUNCT_1, TARSKI, BINOP_1, MCART_1, FUNCOP_1, ALTCAT_2,
FUNCTOR0, MSUALG_6, FUNCT_2, MSUALG_3, WELLORD1, REWRITE1, NATTRA_1,
MEMBER_1, REALSET1, PZFMISC1, ALTCAT_3, ARYTM_0, CAT_3, NUMBERS,
VALUED_1, CARD_3, YELLOW18;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1,
NUMBERS, RELAT_1, RELSET_1, FUNCT_1, PBOOLE, PARTFUN1, FUNCT_2, MCART_1,
ZF_FUND1, BINOP_1, MULTOP_1, CARD_3, FUNCT_4, STRUCT_0, FUNCOP_1,
MSUALG_3, FUNCT_3, ALTCAT_1, ALTCAT_2, FUNCTOR0, ALTCAT_3, FUNCTOR2,
FUNCTOR3;
constructors ZF_FUND1, MSUALG_3, ALTCAT_3, FUNCTOR3, CARD_3, RELSET_1,
XTUPLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FUNCOP_1, PBOOLE, STRUCT_0, ALTCAT_1, ALTCAT_2, FUNCTOR0, FUNCTOR2,
ALTCAT_4, RELSET_1, XTUPLE_0;
requirements SUBSET, BOOLE;
begin
:: Definability of categories and functors
scheme :: YELLOW18:sch 1
AltCatStrLambda { A() -> non empty set, B(object,object) -> set,
C(object,object,object,object,object) -> object }:
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 :: YELLOW18:sch 2
CatAssocSch { A() -> non empty transitive AltCatStr,
C(object,object,object,object,object) -> object }: 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 :: YELLOW18:sch 3
CatUnitsSch { A() -> non empty transitive AltCatStr,
C(object,object,object,object,object) -> object }: 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 :: YELLOW18:sch 4
CategoryLambda { A() -> non empty set, B(object,object) -> set,
C(object,object,object,object,object) -> object }:
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 :: YELLOW18:sch 5
CategoryLambdaUniq { A() -> non empty set, B(object,object) -> object,
C(object,object,object,object,object) -> object }:
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 :: YELLOW18:sch 6
CategoryQuasiLambda { A() -> non empty set,
P[object,object,object],
B(object,object) -> set, C(object,object,object,object,object) -> object }:
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;
registration
let f be Function-yielding Function;
let a,b,c be set;
cluster f.(a,b,c) -> Relation-like Function-like;
end;
scheme :: YELLOW18:sch 7
SubcategoryEx { A() -> category, P[object], Q[object,object,object]}:
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(), a9,b9 being Object of B
st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds f in <^a9,b9^> 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 :: YELLOW18:sch 8
CovariantFunctorLambda { A,B() -> category, O(object) -> object,
F(object,object,object) -> object }:
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 a9,b9,c9 being Object of B() st a9 = O(a) & b9 = O(b) & c9 = O(c)
for f9 being Morphism of a9,b9, g9 being Morphism of b9,c9
st f9 = F(a,b,f) & g9 = F(b,c,g) holds F(a,c,g*f) = g9*f9 and
for a being Object of A(), a9 being Object of B() st a9 = O(a)
holds F(a,a,idm a) = idm a9;
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 :: YELLOW18:sch 9
ContravariantFunctorLambda { A,B() -> category, O(object) -> object,
F(object,object,object) -> object }:
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 a9,b9,c9 being Object of B() st a9 = O(a) & b9 = O(b) & c9 = O(c)
for f9 being Morphism of b9,a9, g9 being Morphism of c9,b9
st f9 = F(a,b,f) & g9 = F(b,c,g) holds F(a,c,g*f) = f9*g9 and
for a being Object of A(), a9 being Object of B() st a9 = O(a)
holds F(a,a,idm a) = idm a9;
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
:: Isomorphism and equivalence of categories
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 :: YELLOW18:sch 10
CoBijectiveSch
{ A,B() -> category, F() -> covariant Functor of A(), B(),
O(object) -> object,
F(object,object,object) -> object }: 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 :: YELLOW18:sch 11
CatIsomorphism { A,B() -> category, O(object) -> object,
F(object,object,object) -> object }: 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 :: YELLOW18:sch 12
ContraBijectiveSch
{ A,B() -> category, F() -> contravariant Functor of A(), B(),
O(object) -> object, F(object,object,object) -> object }: 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 :: YELLOW18:sch 13
CatAntiIsomorphism { A,B() -> category, O(object) -> object,
F(object,object,object) -> object }: 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 :: YELLOW18:sch 14
NatTransLambda { A, B() -> category,
F, G() -> covariant Functor of A(), B(), T(object) -> object }:
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 :: YELLOW18:sch 15
NatEquivalenceLambda { A, B() -> category,
F, G() -> covariant Functor of A(), B(), T(object) -> object }:
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
:: Dual categories
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 a9,b9,c9 being Object of C2 st a9 = a & b9 = b & c9 = c
holds (the Comp of C2).(a9,b9,c9) = ~((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, a9,b9 being Object of B st a9 = a & b9 = b
holds <^a,b^> = <^b9,a9^>;
theorem :: YELLOW18:8
for A,B being non empty AltCatStr st A, B are_opposite
for a,b being Object of A, a9,b9 being Object of B st a9 = a & b9 = b
for f being Morphism of a,b holds f is Morphism of b9, a9;
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 a9,b9,c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
<^a,b^> = <^b9,a9^> & (<^a,b^> <> {} & <^b,c^> <> {} implies
for f being Morphism of a,b, g being Morphism of b,c
for f9 being Morphism of b9,a9, g9 being Morphism of c9,b9
st f9 = f & g9 = g holds f9*g9 = 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 A,B being transitive non empty AltCatStr st A,B are_opposite
holds A is associative implies B is associative;
theorem :: YELLOW18:12
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:13
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;
registration
let C be associative transitive non empty AltCatStr;
cluster C opp -> associative;
end;
registration
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:14
for A,B being category st A,B are_opposite
holds dualizing-func(A,B)*dualizing-func(B,A) = id B;
theorem :: YELLOW18:15
for A, B being category st A, B are_opposite
holds dualizing-func(A,B) is bijective;
registration
let A be category;
cluster dualizing-func(A, A opp) -> bijective;
cluster dualizing-func(A opp, A) -> bijective;
end;
theorem :: YELLOW18:16
for A, B being category st A, B are_opposite holds A, B are_anti-isomorphic;
theorem :: YELLOW18:17
for A, B, C being category st A, B are_opposite
holds A, C are_isomorphic iff B, C are_anti-isomorphic;
theorem :: YELLOW18:18
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:19
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:20
for A, B being category st A, B are_opposite
for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {}
for a9, b9 being Object of B st a9 = a & b9 = b
for f being Morphism of a,b, f9 being Morphism of b9,a9 st f9 = f
holds f is retraction iff f9 is coretraction;
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 a9, b9 being Object of B st a9 = a & b9 = b
for f being Morphism of a,b, f9 being Morphism of b9,a9 st f9 = f
holds f is coretraction iff f9 is retraction;
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 a9, b9 being Object of B st a9 = a & b9 = b
for f being Morphism of a,b, f9 being Morphism of b9,a9
st f9 = f & f is retraction coretraction holds f9" = f";
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 a9, b9 being Object of B st a9 = a & b9 = b
for f being Morphism of a,b, f9 being Morphism of b9,a9 st f9 = f
holds f is iso iff f9 is iso;
theorem :: YELLOW18:24
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:25
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:26
for A, B being category st A, B are_anti-isomorphic holds A, B are_dual;
theorem :: YELLOW18:27
for A, B, C being category st A, B are_opposite
holds A, C are_equivalent iff B, C are_dual;
theorem :: YELLOW18:28
for A, B, C being category st A, B are_dual & B, C are_equivalent
holds A, C are_dual;
theorem :: YELLOW18:29
for A, B, C being category st A, B are_dual & B, C are_dual
holds A, C are_equivalent;
begin
:: Concrete categories
theorem :: YELLOW18:30
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 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;
registration
cluster quasi-functional -> para-functional for category;
end;
definition
let C be category;
let a be set;
func C-carrier_of a -> set 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;
notation
let C be category;
let a be Object of C;
synonym the_carrier_of a for C-carrier_of a;
end;
definition
let C be category;
let a be Object of C;
redefine func the_carrier_of a equals
:: YELLOW18:def 9
proj1 idm a;
end;
theorem :: YELLOW18:31
for A being non empty set, a being Object of EnsCat A holds idm a = id a;
theorem :: YELLOW18:32
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;
registration
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;
registration
cluster concrete -> para-functional semi-functional set-id-inheriting
for category;
cluster para-functional semi-functional set-id-inheriting -> concrete
for category;
end;
registration
cluster concrete quasi-functional strict for category;
end;
theorem :: YELLOW18:33
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:34
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;
registration
let A be para-functional category;
let a,b be Object of A;
cluster -> Function-like Relation-like for Morphism of a,b;
end;
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 dom f = the_carrier_of a & rng f c= the_carrier_of b;
theorem :: YELLOW18:36
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:37
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 :: YELLOW18:sch 16
ConcreteCategoryLambda { A() -> non empty set,
B(object,object) -> set,
D(object) -> 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 :: YELLOW18:sch 17
ConcreteCategoryQuasiLambda { A() -> non empty set,
P[object,object,object], D(object) -> 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 :: YELLOW18:sch 18
ConcreteCategoryEx { A() -> non empty set,
B(object) -> set, D[object, object], P[object,object,object] }:
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 :: YELLOW18:sch 19
ConcreteCategoryUniq1 { A() -> non empty set,
B(object,object) -> object }:
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 :: YELLOW18:sch 20
ConcreteCategoryUniq2 { A() -> non empty set,
P[object,object,object], D(object) -> 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 :: YELLOW18:sch 21
ConcreteCategoryUniq3 { A() -> non empty set, B(object) -> set,
D[object,object], P[object,object,object] }:
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
:: Equivalence between concrete categories
theorem :: YELLOW18:38
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:39
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: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 iso
holds f is one-to-one & rng f = the_carrier_of b;
theorem :: YELLOW18:41
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: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" = (f qua Function)";
scheme :: YELLOW18:sch 22
ConcreteCatEquivalence
{ A,B() -> para-functional semi-functional category,
O1, O2(object) -> object,
F1, F2(object,object,object) -> Function, A, B(object) -> 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
:: Concretization of categories
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:43
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]];
registration
let A be category;
let a be Object of A;
cluster (Concretized A)-carrier_of a -> non empty;
end;
theorem :: YELLOW18:44
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) &
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:45
for A being category, a, b being Object of A
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 :: YELLOW18:sch 23
NonUniqMSFunctionEx {I() -> set, A, B() -> ManySortedSet of I(),
P[object,object,object]}:
ex F being ManySortedFunction of A(), B() st
for i,x being object 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 object st i in I() & x in A().i
ex y being object 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;
registration
let A be category;
cluster Concretization A -> bijective;
end;
::$N Representation theorem for categories as concrete categories
theorem :: YELLOW18:46
for A being category holds A, Concretized A are_isomorphic;