:: Introduction to Categories and Functors
:: by Czes{\l}aw Byli\'nski
::
:: Received October 25, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GRAPH_1, STRUCT_0, FUNCT_1, PARTFUN1, ZFMISC_1, SUBSET_1,
XBOOLE_0, CARD_1, FUNCOP_1, RELAT_1, TARSKI, ALGSTR_0, WELLORD1, CAT_1,
MONOID_0, RELAT_2, BINOP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, ORDINAL1, NUMBERS, BINOP_1, FUNCOP_1, STRUCT_0, GRAPH_1;
constructors PARTFUN1, WELLORD2, BINOP_1, PBOOLE, GRAPH_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, STRUCT_0, RELAT_1,
ZFMISC_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities FUNCOP_1, BINOP_1, GRAPH_1;
theorems TARSKI, FUNCT_1, FUNCT_2, PARTFUN1, FUNCOP_1, SUBSET_1, WELLORD2,
ZFMISC_1, XBOOLE_0;
schemes FUNCT_2;
begin :: Structure of a Category
definition
struct(MultiGraphStruct) CatStr (# carrier,carrier' -> set,
Source,Target -> Function of the carrier', the carrier,
Comp -> PartFunc of [:the carrier', the carrier' :],the carrier' #);
end;
reserve C for CatStr;
definition
let C;
mode Object of C is Element of C;
mode Morphism of C is Element of the carrier' of C;
end;
reserve f,g for Morphism of C;
:: Domain and codomain of a Morphism
registration
cluster non void non empty for CatStr;
existence
proof
take CatStr(# {0},{{0}},{0}:->0,{0}:->0,({0},{0}):->{0} #);
thus thesis;
end;
end;
definition
let C,f,g;
assume
A1: [g,f] in dom(the Comp of C);
func g(*)f -> Morphism of C equals
:Def1: ( the Comp of C ).(g,f);
coherence by A1,PARTFUN1:4;
end;
definition
::$CD 2
let C be non void non empty CatStr, a,b be Object of C;
func Hom(a,b) -> Subset of the carrier' of C equals
{f where f is Morphism of C : dom f = a & cod f = b};
correctness
proof
set M = { f where f is Morphism of C : dom(f)=a & cod(f)=b };
M c= the carrier' of C
proof
let x be object;
assume x in M;
then ex f being Morphism of C st x = f & dom(f)=a & cod(f)=b;
hence thesis;
end;
hence thesis;
end;
end;
reserve C for non void non empty CatStr,
f,g for Morphism of C,
a,b,c,d for Object of C;
theorem Th1:
f in Hom(a,b) iff dom(f)=a & cod(f)=b
proof
thus f in Hom(a,b) implies dom(f) = a & cod(f) = b
proof
assume f in Hom(a,b);
then ex g st f = g & dom(g) = a & cod(g) = b;
hence thesis;
end;
thus thesis;
end;
theorem
Hom(dom(f),cod(f)) <> {} by Th1;
definition
let C,a,b;
assume
A1: Hom(a,b)<>{};
mode Morphism of a,b -> Morphism of C means
:Def3: it in Hom(a,b);
existence by A1,SUBSET_1:4;
end;
::$CT
theorem Th3:
for f being Morphism of C holds f is Morphism of dom(f),cod(f)
proof
let f be Morphism of C;
f in Hom(dom(f),cod(f));
hence thesis by Def3;
end;
theorem Th4:
for f being Morphism of a,b st Hom(a,b) <> {} holds dom(f) = a & cod(f) = b
proof
let f be Morphism of a,b;
assume Hom(a,b) <> {};
then f in Hom(a,b) by Def3;
hence thesis by Th1;
end;
theorem
for f being Morphism of a,b for h being Morphism of c,d st Hom(a,b) <>
{} & Hom(c,d) <> {} & f = h holds a = c & b = d
proof
let f be Morphism of a,b;
let h be Morphism of c,d;
assume that
A1: Hom(a,b) <> {} and
A2: Hom(c,d) <> {};
dom(f) = a & cod(f) = b by A1,Th4;
hence thesis by A2,Th4;
end;
theorem Th6:
for f being Morphism of a,b st Hom(a,b) = {f} for g being
Morphism of a,b holds f = g
proof
let f be Morphism of a,b such that
A1: Hom(a,b) = {f};
let g be Morphism of a,b;
g in {f} by A1,Def3;
hence thesis by TARSKI:def 1;
end;
theorem Th7:
for f being Morphism of a,b st Hom(a,b) <> {} & for g being
Morphism of a,b holds f = g holds Hom(a,b) = {f}
proof
let f be Morphism of a,b such that
A1: Hom(a,b) <> {} and
A2: for g being Morphism of a,b holds f = g;
for x being object holds x in Hom(a,b) iff x = f
proof
let x be object;
thus x in Hom(a,b) implies x = f
proof
assume x in Hom(a,b);
then consider g being Morphism of C such that
A3: x = g and
A4: dom(g)=a & cod(g)=b;
g is Morphism of a,b by A4,Th3;
hence thesis by A2,A3;
end;
thus thesis by A1,Def3;
end;
hence thesis by TARSKI:def 1;
end;
theorem
for f being Morphism of a,b st Hom(a,b),Hom(c,d) are_equipotent & Hom(
a,b) = {f} holds ex h being Morphism of c,d st Hom(c,d) = {h}
proof
let f be Morphism of a,b;
assume Hom(a,b),Hom(c,d) are_equipotent;
then consider F being Function such that
F is one-to-one and
A1: dom F = Hom(a,b) & rng F = Hom(c,d) by WELLORD2:def 4;
assume Hom(a,b) = {f};
then
A2: Hom(c,d) = {F.f} by A1,FUNCT_1:4;
then F.f in Hom(c,d) by TARSKI:def 1;
then F.f is Morphism of c,d by Def3;
hence thesis by A2;
end;
:: Category
definition
let C be non empty non void CatStr;
attr C is Category-like means
:Def4:
for f,g being Morphism of C
holds [g,f] in dom(the Comp of C) iff dom g = cod f;
attr C is transitive means
:Def5:
for f,g being Morphism of C st dom g = cod f
holds dom(g(*)f) = dom f & cod(g(*)f) = cod g;
attr C is associative means
:Def6:
for f,g,h being Morphism of C
st dom h = cod g & dom g = cod f
holds h(*)(g(*)f) = (h(*)g)(*)f;
attr C is reflexive means
:Def7:
for b being Element of C holds Hom(b,b) <> {};
attr C is with_identities means
:Def8:
for a being Element of C
ex i being Morphism of a,a st
for b being Element of C holds
(Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g) &
(Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f);
end;
definition
let o,m be object;
func 1Cat(o,m) -> strict CatStr equals
CatStr(# {o},{m},m:->o,m:->o,(m,m):->m #);
correctness;
end;
registration let o,m be object;
cluster 1Cat(o,m) -> non empty trivial non void trivial';
coherence;
end;
registration
cluster non empty trivial -> transitive reflexive
for non empty non void CatStr;
coherence
proof let C be non empty non void CatStr such that
A1: C is non empty trivial;
thus for f,g being Morphism of C st dom g = cod f
holds dom(g(*)f) = dom f & cod(g(*)f) = cod g by A1,ZFMISC_1:def 10;
let b be Element of C;
set i = the Morphism of C;
cod i = b & dom i = b by A1,ZFMISC_1:def 10;
hence Hom(b,b)<>{} by Th1;
end;
end;
registration
cluster non void trivial' -> associative with_identities
for non empty non void CatStr;
coherence
proof let C be non empty non void CatStr such that
A1: C is non void trivial';
thus for f,g,h being Morphism of C
st dom h = cod g & dom g = cod f
holds h(*)(g(*)f) = (h(*)g)(*)f by A1,ZFMISC_1:def 10;
let a be Element of C;
take i = the Morphism of a,a;
let b be Element of C;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g
by A1,ZFMISC_1:def 10;
thus Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f
by A1,ZFMISC_1:def 10;
end;
end;
registration let o,m be object;
cluster 1Cat(o,m) -> Category-like;
coherence
proof let f,g be Morphism of 1Cat(o,m);
thus [g,f] in dom the Comp of 1Cat(o,m) implies dom g = cod f
by ZFMISC_1:def 10;
assume dom g = cod f;
A1: dom the Comp of 1Cat(o,m) = {[m,m]} by FUNCOP_1:13;
f = m & g = m by TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
end;
registration
cluster reflexive transitive associative with_identities Category-like
non void non empty strict for non empty non void CatStr;
existence
proof
take 1Cat(0,0);
thus thesis;
end;
end;
definition
mode Category is reflexive transitive associative with_identities
Category-like non void non empty CatStr;
end;
registration let C be reflexive non void non empty CatStr,
a be Object of C;
cluster Hom(a,a) -> non empty;
coherence by Def7;
end;
::$CT
reserve o,m for set;
theorem Th9:
for a,b being Object of 1Cat(o,m) for f being Morphism of 1Cat(o,m)
holds f in Hom(a,b)
proof
let a,b be Object of 1Cat(o,m);
let f be Morphism of 1Cat(o,m);
dom f = o by TARSKI:def 1;
then dom f = a & cod f = b by TARSKI:def 1;
hence thesis;
end;
theorem
for a,b being Object of 1Cat(o,m) for f being Morphism of 1Cat(o,m)
holds f is Morphism of a,b
proof
let a,b be Object of 1Cat(o,m);
let f be Morphism of 1Cat(o,m);
f in Hom(a,b) by Th9;
hence thesis by Def3;
end;
theorem
for a,b being Object of 1Cat(o,m) holds Hom(a,b) <> {} by Th9;
theorem
for a,b,c,d being Object of 1Cat(o,m) for f being Morphism of a,b for
g being Morphism of c,d holds f=g
proof
let a,b,c,d be Object of 1Cat(o,m);
let f be Morphism of a,b;
let g be Morphism of c,d;
f = m by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
reserve B,C,D for Category;
reserve a,b,c,d for Object of C;
reserve f,f1,f2,g,g1,g2 for Morphism of C;
theorem
dom(g) = cod(f) iff [g,f] in dom(the Comp of C)
by Def4;
theorem Th14:
dom(g) = cod(f) implies g(*)f = ( the Comp of C ).(g,f)
proof
assume dom(g) = cod(f);
then [g,f] in dom(the Comp of C) by Def4;
hence thesis by Def1;
end;
theorem
for f,g being Morphism of C st dom(g) = cod(f) holds dom(g(*)f) =
dom(f) & cod(g(*)f) = cod(g) by Def5;
theorem
for f,g,h being Morphism of C st dom(h) = cod(g) & dom(g) = cod(
f) holds h(*)(g(*)f) = (h(*)g)(*)f by Def6;
definition
let C be with_identities reflexive non void non empty CatStr,
a be Object of C;
func id a -> Morphism of a,a means
:Def10: for b being Object of C holds
(Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)it = f)
& (Hom(b,a) <> {} implies
for f being Morphism of b,a holds it(*)f = f);
existence by Def8;
uniqueness
proof let m1,m2 be Morphism of a,a such that
A1: for b being Object of C holds
(Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)m1 = f)
& (Hom(b,a) <> {} implies
for f being Morphism of b,a holds m1(*)f = f) and
A2: for b being Object of C holds
(Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)m2 = f)
& (Hom(b,a) <> {} implies
for f being Morphism of b,a holds m2(*)f = f);
A3: Hom(a,a) <> {};
hence m1 = m1(*)m2 by A2
.= m2 by A3,A1;
end;
end;
::$CT 2
theorem
for f being Morphism of C st cod(f) = b holds (id b)(*)f = f
proof let f be Morphism of C;
assume
A1: cod f = b;
then reconsider ff=f as Morphism of dom f,b by Th3;
Hom(dom f,b)<>{} by A1,Th1;
then (id b)(*)ff = ff by Def10;
hence thesis;
end;
theorem
for g being Morphism of C st dom(g) = b holds g(*)(id b) = g
proof let f be Morphism of C;
assume
A1: dom f = b;
then reconsider ff=f as Morphism of b,cod f by Th3;
Hom(b,cod f)<>{} by A1,Th1;
then ff(*)(id b) = ff by Def10;
hence thesis;
end;
reserve f,f1,f2 for Morphism of a,b;
reserve f9 for Morphism of b,a;
reserve g for Morphism of b,c;
reserve h,h1,h2 for Morphism of c,d;
theorem Th19:
Hom(a,b)<>{} & Hom(b,c)<>{} implies g(*)f in Hom(a,c)
proof
assume that
A1: Hom(a,b)<>{} and
A2: Hom(b,c)<>{};
A3: f in Hom(a,b) by A1,Def3;
then
A4: cod(f)=b by Th1;
A5: g in Hom(b,c) by A2,Def3;
then
A6: dom(g)=b by Th1;
cod(g)=c by A5,Th1;
then
A7: cod(g(*)f) = c by A6,A4,Def5;
dom(f)=a by A3,Th1;
then dom(g(*)f) = a by A6,A4,Def5;
hence thesis by A7;
end;
definition
let C,a,b,c,f,g;
assume
A1: Hom(a,b)<>{} & Hom(b,c)<>{};
func g*f -> Morphism of a,c equals
:Def11:
g(*)f;
correctness
proof
g(*)f in Hom(a,c) by A1,Th19;
hence thesis by Def3;
end;
end;
theorem
Hom(a,b)<>{} & Hom(b,c)<>{} implies Hom(a,c)<>{} by Th19;
theorem Th21:
Hom(a,b)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{} implies (h*g)*f=h*(g* f)
proof
assume that
A1: Hom(a,b)<>{} and
A2: Hom(b,c)<>{} and
A3: Hom(c,d)<>{};
A4: Hom(a,c)<>{} by A1,A2,Th19;
h in Hom(c,d) by A3,Def3;
then
A5: dom(h) = c by Th1;
g in Hom(b,c) by A2,Def3;
then
A6: cod(g) = c & dom(g) = b by Th1;
reconsider hh = h as Morphism of C;
reconsider gg = g as Morphism of C;
reconsider ff = f as Morphism of C;
f in Hom(a,b) by A1,Def3;
then
A7: cod(f) = b by Th1;
Hom(b,d) <> {} by A2,A3,Th19;
hence (h*g)*f = (h*g)(*)ff by A1,Def11
.= (hh(*)gg)(*)ff by A2,A3,Def11
.= hh(*)(gg(*)ff) by A5,A6,A7,Def6
.= hh(*)(g*f) by A1,A2,Def11
.= h*(g*f) by A3,A4,Def11;
end;
::$CT
theorem
id a in Hom(a,a) by Def3;
theorem Th23:
Hom(a,b)<>{} implies (id b)*f=f
proof
assume
A1: Hom(a,b)<>{};
A2: (id b)(*)f = f by A1,Def10;
Hom(b,b) <> {};
hence thesis by A1,A2,Def11;
end;
theorem Th24:
Hom(b,c)<>{} implies g*(id b)=g
proof
assume
A1: Hom(b,c)<>{};
A2: g(*)(id b) = g by A1,Def10;
Hom(b,b) <> {};
hence thesis by A1,A2,Def11;
end;
registration let C,a; let f be Morphism of a,a;
A1: Hom(a,a) <> {};
reduce f*id a to f;
reducibility by A1,Th24;
reduce (id a)*f to f;
reducibility by A1,Th23;
end;
theorem
(id a)*(id a) = id a;
:: Monics, Epis
definition
let C be Category, b,c be Object of C, g be Morphism of b,c;
attr g is monic means
Hom(b,c) <> {} &
for a being Object of C st Hom(a,b) <> {}
for f1,f2 being Morphism of a,b
st g*f1=g*f2 holds f1=f2;
end;
definition
let C be Category, a,b be Object of C, f be Morphism of a,b;
attr f is epi means
Hom(a,b) <> {} &
for c being Object of C st Hom(b,c) <> {}
for g1,g2 being Morphism of b,c st g1*f=g2*f holds g1=g2;
end;
definition
let C be Category, a,b be Object of C, f be Morphism of a,b;
attr f is invertible means
Hom(a,b) <> {} & Hom(b,a) <> {} &
ex g being Morphism of b,a st f*g = id b & g*f = id a;
end;
theorem
Hom(b,c) <> {} implies (g is monic iff for a for f1,f2 being
Morphism of a,b st Hom(a,b)<>{} & g*f1=g*f2 holds f1=f2);
theorem
g is monic & h is monic implies h*g is monic
proof
assume that
A1: g is monic and
A2: h is monic;
A3: Hom(b,c)<>{} by A1;
A4: Hom(c,d)<>{} by A2;
A5: now
let a,f1,f2 such that
A6: Hom(a,b)<>{} and
A7: (h*g)*f1 = (h*g)*f2;
A8: Hom(a,c) <> {} by A3,A6,Th19;
h*(g*f1) = (h*g)*f1 & (h*g)*f2 = h*(g*f2) by A3,A4,A6,Th21;
then g*f1 = g*f2 by A2,A7,A8;
hence f1 = f2 by A1,A6;
end;
Hom(b,d) <> {} by A3,A4,Th19;
hence thesis by A5;
end;
theorem
Hom(b,c)<>{} & Hom(c,d)<>{} & h*g is monic implies g is monic
proof
assume that
A1: Hom(b,c)<>{} and
A2: Hom(c,d)<>{} and
A3: h*g is monic;
now
let a,f1,f2;
assume
A4: Hom(a,b)<>{};
then h*(g*f1) = (h*g)*f1 & h*(g*f2) = (h*g)*f2 by A1,A2,Th21;
hence g*f1 = g*f2 implies f1 = f2 by A3,A4;
end;
hence thesis by A1;
end;
theorem
for h being Morphism of a,b for g being Morphism of b,a st Hom(a,b) <>
{} & Hom(b,a) <> {} & h*g = id b holds g is monic
proof
let h be Morphism of a,b;
let g be Morphism of b,a such that
A1: Hom(a,b) <> {} and
A2: Hom(b,a) <> {} and
A3: h*g = id b;
now
let c;
let g1,g2 be Morphism of c,b such that
A4: Hom(c,b) <> {} and
A5: g*g1 = g*g2;
thus g1 = (h*g)*g1 by A3,A4,Th23
.= h*(g*g2) by A1,A2,A4,A5,Th21
.= (h*g)*g2 by A1,A2,A4,Th21
.= g2 by A3,A4,Th23;
end;
hence thesis by A2;
end;
theorem
id b is monic
proof
A1: now
let a;
let f1,f2 be Morphism of a,b;
assume
A2: Hom(a,b)<>{};
then (id b)*f1 = f1 by Th23;
hence (id b)*f1 = (id b)*f2 implies f1 = f2 by A2,Th23;
end;
thus thesis by A1;
end;
theorem
Hom(a,b) <> {} implies (f is epi iff for c for g1,g2 being
Morphism of b,c st Hom(b,c)<>{} & g1*f=g2*f holds g1=g2);
theorem
f is epi & g is epi implies g*f is epi
proof
assume that
A1: f is epi and
A2: g is epi;
A3: Hom(a,b)<>{} by A1;
A4: Hom(b,c)<>{} by A2;
A5: now
let d,h1,h2 such that
A6: Hom(c,d)<>{} and
A7: h1*(g*f) = h2*(g*f);
A8: Hom(b,d) <> {} by A4,A6,Th19;
h1*(g*f) = (h1*g)*f & (h2*g)*f = h2*(g*f) by A3,A4,A6,Th21;
then h1*g = h2*g by A1,A7,A8;
hence h1 = h2 by A2,A6;
end;
Hom(a,c) <> {} by A3,A4,Th19;
hence thesis by A5;
end;
theorem
Hom(a,b)<>{} & Hom(b,c)<>{} & g*f is epi implies g is epi
proof
assume that
A1: Hom(a,b)<>{} and
A2: Hom(b,c)<>{} and
A3: g*f is epi;
now
let d,h1,h2;
assume
A4: Hom(c,d)<>{};
then h1*(g*f) = (h1*g)*f & h2*(g*f) = (h2*g)*f by A1,A2,Th21;
hence h1*g = h2*g implies h1 = h2 by A3,A4;
end;
hence thesis by A2;
end;
theorem
for h being Morphism of a,b for g being Morphism of b,a st Hom(a,b) <>
{} & Hom(b,a) <> {} & h*g = id b holds h is epi
proof
let h be Morphism of a,b;
let g be Morphism of b,a;
assume that
A1: Hom(a,b) <> {} and
A2: Hom(b,a) <> {} and
A3: h*g = id b;
now
let c;
let h1,h2 be Morphism of b,c such that
A4: Hom(b,c) <> {} and
A5: h1*h = h2*h;
thus h1 = h1*(h*g) by A3,A4,Th24
.= (h2*h)*g by A1,A2,A4,A5,Th21
.= h2*(h*g) by A1,A2,A4,Th21
.= h2 by A3,A4,Th24;
end;
hence thesis by A1;
end;
theorem
id b is epi
proof
A1: now
let c;
let g1,g2 be Morphism of b,c;
assume
A2: Hom(b,c)<>{};
then g1*(id b) = g1 by Th24;
hence g1*(id b) = g2*(id b) implies g1 = g2 by A2,Th24;
end;
thus thesis by A1;
end;
theorem
Hom(a,b) <> {} implies (f is invertible iff Hom(b,a)<>{} & ex g
being Morphism of b,a st f*g=id b & g*f=id a);
theorem Th37:
Hom(a,b) <> {} & Hom(b,a) <> {} implies for g1,g2 being Morphism
of b,a st f*g1=id b & g2*f=id a holds g1=g2
proof
assume that
A1: Hom(a,b) <> {} and
A2: Hom(b,a) <> {};
let g1,g2 be Morphism of b,a;
assume
A3: f*g1=id b;
assume g2*f=id a;
hence g1 = (g2*f)*g1 by A2,Th23
.= g2*(id b) by A1,A2,A3,Th21
.= g2 by A2,Th24;
end;
definition
let C,a,b,f;
assume that
A1: f is invertible;
func f" -> Morphism of b,a means
:Def15:
f*it = id b & it*f = id a;
existence by A1;
uniqueness
by A1,Th37;
end;
theorem
f is invertible implies f is monic & f is epi
proof
assume that
A1: f is invertible;
A2: Hom(a,b)<>{} by A1;
consider k being Morphism of b,a such that
A3: f*k=id b and
A4: k*f=id a by A1;
A5: Hom(b,a)<>{} by A1;
now
let c be (Object of C),g,h be Morphism of c,a such that
A6: Hom(c,a)<>{} and
A7: f*g=f*h;
g = (k*f)*g by A4,A6,Th23
.= k*(f*h) by A2,A5,A6,A7,Th21
.= (id a)*h by A2,A5,A4,A6,Th21;
hence g=h by A6,Th23;
end;
hence f is monic by A2;
now
let c be (Object of C), g,h be Morphism of b,c such that
A8: Hom(b,c)<>{} and
A9: g*f=h*f;
g = g*(f*k) by A3,A8,Th24
.= (h*f)*k by A2,A5,A8,A9,Th21
.= h*(id b) by A2,A5,A3,A8,Th21;
hence g=h by A8,Th24;
end;
hence thesis by A2;
end;
theorem
id a is invertible
proof
Hom(a,a) <> {} & (id a)*(id a) = id a;
hence thesis;
end;
theorem Th40:
f is invertible & g is invertible implies g*f is invertible
proof
assume
A1: f is invertible;
then
A2: Hom(a,b) <> {} & Hom(b,a) <> {};
consider f1 being Morphism of b,a such that
A3: f*f1 = id b and
A4: f1*f = id a by A1;
assume
A5: g is invertible;
then
A6: Hom(b,c) <> {} & Hom(c,b) <> {};
consider g1 being Morphism of c,b such that
A7: g*g1 = id c and
A8: g1*g = id b by A5;
A9: now
thus
A10: Hom(c,a) <> {} by A2,A6,Th19;
take f1g1 = f1*g1;
thus (g*f)*(f1g1) = g*(f*(f1*g1)) by A2,A6,A10,Th21
.= g*((id b )*g1) by A2,A3,A6,Th21
.= id c by A6,A7,Th23;
Hom(a,c) <> {} by A2,A6,Th19;
hence (f1g1)*(g*f) = f1*(g1*(g*f)) by A2,A6,Th21
.= f1*((id b)*f) by A2,A6,A8,Th21
.= id a by A2,A4,Th23;
end;
Hom(a,c) <> {} by A2,A6,Th19;
hence thesis by A9;
end;
theorem
f is invertible implies f" is invertible
proof
assume
A1: f is invertible;
then
A2: f*(f") = id b by Def15;
A3: Hom(a,b) <> {} by A1;
Hom(b,a) <> {} & (f")*f = id a by A1,Def15;
hence thesis by A3,A2;
end;
theorem
f is invertible & g is invertible
implies (g*f)" = f"*g"
proof
assume that
A1: f is invertible and
A2: g is invertible;
A3: Hom(a,b) <> {} by A1;
A4: Hom(b,c) <> {} by A2;
A5: Hom(c,b) <> {} by A2;
A6: Hom(b,a) <> {} by A1;
then
A7: Hom(c,a) <> {} by A5,Th19;
then
A8: (f"*g")*(g*f) = ((f"*g")*g)*f by A3,A4,Th21
.= (f"*(g"*g))*f by A4,A6,A5,Th21
.= (f"*(id b))*f by A2,Def15
.= f"*f by A6,Th24
.= id a by A1,Def15;
A9: Hom(a,c) <> {} & g*f is invertible by A1,A2,Th19,Th40;
(g*f)*(f"*g") = g*(f*(f"*g")) by A3,A4,A7,Th21
.= g*((f*f")*g") by A3,A6,A5,Th21
.= g*((id b)*g") by A1,Def15
.= g*g" by A5,Th23
.= id c by A2,Def15;
hence thesis by A8,A9,Def15;
end;
definition
let C,a;
attr a is terminal means
Hom(b,a)<>{} & ex f being Morphism of b,a
st for g being Morphism of b,a holds f=g;
attr a is initial means
Hom(a,b)<>{} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f=g;
let b;
pred a,b are_isomorphic means
ex f st f is invertible;
reflexivity
proof let a be Object of C;
take id a;
(id a)*(id a) = id a;
hence thesis;
end;
symmetry
proof let a,b be Object of C;
given f being Morphism of a,b such that
A1: f is invertible;
A2: Hom(b,a) <> {} & Hom(a,b) <> {} by A1;
consider g being Morphism of b,a such that
A3: f*g = id b & g*f = id a by A1;
take g;
thus g is invertible by A2,A3;
end;
end;
theorem
a,b are_isomorphic iff Hom(a,b)<>{} & Hom(b,a)<>{} & ex f,f9 st
f*f9 = id b & f9*f = id a
proof
thus a,b are_isomorphic implies Hom(a,b)<>{} & Hom(b,a)<>{} & ex f,f9 st f*
f9 = id b & f9*f = id a
proof
given f such that
A1: f is invertible;
thus Hom(a,b) <> {} & Hom(b,a) <> {} by A1;
take f;
thus thesis by A1;
end;
assume that
A2: Hom(a,b)<>{} and
A3: Hom(b,a)<>{};
given f such that
A4: ex f9 st f*f9 = id b & f9*f = id a;
take f;
thus thesis by A2,A3,A4;
end;
theorem
a is initial iff for b ex f being Morphism of a,b st Hom(a,b) = {f}
proof
thus a is initial implies for b ex f being Morphism of a,b st Hom(a,b) = {f}
proof
assume
A1: a is initial;
let b;
consider f being Morphism of a,b such that
A2: for g being Morphism of a,b holds f = g by A1;
take f;
thus thesis by A2,Th7,A1;
end;
assume
A3: for b ex f being Morphism of a,b st Hom(a,b) = {f};
let b;
consider f being Morphism of a,b such that
A4: Hom(a,b) = {f} by A3;
thus Hom(a,b) <> {} by A4;
take f;
thus thesis by A4,Th6;
end;
theorem Th45:
a is initial implies for h being Morphism of a,a holds id a = h
proof
assume a is initial;
then consider f being Morphism of a,a such that
A1: for g being Morphism of a,a holds f = g;
let h be Morphism of a,a;
id a = f by A1;
hence thesis by A1;
end;
theorem
a is initial & b is initial implies a,b are_isomorphic
proof
assume that
A1: a is initial and
A2: b is initial;
set g = the Morphism of b,a;
set f = the Morphism of a,b;
A3: Hom(a,b) <> {} by A1;
take f;
now
thus Hom(b,a) <> {} by A2;
take g;
thus f*g = id b & g*f = id a by A1,A2,Th45;
end;
hence thesis by A3;
end;
theorem
a is initial & a,b are_isomorphic implies b is initial
proof
assume that
A1: a is initial;
given f such that
A2: f is invertible;
A3: Hom(b,a) <> {} by A2;
let c;
consider h being Morphism of a,c such that
A4: for g being Morphism of a,c holds h = g by A1;
Hom(a,c) <> {} by A1;
hence
A5: Hom(b,c) <> {} by A3,Th19;
consider f9 such that
A6: f*f9 = id b and
f9*f = id a by A2;
A7: Hom(a,b) <> {} by A2;
take h*f9;
let h9 be Morphism of b,c;
thus h9 = h9*(f*f9) by A6,A5,Th24
.= (h9*f)*f9 by A3,A5,A7,Th21
.= h*f9 by A4;
end;
theorem
b is terminal iff for a ex f being Morphism of a,b st Hom(a,b) = {f}
proof
thus b is terminal implies for a ex f being Morphism of a,b st Hom(a,b) = {f
}
proof
assume
A1: b is terminal;
let a;
consider f being Morphism of a,b such that
A2: for g being Morphism of a,b holds f = g by A1;
take f;
thus thesis by A2,Th7,A1;
end;
assume
A3: for a ex f being Morphism of a,b st Hom(a,b) = {f};
let a;
consider f being Morphism of a,b such that
A4: Hom(a,b) = {f} by A3;
thus Hom(a,b) <> {} by A4;
take f;
thus thesis by A4,Th6;
end;
theorem Th49:
a is terminal implies for h being Morphism of a,a holds id a = h
proof
assume a is terminal;
then consider f being Morphism of a,a such that
A1: for g being Morphism of a,a holds f = g;
let h be Morphism of a,a;
id a = f by A1;
hence thesis by A1;
end;
theorem
a is terminal & b is terminal implies a,b are_isomorphic
proof
assume that
A1: a is terminal and
A2: b is terminal;
set g = the Morphism of b,a;
set f = the Morphism of a,b;
A3: Hom(a,b) <> {} by A2;
take f;
now
thus Hom(b,a) <> {} by A1;
take g;
thus f*g = id b & g*f = id a by A1,A2,Th49;
end;
hence thesis by A3;
end;
theorem
b is terminal & a,b are_isomorphic implies a is terminal
proof
assume that
A1: b is terminal;
given f such that
A2: f is invertible;
A3: Hom(b,a) <> {} by A2;
let c;
consider h being Morphism of c,b such that
A4: for g being Morphism of c,b holds h = g by A1;
Hom(c,b) <> {} by A1;
hence
A5: Hom(c,a) <> {} by A3,Th19;
consider f9 such that
f*f9 = id b and
A6: f9*f = id a by A2;
A7: Hom(a,b) <> {} by A2;
take f9*h;
let h9 be Morphism of c,a;
thus f9*h = f9*(f*h9) by A4
.= (f9*f)*h9 by A3,A5,A7,Th21
.= h9 by A6,A5,Th23;
end;
theorem
Hom(a,b) <> {} & a is terminal implies f is monic
proof
assume that
A1: Hom(a,b) <> {} and
A2: a is terminal;
now
let c be (Object of C),g,h be Morphism of c,a such that
Hom(c,a)<>{} and
f*g=f*h;
consider ff being Morphism of c,a such that
A3: for gg being Morphism of c,a holds ff=gg by A2;
ff = g by A3;
hence g=h by A3;
end;
hence thesis by A1;
end;
registration let C,a;
reduce dom id a to a;
reducibility
proof
id a in Hom(a,a) by Def3;
hence thesis by Th1;
end;
reduce cod id a to a;
reducibility
proof
id a in Hom(a,a) by Def3;
hence thesis by Th1;
end;
end;
theorem Th53:
dom id a = a & cod id a =a;
theorem Th54:
id a = id b implies a = b
proof assume
A1: id a = id b;
thus a = dom id a
.= b by Th53,A1;
end;
theorem
a,b are_isomorphic & b,c are_isomorphic implies a,c are_isomorphic
proof
given f being Morphism of a,b such that
A1: f is invertible;
given g being Morphism of b,c such that
A2: g is invertible;
take g*f;
thus thesis by A1,A2,Th40;
end;
:: Functors (Covariant Functors)
definition
let C,D;
mode Functor of C,D -> Function of the carrier' of C,the carrier' of D means
:Def19:
(for c being Element of C ex d being Element of D st it.id c = id d ) &
(for f being Element of the carrier' of C
holds it.(id dom f) = id dom(it.f) &
it.(id cod f) = id cod(it.f)) &
for f,g being Element of the carrier' of C
st [g,f] in dom(the Comp of C)
holds it.(g(*)f) = (it.g)(*)(it.f);
existence
proof
set d = the Element of D;
reconsider F = (the carrier' of C) --> id d as Function of the
carrier' of C,the carrier' of D;
take F;
thus for c being Element of C ex d being Element of D st F.(id c) = id d
by FUNCOP_1:7;
A1: Hom(d,d) <> {};
thus for f being Element of the carrier' of C
holds F.(id dom f) = id dom(F.f) &
F.(id cod f) = id cod(F.f)
proof
let f be Element of the carrier' of C;
A2: F.f = id d by FUNCOP_1:7;
thus F.(id dom f) = id d by FUNCOP_1:7
.= id dom(F.f) by A2;
thus F.(id cod f) = id d by FUNCOP_1:7
.= id cod(F.f) by A2;
end;
let f,g be Element of the carrier' of C such that
[g,f] in dom(the Comp of C);
thus F.(g(*)f) = (id d)*(id d) by FUNCOP_1:7
.= (id d)(*)(id d) by A1,Def11
.= (id d)(*)(F.f) by FUNCOP_1:7
.= (F.g)(*)(F.f) by FUNCOP_1:7;
end;
end;
theorem Th56:
for T being Function of the carrier' of C,the carrier' of D st
(for c being Object of C ex d being Object of D st T.(id c) = id d) &
(for f being Morphism of C
holds T.(id dom f) = id dom (T.f) &
T.(id cod f) = id cod (T.f)) &
(for f,g being Morphism of C st dom g = cod f
holds T.(g(*)f) = (T.g)(*)(T.f)) holds T is Functor of C,D
proof
let T be Function of the carrier' of C,the carrier' of D such that
A1: for c being Object of C ex d being Object of D st T.(id c) = id d and
A2: for f being Morphism of C holds T.(id dom f) = id dom (T.f) & T.(id
cod f) = id cod (T.f) and
A3: for f,g being Morphism of C st dom g = cod f
holds T.(g(*)f) = (T.g)(*)( T.f);
thus for c being Element of C ex d being Element of D st T.id c = id d
by A1;
thus for f being Element of the carrier' of C
holds T.(id dom f) = id dom(T.f) &
T.(id cod f) = id cod(T.f) by A2;
let f,g be Element of the carrier' of C;
assume [g,f] in dom(the Comp of C);
then
A4: dom g = cod f by Def4;
thus thesis by A3,A4;
end;
theorem
for T being Functor of C,D for c being Object of C ex d being
Object of D st T.(id c) = id d by Def19;
theorem
for T being Functor of C,D for f being Morphism of C
holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f) by Def19;
theorem Th59:
for T being Functor of C,D for f,g being Morphism of C st dom g
= cod f holds dom(T.g) = cod(T.f) & T.(g(*)f) = (T.g)(*)(T.f)
proof
let T be Functor of C,D;
let f,g be Morphism of C;
assume
A1: dom g = cod f;
then
A2: (the Comp of C).(g,f) = g(*)f & [g,f] in dom(the Comp of C)
by Def4,Th14;
id dom (T.g) = T.(id cod f) by A1,Def19
.= id cod (T.f) by Def19;
hence dom (T.g) = cod (T.f) by Th54;
thus thesis by A2,Def19;
end;
theorem Th60:
for T being Function of the carrier' of C,the carrier' of D for
F being Function of the carrier of C, the carrier of D st ( for c being Object
of C holds T.(id c) = id(F.c) ) & ( for f being Morphism of C holds F.(dom f) =
dom (T.f) & F.(cod f) = cod (T.f) ) & ( for f,g being Morphism of C st dom g =
cod f holds T.(g(*)f) = (T.g)(*)(T.f)) holds T is Functor of C,D
proof
let T be Function of the carrier' of C,the carrier' of D;
let F be Function of the carrier of C, the carrier of D;
assume that
A1: for c being Object of C holds T.(id c) = id(F.c) and
A2: for f being Morphism of C holds F.(dom f) = dom (T.f) & F.(cod f) =
cod (T.f) and
A3: for f,g being Morphism of C st dom g = cod f
holds T.(g(*)f) = (T.g)(*)( T.f);
A4: for c being Object of C ex d being Object of D st T.(id c) = id d
proof
let c be Object of C;
take F.c;
thus thesis by A1;
end;
for f being Morphism of C holds T.(id dom f) = id dom (T.f) & T.(id cod
f) = id cod (T.f)
proof
let f be Morphism of C;
thus T.(id dom f) = id (F.(dom f)) by A1
.= id dom (T.f) by A2;
thus T.(id cod f) = id (F.(cod f)) by A1
.= id cod (T.f) by A2;
end;
hence thesis by A3,A4,Th56;
end;
:: Object Function of a Functor
definition
let C,D;
let F be Function of the carrier' of C,the carrier' of D;
assume
A1: for c being Element of C ex d being Element
of D st F.id c = id d;
func Obj(F) -> Function of the carrier of C,the carrier of D means
:Def20:
for c being Element of C for d being Element of D
st F.id c = id d holds it.c = d;
existence
proof
defpred P[Object of C,Object of D] means
for d being Element of D st F.id $1 = id d
holds $2 = d;
A2: for c being Element of C ex y being Element of D st P[c,y]
proof
let c be Element of C;
consider y being Element of D such that
A3: F.id c = id y by A1;
take y;
let d be Element of D;
assume F.id c = id d;
hence thesis by A3,Th54;
end;
thus ex f being Function of the carrier of C,the carrier of D st for x
being Element of C holds P[x,f.x] from FUNCT_2:sch 3 (A2);
end;
uniqueness
proof
let F1,F2 be Function of the carrier of C,the carrier of D such that
A4: for c being Element of C for d being Element
of D st F.id c = id d holds F1.c = d and
A5: for c being Element of C for d being Element
of D st F.id c = id d holds F2.c = d;
for c being Element of C holds F1.c = F2.c
proof
let c be Element of C;
consider d1 being Element of D such that
A6: F.id c = id d1 by A1;
F1.c = d1 by A4,A6;
hence thesis by A5,A6;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem
for T being Function of the carrier' of C,the carrier' of D st
for c being Object of C ex d being Object of D st T.(id c) = id d for c being
Object of C for d being Object of D st T.(id c) = id d holds (Obj T).c = d
by Def20;
theorem Th62:
for T being Functor of C,D for c being Object of C for d being
Object of D st T.(id c) = id d holds (Obj T).c = d
proof
let T be Functor of C,D;
for c being Object of C ex d being Object of D st T.(id c) = id d by Def19;
hence thesis by Def20;
end;
theorem Th63:
for T being (Functor of C,D),c being Object of C holds T.(id c)
= id((Obj T).c)
proof
let T be (Functor of C,D),c be Object of C;
ex d being Object of D st T.(id c) = id d by Def19;
hence thesis by Th62;
end;
theorem Th64:
for T being (Functor of C,D), f being Morphism of C holds (Obj
T).(dom f) = dom (T.f) & (Obj T).(cod f) = cod (T.f)
proof
let T be (Functor of C,D), f be Morphism of C;
T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f)
by Def19;
hence thesis by Th62;
end;
definition
let C,D be Category;
let T be Functor of C,D;
let c be Object of C;
func T.c -> Object of D equals
(Obj T).c;
correctness;
end;
theorem
for T being Functor of C,D for c being Object of C for d being Object
of D st T.(id c) = id d holds T.c = d by Th62;
theorem
for T being (Functor of C, D),c being Object of C holds T.(id c) = id(
T.c) by Th63;
theorem
for T being (Functor of C, D), f being Morphism of C holds T.(dom f) =
dom (T.f) & T.(cod f) = cod (T.f) by Th64;
theorem Th68:
for T being Functor of B,C for S being Functor of C,D holds S*T
is Functor of B,D
proof
let T be Functor of B,C;
let S be Functor of C,D;
reconsider FF = (Obj S)*(Obj T) as Function of the carrier of B, the carrier
of D;
reconsider TT = S*T as Function of the carrier' of B, the carrier' of D;
now
thus for b being Object of B holds TT.(id b) = id(FF.b)
proof
let b be Object of B;
thus TT.(id b) = S.(T.(id b)) by FUNCT_2:15
.= S.(id(T.b)) by Th63
.= id((S.((Obj T).b))) by Th63
.= id(FF.b) by FUNCT_2:15;
end;
thus for f being Morphism of B holds FF.(dom f) = dom (TT.f) & FF.(cod f)
= cod (TT.f)
proof
let f be Morphism of B;
thus FF.(dom f) = (Obj S).((Obj T).(dom f)) by FUNCT_2:15
.= (Obj S).(dom (T.f)) by Th64
.= (dom (S.(T.f))) by Th64
.= dom (TT.f) by FUNCT_2:15;
thus FF.(cod f) = (Obj S).((Obj T).(cod f)) by FUNCT_2:15
.= (Obj S).(cod (T.f)) by Th64
.= (cod (S.(T.f))) by Th64
.= cod (TT.f) by FUNCT_2:15;
end;
let f,g be Morphism of B;
assume
A1: dom g = cod f;
then
A2: dom(T.g) = cod(T.f) by Th59;
thus TT.(g(*)f) = S.(T.(g(*)f)) by FUNCT_2:15
.= S.((T.g)(*)(T.f)) by A1,Th59
.= (S.(T.g))(*)(S.(T.f)) by A2,Th59
.= ((TT.g)(*)(S.(T.f))) by FUNCT_2:15
.= (TT.g)(*)(TT.f) by FUNCT_2:15;
end;
hence thesis by Th60;
end;
:: Composition of Functors
definition
let B,C,D;
let T be Functor of B,C;
let S be Functor of C,D;
redefine func S*T -> Functor of B,D; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence by Th68;
end;
theorem Th69:
id the carrier' of C is Functor of C,C
proof
set F = id the carrier of C;
set T = id the carrier' of C;
(for c being Object of C holds T.(id c) = id(F.c)) &
(for f being Morphism of C holds F.(dom f) = dom (T.f) & F.(cod f) =
cod (T.f)) &
for f,g being Morphism of C st dom g = cod f
holds T.(g(*)f) = (T.g)(*)(T.f);
hence thesis by Th60;
end;
theorem Th70:
for T being (Functor of B,C),S being (Functor of C,D),b being
Object of B holds (Obj (S*T)).b = (Obj S).((Obj T).b)
proof
let T be (Functor of B,C),S be (Functor of C,D),b be Object of B;
A1: (S*T).(id b) = S.(T.(id b)) by FUNCT_2:15;
consider d being Object of D such that
A2: (S*T).(id b) = id d by Def19;
consider c being Object of C such that
A3: T.(id b) = id c by Def19;
thus (Obj (S*T)).b = d by A2,Th62
.= (Obj S).c by A2,A3,A1,Th62
.= (Obj S).((Obj T).b) by A3,Th62;
end;
theorem
for T being Functor of B,C for S being Functor of C,D for b being
Object of B holds (S*T).b = S.(T.b) by Th70;
:: Identity Functor
definition
let C;
func id C -> Functor of C,C equals
id the carrier' of C;
coherence by Th69;
end;
theorem Th72:
for c being Object of C holds (Obj id C).c = c
proof
let c be Object of C;
(id C).(id c) = id c;
hence thesis by Th62;
end;
theorem Th73:
Obj id C = id the carrier of C
proof
dom Obj id C = the carrier of C &
for x be object holds x in the carrier of
C implies (Obj id C).x = x by Th72,FUNCT_2:def 1;
hence thesis by FUNCT_1:17;
end;
theorem
for c being Object of C holds (id C).c = c by Th72;
definition
let C,D be Category;
let T be Functor of C,D;
attr T is isomorphic means
T is one-to-one & rng T = the carrier' of D & rng Obj T = the carrier of D;
attr T is full means
for c,c9 being Object of C st Hom(T.c,T.c9) <>
{} for g being Morphism of T.c,T.c9 holds Hom(c,c9) <> {} & ex f being Morphism
of c,c9 st g = T.f;
attr T is faithful means
for c,c9 being Object of C st Hom(c,c9) <>
{} for f1,f2 being Morphism of c,c9 holds T.f1 = T.f2 implies f1 = f2;
end;
theorem
id C is isomorphic
proof
rng id the carrier of C = the carrier of C;
hence id C is one-to-one & rng id C = the carrier' of C & rng Obj id C = the
carrier of C by Th73;
end;
theorem Th76:
for T being Functor of C,D for c,c9 being Object of C for f
being set st f in Hom(c,c9) holds T.f in Hom(T.c,T.c9)
proof
let T be Functor of C,D;
let c,c9 be Object of C;
let f be set;
assume
A1: f in Hom(c,c9);
then reconsider f9 = f as Morphism of c,c9 by Def3;
cod f9 = c9 by A1,Th1;
then
A2: T.c9 = cod(T.f9) by Th64;
dom f9 = c by A1,Th1;
then T.c = dom (T.f9) by Th64;
hence thesis by A2;
end;
theorem Th77:
for T being Functor of C,D for c,c9 being Object of C st Hom(c,
c9) <> {} for f being Morphism of c,c9 holds T.f in Hom(T.c,T.c9)
proof
let T be Functor of C,D;
let c,c9 be Object of C such that
A1: Hom(c,c9) <> {};
let f be Morphism of c,c9;
f in Hom(c,c9) by A1,Def3;
hence thesis by Th76;
end;
theorem Th78:
for T being Functor of C,D for c,c9 being Object of C st Hom(c,
c9) <> {} for f being Morphism of c,c9 holds T.f is Morphism of T.c,T.c9
proof
let T be Functor of C,D;
let c,c9 be Object of C such that
A1: Hom(c,c9) <> {};
let f be Morphism of c,c9;
T.f in Hom(T.c,T.c9) by A1,Th77;
hence thesis by Def3;
end;
theorem Th79:
for T being Functor of C,D for c,c9 being Object of C st Hom(c,
c9) <> {} holds Hom(T.c,T.c9) <> {}
proof
let T be Functor of C,D;
let c,c9 be Object of C;
set f = the Element of Hom(c,c9);
assume Hom(c,c9) <> {};
then f in Hom(c,c9);
hence thesis by Th76;
end;
theorem
for T being Functor of B,C for S being Functor of C,D st T is full & S
is full holds S*T is full
proof
let T be Functor of B,C;
let S be Functor of C,D;
assume that
A1: T is full and
A2: S is full;
let b,b9 be Object of B such that
A3: Hom((S*T).b,(S*T).b9) <> {};
let g be Morphism of (S*T).b,(S*T).b9;
A4: (S*T).b = S.(T.b) & (S*T).b9 = S.(T.b9) by Th70;
then consider f being Morphism of T.b,T.b9 such that
A5: g = S.f by A2,A3;
A6: Hom(T.b,T.b9) <> {} by A2,A3,A4;
hence Hom(b,b9) <> {} by A1;
consider h being Morphism of b,b9 such that
A7: f = T.h by A1,A6;
take h;
thus thesis by A5,A7,FUNCT_2:15;
end;
theorem
for T being Functor of B,C for S being Functor of C,D st T is faithful
& S is faithful holds S*T is faithful
proof
let T be Functor of B,C;
let S be Functor of C,D;
assume that
A1: T is faithful and
A2: S is faithful;
let b,b9 be Object of B such that
A3: Hom(b,b9) <> {};
let f1,f2 be Morphism of b,b9;
A4: T.f2 is Morphism of T.b,T.b9 by A3,Th78;
assume
A5: (S*T).f1 = (S*T).f2;
A6: (S*T).f1 = S.(T.f1) & (S*T).f2 = S.(T.f2) by FUNCT_2:15;
Hom(T.b,T.b9) <> {} & T.f1 is Morphism of T.b,T.b9 by A3,Th78,Th79;
then T.f1 = T.f2 by A2,A5,A6,A4;
hence thesis by A1,A3;
end;
theorem Th82:
for T being Functor of C,D for c,c9 being Object of C holds T.:
Hom(c,c9) c= Hom(T.c,T.c9)
proof
let T be Functor of C,D;
let c,c9 be Object of C;
let f be object;
assume f in T.:Hom(c,c9);
then ex g being Element of the carrier' of C st g in Hom(c,c9) & f = T.g by
FUNCT_2:65;
hence thesis by Th76;
end;
definition
let C,D be Category;
let T be Functor of C,D;
let c,c9 be Object of C;
func hom(T,c,c9) -> Function of Hom(c,c9) , Hom(T.c,T.c9) equals
T|Hom(c,c9);
correctness
proof
T.:Hom(c,c9) c= Hom(T.c,T.c9) by Th82;
hence thesis by FUNCT_2:101;
end;
end;
theorem Th83:
for T being Functor of C,D for c,c9 being Object of C st Hom(c,
c9) <> {} for f being Morphism of c,c9 holds hom(T,c,c9).f = T.f
proof
let T be Functor of C,D;
let c,c9 be Object of C;
assume
A1: Hom(c,c9) <> {};
let f be Morphism of c,c9;
f in Hom(c,c9) by A1,Def3;
hence thesis by FUNCT_1:49;
end;
theorem
for T being Functor of C,D holds T is full iff for c,c9 being Object
of C holds rng hom(T,c,c9) = Hom(T.c,T.c9)
proof
let T be Functor of C,D;
thus T is full implies for c,c9 being Object of C holds rng hom(T,c,c9) =
Hom(T.c,T.c9)
proof
assume
A1: T is full;
let c,c9 be Object of C;
now
assume
A2: Hom(T.c,T.c9) <> {};
for g being object holds g in rng hom(T,c,c9) iff g in Hom(T.c,T.c9)
proof
let g be object;
thus g in rng hom(T,c,c9) implies g in Hom(T.c,T.c9)
proof
assume g in rng hom(T,c,c9);
then consider f being object such that
A3: f in dom hom(T,c,c9) and
A4: hom(T,c,c9).f = g by FUNCT_1:def 3;
f in Hom(c,c9) by A2,A3,FUNCT_2:def 1;
hence thesis by A2,A4,FUNCT_2:5;
end;
assume g in Hom(T.c,T.c9);
then g is Morphism of T.c,T.c9 by Def3;
then consider f being Morphism of c,c9 such that
A5: g = T.f by A1,A2;
Hom(c,c9) <> {} by A1,A2;
then f in Hom(c,c9) by Def3;
then hom(T,c,c9).f in rng hom(T,c,c9) by A2,FUNCT_2:4;
hence thesis by A5,A1,A2,Th83;
end;
hence thesis by TARSKI:2;
end;
hence thesis;
end;
assume
A6: for c,c9 being Object of C holds rng hom(T,c,c9) = Hom(T.c,T.c9);
let c,c9 be Object of C such that
A7: Hom(T.c,T.c9) <> {};
let g be Morphism of T.c,T.c9;
g in Hom(T.c,T.c9) by A7,Def3;
then g in rng hom(T,c,c9) by A6;
then consider f being object such that
A8: f in dom hom(T,c,c9) and
A9: hom(T,c,c9).f = g by FUNCT_1:def 3;
thus Hom(c,c9) <> {} by A8;
A10: f in Hom(c,c9) by A7,A8,FUNCT_2:def 1;
then reconsider f as Morphism of c,c9 by Def3;
take f;
thus thesis by A9,A10,Th83;
end;
theorem
for T being Functor of C,D holds T is faithful iff for c,c9 being
Object of C holds hom(T,c,c9) is one-to-one
proof
let T be Functor of C,D;
thus T is faithful implies for c,c9 being Object of C holds hom(T,c,c9) is
one-to-one
proof
assume
A1: T is faithful;
let c,c9 be Object of C;
now
A2: now
let f1,f2 be object;
assume that
A3: f1 in Hom(c,c9) and
A4: f2 in Hom(c,c9);
A5: f2 is Morphism of c,c9 by A4,Def3;
then
A6: T.f2 = hom(T,c,c9).f2 by A3,Th83;
A7: f1 is Morphism of c,c9 by A3,Def3;
then T.f1 = hom(T,c,c9).f1 by A3,Th83;
hence hom(T,c,c9).f1 = hom(T,c,c9).f2 implies f1 = f2 by A1,A3,A7,A5,A6
;
end;
assume Hom(T.c,T.c9) <> {};
hence thesis by A2,FUNCT_2:19;
end;
hence thesis;
end;
assume
A8: for c,c9 being Object of C holds hom(T,c,c9) is one-to-one;
let c,c9 be Object of C such that
A9: Hom(c,c9) <> {};
let f1,f2 be Morphism of c,c9;
A10: T.f2 = hom(T,c,c9).f2 by A9,Th83;
A11: f2 in Hom(c,c9) & T.f1 = hom(T,c,c9).f1 by A9,Def3,Th83;
A12: hom(T,c,c9) is one-to-one by A8;
Hom(T.c,T.c9) <> {} & f1 in Hom(c,c9) by A9,Def3,Th79;
hence thesis by A12,A11,A10,FUNCT_2:19;
end;
theorem
for a,b being Element of C st Hom(a,b)<>{}
ex m being Morphism of a,b st m in Hom(a,b)
proof let a,b being Element of C;
assume Hom(a,b)<>{};
then consider m being object such that
A1: m in Hom(a,b) by XBOOLE_0:def 1;
reconsider m as Morphism of a,b by A1,Def3;
take m;
thus thesis by A1;
end;
theorem
the carrier' of C = union the set of all Hom(a,b)
proof
set A = the set of all Hom(a,b), M = union A;
thus the carrier' of C c= M
proof let e be object;
assume e in the carrier' of C;
then reconsider e as Morphism of C;
A1: e in Hom(dom e,cod e);
Hom(dom e,cod e) in A;
hence thesis by A1,TARSKI:def 4;
end;
let e be object;
assume e in M;
then consider X being set such that
A2: e in X and
A3: X in A by TARSKI:def 4;
ex a,b st X = Hom(a,b) by A3;
hence thesis by A2;
end;