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 :
begin
:: deftheorem defines with_finite_product CAT_4:def 3 :
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 :
:: deftheorem defines [x] CAT_4:def 5 :
:: deftheorem defines pr1 CAT_4:def 6 :
:: deftheorem defines pr2 CAT_4:def 7 :
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 :
theorem Th12:
theorem
theorem Th14:
theorem Th15:
:: deftheorem defines term CAT_4:def 10 :
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 :
:: deftheorem defines lambda' CAT_4:def 13 :
:: deftheorem defines rho CAT_4:def 14 :
:: deftheorem defines rho' CAT_4:def 15 :
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 :
theorem Th33:
theorem Th34:
theorem
:: deftheorem defines Delta CAT_4:def 17 :
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 :
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 :
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 :
:: deftheorem defines + CAT_4:def 23 :
:: deftheorem defines in1 CAT_4:def 24 :
:: deftheorem defines in2 CAT_4:def 25 :
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 :
theorem Th57:
theorem
theorem Th59:
:: deftheorem defines init CAT_4:def 28 :
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 :
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 :
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)