:: Concrete Categories
:: by Grzegorz Bancerek
::
:: Received January 12, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users
begin
:: Definability of categories and functors
scheme :: YELLOW18:sch 1
AltCatStrLambda{ F1() -> non empty set , F2( set , set ) -> set , F3( set , set , set , set , set ) -> set } :
ex C being non empty transitive strict AltCatStr st
( the carrier of C = F1() & ( for a, b being object of C holds <^a,b^> = F2(a,b) ) & ( for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being set st f in F2(a,b) & g in F2(b,c) holds
F3(a,b,c,f,g) in F2(a,c)
proofend;
scheme :: YELLOW18:sch 2
CatAssocSch{ F1() -> non empty transitive AltCatStr , F2( set , set , set , set , set ) -> set } :
F1() is associative
provided
A1: for a, b, c being object of F1() st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F2(a,b,c,f,g) and
A2: for a, b, c, d being object of F1()
for f, g, h being set st f in <^a,b^> & g in <^b,c^> & h in <^c,d^> holds
F2(a,c,d,F2(a,b,c,f,g),h) = F2(a,b,d,f,F2(b,c,d,g,h))
proofend;
scheme :: YELLOW18:sch 3
CatUnitsSch{ F1() -> non empty transitive AltCatStr , F2( set , set , set , set , set ) -> set } :
F1() is with_units
provided
A1: for a, b, c being object of F1() st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F2(a,b,c,f,g) and
A2: for a being object of F1() ex f being set st
( f in <^a,a^> & ( for b being object of F1()
for g being set st g in <^a,b^> holds
F2(a,a,b,f,g) = g ) ) and
A3: for a being object of F1() ex f being set st
( f in <^a,a^> & ( for b being object of F1()
for g being set st g in <^b,a^> holds
F2(b,a,a,g,f) = g ) )
proofend;
scheme :: YELLOW18:sch 4
CategoryLambda{ F1() -> non empty set , F2( set , set ) -> set , F3( set , set , set , set , set ) -> set } :
ex C being strict category st
( the carrier of C = F1() & ( for a, b being object of C holds <^a,b^> = F2(a,b) ) & ( for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being set st f in F2(a,b) & g in F2(b,c) holds
F3(a,b,c,f,g) in F2(a,c) and
A2: for a, b, c, d being Element of F1()
for f, g, h being set st f in F2(a,b) & g in F2(b,c) & h in F2(c,d) holds
F3(a,c,d,F3(a,b,c,f,g),h) = F3(a,b,d,f,F3(b,c,d,g,h)) and
A3: for a being Element of F1() ex f being set st
( f in F2(a,a) & ( for b being Element of F1()
for g being set st g in F2(a,b) holds
F3(a,a,b,f,g) = g ) ) and
A4: for a being Element of F1() ex f being set st
( f in F2(a,a) & ( for b being Element of F1()
for g being set st g in F2(b,a) holds
F3(b,a,a,g,f) = g ) )
proofend;
scheme :: YELLOW18:sch 5
CategoryLambdaUniq{ F1() -> non empty set , F2( set , set ) -> set , F3( set , set , set , set , set ) -> set } :
for C1, C2 being non empty transitive AltCatStr st the carrier of C1 = F1() & ( for a, b being object of C1 holds <^a,b^> = F2(a,b) ) & ( for a, b, c being object of C1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) & the carrier of C2 = F1() & ( for a, b being object of C2 holds <^a,b^> = F2(a,b) ) & ( for a, b, c being object of C2 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
proofend;
scheme :: YELLOW18:sch 6
CategoryQuasiLambda{ F1() -> non empty set , P1[ set , set , set ], F2( set , set ) -> set , F3( set , set , set , set , set ) -> set } :
ex C being strict category st
( the carrier of C = F1() & ( for a, b being object of C
for f being set holds
( f in <^a,b^> iff ( f in F2(a,b) & P1[a,b,f] ) ) ) & ( for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being set st f in F2(a,b) & P1[a,b,f] & g in F2(b,c) & P1[b,c,g] holds
( F3(a,b,c,f,g) in F2(a,c) & P1[a,c,F3(a,b,c,f,g)] ) and
A2: for a, b, c, d being Element of F1()
for f, g, h being set st f in F2(a,b) & P1[a,b,f] & g in F2(b,c) & P1[b,c,g] & h in F2(c,d) & P1[c,d,h] holds
F3(a,c,d,F3(a,b,c,f,g),h) = F3(a,b,d,f,F3(b,c,d,g,h)) and
A3: for a being Element of F1() ex f being set st
( f in F2(a,a) & P1[a,a,f] & ( for b being Element of F1()
for g being set st g in F2(a,b) & P1[a,b,g] holds
F3(a,a,b,f,g) = g ) ) and
A4: for a being Element of F1() ex f being set st
( f in F2(a,a) & P1[a,a,f] & ( for b being Element of F1()
for g being set st g in F2(b,a) & P1[b,a,g] holds
F3(b,a,a,g,f) = g ) )
proofend;
registration
let f be Function-yielding Function;
let a, b, c be set ;
clusterf . (a,b,c) -> Relation-like Function-like ;
coherence
( f . (a,b,c) is Relation-like & f . (a,b,c) is Function-like )
proofend;
end;
scheme :: YELLOW18:sch 7
SubcategoryEx{ F1() -> category, P1[ set ], P2[ set , set , set ] } :
ex B being non empty strict subcategory of F1() st
( ( for a being object of F1() holds
( a is object of B iff P1[a] ) ) & ( for a, b being object of F1()
for a9, b9 being object of B st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff P2[a,b,f] ) ) )
provided
A1: ex a being object of F1() st P1[a] and
A2: for a, b, c being object of F1() st P1[a] & P1[b] & P1[c] & <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f] and
A3: for a being object of F1() st P1[a] holds
P2[a,a, idm a]
proofend;
scheme :: YELLOW18:sch 8
CovariantFunctorLambda{ F1() -> category, F2() -> category, F3( set ) -> set , F4( set , set , set ) -> set } :
ex F being strict covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) )
provided
A1: for a being object of F1() holds F3(a) is object of F2() and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) and
A3: for a, b, c being object of F1() st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9 and
A4: for a being object of F1()
for a9 being object of F2() st a9 = F3(a) holds
F4(a,a,(idm a)) = idm a9
proofend;
theorem Th1: :: YELLOW18:1
for A, B being category
for 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^> <> {} holds
for f being Morphism of a,b holds F . f = G . f ) holds
FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #)
proofend;
scheme :: YELLOW18:sch 9
ContravariantFunctorLambda{ F1() -> category, F2() -> category, F3( set ) -> set , F4( set , set , set ) -> set } :
ex F being strict contravariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) )
provided
A1: for a being object of F1() holds F3(a) is object of F2() and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a)) and
A3: for a, b, c being object of F1() st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9 and
A4: for a being object of F1()
for a9 being object of F2() st a9 = F3(a) holds
F4(a,a,(idm a)) = idm a9
proofend;
theorem Th2: :: YELLOW18:2
for A, B being category
for 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^> <> {} holds
for f being Morphism of a,b holds F . f = G . f ) holds
FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #)
proofend;
begin
:: Isomorphism and equivalence of categories
definition
let A, B, C be non empty set ;
let f be Function of [:A,B:],C;
:: original:one-to-one
redefine attrf is one-to-one means :: YELLOW18:def 1
for a1, a2 being Element of A
for b1, b2 being Element of B st f . (a1,b1) = f . (a2,b2) holds
( a1 = a2 & b1 = b2 );
compatibility
( f is one-to-one iff for a1, a2 being Element of A
for b1, b2 being Element of B st f . (a1,b1) = f . (a2,b2) holds
( a1 = a2 & b1 = b2 ) )
proofend;
end;
:: deftheorem defines one-to-one YELLOW18:def_1_:_
for A, B, C being non empty set
for f being Function of [:A,B:],C holds
( f is one-to-one iff for a1, a2 being Element of A
for b1, b2 being Element of B st f . (a1,b1) = f . (a2,b2) holds
( a1 = a2 & b1 = b2 ) );
scheme :: YELLOW18:sch 10
CoBijectiveSch{ F1() -> category, F2() -> category, F3() -> covariant Functor of F1(),F2(), F4( set ) -> set , F5( set , set , set ) -> set } :
F3() is bijective
provided
A1: for a being object of F1() holds F3() . a = F4(a) and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F3() . f = F5(a,b,f) and
A3: for a, b being object of F1() st F4(a) = F4(b) holds
a = b and
A4: for a, b being object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F5(a,b,f) = F5(a,b,g) holds
f = g and
A5: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( a = F4(c) & b = F4(d) & <^c,d^> <> {} & f = F5(c,d,g) )
proofend;
scheme :: YELLOW18:sch 11
CatIsomorphism{ F1() -> category, F2() -> category, F3( set ) -> set , F4( set , set , set ) -> set } :
F1(),F2() are_isomorphic
provided
A1: ex F being covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) and
A2: for a, b being object of F1() st F3(a) = F3(b) holds
a = b and
A3: for a, b being object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g and
A4: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( a = F3(c) & b = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )
proofend;
scheme :: YELLOW18:sch 12
ContraBijectiveSch{ F1() -> category, F2() -> category, F3() -> contravariant Functor of F1(),F2(), F4( set ) -> set , F5( set , set , set ) -> set } :
F3() is bijective
provided
A1: for a being object of F1() holds F3() . a = F4(a) and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F3() . f = F5(a,b,f) and
A3: for a, b being object of F1() st F4(a) = F4(b) holds
a = b and
A4: for a, b being object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F5(a,b,f) = F5(a,b,g) holds
f = g and
A5: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( b = F4(c) & a = F4(d) & <^c,d^> <> {} & f = F5(c,d,g) )
proofend;
scheme :: YELLOW18:sch 13
CatAntiIsomorphism{ F1() -> category, F2() -> category, F3( set ) -> set , F4( set , set , set ) -> set } :
F1(),F2() are_anti-isomorphic
provided
A1: ex F being contravariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) and
A2: for a, b being object of F1() st F3(a) = F3(b) holds
a = b and
A3: for a, b being object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g and
A4: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )
proofend;
definition
let A, B be category;
predA,B are_equivalent means :: YELLOW18:def 2
ex F being covariant Functor of A,B ex G being covariant Functor of B,A st
( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent );
reflexivity
for A being category ex F, G being covariant Functor of A,A st
( G * F, id A are_naturally_equivalent & F * G, id A are_naturally_equivalent )
proofend;
symmetry
for A, B being category st ex F being covariant Functor of A,B ex G being covariant Functor of B,A st
( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent ) holds
ex F being covariant Functor of B,A ex G being covariant Functor of A,B st
( G * F, id B are_naturally_equivalent & F * G, id A are_naturally_equivalent ) ;
end;
:: deftheorem defines are_equivalent YELLOW18:def_2_:_
for A, B being category holds
( A,B are_equivalent iff ex F being covariant Functor of A,B ex G being covariant Functor of B,A st
( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent ) );
theorem Th3: :: 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 FunctorStr(# the ObjectMap of F1, the MorphMap of F1 #) = FunctorStr(# the ObjectMap of F2, the MorphMap of F2 #) & FunctorStr(# the ObjectMap of G1, the MorphMap of G1 #) = FunctorStr(# the ObjectMap of G2, the MorphMap of G2 #) holds
G1 * F1 = G2 * F2
proofend;
theorem Th4: :: YELLOW18:4
for A, B, C being category st A,B are_equivalent & B,C are_equivalent holds
A,C are_equivalent
proofend;
theorem Th5: :: YELLOW18:5
for A, B being category st A,B are_isomorphic holds
A,B are_equivalent
proofend;
scheme :: YELLOW18:sch 14
NatTransLambda{ F1() -> category, F2() -> category, F3() -> covariant Functor of F1(),F2(), F4() -> covariant Functor of F1(),F2(), F5( set ) -> set } :
ex t being natural_transformation of F3(),F4() st
( F3() is_naturally_transformable_to F4() & ( for a being object of F1() holds t ! a = F5(a) ) )
provided
A1: for a being object of F1() holds F5(a) in <^(F3() . a),(F4() . a)^> and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of (F3() . a),(F4() . a) st g1 = F5(a) holds
for g2 being Morphism of (F3() . b),(F4() . b) st g2 = F5(b) holds
g2 * (F3() . f) = (F4() . f) * g1
proofend;
scheme :: YELLOW18:sch 15
NatEquivalenceLambda{ F1() -> category, F2() -> category, F3() -> covariant Functor of F1(),F2(), F4() -> covariant Functor of F1(),F2(), F5( set ) -> set } :
ex t being natural_equivalence of F3(),F4() st
( F3(),F4() are_naturally_equivalent & ( for a being object of F1() holds t ! a = F5(a) ) )
provided
A1: for a being object of F1() holds
( F5(a) in <^(F3() . a),(F4() . a)^> & <^(F4() . a),(F3() . a)^> <> {} & ( for f being Morphism of (F3() . a),(F4() . a) st f = F5(a) holds
f is iso ) ) and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of (F3() . a),(F4() . a) st g1 = F5(a) holds
for g2 being Morphism of (F3() . b),(F4() . b) st g2 = F5(b) holds
g2 * (F3() . f) = (F4() . f) * g1
proofend;
begin
:: Dual categories
definition
let C1, C2 be non empty AltCatStr ;
predC1,C2 are_opposite means :Def3: :: 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
for C1, C2 being non empty AltCatStr st 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)) ) holds
( the carrier of C1 = the carrier of C2 & the Arrows of C1 = ~ the Arrows of C2 & ( for a, b, c being object of C2
for a9, b9, c9 being object of C1 st a9 = a & b9 = b & c9 = c holds
the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a)) ) )
proofend;
end;
:: deftheorem Def3 defines are_opposite YELLOW18:def_3_:_
for C1, C2 being non empty AltCatStr holds
( C1,C2 are_opposite iff ( 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)) ) ) );
theorem Th6: :: YELLOW18:6
for A, B being non empty AltCatStr st A,B are_opposite holds
for a being object of A holds a is object of B
proofend;
theorem Th7: :: YELLOW18:7
for A, B being non empty AltCatStr st A,B are_opposite holds
for a, b being object of A
for a9, b9 being object of B st a9 = a & b9 = b holds
<^a,b^> = <^b9,a9^>
proofend;
theorem :: YELLOW18:8
for A, B being non empty AltCatStr st A,B are_opposite holds
for a, b being object of A
for a9, b9 being object of B st a9 = a & b9 = b holds
for f being Morphism of a,b holds f is Morphism of b9,a9 by Th7;
theorem Th9: :: 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
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f ) ) ) ) )
proofend;
theorem Th10: :: YELLOW18:10
for A, B being category st A,B are_opposite holds
for a being object of A
for b being object of B st a = b holds
idm a = idm b
proofend;
theorem Th11: :: YELLOW18:11
for A, B being non empty transitive AltCatStr st A,B are_opposite & A is associative holds
B is associative
proofend;
theorem Th12: :: YELLOW18:12
for A, B being non empty transitive AltCatStr st A,B are_opposite & A is with_units holds
B is with_units
proofend;
theorem Th13: :: YELLOW18:13
for C, C1, C2 being non empty AltCatStr st C,C1 are_opposite holds
( C,C2 are_opposite iff AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) )
proofend;
definition
let C be non empty transitive AltCatStr ;
funcC opp -> non empty transitive strict AltCatStr means :Def4: :: YELLOW18:def 4
C,it are_opposite ;
uniqueness
for b1, b2 being non empty transitive strict AltCatStr st C,b1 are_opposite & C,b2 are_opposite holds
b1 = b2 by Th13;
existence
ex b1 being non empty transitive strict AltCatStr st C,b1 are_opposite
proofend;
end;
:: deftheorem Def4 defines opp YELLOW18:def_4_:_
for C being non empty transitive AltCatStr
for b2 being non empty transitive strict AltCatStr holds
( b2 = C opp iff C,b2 are_opposite );
registration
let C be non empty transitive associative AltCatStr ;
clusterC opp -> non empty transitive strict associative ;
coherence
C opp is associative
proofend;
end;
registration
let C be non empty transitive with_units AltCatStr ;
clusterC opp -> non empty transitive strict with_units ;
coherence
C opp is with_units
proofend;
end;
definition
let A, B be category;
assume B1: A,B are_opposite ;
deffunc H1( set ) -> set = $1;
deffunc H2( set , set , set ) -> set = $3;
A1: for a being object of A holds H1(a) is object of B by B1, Def3;
A2: now__::_thesis:_for_a,_b_being_object_of_A_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_H2(a,b,f)_in_the_Arrows_of_B_._(H1(b),H1(a))
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds H2(a,b,f) in the Arrows of B . (H1(b),H1(a)) )
assume A3: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds H2(a,b,f) in the Arrows of B . (H1(b),H1(a))
let f be Morphism of a,b; ::_thesis: H2(a,b,f) in the Arrows of B . (H1(b),H1(a))
reconsider a9 = a, b9 = b as object of B by A1;
<^a,b^> = <^b9,a9^> by B1, Th9
.= the Arrows of B . (b,a) ;
hence H2(a,b,f) in the Arrows of B . (H1(b),H1(a)) by A3; ::_thesis: verum
end;
A4: for a, b, c being object of A st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being object of B st a9 = H1(a) & b9 = H1(b) & c9 = H1(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = H2(a,b,f) & g9 = H2(b,c,g) holds
H2(a,c,g * f) = f9 * g9 by B1, Th9;
A5: for a being object of A
for a9 being object of B st a9 = H1(a) holds
H2(a,a, idm a) = idm a9 by B1, Th10;
func dualizing-func (A,B) -> strict contravariant Functor of A,B means :Def5: :: YELLOW18:def 5
( ( for a being object of A holds it . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds it . f = f ) );
existence
ex b1 being strict contravariant Functor of A,B st
( ( for a being object of A holds b1 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = f ) )
proofend;
uniqueness
for b1, b2 being strict contravariant Functor of A,B st ( for a being object of A holds b1 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = f ) & ( for a being object of A holds b2 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = f ) holds
b1 = b2
proofend;
end;
:: deftheorem Def5 defines dualizing-func YELLOW18:def_5_:_
for A, B being category st A,B are_opposite holds
for b3 being strict contravariant Functor of A,B holds
( b3 = dualizing-func (A,B) iff ( ( for a being object of A holds b3 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds b3 . f = f ) ) );
theorem Th14: :: YELLOW18:14
for A, B being category st A,B are_opposite holds
(dualizing-func (A,B)) * (dualizing-func (B,A)) = id B
proofend;
theorem Th15: :: YELLOW18:15
for A, B being category st A,B are_opposite holds
dualizing-func (A,B) is bijective
proofend;
registration
let A be category;
cluster dualizing-func (A,(A opp)) -> strict contravariant bijective ;
coherence
dualizing-func (A,(A opp)) is bijective
proofend;
cluster dualizing-func ((A opp),A) -> strict contravariant bijective ;
coherence
dualizing-func ((A opp),A) is bijective
proofend;
end;
theorem :: YELLOW18:16
for A, B being category st A,B are_opposite holds
A,B are_anti-isomorphic
proofend;
theorem Th17: :: YELLOW18:17
for A, B, C being category st A,B are_opposite holds
( A,C are_isomorphic iff B,C are_anti-isomorphic )
proofend;
theorem :: YELLOW18:18
for A, B, C, D being category st A,B are_opposite & C,D are_opposite & A,C are_isomorphic holds
B,D are_isomorphic
proofend;
theorem :: YELLOW18:19
for A, B, C, D being category st A,B are_opposite & C,D are_opposite & A,C are_anti-isomorphic holds
B,D are_anti-isomorphic
proofend;
Lm1: now__::_thesis:_for_A,_B_being_category_st_A,B_are_opposite_holds_
for_a,_b_being_object_of_A_st_<^a,b^>_<>_{}_&_<^b,a^>_<>_{}_holds_
for_a9,_b9_being_object_of_B_st_a9_=_a_&_b9_=_b_holds_
for_f_being_Morphism_of_a,b
for_f9_being_Morphism_of_b9,a9_st_f9_=_f_holds_
(_(_f_is_retraction_implies_f9_is_coretraction_)_&_(_f_is_coretraction_implies_f9_is_retraction_)_)
let A, B be category; ::_thesis: ( A,B are_opposite implies for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )
assume A1: A,B are_opposite ; ::_thesis: for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for a9, b9 being object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )
assume that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {} ; ::_thesis: for a9, b9 being object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )
let a9, b9 be object of B; ::_thesis: ( a9 = a & b9 = b implies for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )
assume that
A4: a9 = a and
A5: b9 = b ; ::_thesis: for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )
let f be Morphism of a,b; ::_thesis: for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )
let f9 be Morphism of b9,a9; ::_thesis: ( f9 = f implies ( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )
assume A6: f9 = f ; ::_thesis: ( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )
thus ( f is retraction implies f9 is coretraction ) ::_thesis: ( f is coretraction implies f9 is retraction )
proof
given g being Morphism of b,a such that A7: g is_right_inverse_of f ; :: according toALTCAT_3:def_2 ::_thesis: f9 is coretraction
reconsider g9 = g as Morphism of a9,b9 by A1, A4, A5, Th7;
take g9 ; :: according toALTCAT_3:def_3 ::_thesis: g9 is_left_inverse_of f9
f * g = idm b by A7, ALTCAT_3:def_1
.= idm b9 by A1, A5, Th10 ;
hence g9 * f9 = idm b9 by A1, A2, A3, A4, A5, A6, Th9; :: according toALTCAT_3:def_1 ::_thesis: verum
end;
thus ( f is coretraction implies f9 is retraction ) ::_thesis: verum
proof
given g being Morphism of b,a such that A8: g is_left_inverse_of f ; :: according toALTCAT_3:def_3 ::_thesis: f9 is retraction
reconsider g9 = g as Morphism of a9,b9 by A1, A4, A5, Th7;
take g9 ; :: according toALTCAT_3:def_2 ::_thesis: f9 is_left_inverse_of g9
g * f = idm a by A8, ALTCAT_3:def_1
.= idm a9 by A1, A4, Th10 ;
hence f9 * g9 = idm a9 by A1, A2, A3, A4, A5, A6, Th9; :: according toALTCAT_3:def_1 ::_thesis: verum
end;
end;
theorem :: YELLOW18:20
for A, B being category st A,B are_opposite holds
for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is retraction iff f9 is coretraction )
proofend;
theorem :: YELLOW18:21
for A, B being category st A,B are_opposite holds
for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is coretraction iff f9 is retraction )
proofend;
theorem Th22: :: YELLOW18:22
for A, B being category st A,B are_opposite holds
for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is retraction & f is coretraction holds
f9 " = f "
proofend;
theorem Th23: :: YELLOW18:23
for A, B being category st A,B are_opposite holds
for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso )
proofend;
theorem Th24: :: YELLOW18:24
for A, B, C, D being category st A,B are_opposite & C,D are_opposite holds
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
proofend;
theorem Th25: :: YELLOW18:25
for A, B, C, D being category st A,B are_opposite & C,D are_opposite & A,C are_equivalent holds
B,D are_equivalent
proofend;
definition
let A, B be category;
predA,B are_dual means :Def6: :: YELLOW18:def 6
A,B opp are_equivalent ;
symmetry
for A, B being category st A,B opp are_equivalent holds
B,A opp are_equivalent
proofend;
end;
:: deftheorem Def6 defines are_dual YELLOW18:def_6_:_
for A, B being category holds
( A,B are_dual iff A,B opp are_equivalent );
theorem :: YELLOW18:26
for A, B being category st A,B are_anti-isomorphic holds
A,B are_dual
proofend;
theorem :: YELLOW18:27
for A, B, C being category st A,B are_opposite holds
( A,C are_equivalent iff B,C are_dual )
proofend;
theorem :: YELLOW18:28
for A, B, C being category st A,B are_dual & B,C are_equivalent holds
A,C are_dual
proofend;
theorem :: YELLOW18:29
for A, B, C being category st A,B are_dual & B,C are_dual holds
A,C are_equivalent
proofend;
begin
:: Concrete categories
theorem Th30: :: 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 ) )
proofend;
definition
let C be category;
attrC 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;
:: deftheorem defines para-functional YELLOW18:def_7_:_
for C being category holds
( C is para-functional iff ex F being ManySortedSet of C st
for a1, a2 being object of C holds <^a1,a2^> c= Funcs ((F . a1),(F . a2)) );
registration
cluster non empty transitive quasi-functional associative with_units -> para-functional for AltCatStr ;
coherence
for b1 being category st b1 is quasi-functional holds
b1 is para-functional
proofend;
end;
definition
let C be category;
let a be set ;
funcC -carrier_of a -> set means :Def8: :: YELLOW18:def 8
ex b being object of C st
( b = a & it = proj1 (idm b) ) if a is object of C
otherwise it = {} ;
consistency
for b1 being set holds verum ;
existence
( ( a is object of C implies ex b1 being set ex b being object of C st
( b = a & b1 = proj1 (idm b) ) ) & ( a is not object of C implies ex b1 being set st b1 = {} ) )
proofend;
uniqueness
for b1, b2 being set holds
( ( a is object of C & ex b being object of C st
( b = a & b1 = proj1 (idm b) ) & ex b being object of C st
( b = a & b2 = proj1 (idm b) ) implies b1 = b2 ) & ( a is not object of C & b1 = {} & b2 = {} implies b1 = b2 ) ) ;
end;
:: deftheorem Def8 defines -carrier_of YELLOW18:def_8_:_
for C being category
for a being set
for b3 being set holds
( ( a is object of C implies ( b3 = C -carrier_of a iff ex b being object of C st
( b = a & b3 = proj1 (idm b) ) ) ) & ( a is not object of C implies ( b3 = C -carrier_of a iff b3 = {} ) ) );
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 C -carrier_of a equals :: YELLOW18:def 9
proj1 (idm a);
compatibility
for b1 being set holds
( b1 = C -carrier_of a iff b1 = proj1 (idm a) ) by Def8;
end;
:: deftheorem defines -carrier_of YELLOW18:def_9_:_
for C being category
for a being object of C holds C -carrier_of a = proj1 (idm a);
theorem Th31: :: YELLOW18:31
for A being non empty set
for a being object of (EnsCat A) holds idm a = id a
proofend;
theorem Th32: :: YELLOW18:32
for A being non empty set
for a being object of (EnsCat A) holds the_carrier_of a = a
proofend;
definition
let C be category;
attrC is set-id-inheriting means :Def10: :: YELLOW18:def 10
for a being object of C holds idm a = id (the_carrier_of a);
end;
:: deftheorem Def10 defines set-id-inheriting YELLOW18:def_10_:_
for C being category holds
( C is set-id-inheriting iff for a being object of C holds idm a = id (the_carrier_of a) );
registration
let A be non empty set ;
cluster EnsCat A -> set-id-inheriting ;
coherence
EnsCat A is set-id-inheriting
proofend;
end;
definition
let C be category;
attrC is concrete means :Def11: :: YELLOW18:def 11
( C is para-functional & C is semi-functional & C is set-id-inheriting );
end;
:: deftheorem Def11 defines concrete YELLOW18:def_11_:_
for C being category holds
( C is concrete iff ( C is para-functional & C is semi-functional & C is set-id-inheriting ) );
registration
cluster non empty transitive associative with_units concrete -> semi-functional para-functional set-id-inheriting for AltCatStr ;
coherence
for b1 being category st b1 is concrete holds
( b1 is para-functional & b1 is semi-functional & b1 is set-id-inheriting ) by Def11;
cluster non empty transitive semi-functional associative with_units para-functional set-id-inheriting -> concrete for AltCatStr ;
coherence
for b1 being category st b1 is para-functional & b1 is semi-functional & b1 is set-id-inheriting holds
b1 is concrete by Def11;
end;
registration
cluster non empty transitive strict quasi-functional associative with_units reflexive concrete for AltCatStr ;
existence
ex b1 being category st
( b1 is concrete & b1 is quasi-functional & b1 is strict )
proofend;
end;
theorem Th33: :: 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)) )
proofend;
theorem Th34: :: YELLOW18:34
for C being para-functional category
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds f is Function of (the_carrier_of a),(the_carrier_of b)
proofend;
registration
let A be para-functional category;
let a, b be object of A;
cluster -> Relation-like Function-like for Element of <^a,b^>;
coherence
for b1 being Morphism of a,b holds
( b1 is Function-like & b1 is Relation-like )
proofend;
end;
theorem Th35: :: YELLOW18:35
for C being para-functional category
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds
( dom f = the_carrier_of a & rng f c= the_carrier_of b )
proofend;
theorem Th36: :: YELLOW18:36
for C being semi-functional para-functional category
for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = g * f
proofend;
theorem Th37: :: YELLOW18:37
for C being semi-functional para-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)
proofend;
scheme :: YELLOW18:sch 16
ConcreteCategoryLambda{ F1() -> non empty set , F2( set , set ) -> set , F3( set ) -> set } :
ex C being strict concrete category st
( the carrier of C = F1() & ( for a being object of C holds the_carrier_of a = F3(a) ) & ( for a, b being object of C holds <^a,b^> = F2(a,b) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being Function st f in F2(a,b) & g in F2(b,c) holds
g * f in F2(a,c) and
A2: for a, b being Element of F1() holds F2(a,b) c= Funcs (F3(a),F3(b)) and
A3: for a being Element of F1() holds id F3(a) in F2(a,a)
proofend;
scheme :: YELLOW18:sch 17
ConcreteCategoryQuasiLambda{ F1() -> non empty set , P1[ set , set , set ], F2( set ) -> set } :
ex C being strict concrete category st
( the carrier of C = F1() & ( for a being object of C holds the_carrier_of a = F2(a) ) & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C . (a,b) iff ( f in Funcs (F2(a),F2(b)) & P1[a,b,f] ) ) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being Function st P1[a,b,f] & P1[b,c,g] holds
P1[a,c,g * f] and
A2: for a being Element of F1() holds P1[a,a, id F2(a)]
proofend;
scheme :: YELLOW18:sch 18
ConcreteCategoryEx{ F1() -> non empty set , F2( set ) -> set , P1[ set , set ], P2[ set , set , set ] } :
ex C being strict concrete category st
( the carrier of C = F1() & ( for a being object of C
for x being set holds
( x in the_carrier_of a iff ( x in F2(a) & P1[a,x] ) ) ) & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C . (a,b) iff ( f in Funcs ((C -carrier_of a),(C -carrier_of b)) & P2[a,b,f] ) ) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being Function st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f] and
A2: for a being Element of F1()
for X being set st ( for x being set holds
( x in X iff ( x in F2(a) & P1[a,x] ) ) ) holds
P2[a,a, id X]
proofend;
scheme :: YELLOW18:sch 19
ConcreteCategoryUniq1{ F1() -> non empty set , F2( set , set ) -> set } :
for C1, C2 being semi-functional para-functional category st the carrier of C1 = F1() & ( for a, b being object of C1 holds <^a,b^> = F2(a,b) ) & the carrier of C2 = F1() & ( for a, b being object of C2 holds <^a,b^> = F2(a,b) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
proofend;
scheme :: YELLOW18:sch 20
ConcreteCategoryUniq2{ F1() -> non empty set , P1[ set , set , set ], F2( set ) -> set } :
for C1, C2 being semi-functional para-functional category st the carrier of C1 = F1() & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C1 . (a,b) iff ( f in Funcs (F2(a),F2(b)) & P1[a,b,f] ) ) ) & the carrier of C2 = F1() & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C2 . (a,b) iff ( f in Funcs (F2(a),F2(b)) & P1[a,b,f] ) ) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
proofend;
scheme :: YELLOW18:sch 21
ConcreteCategoryUniq3{ F1() -> non empty set , F2( set ) -> set , P1[ set , set ], P2[ set , set , set ] } :
for C1, C2 being semi-functional para-functional category st the carrier of C1 = F1() & ( for a being object of C1
for x being set holds
( x in the_carrier_of a iff ( x in F2(a) & P1[a,x] ) ) ) & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C1 . (a,b) iff ( f in Funcs ((C1 -carrier_of a),(C1 -carrier_of b)) & P2[a,b,f] ) ) ) & the carrier of C2 = F1() & ( for a being object of C2
for x being set holds
( x in the_carrier_of a iff ( x in F2(a) & P1[a,x] ) ) ) & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C2 . (a,b) iff ( f in Funcs ((C2 -carrier_of a),(C2 -carrier_of b)) & P2[a,b,f] ) ) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
proofend;
begin
:: Equivalence between concrete categories
theorem Th38: :: YELLOW18:38
for C being concrete category
for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is retraction holds
rng f = the_carrier_of b
proofend;
theorem Th39: :: YELLOW18:39
for C being concrete category
for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is coretraction holds
f is one-to-one
proofend;
theorem Th40: :: YELLOW18:40
for C being concrete category
for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is iso holds
( f is one-to-one & rng f = the_carrier_of b )
proofend;
theorem Th41: :: YELLOW18:41
for C being semi-functional para-functional category
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b st f is one-to-one & f " in <^b,a^> holds
f is iso
proofend;
theorem :: YELLOW18:42
for C being concrete category
for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is iso holds
f " = f "
proofend;
scheme :: YELLOW18:sch 22
ConcreteCatEquivalence{ F1() -> semi-functional para-functional category, F2() -> semi-functional para-functional category, F3( set ) -> set , F4( set ) -> set , F5( set , set , set ) -> Function, F6( set , set , set ) -> Function, F7( set ) -> Function, F8( set ) -> Function } :
F1(),F2() are_equivalent
provided
A1: ex F being covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F5(a,b,f) ) ) and
A2: ex G being covariant Functor of F2(),F1() st
( ( for a being object of F2() holds G . a = F4(a) ) & ( for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = F6(a,b,f) ) ) and
A3: for a, b being object of F1() st a = F4(F3(b)) holds
( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one ) and
A4: for a, b being object of F2() st b = F3(F4(a)) holds
( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one ) and
A5: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) and
A6: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f
proofend;
begin
:: Concretization of categories
definition
let C be category;
defpred S1[ set , set ] means $1 = $2 `22 ;
defpred S2[ set , set , Function] means ex fa, fb being object of C ex g being Morphism of fa,fb st
( fa = $1 & fb = $2 & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds $3 . [h,[o,fa]] = [(g * h),[o,fb]] ) );
deffunc H1( set ) -> set = Union (disjoin the Arrows of C);
A1: for a, b, c being Element of C
for f, g being Function st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
proofend;
A13: for a being Element of C
for X being set st ( for x being set holds
( x in X iff ( x in H1(a) & S1[a,x] ) ) ) holds
S2[a,a, id X]
proofend;
func Concretized C -> strict concrete category means :Def12: :: 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
for 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 ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) );
uniqueness
for b1, b2 being strict concrete category st the carrier of b1 = the carrier of C & ( for a being object of b1
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
for f being Function holds
( f in the Arrows of b1 . (a,b) iff ( f in Funcs ((b1 -carrier_of a),(b1 -carrier_of b)) & ex fa, fb being object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) & the carrier of b2 = the carrier of C & ( for a being object of b2
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
for f being Function holds
( f in the Arrows of b2 . (a,b) iff ( f in Funcs ((b2 -carrier_of a),(b2 -carrier_of b)) & ex fa, fb being object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) holds
b1 = b2
proofend;
existence
ex b1 being strict concrete category st
( the carrier of b1 = the carrier of C & ( for a being object of b1
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
for f being Function holds
( f in the Arrows of b1 . (a,b) iff ( f in Funcs ((b1 -carrier_of a),(b1 -carrier_of b)) & ex fa, fb being object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) )
proofend;
end;
:: deftheorem Def12 defines Concretized YELLOW18:def_12_:_
for C being category
for b2 being strict concrete category holds
( b2 = Concretized C iff ( the carrier of b2 = the carrier of C & ( for a being object of b2
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
for f being Function holds
( f in the Arrows of b2 . (a,b) iff ( f in Funcs ((b2 -carrier_of a),(b2 -carrier_of b)) & ex fa, fb being object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) ) );
theorem Th43: :: YELLOW18:43
for A being category
for a being object of A
for x being set holds
( x in (Concretized A) -carrier_of a iff ex b being object of A ex f being Morphism of b,a st
( <^b,a^> <> {} & x = [f,[b,a]] ) )
proofend;
registration
let A be category;
let a be object of A;
cluster(Concretized A) -carrier_of a -> non empty ;
coherence
not (Concretized A) -carrier_of a is empty
proofend;
end;
theorem Th44: :: YELLOW18:44
for A being category
for a, b being object of A st <^a,b^> <> {} holds
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
for g being Morphism of c,a st <^c,a^> <> {} holds
F . [g,[c,a]] = [(f * g),[c,b]] ) )
proofend;
theorem Th45: :: YELLOW18:45
for A being category
for 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
proofend;
scheme :: YELLOW18:sch 23
NonUniqMSFunctionEx{ F1() -> set , F2() -> ManySortedSet of F1(), F3() -> ManySortedSet of F1(), P1[ set , set , set ] } :
ex F being ManySortedFunction of F2(),F3() st
for i, x being set st i in F1() & x in F2() . i holds
( (F . i) . x in F3() . i & P1[i,x,(F . i) . x] )
provided
A1: for i, x being set st i in F1() & x in F2() . i holds
ex y being set st
( y in F3() . i & P1[i,x,y] )
proofend;
definition
let A be category;
set B = Concretized A;
func Concretization A -> strict covariant Functor of A, Concretized A means :Def13: :: YELLOW18:def 13
( ( for a being object of A holds it . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (it . f) . [(idm a),[a,a]] = [f,[a,b]] ) );
uniqueness
for b1, b2 being strict covariant Functor of A, Concretized A st ( for a being object of A holds b1 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b1 . f) . [(idm a),[a,a]] = [f,[a,b]] ) & ( for a being object of A holds b2 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b2 . f) . [(idm a),[a,a]] = [f,[a,b]] ) holds
b1 = b2
proofend;
existence
ex b1 being strict covariant Functor of A, Concretized A st
( ( for a being object of A holds b1 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b1 . f) . [(idm a),[a,a]] = [f,[a,b]] ) )
proofend;
end;
:: deftheorem Def13 defines Concretization YELLOW18:def_13_:_
for A being category
for b2 being strict covariant Functor of A, Concretized A holds
( b2 = Concretization A iff ( ( for a being object of A holds b2 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b2 . f) . [(idm a),[a,a]] = [f,[a,b]] ) ) );
registration
let A be category;
cluster Concretization A -> strict covariant bijective ;
coherence
Concretization A is bijective
proofend;
end;
:: [WP: ] Representation_theorem_for_categories_as_concrete_categories
theorem :: YELLOW18:46
for A being category holds A, Concretized A are_isomorphic
proofend;