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


begin

theorem :: CAT_2:1
canceled;

theorem :: CAT_2:2
canceled;

theorem :: CAT_2:3
canceled;

theorem :: CAT_2:4
canceled;

:: Auxiliary theorems on Functors
definition
let B, C be Category;
let c be Object of C;
funcB --> 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
proofend;
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
for C, B being Category
for c being Object of C
for b being Object of B holds (Obj (B --> c)) . b = c
proofend;

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 b1 being set st
for x being set holds
( x in b1 iff x is Functor of C,D )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Functor of C,D ) ) & ( for x being set holds
( x in b2 iff x is Functor of C,D ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Funct CAT_2:def_2_:_
 for C, D being Category
for b3 being set holds
( b3 = Funct (C,D) iff for x being set holds
( x in b3 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
proofend;
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 b1 being non empty set st
for x being Element of b1 holds x is Functor of C,D
proofend;
end;

:: deftheorem Def3 defines FUNCTOR-DOMAIN CAT_2:def_3_:_
 for C, D being Category
for b3 being non empty set holds
( b3 is FUNCTOR-DOMAIN of C,D iff for x being Element of b3 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 b1 being Element of F holds b1 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 funcT . x ->  Element of F;
coherence
 T . x is Element of F
proofend;
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
proofend;
end;

:: Subcategory
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 b1 being Category st
( the carrier of b1 c= the carrier of C & ( for a, b being Object of b1
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of b1 c= the Comp of C & ( for a being Object of b1
for a9 being Object of C st a = a9 holds
id a = id a9 ) )
proofend;
end;

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

registration
let C be Category;
cluster non empty non void V55() strict Category-like transitive associative reflexive with_identities for Subcategory of C;
existence
 ex b1 being Subcategory of C st b1 is strict
proofend;
end;

theorem Th6: :: CAT_2:6
for C being Category
for E being Subcategory of C
for e being Object of E holds e is Object of C
proofend;

theorem Th7: :: CAT_2:7
for C being Category
for E being Subcategory of C holds the carrier' of E c= the carrier' of C
proofend;

theorem Th8: :: CAT_2:8
for C being Category
for E being Subcategory of C
for f being Morphism of E holds f is Morphism of C
proofend;

theorem Th9: :: CAT_2:9
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 )
proofend;

theorem :: CAT_2:10
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 &amp; b = b9 &amp; Hom (a,b) <> {} holds
f is Morphism of a9,b9
proofend;

theorem Th11: :: CAT_2:11
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 &amp; g = g9 &amp; dom g = cod f holds
g (*) f = g9 (*) f9
proofend;

theorem Th12: :: CAT_2:12
for C being Category holds C is Subcategory of C
proofend;

theorem Th13: :: CAT_2:13
for C being Category
for E being Subcategory of C holds id E is Functor of E,C
proofend;

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 Th13;
end;

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

theorem Th14: :: CAT_2:14
for C being Category
for E being Subcategory of C
for a being Object of E holds (Obj (incl E)) . a = a
proofend;

theorem :: CAT_2:15
for C being Category
for E being Subcategory of C
for a being Object of E holds (incl E) . a = a by Th14;

theorem :: CAT_2:16
for C being Category
for E being Subcategory of C holds incl E is faithful
proofend;

theorem Th17: :: CAT_2:17
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 &amp; b = b9 holds
Hom (a,b) = Hom (a9,b9) )
proofend;

definition
let D be Category;
let C be Subcategory of D;
attrC is full  means :Def6: :: CAT_2:def 6
 for c1, c2 being Object of C
for d1, d2 being Object of D st c1 = d1 &amp; c2 = d2 holds
Hom (c1,c2) = Hom (d1,d2);
end;

:: deftheorem Def6 defines full CAT_2:def_6_:_
 for D being Category
for C being Subcategory of D holds
( C is full iff for c1, c2 being Object of C
for d1, d2 being Object of D st c1 = d1 &amp; c2 = d2 holds
Hom (c1,c2) = Hom (d1,d2) );

registration
let D be Category;
cluster non empty non void V55() Category-like transitive associative reflexive with_identities full for Subcategory of D;
existence
 ex b1 being Subcategory of D st b1 is full
proofend;
end;

theorem :: CAT_2:18
for C being Category
for E being Subcategory of C holds
( E is full iff incl E is full )
proofend;

theorem Th19: :: CAT_2:19
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 &amp; b in O )  }  is non empty Subset of the carrier' of C
proofend;

theorem Th20: :: CAT_2:20
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 &amp; b in O )  }  holds
( the Source of C | M is Function of M,O &amp; the Target of C | M is Function of M,O &amp; the Comp of C || M is PartFunc of [:M,M:],M )
proofend;

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

Lm1:  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 &amp; b in O )  }  &amp; d = the Source of C | M &amp; c = the Target of C | M &amp; p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
proofend;

Lm2:  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 &amp; b in O )  }  &amp; d = the Source of C | M &amp; c = the Target of C | M &amp; p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Subcategory of C
proofend;

theorem :: CAT_2:21
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 &amp; b in O )  }  &amp; d = the Source of C | M &amp; c = the Target of C | M &amp; p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
proofend;

theorem :: CAT_2:22
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 st CatStr(# O,M,d,c,p #) is full Subcategory of C holds
( M = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O &amp; b in O )  }  &amp; d = the Source of C | M &amp; c = the Target of C | M &amp; p = the Comp of C || M )
proofend;

:: Product of Categories
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:]
proofend;
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:59;
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:| #);
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:| #) is Category
proofend;
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:| #);

theorem :: CAT_2:23
for C, D being Category holds
( the carrier of [:C,D:] = [: the carrier of C, the carrier of D:] &amp; the carrier' of [:C,D:] = [: the carrier' of C, the carrier' of D:] &amp; the Source of [:C,D:] = [: the Source of C, the Source of D:] &amp; the Target of [:C,D:] = [: the Target of C, the Target of D:] &amp; the Comp of [:C,D:] = |: the Comp of C, the Comp of 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:]
proofend;
end;

theorem :: CAT_2:24
canceled;

theorem :: CAT_2:25
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:1;

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:]
proofend;
end;

theorem :: CAT_2:26
canceled;

theorem :: CAT_2:27
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:1;

theorem Th28: :: CAT_2:28
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)] &amp; cod [f,g] = [(cod f),(cod g)] )
proofend;

theorem Th29: :: CAT_2:29
for C, D being Category
for f, f9 being Morphism of C
for g, g9 being Morphism of D st dom f9 = cod f &amp; dom g9 = cod g holds
[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]
proofend;

theorem Th30: :: CAT_2:30
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)]
proofend;

theorem Th31: :: CAT_2:31
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)]
proofend;

theorem :: CAT_2:32
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)):]
proofend;

theorem :: CAT_2:33
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) <> {} &amp; Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]
proofend;

:: Bifunctors
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 funcS . (m,m9) ->  Morphism of D;
coherence
 S . (m,m9) is Morphism of D
proofend;
end;

theorem Th34: :: CAT_2:34
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
proofend;

theorem Th35: :: CAT_2:35
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
proofend;

:: Partial Functors
definition
let C, C9, D be Category;
let S be Functor of [:C,C9:],D;
let c be Object of C;
funcS ?- 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 Th34;
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:36
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 FUNCT_5:69;

theorem :: CAT_2:37
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)
proofend;

definition
let C, C9, D be Category;
let S be Functor of [:C,C9:],D;
let c9 be Object of C9;
funcS -? 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 Th35;
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:38
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 FUNCT_5:70;

theorem :: CAT_2:39
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)
proofend;

theorem :: CAT_2:40
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) ) &amp; ( 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)
proofend;

theorem :: CAT_2:41
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 &amp; 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)
proofend;

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
proofend;
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
proofend;
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:42
canceled;

theorem :: CAT_2:43
canceled;

theorem :: CAT_2:44
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
proofend;

theorem :: CAT_2:45
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
proofend;

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:]
proofend;
end;

theorem :: CAT_2:46
canceled;

theorem :: CAT_2:47
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)]
proofend;

theorem Th48: :: CAT_2:48
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))):>
proofend;

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:]
proofend;
end;

theorem :: CAT_2:49
canceled;

theorem :: CAT_2:50
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)]
proofend;