Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001
Association of Mizar Users
The abstract of the Mizar article:
-
- 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