ALTCAT_1: Categories without Uniqueness of { \bf cod } and { \bf dom }

:: Categories without Uniqueness of { \bf cod } and { \bf dom }
:: by Andrzej Trybulec
::
:: Received February 28, 1995
:: 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 FUNCT_1:49, ZFMISC_1:87;

scheme :: ALTCAT_1:sch 1
MSSLambda2{ F₁() -> set , F₂() -> set , F₃( object , object ) -> object } :

ex M being ManySortedSet of [:F₁(),F₂():] st
for i, j being set st i in F₁() & j in F₂() holds
M . (i,j) = F₃(i,j)

proof end;

scheme :: ALTCAT_1:sch 2
MSSLambda2D{ F₁() -> non empty set , F₂() -> non empty set , F₃( object , object ) -> object } :

ex M being ManySortedSet of [:F₁(),F₂():] st
for i being Element of F₁()
for j being Element of F₂() holds M . (i,j) = F₃(i,j)

proof end;

scheme :: ALTCAT_1:sch 3
MSSLambda3{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( object , object , object ) -> object } :

ex M being ManySortedSet of [:F₁(),F₂(),F₃():] st
for i, j, k being set st i in F₁() & j in F₂() & k in F₃() holds
M . (i,j,k) = F₄(i,j,k)

proof end;

scheme :: ALTCAT_1:sch 4
MSSLambda3D{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( object , object , object ) -> object } :

ex M being ManySortedSet of [:F₁(),F₂(),F₃():] st
for i being Element of F₁()
for j being Element of F₂()
for k being Element of F₃() holds M . (i,j,k) = F₄(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 c₁ is strict ;
struct AltGraph -> 1-sorted ;
aggr AltGraph(# carrier, Arrows #) -> AltGraph ;
sel Arrows c₁ -> ManySortedSet of [: the carrier of c₁, the carrier of c₁:];

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);

end;

:: deftheorem defines <^ ALTCAT_1:def 1 :

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 :

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);

proof end;

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)):];

proof end;

proof end;

end;

:: deftheorem Def3 defines {| ALTCAT_1:def 3 :

:: deftheorem Def4 defines {| ALTCAT_1:def 4 :

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

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 :

:: deftheorem defines with_right_units ALTCAT_1:def 6 :

:: deftheorem defines with_left_units ALTCAT_1:def 7 :

definition

attr c₁ is strict ;
struct AltCatStr -> AltGraph ;
aggr AltCatStr(# carrier, Arrows, Comp #) -> AltCatStr ;
sel Comp c₁ -> BinComp of the Arrows of c₁;

end;

registration

cluster non empty strict for AltCatStr ;

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);

proof end;

end;

:: deftheorem Def8 defines * ALTCAT_1:def 8 :

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 :

registration

let A, B be functional set ;

cluster Relation-like [:A,B:] -defined Function-like V14([:A,B:]) Function-yielding V25() compositional for set ;

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;

proof end;

end;

:: deftheorem Def10 defines FuncComp ALTCAT_1:def 10 :

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 :

:: deftheorem defines semi-functional ALTCAT_1:def 12 :

:: deftheorem Def13 defines pseudo-functional ALTCAT_1:def 13 :

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 ;

end;

registration

cluster non empty strict pseudo-functional for AltCatStr ;

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) ) );

proof end;

proof end;

end;

:: deftheorem Def14 defines EnsCat ALTCAT_1:def 14 :

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 :

:: deftheorem Def16 defines with_units ALTCAT_1:def 16 :

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

proof end;

registration

cluster non empty transitive strict associative with_units for AltCatStr ;

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 ;

cluster EnsCat A -> non empty transitive strict pseudo-functional associative with_units ;

coherence by Lm1;

end;

registration

cluster non empty transitive quasi-functional semi-functional -> non empty pseudo-functional for AltCatStr ;

proof end;

cluster non empty transitive pseudo-functional with_units -> non empty quasi-functional semi-functional for AltCatStr ;

proof end;

end;

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

definition

mode category is non empty transitive associative with_units AltCatStr ;

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;

proof end;

proof end;

end;

:: deftheorem Def17 defines idm ALTCAT_1:def 17 :

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 :

:: deftheorem defines pseudo-discrete ALTCAT_1:def 19 :

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

cluster 1 -element -> quasi-discrete for AltCatStr ;

coherence by STRUCT_0:def 10;

end;

theorem Th17: :: ALTCAT_1:23

( EnsCat {0} is pseudo-discrete & EnsCat {0} is 1 -element )

proof end;

registration

cluster non empty trivial transitive strict associative with_units pseudo-discrete for AltCatStr ;

existence by Th17;

end;

registration

cluster non empty trivial transitive strict associative with_units quasi-discrete pseudo-discrete for AltCatStr ;

existence by Th17;

end;

definition

mode discrete_category is quasi-discrete pseudo-discrete category;

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)} ) );

proof end;

proof end;

end;

:: deftheorem Def20 defines DiscrCat ALTCAT_1:def 20 :

registration

cluster quasi-discrete -> transitive for AltCatStr ;

end;

theorem Th18: :: ALTCAT_1:24

for A being non empty set
for o1, o2, o3 being Object of (DiscrCat A) st ( o1 <> o2 or o2 <> o3 ) holds
the Comp of (DiscrCat A) . (o1,o2,o3) = {}

proof end;

theorem Th19: :: ALTCAT_1:25

for A being non empty set
for o being Object of (DiscrCat A) holds the Comp of (DiscrCat A) . (o,o,o) = ((id o),(id o)) :-> (id o)

proof end;

registration

let A be non empty set ;

cluster DiscrCat A -> non empty strict pseudo-functional associative with_units quasi-discrete pseudo-discrete ;

proof end;

end;