:: Subcategories and Products of Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received May 31, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

let D be non empty set ;
let X be set ;
let E be non empty set ;
let F be FUNCTION_DOMAIN of X,E;
let f be Function of D,F;
let d be Element of D;
:: original: .
redefine func f . d -> Element of F;
coherence
f . d is Element of F

proof end;

end;

theorem Th1: :: CAT_2:1

for C, D, E being non empty set
for f being Function of [:C,D:],E holds curry f is Function of C,(Funcs (D,E))

proof end;

theorem Th2: :: CAT_2:2

for D, C, E being non empty set
for f being Function of [:C,D:],E holds curry' f is Function of D,(Funcs (C,E))

proof end;

definition

let C, D, E be non empty set ;
let f be Function of [:C,D:],E;
:: original: curry
redefine func curry f -> Function of C,(Funcs (D,E));
coherence
curry f is Function of C,(Funcs (D,E)) by Th1;
:: original: curry'
redefine func curry' f -> Function of D,(Funcs (C,E));
coherence
curry' f is Function of D,(Funcs (C,E)) by Th2;

end;

theorem Th3: :: CAT_2:3

for C, D, E being non empty set
for c being Element of C
for d being Element of D
for f being Function of [:C,D:],E holds f . (c,d) = ((curry f) . c) . d

proof end;

theorem Th4: :: CAT_2:4

for C, D, E being non empty set
for c being Element of C
for d being Element of D
for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c

proof end;

definition

let B, C be Category;
let c be Object of C;
func B --> c -> Functor of B,C equals :: CAT_2:def 1
the carrier' of B --> (id c);
coherence
the carrier' of B --> (id c) is Functor of B,C

proof end;

end;

:: deftheorem defines --> CAT_2:def 1 :
for B, C being Category
for c being Object of C holds B --> c = the carrier' of B --> (id c);

theorem :: CAT_2:5

canceled;

theorem :: CAT_2:6

canceled;

theorem :: CAT_2:7

for C, B being Category
for c being Object of C
for b being Object of B holds (Obj (B --> c)) . b = c

proof end;

definition

let C, D be Category;
func Funct (C,D) -> set means :Def2: :: CAT_2:def 2
for x being set holds
( x in it iff x is Functor of C,D );
existence
ex b₁ being set st
for x being set holds
( x in b₁ iff x is Functor of C,D )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is Functor of C,D ) ) & ( for x being set holds
( x in b₂ iff x is Functor of C,D ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Funct CAT_2:def 2 :
for C, D being Category
for b₃ being set holds
( b₃ = Funct (C,D) iff for x being set holds
( x in b₃ iff x is Functor of C,D ) );

registration

let C, D be Category;
cluster Funct (C,D) -> non empty ;
coherence
not Funct (C,D) is empty

proof end;

end;

definition

let C, D be Category;
mode FUNCTOR-DOMAIN of C,D -> non empty set means :Def3: :: CAT_2:def 3
for x being Element of it holds x is Functor of C,D;
existence
ex b₁ being non empty set st
for x being Element of b₁ holds x is Functor of C,D

proof end;

end;

:: deftheorem Def3 defines FUNCTOR-DOMAIN CAT_2:def 3 :
for C, D being Category
for b₃ being non empty set holds
( b₃ is FUNCTOR-DOMAIN of C,D iff for x being Element of b₃ holds x is Functor of C,D );

definition

let C, D be Category;
let F be FUNCTOR-DOMAIN of C,D;
:: original: Element
redefine mode Element of F -> Functor of C,D;
coherence
for b₁ being Element of F holds b₁ is Functor of C,D by Def3;

end;

definition

let A be non empty set ;
let C, D be Category;
let F be FUNCTOR-DOMAIN of C,D;
let T be Function of A,F;
let x be Element of A;
:: original: .
redefine func T . x -> Element of F;
coherence
T . x is Element of F

proof end;

end;

definition

let C, D be Category;
:: original: Funct
redefine func Funct (C,D) -> FUNCTOR-DOMAIN of C,D;
coherence
Funct (C,D) is FUNCTOR-DOMAIN of C,D

proof end;

end;

definition

let C be Category;
mode Subcategory of C -> Category means :Def4: :: CAT_2:def 4
( the carrier of it c= the carrier of C & ( for a, b being Object of it
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of it c= the Comp of C & ( for a being Object of it
for a9 being Object of C st a = a9 holds
id a = id a9 ) );
existence
ex b₁ being Category st
( the carrier of b₁ c= the carrier of C & ( for a, b being Object of b₁
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of b₁ c= the Comp of C & ( for a being Object of b₁
for a9 being Object of C st a = a9 holds
id a = id a9 ) )

proof end;

end;

:: deftheorem Def4 defines Subcategory CAT_2:def 4 :
for C, b₂ being Category holds
( b₂ is Subcategory of C iff ( the carrier of b₂ c= the carrier of C & ( for a, b being Object of b₂
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of b₂ c= the Comp of C & ( for a being Object of b₂
for a9 being Object of C st a = a9 holds
id a = id a9 ) ) );

registration

let C be Category;
cluster non empty non void strict Category-like Subcategory of C;
existence
ex b₁ being Subcategory of C st b₁ is strict

proof end;

end;

theorem :: CAT_2:8

canceled;

theorem :: CAT_2:9

canceled;

theorem :: CAT_2:10

canceled;

theorem :: CAT_2:11

canceled;

theorem Th12: :: CAT_2:12

for C being Category
for E being Subcategory of C
for e being Object of E holds e is Object of C

proof end;

theorem Th13: :: CAT_2:13

for C being Category
for E being Subcategory of C holds the carrier' of E c= the carrier' of C

proof end;

theorem Th14: :: CAT_2:14

for C being Category
for E being Subcategory of C
for f being Morphism of E holds f is Morphism of C

proof end;

theorem Th15: :: CAT_2:15

for C being Category
for E being Subcategory of C
for f being Morphism of E
for f9 being Morphism of C st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )

proof end;

theorem :: CAT_2:16

for C being Category
for E being Subcategory of C
for a, b being Object of E
for a9, b9 being Object of C
for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds
f is Morphism of a9,b9

proof end;

theorem Th17: :: CAT_2:17

for C being Category
for E being Subcategory of C
for f, g being Morphism of E
for f9, g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds
g * f = g9 * f9

proof end;

theorem :: CAT_2:18

for C being Category holds C is Subcategory of C

proof end;

theorem Th19: :: CAT_2:19

for C being Category
for E being Subcategory of C holds id E is Functor of E,C

proof end;

definition

let C be Category;
let E be Subcategory of C;
func incl E -> Functor of E,C equals :: CAT_2:def 5
id E;
coherence
id E is Functor of E,C by Th19;

end;

:: deftheorem defines incl CAT_2:def 5 :
for C being Category
for E being Subcategory of C holds incl E = id E;

theorem :: CAT_2:20

canceled;

theorem :: CAT_2:21

canceled;

theorem Th22: :: CAT_2:22

for C being Category
for E being Subcategory of C
for a being Object of E holds (Obj (incl E)) . a = a

proof end;

theorem :: CAT_2:23

for C being Category
for E being Subcategory of C
for a being Object of E holds (incl E) . a = a by Th22;

theorem :: CAT_2:24

for C being Category
for E being Subcategory of C holds incl E is faithful

proof end;

theorem Th25: :: CAT_2:25

for C being Category
for E being Subcategory of C holds
( incl E is full iff for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) )

proof end;

definition

let C be non empty non void CatStr ;
let D be Category;
pred C is_full_subcategory_of D means :Def6: :: CAT_2:def 6
( C is Subcategory of D & ( for a, b being Object of C
for a9, b9 being Object of D st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) ) );

end;

:: deftheorem Def6 defines is_full_subcategory_of CAT_2:def 6 :
for C being non empty non void CatStr
for D being Category holds
( C is_full_subcategory_of D iff ( C is Subcategory of D & ( for a, b being Object of C
for a9, b9 being Object of D st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) ) ) );

theorem :: CAT_2:26

canceled;

theorem :: CAT_2:27

for C being Category
for E being Subcategory of C holds
( E is_full_subcategory_of C iff incl E is full )

proof end;

theorem Th28: :: CAT_2:28

for C being Category
for O being non empty Subset of the carrier of C holds union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C

proof end;

theorem Th29: :: CAT_2:29

for C being Category
for O being non empty Subset of the carrier of C
for M being non empty set st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } holds
( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M & the Id of C | O is Function of O,M )

proof end;

registration

let O, M be non empty set ;
let d, c be Function of M,O;
let p be PartFunc of [:M,M:],M;
let i be Function of O,M;
cluster CatStr(# O,M,d,c,p,i #) -> non empty non void ;
coherence
( not CatStr(# O,M,d,c,p,i #) is void & not CatStr(# O,M,d,c,p,i #) is empty ) ;

end;

theorem :: CAT_2:30

for C being Category
for O being non empty Subset of the carrier of C
for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M & i = the Id of C | O holds
CatStr(# O,M,d,c,p,i #) is_full_subcategory_of C

proof end;

theorem :: CAT_2:31

for C being Category
for O being non empty Subset of the carrier of C
for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st CatStr(# O,M,d,c,p,i #) is_full_subcategory_of C holds
( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M & i = the Id of C | O )

proof end;

definition

let X1, X2, Y1, Y2 be non empty set ;
let f1 be Function of X1,Y1;
let f2 be Function of X2,Y2;
:: original: [:
redefine func [:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:];
coherence
[:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:]

proof end;

end;

definition

let A, B be non empty set ;
let f be PartFunc of [:A,A:],A;
let g be PartFunc of [:B,B:],B;
:: original: |:
redefine func |:f,g:| -> PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:];
coherence
|:f,g:| is PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:] by FUNCT_4:62;

end;

definition

let C, D be Category;
func [:C,D:] -> Category equals :: CAT_2:def 7
CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:|,[: the Id of C, the Id of D:] #);
coherence
CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:|,[: the Id of C, the Id of D:] #) is Category

proof end;

end;

:: deftheorem defines [: CAT_2:def 7 :
for C, D being Category holds [:C,D:] = CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:|,[: the Id of C, the Id of D:] #);

registration

let C, D be Category;
cluster [:C,D:] -> strict ;
coherence
[:C,D:] is strict ;

end;

theorem :: CAT_2:32

canceled;

theorem :: CAT_2:33

for C, D being Category holds
( the carrier of [:C,D:] = [: the carrier of C, the carrier of D:] & the carrier' of [:C,D:] = [: the carrier' of C, the carrier' of D:] & the Source of [:C,D:] = [: the Source of C, the Source of D:] & the Target of [:C,D:] = [: the Target of C, the Target of D:] & the Comp of [:C,D:] = |: the Comp of C, the Comp of D:| & the Id of [:C,D:] = [: the Id of C, the Id of D:] ) ;

theorem Th34: :: CAT_2:34

for C, D being Category
for c being Object of C
for d being Object of D holds [c,d] is Object of [:C,D:] ;

definition

let C, D be Category;
let c be Object of C;
let d be Object of D;
:: original: [
redefine func [c,d] -> Object of [:C,D:];
coherence
[c,d] is Object of [:C,D:] by Th34;

end;

theorem :: CAT_2:35

for C, D being Category
for cd being Object of [:C,D:] ex c being Object of C ex d being Object of D st cd = [c,d] by DOMAIN_1:9;

theorem Th36: :: CAT_2:36

for C, D being Category
for f being Morphism of C
for g being Morphism of D holds [f,g] is Morphism of [:C,D:] ;

definition

let C, D be Category;
let f be Morphism of C;
let g be Morphism of D;
:: original: [
redefine func [f,g] -> Morphism of [:C,D:];
coherence
[f,g] is Morphism of [:C,D:] by Th36;

end;

theorem :: CAT_2:37

for C, D being Category
for fg being Morphism of [:C,D:] ex f being Morphism of C ex g being Morphism of D st fg = [f,g] by DOMAIN_1:9;

theorem Th38: :: CAT_2:38

for C, D being Category
for f being Morphism of C
for g being Morphism of D holds
( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] )

proof end;

theorem Th39: :: CAT_2:39

for C, D being Category
for f, f9 being Morphism of C
for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds
[f9,g9] * [f,g] = [(f9 * f),(g9 * g)]

proof end;

theorem Th40: :: CAT_2:40

for C, D being Category
for f, f9 being Morphism of C
for g, g9 being Morphism of D st dom [f9,g9] = cod [f,g] holds
[f9,g9] * [f,g] = [(f9 * f),(g9 * g)]

proof end;

theorem Th41: :: CAT_2:41

for C, D being Category
for c being Object of C
for d being Object of D holds id [c,d] = [(id c),(id d)]

proof end;

theorem :: CAT_2:42

for C, D being Category
for c, c9 being Object of C
for d, d9 being Object of D holds Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]

proof end;

theorem :: CAT_2:43

for C, D being Category
for c, c9 being Object of C
for f being Morphism of c,c9
for d, d9 being Object of D
for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]

proof end;

definition

let C, C9, D be Category;
let S be Functor of [:C,C9:],D;
let m be Morphism of C;
let m9 be Morphism of C9;
:: original: .
redefine func S . (m,m9) -> Morphism of D;
coherence
S . (m,m9) is Morphism of D

proof end;

end;

theorem Th44: :: CAT_2:44

for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c being Object of C holds (curry S) . (id c) is Functor of C9,D

proof end;

theorem Th45: :: CAT_2:45

for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D

proof end;

definition

let C, C9, D be Category;
let S be Functor of [:C,C9:],D;
let c be Object of C;
func S ?- c -> Functor of C9,D equals :: CAT_2:def 8
(curry S) . (id c);
coherence
(curry S) . (id c) is Functor of C9,D by Th44;

end;

:: deftheorem defines ?- CAT_2:def 8 :
for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c being Object of C holds S ?- c = (curry S) . (id c);

theorem :: CAT_2:46

canceled;

theorem :: CAT_2:47

for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c being Object of C
for f being Morphism of C9 holds (S ?- c) . f = S . ((id c),f) by Th3;

theorem :: CAT_2:48

for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c being Object of C
for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . (c,c9)

proof end;

definition

let C, C9, D be Category;
let S be Functor of [:C,C9:],D;
let c9 be Object of C9;
func S -? c9 -> Functor of C,D equals :: CAT_2:def 9
(curry' S) . (id c9);
coherence
(curry' S) . (id c9) is Functor of C,D by Th45;

end;

:: deftheorem defines -? CAT_2:def 9 :
for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c9 being Object of C9 holds S -? c9 = (curry' S) . (id c9);

theorem :: CAT_2:49

canceled;

theorem :: CAT_2:50

for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c9 being Object of C9
for f being Morphism of C holds (S -? c9) . f = S . (f,(id c9)) by Th4;

theorem :: CAT_2:51

for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c being Object of C
for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . (c,c9)

proof end;

theorem :: CAT_2:52

for C, B, D being Category
for L being Function of the carrier of C,(Funct (B,D))
for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C
for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) * ((L . (dom g)) . f) = ((L . (cod g)) . f) * ((M . (dom f)) . g) ) holds
ex S being Functor of [:B,C:],D st
for f being Morphism of B
for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) * ((M . (dom f)) . g)

proof end;

theorem :: CAT_2:53

for C, B, D being Category
for L being Function of the carrier of C,(Funct (B,D))
for M being Function of the carrier of B,(Funct (C,D)) st ex S being Functor of [:B,C:],D st
for c being Object of C
for b being Object of B holds
( S -? c = L . c & S ?- b = M . b ) holds
for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) * ((L . (dom g)) . f) = ((L . (cod g)) . f) * ((M . (dom f)) . g)

proof end;

theorem Th54: :: CAT_2:54

for C, D being Category holds pr1 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],C

proof end;

theorem Th55: :: CAT_2:55

for C, D being Category holds pr2 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],D

proof end;

definition

let C, D be Category;
func pr1 (C,D) -> Functor of [:C,D:],C equals :: CAT_2:def 10
pr1 ( the carrier' of C, the carrier' of D);
coherence
pr1 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],C by Th54;
func pr2 (C,D) -> Functor of [:C,D:],D equals :: CAT_2:def 11
pr2 ( the carrier' of C, the carrier' of D);
coherence
pr2 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],D by Th55;

end;

:: deftheorem defines pr1 CAT_2:def 10 :
for C, D being Category holds pr1 (C,D) = pr1 ( the carrier' of C, the carrier' of D);

:: deftheorem defines pr2 CAT_2:def 11 :
for C, D being Category holds pr2 (C,D) = pr2 ( the carrier' of C, the carrier' of D);

theorem :: CAT_2:56

canceled;

theorem :: CAT_2:57

canceled;

theorem :: CAT_2:58

canceled;

theorem :: CAT_2:59

for C, D being Category
for c being Object of C
for d being Object of D holds (Obj (pr1 (C,D))) . (c,d) = c

proof end;

theorem :: CAT_2:60

canceled;

theorem :: CAT_2:61

for C, D being Category
for c being Object of C
for d being Object of D holds (Obj (pr2 (C,D))) . (c,d) = d

proof end;

theorem Th62: :: CAT_2:62

for C, D, D9 being Category
for T being Functor of C,D
for T9 being Functor of C,D9 holds <:T,T9:> is Functor of C,[:D,D9:]

proof end;

definition

let C, D, D9 be Category;
let T be Functor of C,D;
let T9 be Functor of C,D9;
:: original: <:
redefine func <:T,T9:> -> Functor of C,[:D,D9:];
coherence
<:T,T9:> is Functor of C,[:D,D9:] by Th62;

end;

theorem :: CAT_2:63

for C, D, D9 being Category
for T being Functor of C,D
for T9 being Functor of C,D9
for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]

proof end;

theorem Th64: :: CAT_2:64

for C, D, C9, D9 being Category
for T being Functor of C,D
for T9 being Functor of C9,D9 holds [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):>

proof end;

theorem Th65: :: CAT_2:65

for C, D, C9, D9 being Category
for T being Functor of C,D
for T9 being Functor of C9,D9 holds [:T,T9:] is Functor of [:C,C9:],[:D,D9:]

proof end;

definition

let C, C9, D, D9 be Category;
let T be Functor of C,D;
let T9 be Functor of C9,D9;
:: original: [:
redefine func [:T,T9:] -> Functor of [:C,C9:],[:D,D9:];
coherence
[:T,T9:] is Functor of [:C,C9:],[:D,D9:] by Th65;

end;

theorem :: CAT_2:66

for C, D, C9, D9 being Category
for T being Functor of C,D
for T9 being Functor of C9,D9
for c being Object of C
for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)]

proof end;