:: by Andrzej Trybulec

::

:: Received February 28, 1995

:: Copyright (c) 1995-2019 Association of Mizar Users

::$CT 4

theorem :: ALTCAT_1:5

scheme :: ALTCAT_1:sch 3

MSSLambda3{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}( object , object , object ) -> object } :

MSSLambda3{ F

ex M being ManySortedSet of [:F_{1}(),F_{2}(),F_{3}():] st

for i, j, k being set st i in F_{1}() & j in F_{2}() & k in F_{3}() holds

M . (i,j,k) = F_{4}(i,j,k)

for i, j, k being set st i in F

M . (i,j,k) = F

proof end;

scheme :: ALTCAT_1:sch 4

MSSLambda3D{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( object , object , object ) -> object } :

MSSLambda3D{ F

ex M being ManySortedSet of [:F_{1}(),F_{2}(),F_{3}():] st

for i being Element of F_{1}()

for j being Element of F_{2}()

for k being Element of F_{3}() holds M . (i,j,k) = F_{4}(i,j,k)

for i being Element of F

for j being Element of F

for k being Element of F

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

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

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

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_{1} is strict ;

struct AltGraph -> 1-sorted ;

aggr AltGraph(# carrier, Arrows #) -> AltGraph ;

sel Arrows c_{1} -> ManySortedSet of [: the carrier of c_{1}, the carrier of c_{1}:];

end;
struct AltGraph -> 1-sorted ;

aggr AltGraph(# carrier, Arrows #) -> AltGraph ;

sel Arrows c

definition

let G be AltGraph ;

let o1, o2 be Object of G;

correctness

coherence

the Arrows of G . (o1,o2) is set ;

;

end;
let o1, o2 be Object of G;

correctness

coherence

the Arrows of G . (o1,o2) is set ;

;

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

for G being AltGraph

for o1, o2 being Object of G holds <^o1,o2^> = the Arrows of G . (o1,o2);

definition
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^> <> {} );

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

ex b_{1} being ManySortedSet of [:I,I,I:] st

for i, j, k being object st i in I & j in I & k in I holds

b_{1} . (i,j,k) = G . (i,k)

for b_{1}, b_{2} being ManySortedSet of [:I,I,I:] st ( for i, j, k being object st i in I & j in I & k in I holds

b_{1} . (i,j,k) = G . (i,k) ) & ( for i, j, k being object st i in I & j in I & k in I holds

b_{2} . (i,j,k) = G . (i,k) ) holds

b_{1} = b_{2}

ex b_{1} being ManySortedSet of [:I,I,I:] st

for i, j, k being object st i in I & j in I & k in I holds

b_{1} . (i,j,k) = [:(H . (j,k)),(G . (i,j)):]

for b_{1}, b_{2} being ManySortedSet of [:I,I,I:] st ( for i, j, k being object st i in I & j in I & k in I holds

b_{1} . (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

b_{2} . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ) holds

b_{1} = b_{2}

end;
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 for i, j, k being object st i in I & j in I & k in I holds

it . (i,j,k) = G . (i,k);

ex b

for i, j, k being object st i in I & j in I & k in I holds

b

proof end;

uniqueness for b

b

b

b

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

ex b

for i, j, k being object st i in I & j in I & k in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for I being set

for G being ManySortedSet of [:I,I:]

for b_{3} being ManySortedSet of [:I,I,I:] holds

( b_{3} = {|G|} iff for i, j, k being object st i in I & j in I & k in I holds

b_{3} . (i,j,k) = G . (i,k) );

for I being set

for G being ManySortedSet of [:I,I:]

for b

( b

b

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

for I being set

for G, H being ManySortedSet of [:I,I:]

for b_{4} being ManySortedSet of [:I,I,I:] holds

( b_{4} = {|G,H|} iff for i, j, k being object st i in I & j in I & k in I holds

b_{4} . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] );

for I being set

for G, H being ManySortedSet of [:I,I:]

for b

( b

b

definition

let I be set ;

let G be ManySortedSet of [:I,I:];

mode BinComp of G is ManySortedFunction of {|G,G|},{|G|};

end;
let G be ManySortedSet of [:I,I:];

mode BinComp of G is ManySortedFunction of {|G,G|},{|G|};

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

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

definition

let I be non empty set ;

let G be ManySortedSet of [:I,I:];

let IT be BinComp of G;

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

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

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

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

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 c_{1} is strict ;

struct AltCatStr -> AltGraph ;

aggr AltCatStr(# carrier, Arrows, Comp #) -> AltCatStr ;

sel Comp c_{1} -> BinComp of the Arrows of c_{1};

end;
struct AltCatStr -> AltGraph ;

aggr AltCatStr(# carrier, Arrows, Comp #) -> AltCatStr ;

sel Comp c

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

( the Comp of C . (o1,o2,o3)) . (g,f) is Morphism of o1,o3

;

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

( the Comp of C . (o1,o2,o3)) . (g,f) is Morphism of o1,o3

proof end;

correctness ;

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

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

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

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 ;

ex b_{1} being ManySortedFunction of [:A,B:] st b_{1} is compositional

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

existence ex b

proof end;

::$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

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 ;

for b_{1}, b_{2} being compositional ManySortedFunction of [:B,A:] holds b_{1} = b_{2}

existence

ex b_{1} being compositional ManySortedFunction of [:B,A:] st verum;

;

end;
func FuncComp (A,B) -> compositional ManySortedFunction of [:B,A:] means :Def10: :: ALTCAT_1:def 10

verum;

uniqueness verum;

for b

proof end;

correctness existence

ex b

;

:: deftheorem Def10 defines FuncComp ALTCAT_1:def 10 :

for A, B being functional set

for b_{3} being compositional ManySortedFunction of [:B,A:] holds

( b_{3} = FuncComp (A,B) iff verum );

for A, B being functional set

for b

( b

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

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 ;

end;
attr C is quasi-functional means :: ALTCAT_1:def 11

for a1, a2 being Object of C holds <^a1,a2^> c= Funcs (a1,a2);

for a1, a2 being Object of C holds <^a1,a2^> c= Funcs (a1,a2);

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

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

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

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;

coherence

not AltCatStr(# X,A,C #) is empty ;

end;
let A be ManySortedSet of [:X,X:];

let C be BinComp of A;

coherence

not AltCatStr(# X,A,C #) is empty ;

registration

existence

ex b_{1} being non empty AltCatStr st

( b_{1} is strict & b_{1} is pseudo-functional )

end;
ex b

( b

proof end;

theorem :: ALTCAT_1:15

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

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

:: ale bez parametryzacji

definition

let A be non empty set ;

ex b_{1} being non empty strict pseudo-functional AltCatStr st

( the carrier of b_{1} = A & ( for a1, a2 being Object of b_{1} holds <^a1,a2^> = Funcs (a1,a2) ) )

for b_{1}, b_{2} being non empty strict pseudo-functional AltCatStr st the carrier of b_{1} = A & ( for a1, a2 being Object of b_{1} holds <^a1,a2^> = Funcs (a1,a2) ) & the carrier of b_{2} = A & ( for a1, a2 being Object of b_{2} holds <^a1,a2^> = Funcs (a1,a2) ) holds

b_{1} = b_{2}

end;
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 ( the carrier of it = A & ( for a1, a2 being Object of it holds <^a1,a2^> = Funcs (a1,a2) ) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines EnsCat ALTCAT_1:def 14 :

for A being non empty set

for b_{2} being non empty strict pseudo-functional AltCatStr holds

( b_{2} = EnsCat A iff ( the carrier of b_{2} = A & ( for a1, a2 being Object of b_{2} holds <^a1,a2^> = Funcs (a1,a2) ) ) );

for A being non empty set

for b

( b

definition

let C be non empty AltCatStr ;

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

( the Comp of C is with_left_units & the Comp of C is with_right_units );

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

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

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 b_{1} being non empty AltCatStr st

( b_{1} is transitive & b_{1} is associative & b_{1} is with_units & b_{1} is strict )

end;
ex b

( b

proof 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^> )

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;

registration

let A be non empty set ;

coherence

( EnsCat A is transitive & EnsCat A is associative & EnsCat A is with_units ) by Lm1;

end;
coherence

( EnsCat A is transitive & EnsCat A is associative & EnsCat A is with_units ) by Lm1;

registration

for b_{1} being non empty AltCatStr st b_{1} is quasi-functional & b_{1} is semi-functional & b_{1} is transitive holds

b_{1} is pseudo-functional

for b_{1} being non empty AltCatStr st b_{1} is with_units & b_{1} is pseudo-functional & b_{1} is transitive holds

( b_{1} is quasi-functional & b_{1} is semi-functional )
end;

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

coherence for b

b

proof end;

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

coherence for b

( b

proof end;

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

definition

let C be non empty with_units AltCatStr ;

let o be Object of C;

ex b_{1} 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 * b_{1} = a

for b_{1}, b_{2} 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 * b_{1} = a ) & ( for o9 being Object of C st <^o,o9^> <> {} holds

for a being Morphism of o,o9 holds a * b_{2} = a ) holds

b_{1} = b_{2}

end;
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 for o9 being Object of C st <^o,o9^> <> {} holds

for a being Morphism of o,o9 holds a * it = a;

ex b

for o9 being Object of C st <^o,o9^> <> {} holds

for a being Morphism of o,o9 holds a * b

proof end;

uniqueness for b

for a being Morphism of o,o9 holds a * b

for a being Morphism of o,o9 holds a * b

b

proof end;

:: deftheorem Def17 defines idm ALTCAT_1:def 17 :

for C being non empty with_units AltCatStr

for o being Object of C

for b_{3} being Morphism of o,o holds

( b_{3} = idm o iff for o9 being Object of C st <^o,o9^> <> {} holds

for a being Morphism of o,o9 holds a * b_{3} = a );

for C being non empty with_units AltCatStr

for o being Object of C

for b

( b

for a being Morphism of o,o9 holds a * b

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

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

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 ;

end;
attr C is quasi-discrete means :Def18: :: ALTCAT_1:def 18

for i, j being Object of C st <^i,j^> <> {} holds

i = j;

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 ;

for i being Object of C holds <^i,i^> is trivial ;

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

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

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

( C is pseudo-discrete iff for o being Object of C holds <^o,o^> = {(idm o)} )

proof end;

registration

coherence

for b_{1} being AltCatStr st b_{1} is 1 -element holds

b_{1} is quasi-discrete
by STRUCT_0:def 10;

end;
for b

b

registration

existence

ex b_{1} being category st

( b_{1} is pseudo-discrete & b_{1} is trivial & b_{1} is strict )
by Th17;

end;
ex b

( b

registration

ex b_{1} being category st

( b_{1} is quasi-discrete & b_{1} is pseudo-discrete & b_{1} is trivial & b_{1} is strict )
by Th17;

end;

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

existence ex b

( b

definition

let A be non empty set ;

ex b_{1} being non empty strict quasi-discrete AltCatStr st

( the carrier of b_{1} = A & ( for i being Object of b_{1} holds <^i,i^> = {(id i)} ) )

uniqueness

for b_{1}, b_{2} being non empty strict quasi-discrete AltCatStr st the carrier of b_{1} = A & ( for i being Object of b_{1} holds <^i,i^> = {(id i)} ) & the carrier of b_{2} = A & ( for i being Object of b_{2} holds <^i,i^> = {(id i)} ) holds

b_{1} = b_{2};

end;
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 ( the carrier of it = A & ( for i being Object of it holds <^i,i^> = {(id i)} ) );

ex b

( the carrier of b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def20 defines DiscrCat ALTCAT_1:def 20 :

for A being non empty set

for b_{2} being non empty strict quasi-discrete AltCatStr holds

( b_{2} = DiscrCat A iff ( the carrier of b_{2} = A & ( for i being Object of b_{2} holds <^i,i^> = {(id i)} ) ) );

for A being non empty set

for b

( b

registration
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) = {}

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)

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 ;

( DiscrCat A is pseudo-functional & DiscrCat A is pseudo-discrete & DiscrCat A is with_units & DiscrCat A is associative )

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

coherence ( DiscrCat A is pseudo-functional & DiscrCat A is pseudo-discrete & DiscrCat A is with_units & DiscrCat A is associative )

proof end;