begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
canceled;
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
for
i,
j,
k being
set holds
(i,j :-> k) . i,
j = k
begin
:: deftheorem ALTCAT_1:def 1 :
canceled;
:: deftheorem defines <^ ALTCAT_1:def 2 :
for G being AltGraph
for o1, o2 being object of G holds <^o1,o2^> = the Arrows of G . o1,o2;
:: deftheorem ALTCAT_1:def 3 :
canceled;
:: deftheorem Def4 defines transitive ALTCAT_1:def 4 :
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^> <> {} );
begin
definition
let I be
set ;
let G be
ManySortedSet of
[:I,I:];
func {|G|} -> ManySortedSet of
[:I,I,I:] means :
Def5:
for
i,
j,
k being
set 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 set st i in I & j in I & k in I holds
b1 . i,j,k = G . i,k
uniqueness
for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being set st i in I & j in I & k in I holds
b1 . i,j,k = G . i,k ) & ( for i, j, k being set st i in I & j in I & k in I holds
b2 . i,j,k = G . i,k ) holds
b1 = b2
let H be
ManySortedSet of
[:I,I:];
func {|G,H|} -> ManySortedSet of
[:I,I,I:] means :
Def6:
for
i,
j,
k being
set 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 set st i in I & j in I & k in I holds
b1 . i,j,k = [:(H . j,k),(G . i,j):]
uniqueness
for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being set 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 set st i in I & j in I & k in I holds
b2 . i,j,k = [:(H . j,k),(G . i,j):] ) holds
b1 = b2
end;
:: deftheorem Def5 defines {| ALTCAT_1:def 5 :
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 set st i in I & j in I & k in I holds
b3 . i,j,k = G . i,k );
:: deftheorem Def6 defines {| ALTCAT_1:def 6 :
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 set 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 non
empty set ;
let G be
ManySortedSet of
[:I,I:];
let o be
BinComp of
G;
let i,
j,
k be
Element of
I;
.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;
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 :
Def7:
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 :
Def8:
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 :
Def9:
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 Def7 defines associative 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 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 Def8 defines with_right_units ALTCAT_1:def 8 :
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 Def9 defines with_left_units ALTCAT_1:def 9 :
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 ) ) );
begin
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 :
Def10:
(the Comp of C . o1,o2,o3) . g,
f;
coherence
(the Comp of C . o1,o2,o3) . g,f is Morphism of o1,o3
correctness
;
end;
:: deftheorem Def10 defines * ALTCAT_1:def 10 :
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 Def11 defines compositional ALTCAT_1:def 11 :
for IT being Function holds
( IT is compositional iff for x being set st x in dom IT holds
ex f, g being Function st
( x = [g,f] & IT . x = g * f ) );
theorem Th13:
:: deftheorem Def12 defines FuncComp ALTCAT_1:def 12 :
for A, B being functional set
for b3 being compositional ManySortedFunction of [:B,A:] holds
( b3 = FuncComp A,B iff verum );
theorem Th14:
theorem Th15:
theorem Th16:
definition
let C be non
empty AltCatStr ;
attr C is
quasi-functional means :
Def13:
for
a1,
a2 being
object of
C holds
<^a1,a2^> c= Funcs a1,
a2;
attr C is
semi-functional means :
Def14:
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 :
Def15:
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 Def13 defines quasi-functional ALTCAT_1:def 13 :
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 Def14 defines semi-functional ALTCAT_1:def 14 :
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 Def15 defines pseudo-functional ALTCAT_1:def 15 :
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^>:] );
theorem
theorem Th18:
definition
let A be non
empty set ;
func EnsCat A -> non
empty strict pseudo-functional AltCatStr means :
Def16:
( 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 ) )
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
end;
:: deftheorem Def16 defines EnsCat ALTCAT_1:def 16 :
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 ) ) );
:: deftheorem Def17 defines associative ALTCAT_1:def 17 :
for C being non empty AltCatStr holds
( C is associative iff the Comp of C is associative );
:: deftheorem Def18 defines with_units ALTCAT_1:def 18 :
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 )
theorem
canceled;
theorem
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^> )
theorem Th21:
begin
definition
let C be non
empty with_units AltCatStr ;
let o be
object of
C;
func idm o -> Morphism of
o,
o means :
Def19:
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
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
end;
:: deftheorem Def19 defines idm ALTCAT_1:def 19 :
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
canceled;
theorem Th23:
theorem
theorem
begin
:: deftheorem Def20 defines quasi-discrete ALTCAT_1:def 20 :
for C being AltCatStr holds
( C is quasi-discrete iff for i, j being object of C st <^i,j^> <> {} holds
i = j );
:: deftheorem Def21 defines pseudo-discrete ALTCAT_1:def 21 :
for C being AltCatStr holds
( C is pseudo-discrete iff for i being object of C holds <^i,i^> is trivial );
theorem
theorem Th27:
:: deftheorem Def22 defines DiscrCat ALTCAT_1:def 22 :
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)} ) ) );
theorem Th28:
theorem Th29: