begin
definition
let C be
Category;
let a,
b be
Object of
C;
canceled;redefine pred a,
b are_isomorphic means
(
Hom (
a,
b)
<> {} &
Hom (
b,
a)
<> {} & ex
f being
Morphism of
a,
b ex
f9 being
Morphism of
b,
a st
(
f * f9 = id b &
f9 * f = id a ) );
compatibility
( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )
by CAT_1:81;
end;
:: deftheorem CAT_4:def 1 :
canceled;
:: deftheorem defines are_isomorphic CAT_4:def 2 :
for C being Category
for a, b being Object of C holds
( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) );
begin
:: deftheorem defines with_finite_product CAT_4:def 3 :
for C being Category holds
( C is with_finite_product iff for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 ) );
theorem Th1:
definition
attr c1 is
strict ;
struct ProdCatStr -> CatStr ;
aggr ProdCatStr(#
carrier,
carrier',
Source,
Target,
Comp,
Id,
TerminalObj,
CatProd,
Proj1,
Proj2 #)
-> ProdCatStr ;
sel TerminalObj c1 -> Element of the
carrier of
c1;
sel CatProd c1 -> Function of
[: the carrier of c1, the carrier of c1:], the
carrier of
c1;
sel Proj1 c1 -> Function of
[: the carrier of c1, the carrier of c1:], the
carrier' of
c1;
sel Proj2 c1 -> Function of
[: the carrier of c1, the carrier of c1:], the
carrier' of
c1;
end;
:: deftheorem defines [1] CAT_4:def 4 :
for C being non empty non void ProdCatStr holds [1] C = the TerminalObj of C;
:: deftheorem defines [x] CAT_4:def 5 :
for C being non empty non void ProdCatStr
for a, b being Object of C holds a [x] b = the CatProd of C . (a,b);
:: deftheorem defines pr1 CAT_4:def 6 :
for C being non empty non void ProdCatStr
for a, b being Object of C holds pr1 (a,b) = the Proj1 of C . (a,b);
:: deftheorem defines pr2 CAT_4:def 7 :
for C being non empty non void ProdCatStr
for a, b being Object of C holds pr2 (a,b) = the Proj2 of C . (a,b);
definition
let o,
m be
set ;
func c1Cat (
o,
m)
-> strict ProdCatStr equals
ProdCatStr(#
{o},
{m},
(m :-> o),
(m :-> o),
((m,m) :-> m),
(o :-> m),
(Extract o),
((o,o) :-> o),
((o,o) :-> m),
((o,o) :-> m) #);
correctness
coherence
ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is strict ProdCatStr ;
;
end;
:: deftheorem defines c1Cat CAT_4:def 8 :
for o, m being set holds c1Cat (o,m) = ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);
theorem
for
o,
m being
set holds
CatStr(# the
carrier of
(c1Cat (o,m)), the
carrier' of
(c1Cat (o,m)), the
Source of
(c1Cat (o,m)), the
Target of
(c1Cat (o,m)), the
Comp of
(c1Cat (o,m)), the
Id of
(c1Cat (o,m)) #)
= 1Cat (
o,
m) ;
Lm1:
for o, m being set holds c1Cat (o,m) is Category-like
theorem
canceled;
theorem Th4:
theorem
canceled;
theorem Th6:
theorem Th7:
theorem
theorem
theorem Th10:
theorem Th11:
:: deftheorem Def9 defines Cartesian CAT_4:def 9 :
for IT being non empty non void Category-like ProdCatStr holds
( IT is Cartesian iff ( the TerminalObj of IT is terminal & ( for a, b being Object of IT holds
( cod ( the Proj1 of IT . (a,b)) = a & cod ( the Proj2 of IT . (a,b)) = b & the CatProd of IT . (a,b) is_a_product_wrt the Proj1 of IT . (a,b), the Proj2 of IT . (a,b) ) ) ) );
theorem Th12:
theorem
theorem Th14:
theorem Th15:
:: deftheorem defines term CAT_4:def 10 :
for C being Cartesian_category
for a being Object of C
for b3 being Morphism of a, [1] C holds
( b3 = term a iff verum );
theorem Th16:
theorem
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem
theorem
definition
let C be
Cartesian_category;
let a,
b,
c be
Object of
C;
let f be
Morphism of
c,
a;
let g be
Morphism of
c,
b;
assume A1:
(
Hom (
c,
a)
<> {} &
Hom (
c,
b)
<> {} )
;
func <:f,g:> -> Morphism of
c,
a [x] b means :
Def11:
(
(pr1 (a,b)) * it = f &
(pr2 (a,b)) * it = g );
existence
ex b1 being Morphism of c,a [x] b st
( (pr1 (a,b)) * b1 = f & (pr2 (a,b)) * b1 = g )
uniqueness
for b1, b2 being Morphism of c,a [x] b st (pr1 (a,b)) * b1 = f & (pr2 (a,b)) * b1 = g & (pr1 (a,b)) * b2 = f & (pr2 (a,b)) * b2 = g holds
b1 = b2
end;
:: deftheorem Def11 defines <: CAT_4:def 11 :
for C being Cartesian_category
for a, b, c being Object of C
for f being Morphism of c,a
for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
for b7 being Morphism of c,a [x] b holds
( b7 = <:f,g:> iff ( (pr1 (a,b)) * b7 = f & (pr2 (a,b)) * b7 = g ) );
theorem Th25:
theorem Th26:
theorem Th27:
for
C being
Cartesian_category for
c,
a,
b,
d being
Object of
C for
f being
Morphism of
c,
a for
g being
Morphism of
c,
b for
h being
Morphism of
d,
c st
Hom (
c,
a)
<> {} &
Hom (
c,
b)
<> {} &
Hom (
d,
c)
<> {} holds
<:(f * h),(g * h):> = <:f,g:> * h
theorem Th28:
for
C being
Cartesian_category for
c,
a,
b being
Object of
C for
f,
k being
Morphism of
c,
a for
g,
h being
Morphism of
c,
b st
Hom (
c,
a)
<> {} &
Hom (
c,
b)
<> {} &
<:f,g:> = <:k,h:> holds
(
f = k &
g = h )
theorem
theorem Th30:
definition
let C be
Cartesian_category;
let a be
Object of
C;
func lambda a -> Morphism of
([1] C) [x] a,
a equals
pr2 (
([1] C),
a);
correctness
coherence
pr2 (([1] C),a) is Morphism of ([1] C) [x] a,a;
;
func lambda' a -> Morphism of
a,
([1] C) [x] a equals
<:(term a),(id a):>;
correctness
coherence
<:(term a),(id a):> is Morphism of a,([1] C) [x] a;
;
func rho a -> Morphism of
a [x] ([1] C),
a equals
pr1 (
a,
([1] C));
correctness
coherence
pr1 (a,([1] C)) is Morphism of a [x] ([1] C),a;
;
func rho' a -> Morphism of
a,
a [x] ([1] C) equals
<:(id a),(term a):>;
correctness
coherence
<:(id a),(term a):> is Morphism of a,a [x] ([1] C);
;
end;
:: deftheorem defines lambda CAT_4:def 12 :
for C being Cartesian_category
for a being Object of C holds lambda a = pr2 (([1] C),a);
:: deftheorem defines lambda' CAT_4:def 13 :
for C being Cartesian_category
for a being Object of C holds lambda' a = <:(term a),(id a):>;
:: deftheorem defines rho CAT_4:def 14 :
for C being Cartesian_category
for a being Object of C holds rho a = pr1 (a,([1] C));
:: deftheorem defines rho' CAT_4:def 15 :
for C being Cartesian_category
for a being Object of C holds rho' a = <:(id a),(term a):>;
theorem Th31:
theorem
definition
let C be
Cartesian_category;
let a,
b be
Object of
C;
func Switch (
a,
b)
-> Morphism of
a [x] b,
b [x] a equals
<:(pr2 (a,b)),(pr1 (a,b)):>;
correctness
coherence
<:(pr2 (a,b)),(pr1 (a,b)):> is Morphism of a [x] b,b [x] a;
;
end;
:: deftheorem defines Switch CAT_4:def 16 :
for C being Cartesian_category
for a, b being Object of C holds Switch (a,b) = <:(pr2 (a,b)),(pr1 (a,b)):>;
theorem Th33:
theorem Th34:
theorem
:: deftheorem defines Delta CAT_4:def 17 :
for C being Cartesian_category
for a being Object of C holds Delta a = <:(id a),(id a):>;
theorem
theorem
definition
let C be
Cartesian_category;
let a,
b,
c be
Object of
C;
func Alpha (
a,
b,
c)
-> Morphism of
(a [x] b) [x] c,
a [x] (b [x] c) equals
<:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>;
correctness
coherence
<:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:> is Morphism of (a [x] b) [x] c,a [x] (b [x] c);
;
func Alpha' (
a,
b,
c)
-> Morphism of
a [x] (b [x] c),
(a [x] b) [x] c equals
<:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>;
correctness
coherence
<:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> is Morphism of a [x] (b [x] c),(a [x] b) [x] c;
;
end;
:: deftheorem defines Alpha CAT_4:def 18 :
for C being Cartesian_category
for a, b, c being Object of C holds Alpha (a,b,c) = <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>;
:: deftheorem defines Alpha' CAT_4:def 19 :
for C being Cartesian_category
for a, b, c being Object of C holds Alpha' (a,b,c) = <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>;
theorem Th38:
theorem Th39:
for
C being
Cartesian_category for
a,
b,
c being
Object of
C holds
(
(Alpha (a,b,c)) * (Alpha' (a,b,c)) = id (a [x] (b [x] c)) &
(Alpha' (a,b,c)) * (Alpha (a,b,c)) = id ((a [x] b) [x] c) )
theorem
definition
let C be
Cartesian_category;
let a,
b,
c,
d be
Object of
C;
let f be
Morphism of
a,
b;
let g be
Morphism of
c,
d;
func f [x] g -> Morphism of
a [x] c,
b [x] d equals
<:(f * (pr1 (a,c))),(g * (pr2 (a,c))):>;
correctness
coherence
<:(f * (pr1 (a,c))),(g * (pr2 (a,c))):> is Morphism of a [x] c,b [x] d;
;
end;
:: deftheorem defines [x] CAT_4:def 20 :
for C being Cartesian_category
for a, b, c, d being Object of C
for f being Morphism of a,b
for g being Morphism of c,d holds f [x] g = <:(f * (pr1 (a,c))),(g * (pr2 (a,c))):>;
theorem
theorem
theorem Th43:
for
C being
Cartesian_category for
a,
b,
c,
d,
e being
Object of
C for
f being
Morphism of
a,
b for
h being
Morphism of
c,
d for
g being
Morphism of
e,
a for
k being
Morphism of
e,
c st
Hom (
a,
b)
<> {} &
Hom (
c,
d)
<> {} &
Hom (
e,
a)
<> {} &
Hom (
e,
c)
<> {} holds
(f [x] h) * <:g,k:> = <:(f * g),(h * k):>
theorem
theorem
for
C being
Cartesian_category for
a,
b,
c,
d,
e,
s being
Object of
C for
f being
Morphism of
a,
b for
h being
Morphism of
c,
d for
g being
Morphism of
e,
a for
k being
Morphism of
s,
c st
Hom (
a,
b)
<> {} &
Hom (
c,
d)
<> {} &
Hom (
e,
a)
<> {} &
Hom (
s,
c)
<> {} holds
(f [x] h) * (g [x] k) = (f * g) [x] (h * k)
begin
:: deftheorem defines with_finite_coproduct CAT_4:def 21 :
for C being Category holds
( C is with_finite_coproduct iff for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 ) );
theorem Th46:
definition
attr c1 is
strict ;
struct CoprodCatStr -> CatStr ;
aggr CoprodCatStr(#
carrier,
carrier',
Source,
Target,
Comp,
Id,
Initial,
Coproduct,
Incl1,
Incl2 #)
-> CoprodCatStr ;
sel Initial c1 -> Element of the
carrier of
c1;
sel Coproduct c1 -> Function of
[: the carrier of c1, the carrier of c1:], the
carrier of
c1;
sel Incl1 c1 -> Function of
[: the carrier of c1, the carrier of c1:], the
carrier' of
c1;
sel Incl2 c1 -> Function of
[: the carrier of c1, the carrier of c1:], the
carrier' of
c1;
end;
:: deftheorem defines [[0]] CAT_4:def 22 :
for C being non empty non void CoprodCatStr holds [[0]] C = the Initial of C;
:: deftheorem defines + CAT_4:def 23 :
for C being non empty non void CoprodCatStr
for a, b being Object of C holds a + b = the Coproduct of C . (a,b);
:: deftheorem defines in1 CAT_4:def 24 :
for C being non empty non void CoprodCatStr
for a, b being Object of C holds in1 (a,b) = the Incl1 of C . (a,b);
:: deftheorem defines in2 CAT_4:def 25 :
for C being non empty non void CoprodCatStr
for a, b being Object of C holds in2 (a,b) = the Incl2 of C . (a,b);
definition
let o,
m be
set ;
func c1Cat* (
o,
m)
-> strict CoprodCatStr equals
CoprodCatStr(#
{o},
{m},
(m :-> o),
(m :-> o),
((m,m) :-> m),
(o :-> m),
(Extract o),
((o,o) :-> o),
((o,o) :-> m),
((o,o) :-> m) #);
correctness
coherence
CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is strict CoprodCatStr ;
;
end;
:: deftheorem defines c1Cat* CAT_4:def 26 :
for o, m being set holds c1Cat* (o,m) = CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);
theorem
for
o,
m being
set holds
CatStr(# the
carrier of
(c1Cat* (o,m)), the
carrier' of
(c1Cat* (o,m)), the
Source of
(c1Cat* (o,m)), the
Target of
(c1Cat* (o,m)), the
Comp of
(c1Cat* (o,m)), the
Id of
(c1Cat* (o,m)) #)
= 1Cat (
o,
m) ;
Lm2:
for o, m being set holds c1Cat* (o,m) is Category-like
theorem
canceled;
theorem Th49:
theorem
canceled;
theorem Th51:
theorem Th52:
theorem
theorem
theorem Th55:
theorem Th56:
:: deftheorem Def27 defines Cocartesian CAT_4:def 27 :
for IT being non empty non void Category-like CoprodCatStr holds
( IT is Cocartesian iff ( the Initial of IT is initial & ( for a, b being Object of IT holds
( dom ( the Incl1 of IT . (a,b)) = a & dom ( the Incl2 of IT . (a,b)) = b & the Coproduct of IT . (a,b) is_a_coproduct_wrt the Incl1 of IT . (a,b), the Incl2 of IT . (a,b) ) ) ) );
theorem Th57:
theorem
theorem Th59:
:: deftheorem defines init CAT_4:def 28 :
for C being Cocartesian_category
for a being Object of C
for b3 being Morphism of [[0]] C,a holds
( b3 = init a iff verum );
theorem Th60:
theorem Th61:
theorem
theorem
theorem Th64:
theorem Th65:
theorem Th66:
theorem
theorem
theorem
definition
let C be
Cocartesian_category;
let a,
b,
c be
Object of
C;
let f be
Morphism of
a,
c;
let g be
Morphism of
b,
c;
assume A1:
(
Hom (
a,
c)
<> {} &
Hom (
b,
c)
<> {} )
;
func [$f,g$] -> Morphism of
a + b,
c means :
Def29:
(
it * (in1 (a,b)) = f &
it * (in2 (a,b)) = g );
existence
ex b1 being Morphism of a + b,c st
( b1 * (in1 (a,b)) = f & b1 * (in2 (a,b)) = g )
uniqueness
for b1, b2 being Morphism of a + b,c st b1 * (in1 (a,b)) = f & b1 * (in2 (a,b)) = g & b2 * (in1 (a,b)) = f & b2 * (in2 (a,b)) = g holds
b1 = b2
end;
:: deftheorem Def29 defines [$ CAT_4:def 29 :
for C being Cocartesian_category
for a, b, c being Object of C
for f being Morphism of a,c
for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds
for b7 being Morphism of a + b,c holds
( b7 = [$f,g$] iff ( b7 * (in1 (a,b)) = f & b7 * (in2 (a,b)) = g ) );
theorem Th70:
theorem Th71:
theorem Th72:
for
C being
Cocartesian_category for
a,
c,
b,
d being
Object of
C for
f being
Morphism of
a,
c for
g being
Morphism of
b,
c for
h being
Morphism of
c,
d st
Hom (
a,
c)
<> {} &
Hom (
b,
c)
<> {} &
Hom (
c,
d)
<> {} holds
[$(h * f),(h * g)$] = h * [$f,g$]
theorem Th73:
for
C being
Cocartesian_category for
a,
c,
b being
Object of
C for
f,
k being
Morphism of
a,
c for
g,
h being
Morphism of
b,
c st
Hom (
a,
c)
<> {} &
Hom (
b,
c)
<> {} &
[$f,g$] = [$k,h$] holds
(
f = k &
g = h )
theorem
theorem
theorem
theorem
:: deftheorem defines nabla CAT_4:def 30 :
for C being Cocartesian_category
for a being Object of C holds nabla a = [$(id a),(id a)$];
definition
let C be
Cocartesian_category;
let a,
b,
c,
d be
Object of
C;
let f be
Morphism of
a,
c;
let g be
Morphism of
b,
d;
func f + g -> Morphism of
a + b,
c + d equals
[$((in1 (c,d)) * f),((in2 (c,d)) * g)$];
correctness
coherence
[$((in1 (c,d)) * f),((in2 (c,d)) * g)$] is Morphism of a + b,c + d;
;
end;
:: deftheorem defines + CAT_4:def 31 :
for C being Cocartesian_category
for a, b, c, d being Object of C
for f being Morphism of a,c
for g being Morphism of b,d holds f + g = [$((in1 (c,d)) * f),((in2 (c,d)) * g)$];
theorem
theorem
theorem Th80:
for
C being
Cocartesian_category for
a,
c,
b,
d,
e being
Object of
C for
f being
Morphism of
a,
c for
h being
Morphism of
b,
d for
g being
Morphism of
c,
e for
k being
Morphism of
d,
e st
Hom (
a,
c)
<> {} &
Hom (
b,
d)
<> {} &
Hom (
c,
e)
<> {} &
Hom (
d,
e)
<> {} holds
[$g,k$] * (f + h) = [$(g * f),(k * h)$]
theorem
theorem
for
C being
Cocartesian_category for
a,
c,
b,
d,
e,
s being
Object of
C for
f being
Morphism of
a,
c for
h being
Morphism of
b,
d for
g being
Morphism of
c,
e for
k being
Morphism of
d,
s st
Hom (
a,
c)
<> {} &
Hom (
b,
d)
<> {} &
Hom (
c,
e)
<> {} &
Hom (
d,
s)
<> {} holds
(g + k) * (f + h) = (g * f) + (k * h)