:: Categories without Uniqueness of { \bf cod } and { \bf dom }
:: by Andrzej Trybulec
::
:: Copyright (c) 1995-2021 Association of Mizar Users

theorem :: ALTCAT_1:1
canceled;

theorem :: ALTCAT_1:2
canceled;

theorem :: ALTCAT_1:3
canceled;

theorem :: ALTCAT_1:4
canceled;

::$CT 4 theorem :: ALTCAT_1:5 for A, B being set for F being ManySortedSet of [:B,A:] for C being Subset of A for D being Subset of B for x, y being set st x in C & y in D holds F . (y,x) = (F | [:D,C:]) . (y,x) by ; scheme :: ALTCAT_1:sch 1 MSSLambda2{ F1() -> set , F2() -> set , F3( object , object ) -> object } : ex M being ManySortedSet of [:F1(),F2():] st for i, j being set st i in F1() & j in F2() holds M . (i,j) = F3(i,j) proof end; scheme :: ALTCAT_1:sch 2 MSSLambda2D{ F1() -> non empty set , F2() -> non empty set , F3( object , object ) -> object } : ex M being ManySortedSet of [:F1(),F2():] st for i being Element of F1() for j being Element of F2() holds M . (i,j) = F3(i,j) proof end; scheme :: ALTCAT_1:sch 3 MSSLambda3{ F1() -> set , F2() -> set , F3() -> set , F4( object , object , object ) -> object } : ex M being ManySortedSet of [:F1(),F2(),F3():] st for i, j, k being set st i in F1() & j in F2() & k in F3() holds M . (i,j,k) = F4(i,j,k) proof end; scheme :: ALTCAT_1:sch 4 MSSLambda3D{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4( object , object , object ) -> object } : ex M being ManySortedSet of [:F1(),F2(),F3():] st for i being Element of F1() for j being Element of F2() for k being Element of F3() holds M . (i,j,k) = F4(i,j,k) proof end; theorem Th2: :: ALTCAT_1:6 for A, B being set for N, M being ManySortedSet of [:A,B:] st ( for i, j being object st i in A & j in B holds N . (i,j) = M . (i,j) ) holds M = N proof end; theorem Th3: :: ALTCAT_1:7 for A, B being non empty set for N, M being ManySortedSet of [:A,B:] st ( for i being Element of A for j being Element of B holds N . (i,j) = M . (i,j) ) holds M = N proof end; theorem Th4: :: ALTCAT_1:8 for A being set for N, M being ManySortedSet of [:A,A,A:] st ( for i, j, k being object st i in A & j in A & k in A holds N . (i,j,k) = M . (i,j,k) ) holds M = N proof end; definition attr c1 is strict ; struct AltGraph -> 1-sorted ; aggr AltGraph(# carrier, Arrows #) -> AltGraph ; sel Arrows c1 -> ManySortedSet of [: the carrier of c1, the carrier of c1:]; end; definition let G be AltGraph ; mode Object of G is Element of G; end; definition let G be AltGraph ; let o1, o2 be Object of G; func <^o1,o2^> -> set equals :: ALTCAT_1:def 1 the Arrows of G . (o1,o2); correctness coherence the Arrows of G . (o1,o2) is set ; ; end; :: deftheorem defines <^ ALTCAT_1:def 1 : for G being AltGraph for o1, o2 being Object of G holds <^o1,o2^> = the Arrows of G . (o1,o2); definition let G be AltGraph ; let o1, o2 be Object of G; mode Morphism of o1,o2 is Element of <^o1,o2^>; end; definition let G be AltGraph ; attr G is transitive means :Def2: :: ALTCAT_1:def 2 for o1, o2, o3 being Object of G st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds <^o1,o3^> <> {} ; end; :: deftheorem Def2 defines transitive ALTCAT_1:def 2 : for G being AltGraph holds ( G is transitive iff for o1, o2, o3 being Object of G st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds <^o1,o3^> <> {} ); definition let I be set ; let G be ManySortedSet of [:I,I:]; func {|G|} -> ManySortedSet of [:I,I,I:] means :Def3: :: ALTCAT_1:def 3 for i, j, k being object st i in I & j in I & k in I holds it . (i,j,k) = G . (i,k); existence ex b1 being ManySortedSet of [:I,I,I:] st for i, j, k being object st i in I & j in I & k in I holds b1 . (i,j,k) = G . (i,k) proof end; uniqueness for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being object st i in I & j in I & k in I holds b1 . (i,j,k) = G . (i,k) ) & ( for i, j, k being object st i in I & j in I & k in I holds b2 . (i,j,k) = G . (i,k) ) holds b1 = b2 proof end; let H be ManySortedSet of [:I,I:]; func {|G,H|} -> ManySortedSet of [:I,I,I:] means :Def4: :: ALTCAT_1:def 4 for i, j, k being object st i in I & j in I & k in I holds it . (i,j,k) = [:(H . (j,k)),(G . (i,j)):]; existence ex b1 being ManySortedSet of [:I,I,I:] st for i, j, k being object st i in I & j in I & k in I holds b1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] proof end; uniqueness for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being object st i in I & j in I & k in I holds b1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ) & ( for i, j, k being object st i in I & j in I & k in I holds b2 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ) holds b1 = b2 proof end; end; :: deftheorem Def3 defines {| ALTCAT_1:def 3 : for I being set for G being ManySortedSet of [:I,I:] for b3 being ManySortedSet of [:I,I,I:] holds ( b3 = {|G|} iff for i, j, k being object st i in I & j in I & k in I holds b3 . (i,j,k) = G . (i,k) ); :: deftheorem Def4 defines {| ALTCAT_1:def 4 : for I being set for G, H being ManySortedSet of [:I,I:] for b4 being ManySortedSet of [:I,I,I:] holds ( b4 = {|G,H|} iff for i, j, k being object st i in I & j in I & k in I holds b4 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ); definition let I be set ; let G be ManySortedSet of [:I,I:]; mode BinComp of G is ManySortedFunction of {|G,G|},{|G|}; end; definition let I be non empty set ; let G be ManySortedSet of [:I,I:]; let o be BinComp of G; let i, j, k be Element of I; :: original: . redefine func o . (i,j,k) -> Function of [:(G . (j,k)),(G . (i,j)):],(G . (i,k)); coherence o . (i,j,k) is Function of [:(G . (j,k)),(G . (i,j)):],(G . (i,k)) proof end; end; definition let I be non empty set ; let G be ManySortedSet of [:I,I:]; let IT be BinComp of G; attr IT is associative means :: ALTCAT_1:def 5 for i, j, k, l being Element of I for f, g, h being set st f in G . (i,j) & g in G . (j,k) & h in G . (k,l) holds (IT . (i,k,l)) . (h,((IT . (i,j,k)) . (g,f))) = (IT . (i,j,l)) . (((IT . (j,k,l)) . (h,g)),f); attr IT is with_right_units means :: ALTCAT_1:def 6 for i being Element of I ex e being set st ( e in G . (i,i) & ( for j being Element of I for f being set st f in G . (i,j) holds (IT . (i,i,j)) . (f,e) = f ) ); attr IT is with_left_units means :: ALTCAT_1:def 7 for j being Element of I ex e being set st ( e in G . (j,j) & ( for i being Element of I for f being set st f in G . (i,j) holds (IT . (i,j,j)) . (e,f) = f ) ); end; :: deftheorem defines associative ALTCAT_1:def 5 : for I being non empty set for G being ManySortedSet of [:I,I:] for IT being BinComp of G holds ( IT is associative iff for i, j, k, l being Element of I for f, g, h being set st f in G . (i,j) & g in G . (j,k) & h in G . (k,l) holds (IT . (i,k,l)) . (h,((IT . (i,j,k)) . (g,f))) = (IT . (i,j,l)) . (((IT . (j,k,l)) . (h,g)),f) ); :: deftheorem defines with_right_units ALTCAT_1:def 6 : for I being non empty set for G being ManySortedSet of [:I,I:] for IT being BinComp of G holds ( IT is with_right_units iff for i being Element of I ex e being set st ( e in G . (i,i) & ( for j being Element of I for f being set st f in G . (i,j) holds (IT . (i,i,j)) . (f,e) = f ) ) ); :: deftheorem defines with_left_units ALTCAT_1:def 7 : for I being non empty set for G being ManySortedSet of [:I,I:] for IT being BinComp of G holds ( IT is with_left_units iff for j being Element of I ex e being set st ( e in G . (j,j) & ( for i being Element of I for f being set st f in G . (i,j) holds (IT . (i,j,j)) . (e,f) = f ) ) ); definition attr c1 is strict ; struct AltCatStr -> AltGraph ; aggr AltCatStr(# carrier, Arrows, Comp #) -> AltCatStr ; sel Comp c1 -> BinComp of the Arrows of c1; end; registration cluster non empty strict for AltCatStr ; existence ex b1 being AltCatStr st ( b1 is strict & not b1 is empty ) proof end; end; definition let C be non empty AltCatStr ; let o1, o2, o3 be Object of C; assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; let f be Morphism of o1,o2; let g be Morphism of o2,o3; func g * f -> Morphism of o1,o3 equals :Def8: :: ALTCAT_1:def 8 ( the Comp of C . (o1,o2,o3)) . (g,f); coherence ( the Comp of C . (o1,o2,o3)) . (g,f) is Morphism of o1,o3 proof end; correctness ; end; :: deftheorem Def8 defines * ALTCAT_1:def 8 : for C being non empty AltCatStr for o1, o2, o3 being Object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds for f being Morphism of o1,o2 for g being Morphism of o2,o3 holds g * f = ( the Comp of C . (o1,o2,o3)) . (g,f); definition let IT be Function; attr IT is compositional means :Def9: :: ALTCAT_1:def 9 for x being object st x in dom IT holds ex f, g being Function st ( x = [g,f] & IT . x = g * f ); end; :: deftheorem Def9 defines compositional ALTCAT_1:def 9 : for IT being Function holds ( IT is compositional iff for x being object st x in dom IT holds ex f, g being Function st ( x = [g,f] & IT . x = g * f ) ); registration let A, B be functional set ; existence ex b1 being ManySortedFunction of [:A,B:] st b1 is compositional proof end; end; theorem :: ALTCAT_1:9 canceled; theorem :: ALTCAT_1:10 canceled; ::$CT 2
theorem Th5: :: ALTCAT_1:11
for A, B being functional set
for F being compositional ManySortedSet of [:A,B:]
for g, f being Function st g in A & f in B holds
F . (g,f) = g * f
proof end;

definition
let A, B be functional set ;
func FuncComp (A,B) -> compositional ManySortedFunction of [:B,A:] means :Def10: :: ALTCAT_1:def 10
verum;
uniqueness
for b1, b2 being compositional ManySortedFunction of [:B,A:] holds b1 = b2
proof end;
correctness
existence
ex b1 being compositional ManySortedFunction of [:B,A:] st verum
;
;
end;

:: deftheorem Def10 defines FuncComp ALTCAT_1:def 10 :
for A, B being functional set
for b3 being compositional ManySortedFunction of [:B,A:] holds
( b3 = FuncComp (A,B) iff verum );

theorem Th6: :: ALTCAT_1:12
for A, B, C being set holds rng (FuncComp ((Funcs (A,B)),(Funcs (B,C)))) c= Funcs (A,C)
proof end;

theorem Th7: :: ALTCAT_1:13
for o being set holds FuncComp ({(id o)},{(id o)}) = ((id o),(id o)) :-> (id o)
proof end;

theorem Th8: :: ALTCAT_1:14
for A, B being functional set
for A1 being Subset of A
for B1 being Subset of B holds FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
proof end;

:: Kategorie przeksztalcen, Semadeni Wiweger, 1.2.2, str.15
definition
let C be non empty AltCatStr ;
attr C is quasi-functional means :: ALTCAT_1:def 11
for a1, a2 being Object of C holds <^a1,a2^> c= Funcs (a1,a2);
attr C is semi-functional means :: ALTCAT_1:def 12
for a1, a2, a3 being Object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9;
attr C is pseudo-functional means :Def13: :: ALTCAT_1:def 13
for o1, o2, o3 being Object of C holds the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:];
end;

:: deftheorem defines quasi-functional ALTCAT_1:def 11 :
for C being non empty AltCatStr holds
( C is quasi-functional iff for a1, a2 being Object of C holds <^a1,a2^> c= Funcs (a1,a2) );

:: deftheorem defines semi-functional ALTCAT_1:def 12 :
for C being non empty AltCatStr holds
( C is semi-functional iff for a1, a2, a3 being Object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9 );

:: deftheorem Def13 defines pseudo-functional ALTCAT_1:def 13 :
for C being non empty AltCatStr holds
( C is pseudo-functional iff for o1, o2, o3 being Object of C holds the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] );

registration
let X be non empty set ;
let A be ManySortedSet of [:X,X:];
let C be BinComp of A;
cluster AltCatStr(# X,A,C #) -> non empty ;
coherence
not AltCatStr(# X,A,C #) is empty
;
end;

registration
existence
ex b1 being non empty AltCatStr st
( b1 is strict & b1 is pseudo-functional )
proof end;
end;

theorem :: ALTCAT_1:15
for C being non empty AltCatStr
for a1, a2, a3 being Object of C holds the Comp of C . (a1,a2,a3) is Function of [:<^a2,a3^>,<^a1,a2^>:],<^a1,a3^> ;

theorem Th10: :: ALTCAT_1:16
for C being non empty pseudo-functional AltCatStr
for a1, a2, a3 being Object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9
proof end;

:: Kategorie EnsCat(A), Semadeni Wiweger 1.2.3, str. 15
:: ale bez parametryzacji
definition
let A be non empty set ;
func EnsCat A -> non empty strict pseudo-functional AltCatStr means :Def14: :: ALTCAT_1:def 14
( the carrier of it = A & ( for a1, a2 being Object of it holds <^a1,a2^> = Funcs (a1,a2) ) );
existence
ex b1 being non empty strict pseudo-functional AltCatStr st
( the carrier of b1 = A & ( for a1, a2 being Object of b1 holds <^a1,a2^> = Funcs (a1,a2) ) )
proof end;
uniqueness
for b1, b2 being non empty strict pseudo-functional AltCatStr st the carrier of b1 = A & ( for a1, a2 being Object of b1 holds <^a1,a2^> = Funcs (a1,a2) ) & the carrier of b2 = A & ( for a1, a2 being Object of b2 holds <^a1,a2^> = Funcs (a1,a2) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines EnsCat ALTCAT_1:def 14 :
for A being non empty set
for b2 being non empty strict pseudo-functional AltCatStr holds
( b2 = EnsCat A iff ( the carrier of b2 = A & ( for a1, a2 being Object of b2 holds <^a1,a2^> = Funcs (a1,a2) ) ) );

definition
let C be non empty AltCatStr ;
attr C is associative means :Def15: :: ALTCAT_1:def 15
the Comp of C is associative ;
attr C is with_units means :Def16: :: ALTCAT_1:def 16
( the Comp of C is with_left_units & the Comp of C is with_right_units );
end;

:: deftheorem Def15 defines associative ALTCAT_1:def 15 :
for C being non empty AltCatStr holds
( C is associative iff the Comp of C is associative );

:: deftheorem Def16 defines with_units ALTCAT_1:def 16 :
for C being non empty AltCatStr holds
( C is with_units iff ( the Comp of C is with_left_units & the Comp of C is with_right_units ) );

Lm1: for A being non empty set holds
( EnsCat A is transitive & EnsCat A is associative & EnsCat A is with_units )

proof end;

registration
existence
ex b1 being non empty AltCatStr st
( b1 is transitive & b1 is associative & b1 is with_units & b1 is strict )
proof end;
end;

theorem :: ALTCAT_1:17
for C being non empty transitive AltCatStr
for a1, a2, a3 being Object of C holds
( dom ( the Comp of C . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] & rng ( the Comp of C . (a1,a2,a3)) c= <^a1,a3^> )
proof end;

theorem Th12: :: ALTCAT_1:18
for C being non empty with_units AltCatStr
for o being Object of C holds <^o,o^> <> {}
proof end;

registration
let A be non empty set ;
coherence
( EnsCat A is transitive & EnsCat A is associative & EnsCat A is with_units )
by Lm1;
end;

registration
coherence
for b1 being non empty AltCatStr st b1 is quasi-functional & b1 is semi-functional & b1 is transitive holds
b1 is pseudo-functional
proof end;
coherence
for b1 being non empty AltCatStr st b1 is with_units & b1 is pseudo-functional & b1 is transitive holds
( b1 is quasi-functional & b1 is semi-functional )
proof end;
end;

:: Definicja kategorii, Semadeni Wiweger 1.3.1, str. 16-17
definition end;

definition
let C be non empty with_units AltCatStr ;
let o be Object of C;
func idm o -> Morphism of o,o means :Def17: :: ALTCAT_1:def 17
for o9 being Object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * it = a;
existence
ex b1 being Morphism of o,o st
for o9 being Object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b1 = a
proof end;
uniqueness
for b1, b2 being Morphism of o,o st ( for o9 being Object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b1 = a ) & ( for o9 being Object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b2 = a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines idm ALTCAT_1:def 17 :
for C being non empty with_units AltCatStr
for o being Object of C
for b3 being Morphism of o,o holds
( b3 = idm o iff for o9 being Object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b3 = a );

theorem Th13: :: ALTCAT_1:19
for C being non empty with_units AltCatStr
for o being Object of C holds idm o in <^o,o^>
proof end;

theorem :: ALTCAT_1:20
for C being non empty with_units AltCatStr
for o1, o2 being Object of C st <^o1,o2^> <> {} holds
for a being Morphism of o1,o2 holds (idm o2) * a = a
proof end;

theorem :: ALTCAT_1:21
for C being non empty transitive associative AltCatStr
for o1, o2, o3, o4 being Object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a
proof end;

:: kategoria dyskretna, Semadeni Wiweger, 1.3.1, str.18
definition
let C be AltCatStr ;
attr C is quasi-discrete means :Def18: :: ALTCAT_1:def 18
for i, j being Object of C st <^i,j^> <> {} holds
i = j;
attr C is pseudo-discrete means :: ALTCAT_1:def 19
for i being Object of C holds <^i,i^> is trivial ;
end;

:: deftheorem Def18 defines quasi-discrete ALTCAT_1:def 18 :
for C being AltCatStr holds
( C is quasi-discrete iff for i, j being Object of C st <^i,j^> <> {} holds
i = j );

:: deftheorem defines pseudo-discrete ALTCAT_1:def 19 :
for C being AltCatStr holds
( C is pseudo-discrete iff for i being Object of C holds <^i,i^> is trivial );

theorem :: ALTCAT_1:22
for C being non empty with_units AltCatStr holds
( C is pseudo-discrete iff for o being Object of C holds <^o,o^> = {(idm o)} )
proof end;

registration
coherence
for b1 being AltCatStr st b1 is 1 -element holds
b1 is quasi-discrete
by STRUCT_0:def 10;
end;

theorem Th17: :: ALTCAT_1:23
proof end;

registration
existence
ex b1 being category st
( b1 is pseudo-discrete & b1 is trivial & b1 is strict )
by Th17;
end;

registration
existence
ex b1 being category st
( b1 is quasi-discrete & b1 is pseudo-discrete & b1 is trivial & b1 is strict )
by Th17;
end;

definition end;

definition
let A be non empty set ;
func DiscrCat A -> non empty strict quasi-discrete AltCatStr means :Def20: :: ALTCAT_1:def 20
( the carrier of it = A & ( for i being Object of it holds <^i,i^> = {(id i)} ) );
existence
ex b1 being non empty strict quasi-discrete AltCatStr st
( the carrier of b1 = A & ( for i being Object of b1 holds <^i,i^> = {(id i)} ) )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict quasi-discrete AltCatStr st the carrier of b1 = A & ( for i being Object of b1 holds <^i,i^> = {(id i)} ) & the carrier of b2 = A & ( for i being Object of b2 holds <^i,i^> = {(id i)} ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def20 defines DiscrCat ALTCAT_1:def 20 :
for A being non empty set
for b2 being non empty strict quasi-discrete AltCatStr holds
( b2 = DiscrCat A iff ( the carrier of b2 = A & ( for i being Object of b2 holds <^i,i^> = {(id i)} ) ) );

registration
coherence
for b1 being AltCatStr st b1 is quasi-discrete holds
b1 is transitive
;
end;

theorem Th18: :: ALTCAT_1:24
for A being non empty set
for o1, o2, o3 being Object of () st ( o1 <> o2 or o2 <> o3 ) holds
the Comp of () . (o1,o2,o3) = {}
proof end;

theorem Th19: :: ALTCAT_1:25
for A being non empty set
for o being Object of () holds the Comp of () . (o,o,o) = ((id o),(id o)) :-> (id o)
proof end;

registration
let A be non empty set ;
coherence
proof end;
end;