let C be Category; :: thesis: 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 holds
CatStr(# O,M,d,c,p #) is Category
let O be non empty Subset of the carrier of C; :: thesis: 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 holds
CatStr(# O,M,d,c,p #) is Category
let M be non empty set ; :: thesis: 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 holds
CatStr(# O,M,d,c,p #) is Category
let d, c be Function of M,O; :: thesis: 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 holds
CatStr(# O,M,d,c,p #) is Category
let p be PartFunc of [:M,M:],M; :: thesis: 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 holds
CatStr(# O,M,d,c,p #) is Category
let i be Function of O,M; :: thesis: ( 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 implies CatStr(# O,M,d,c,p #) is Category )
set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
assume that
A1: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } and
A2: d = the Source of C | M and
A3: c = the Target of C | M and
A4: p = the Comp of C || M ; :: thesis: CatStr(# O,M,d,c,p #) is Category
set B = CatStr(# O,M,d,c,p #);
A5: now :: thesis: for f being Morphism of CatStr(# O,M,d,c,p #) holds f is Morphism of C
let f be Morphism of CatStr(# O,M,d,c,p #); :: thesis: f is Morphism of C
consider X being set such that
A6: f in X and
A7: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A1, TARSKI:def 4;
ex a, b being Object of C st
( X = Hom (a,b) & a in O & b in O ) by A7;
hence f is Morphism of C by A6; :: thesis: verum
end;
A8: for f, g being Morphism of CatStr(# O,M,d,c,p #) holds
( [g,f] in dom p iff d . g = c . f )
proof
let f, g be Morphism of CatStr(# O,M,d,c,p #); :: thesis: ( [g,f] in dom p iff d . g = c . f )
reconsider gg = g, ff = f as Morphism of C by A5;
A9: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49;
thus ( [g,f] in dom p implies d . g = c . f ) :: thesis: ( d . g = c . f implies [g,f] in dom p )
proof
assume [g,f] in dom p ; :: thesis: d . g = c . f
then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4, RELAT_1:61;
then [gg,ff] in dom the Comp of C by XBOOLE_0:def 4;
hence d . g = c . f by A9, CAT_1:def 6; :: thesis: verum
end;
assume d . g = c . f ; :: thesis: [g,f] in dom p
then [g,f] in dom the Comp of C by A9, CAT_1:def 6;
then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def 4;
hence [g,f] in dom p by A4, RELAT_1:61; :: thesis: verum
end;
A10: CatStr(# O,M,d,c,p #) is Category-like by A8;
A11: CatStr(# O,M,d,c,p #) is transitive
proof
thus for f, g being Morphism of CatStr(# O,M,d,c,p #) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) :: according to CAT_1:def 7 :: thesis: verum
proof
let f, g be Morphism of CatStr(# O,M,d,c,p #); :: thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
reconsider ff = f, gg = g as Morphism of C by A5;
A12: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49;
assume A13: dom g = cod f ; :: thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
A14: [g,f] in dom the Comp of CatStr(# O,M,d,c,p #) by A13, A8;
A15: p . (g,f) = g (*) f by A13, A8, CAT_1:def 1;
A16: dom p c= dom the Comp of C by A4, RELAT_1:60;
A17: p . [g,f] = the Comp of C . (g,f) by A4, A8, A13, FUNCT_1:47
.= gg (*) ff by A16, A14, CAT_1:def 1 ;
thus dom (g (*) f) = dom (gg (*) ff) by A17, A2, A15, FUNCT_1:49
.= dom ff by A13, A12, CAT_1:def 7
.= dom f by A2, FUNCT_1:49 ; :: thesis: cod (g (*) f) = cod g
thus cod (g (*) f) = cod (gg (*) ff) by A17, A3, A15, FUNCT_1:49
.= cod gg by A13, A12, CAT_1:def 7
.= cod g by A3, FUNCT_1:49 ; :: thesis: verum
end;
end;
A18: CatStr(# O,M,d,c,p #) is associative
proof
thus for f, g, h being Morphism of CatStr(# O,M,d,c,p #) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f :: according to CAT_1:def 8 :: thesis: verum
proof
let f, g, h be Morphism of CatStr(# O,M,d,c,p #); :: thesis: ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )
reconsider ff = f, gg = g, hh = h as Morphism of C by A5;
assume that
A19: dom h = cod g and
A20: dom g = cod f ; :: thesis: h (*) (g (*) f) = (h (*) g) (*) f
A21: h (*) g = the Comp of CatStr(# O,M,d,c,p #) . (h,g) by A19, A8, CAT_1:def 1;
A22: g (*) f = the Comp of CatStr(# O,M,d,c,p #) . (g,f) by A20, A8, CAT_1:def 1;
A23: dom (h (*) g) = dom g by A11, A19;
A24: ( c . g = cod gg & d . g = dom gg ) by A2, A3, FUNCT_1:49;
A25: c . f = cod ff by A3, FUNCT_1:49;
A26: ( f is Morphism of C & d . h = dom hh ) by A2, A5, FUNCT_1:49;
A27: dom gg = d . g by A2, FUNCT_1:49
.= cod ff by A3, A20, FUNCT_1:49 ;
then A28: gg (*) ff = the Comp of C . (gg,ff) by CAT_1:16;
A29: dom hh = d . h by A2, FUNCT_1:49
.= cod gg by A3, A19, FUNCT_1:49 ;
then A30: cod (gg (*) ff) = dom hh by A27, CAT_1:def 7;
A31: hh (*) gg = the Comp of C . (hh,gg) by A29, CAT_1:16;
A32: cod ff = dom (hh (*) gg) by A27, A29, CAT_1:def 7;
A33: cod (g (*) f) = cod g by A11, A20;
hence h (*) (g (*) f) = the Comp of CatStr(# O,M,d,c,p #) . (h,( the Comp of CatStr(# O,M,d,c,p #) . (g,f))) by A22, A19, A8, CAT_1:def 1
.= the Comp of C . [h,(p . [g,f])] by A4, A8, A19, A33, A22, FUNCT_1:47
.= the Comp of C . (hh,(gg (*) ff)) by A4, A8, A20, A28, FUNCT_1:47
.= hh (*) (gg (*) ff) by A30, CAT_1:16
.= (hh (*) gg) (*) ff by A19, A20, A26, A24, A25, CAT_1:def 8
.= the Comp of C . (( the Comp of C . (hh,gg)),ff) by A31, A32, CAT_1:16
.= the Comp of C . [(p . [h,g]),f] by A4, A8, A19, FUNCT_1:47
.= the Comp of CatStr(# O,M,d,c,p #) . (( the Comp of CatStr(# O,M,d,c,p #) . (h,g)),f) by A4, A8, A20, A23, A21, FUNCT_1:47
.= (h (*) g) (*) f by A21, A20, A8, A23, CAT_1:def 1 ;
:: thesis: verum
end;
end;
A34: CatStr(# O,M,d,c,p #) is reflexive
proof
let b be Object of CatStr(# O,M,d,c,p #); :: according to CAT_1:def 9 :: thesis: not Hom (b,b) = {}
b in O ;
then reconsider bb = b as Object of C ;
A35: Hom (bb,bb) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
id bb in Hom (bb,bb) by CAT_1:27;
then reconsider ii = id bb as Morphism of CatStr(# O,M,d,c,p #) by A35, A1, TARSKI:def 4;
A36: dom ii = dom (id bb) by A2, FUNCT_1:49
.= bb ;
cod ii = cod (id bb) by A3, FUNCT_1:49
.= bb ;
then ii in Hom (b,b) by A36;
hence Hom (b,b) <> {} ; :: thesis: verum
end;
CatStr(# O,M,d,c,p #) is with_identities
proof
let a be Element of CatStr(# O,M,d,c,p #); :: according to CAT_1:def 10 :: thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of CatStr(# O,M,d,c,p #) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
a in O ;
then reconsider aa = a as Object of C ;
A37: Hom (aa,aa) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
id aa in Hom (aa,aa) by CAT_1:27;
then reconsider ii = id aa as Morphism of CatStr(# O,M,d,c,p #) by A37, A1, TARSKI:def 4;
A38: dom ii = dom (id aa) by A2, FUNCT_1:49
.= aa ;
A39: cod ii = cod (id aa) by A3, FUNCT_1:49
.= aa ;
then reconsider ii = ii as Morphism of a,a by A38, CAT_1:4;
take ii ; :: thesis: for b1 being Element of the carrier of CatStr(# O,M,d,c,p #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
let b be Element of CatStr(# O,M,d,c,p #); :: thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
b in O ;
then reconsider bb = b as Object of C ;
thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) :: thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )
proof
assume A40: Hom (a,b) <> {} ; :: thesis: for g being Morphism of a,b holds g (*) ii = g
let g be Morphism of a,b; :: thesis: g (*) ii = g
reconsider gg = g as Morphism of C by A5;
A41: dom gg = dom g by A2, FUNCT_1:49
.= aa by A40, CAT_1:5 ;
A42: cod (id aa) = aa ;
cod gg = cod g by A3, FUNCT_1:49
.= bb by A40, CAT_1:5 ;
then reconsider gg = gg as Morphism of aa,bb by A41, CAT_1:4;
A43: dom g = a by A40, CAT_1:5;
hence g (*) ii = p . (g,ii) by A39, A8, CAT_1:def 1
.= the Comp of C . (gg,(id aa)) by A43, A4, A39, A8, FUNCT_1:47
.= gg (*) (id aa) by A41, A42, CAT_1:16
.= g by A41, CAT_1:22 ;
:: thesis: verum
end;
thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) :: thesis: verum
proof
assume A44: Hom (b,a) <> {} ; :: thesis: for f being Morphism of b,a holds ii (*) f = f
let g be Morphism of b,a; :: thesis: ii (*) g = g
reconsider gg = g as Morphism of C by A5;
A45: cod gg = cod g by A3, FUNCT_1:49
.= aa by A44, CAT_1:5 ;
A46: dom (id aa) = aa ;
dom gg = dom g by A2, FUNCT_1:49
.= bb by A44, CAT_1:5 ;
then reconsider gg = gg as Morphism of bb,aa by A45, CAT_1:4;
A47: cod g = a by A44, CAT_1:5;
hence ii (*) g = p . (ii,g) by A38, A8, CAT_1:def 1
.= the Comp of C . ((id aa),gg) by A4, A47, A38, A8, FUNCT_1:47
.= (id aa) (*) gg by A45, A46, CAT_1:16
.= g by A45, CAT_1:21 ;
:: thesis: verum
end;
end;
hence CatStr(# O,M,d,c,p #) is Category by A10, A11, A18, A34; :: thesis: verum