altcat_1.miz
begin
reserve i,j,k,x for
object;
::$Canceled
theorem ::
ALTCAT_1:5
for A,B be
set, F be
ManySortedSet of
[:B, A:], C be
Subset of A, D be
Subset of B, x,y be
set st x
in C & y
in D holds (F
. (y,x))
= ((F
|
[:D, C:] qua
set)
. (y,x)) by
FUNCT_1: 49,
ZFMISC_1: 87;
scheme ::
ALTCAT_1:sch1
MSSLambda2 { A,B() ->
set , F(
object,
object) ->
object } :
ex M be
ManySortedSet of
[:A(), B():] st for i,j be
set st i
in A() & j
in B() holds (M
. (i,j))
= F(i,j);
deffunc
F(
object) = F(`1,`2);
consider f be
Function such that
A1: (
dom f)
=
[:A(), B():] and
A2: for x be
object st x
in
[:A(), B():] holds (f
. x)
=
F(x) from
FUNCT_1:sch 3;
reconsider f as
ManySortedSet of
[:A(), B():] by
A1,
PARTFUN1:def 2,
RELAT_1:def 18;
take f;
let i,j be
set;
assume i
in A() & j
in B();
then
A3:
[i, j]
in
[:A(), B():] by
ZFMISC_1: 87;
(
[i, j]
`1 )
= i & (
[i, j]
`2 )
= j;
hence thesis by
A2,
A3;
end;
scheme ::
ALTCAT_1:sch2
MSSLambda2D { A,B() -> non
empty
set , F(
object,
object) ->
object } :
ex M be
ManySortedSet of
[:A(), B():] st for i be
Element of A(), j be
Element of B() holds (M
. (i,j))
= F(i,j);
consider M be
ManySortedSet of
[:A(), B():] such that
A1: for i,j be
set st i
in A() & j
in B() holds (M
. (i,j))
= F(i,j) from
MSSLambda2;
take M;
thus thesis by
A1;
end;
scheme ::
ALTCAT_1:sch3
MSSLambda3 { A,B,C() ->
set , F(
object,
object,
object) ->
object } :
ex M be
ManySortedSet of
[:A(), B(), C():] st for i,j,k be
set st i
in A() & j
in B() & k
in C() holds (M
. (i,j,k))
= F(i,j,k);
deffunc
F(
object) = F(`1,`2,`2);
consider f be
Function such that
A1: (
dom f)
=
[:A(), B(), C():] and
A2: for x be
object st x
in
[:A(), B(), C():] holds (f
. x)
=
F(x) from
FUNCT_1:sch 3;
reconsider f as
ManySortedSet of
[:A(), B(), C():] by
A1,
PARTFUN1:def 2,
RELAT_1:def 18;
take f;
let i,j,k be
set;
A3: (
[
[i, j], k]
`2 )
= k &
[i, j, k]
=
[
[i, j], k];
A4: ((
[
[i, j], k]
`1 )
`2 )
= j;
A5: ((
[
[i, j], k]
`1 )
`1 )
= i;
assume i
in A() & j
in B() & k
in C();
then
A6:
[i, j, k]
in
[:A(), B(), C():] by
MCART_1: 69;
thus (f
. (i,j,k))
= (f
.
[i, j, k]) by
MULTOP_1:def 1
.= F(i,j,k) by
A2,
A6,
A5,
A4,
A3;
end;
scheme ::
ALTCAT_1:sch4
MSSLambda3D { A,B,C() -> non
empty
set , F(
object,
object,
object) ->
object } :
ex M be
ManySortedSet of
[:A(), B(), C():] st for i be
Element of A(), j be
Element of B(), k be
Element of C() holds (M
. (i,j,k))
= F(i,j,k);
consider M be
ManySortedSet of
[:A(), B(), C():] such that
A1: for i,j,k be
set st i
in A() & j
in B() & k
in C() holds (M
. (i,j,k))
= F(i,j,k) from
MSSLambda3;
take M;
thus thesis by
A1;
end;
theorem ::
ALTCAT_1:6
Th2: for A,B be
set, N,M be
ManySortedSet of
[:A, B:] st for i, j st i
in A & j
in B holds (N
. (i,j))
= (M
. (i,j)) holds M
= N
proof
let A,B be
set, N,M be
ManySortedSet of
[:A, B:];
assume
A1: for i, j st i
in A & j
in B holds (N
. (i,j))
= (M
. (i,j));
A2:
now
let x be
object;
assume
A3: x
in
[:A, B:];
then
reconsider A1 = A, B1 = B as non
empty
set;
consider i be
Element of A1, j be
Element of B1 such that
A4: x
=
[i, j] by
A3,
DOMAIN_1: 1;
thus (N
. x)
= (N
. (i,j)) by
A4
.= (M
. (i,j)) by
A1
.= (M
. x) by
A4;
end;
(
dom M)
=
[:A, B:] & (
dom N)
=
[:A, B:] by
PARTFUN1:def 2;
hence thesis by
A2,
FUNCT_1: 2;
end;
theorem ::
ALTCAT_1:7
Th3: for A,B be non
empty
set, N,M be
ManySortedSet of
[:A, B:] st for i be
Element of A, j be
Element of B holds (N
. (i,j))
= (M
. (i,j)) holds M
= N
proof
let A,B be non
empty
set, N,M be
ManySortedSet of
[:A, B:];
assume for i be
Element of A, j be
Element of B holds (N
. (i,j))
= (M
. (i,j));
then for i, j st i
in A & j
in B holds (N
. (i,j))
= (M
. (i,j));
hence thesis by
Th2;
end;
theorem ::
ALTCAT_1:8
Th4: for A be
set, N,M be
ManySortedSet of
[:A, A, A:] st for i, j, k st i
in A & j
in A & k
in A holds (N
. (i,j,k))
= (M
. (i,j,k)) holds M
= N
proof
let A be
set, N,M be
ManySortedSet of
[:A, A, A:];
assume
A1: for i, j, k st i
in A & j
in A & k
in A holds (N
. (i,j,k))
= (M
. (i,j,k));
A2:
now
let x be
object;
assume
A3: x
in
[:A, A, A:];
then
reconsider A as non
empty
set by
MCART_1: 31;
consider i,j,k be
Element of A such that
A4: x
=
[i, j, k] by
A3,
DOMAIN_1: 3;
thus (M
. x)
= (M
. (i,j,k)) by
A4,
MULTOP_1:def 1
.= (N
. (i,j,k)) by
A1
.= (N
. x) by
A4,
MULTOP_1:def 1;
end;
(
dom M)
=
[:A, A, A:] & (
dom N)
=
[:A, A, A:] by
PARTFUN1:def 2;
hence thesis by
A2,
FUNCT_1: 2;
end;
begin
definition
struct (
1-sorted)
AltGraph
(# the
carrier ->
set,
the
Arrows ->
ManySortedSet of
[: the carrier, the carrier:] #)
attr strict
strict;
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;
::
ALTCAT_1:def1
func
<^o1,o2^> ->
set equals (the
Arrows of G
. (o1,o2));
correctness ;
end
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;
::
ALTCAT_1:def2
attr G is
transitive means
:
Def2: for o1,o2,o3 be
Object of G st
<^o1, o2^>
<>
{} &
<^o2, o3^>
<>
{} holds
<^o1, o3^>
<>
{} ;
end
begin
definition
let I be
set;
let G be
ManySortedSet of
[:I, I:];
::
ALTCAT_1:def3
func
{|G|} ->
ManySortedSet of
[:I, I, I:] means
:
Def3: for i,j,k be
object st i
in I & j
in I & k
in I holds (it
. (i,j,k))
= (G
. (i,k));
existence
proof
deffunc
F(
object,
object,
object) = (G
. ($1,$3));
consider M be
ManySortedSet of
[:I, I, I:] such that
A1: for i,j,k be
set st i
in I & j
in I & k
in I holds (M
. (i,j,k))
=
F(i,j,k) from
MSSLambda3;
take M;
let i,j,k be
object;
thus thesis by
A1;
end;
uniqueness
proof
let M1,M2 be
ManySortedSet of
[:I, I, I:] such that
A2: for i,j,k be
object st i
in I & j
in I & k
in I holds (M1
. (i,j,k))
= (G
. (i,k)) and
A3: for i,j,k be
object st i
in I & j
in I & k
in I holds (M2
. (i,j,k))
= (G
. (i,k));
now
let i, j, k;
assume
A4: i
in I & j
in I & k
in I;
hence (M1
. (i,j,k))
= (G
. (i,k)) by
A2
.= (M2
. (i,j,k)) by
A3,
A4;
end;
hence M1
= M2 by
Th4;
end;
let H be
ManySortedSet of
[:I, I:];
::
ALTCAT_1:def4
func
{|G,H|} ->
ManySortedSet of
[:I, I, I:] means
:
Def4: for i,j,k be
object st i
in I & j
in I & k
in I holds (it
. (i,j,k))
=
[:(H
. (j,k)), (G
. (i,j)):];
existence
proof
deffunc
F(
object,
object,
object) =
[:(H
. ($2,$3)), (G
. ($1,$2)):];
consider M be
ManySortedSet of
[:I, I, I:] such that
A5: for i,j,k be
set st i
in I & j
in I & k
in I holds (M
. (i,j,k))
=
F(i,j,k) from
MSSLambda3;
take M;
let i,j,k be
object;
thus thesis by
A5;
end;
uniqueness
proof
let M1,M2 be
ManySortedSet of
[:I, I, I:] such that
A6: for i,j,k be
object st i
in I & j
in I & k
in I holds (M1
. (i,j,k))
=
[:(H
. (j,k)), (G
. (i,j)):] and
A7: for i,j,k be
object st i
in I & j
in I & k
in I holds (M2
. (i,j,k))
=
[:(H
. (j,k)), (G
. (i,j)):];
now
let i, j, k;
assume
A8: i
in I & j
in I & k
in I;
hence (M1
. (i,j,k))
=
[:(H
. (j,k)), (G
. (i,j)):] by
A6
.= (M2
. (i,j,k)) by
A7,
A8;
end;
hence M1
= M2 by
Th4;
end;
end
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
A1: (
{|G|}
.
[i, j, k])
= (
{|G|}
. (i,j,k)) by
MULTOP_1:def 1
.= (G
. (i,k)) by
Def3;
A2: (o
.
[i, j, k])
= (o
. (i,j,k)) by
MULTOP_1:def 1;
(
{|G, G|}
.
[i, j, k])
= (
{|G, G|}
. (i,j,k)) by
MULTOP_1:def 1
.=
[:(G
. (j,k)), (G
. (i,j)):] by
Def4;
hence thesis by
A2,
A1,
PBOOLE:def 15;
end;
end
definition
let I be non
empty
set;
let G be
ManySortedSet of
[:I, I:];
let IT be
BinComp of G;
::
ALTCAT_1:def5
attr IT is
associative means for i,j,k,l be
Element of I holds for f,g,h be
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));
::
ALTCAT_1:def6
attr IT is
with_right_units means for i be
Element of I holds ex e be
set st e
in (G
. (i,i)) & for j be
Element of I, f be
set st f
in (G
. (i,j)) holds ((IT
. (i,i,j))
. (f,e))
= f;
::
ALTCAT_1:def7
attr IT is
with_left_units means for j be
Element of I holds ex e be
set st e
in (G
. (j,j)) & for i be
Element of I, f be
set st f
in (G
. (i,j)) holds ((IT
. (i,j,j))
. (e,f))
= f;
end
begin
definition
struct (
AltGraph)
AltCatStr
(# the
carrier ->
set,
the
Arrows ->
ManySortedSet of
[: the carrier, the carrier:],
the
Comp ->
BinComp of the Arrows #)
attr strict
strict;
end
registration
cluster
strict non
empty for
AltCatStr;
existence
proof
set X = the non
empty
set, A = the
ManySortedSet of
[:X, X:], C = the
BinComp of A;
take
AltCatStr (# X, A, C #);
thus
AltCatStr (# X, A, C #) is
strict;
thus the
carrier of
AltCatStr (# X, A, C #) is non
empty;
end;
end
definition
let C be non
empty
AltCatStr;
let o1,o2,o3 be
Object of C;
let f be
Morphism of o1, o2, g be
Morphism of o2, o3;
::
ALTCAT_1:def8
func g
* f ->
Morphism of o1, o3 equals
:
Def8: ((the
Comp of C
. (o1,o2,o3))
. (g,f));
coherence
proof
reconsider H1 =
<^o1, o2^>, H2 =
<^o2, o3^> as non
empty
set by
A1;
reconsider F = (the
Comp of C
. (o1,o2,o3)) as
Function of
[:H2, H1:],
<^o1, o3^>;
reconsider y = g as
Element of H2;
reconsider x = f as
Element of H1;
(F
. (y,x)) is
Element of
<^o1, o3^>;
hence thesis;
end;
correctness ;
end
definition
let IT be
Function;
::
ALTCAT_1:def9
attr IT is
compositional means
:
Def9: x
in (
dom IT) implies ex f,g be
Function st x
=
[g, f] & (IT
. x)
= (g
* f);
end
registration
let A,B be
functional
set;
cluster
compositional for
ManySortedFunction of
[:A, B:];
existence
proof
per cases ;
suppose
A1: A
=
{} or B
=
{} ;
set M = (
EmptyMS
[:A, B:]);
M is
Function-yielding by
A1;
then
reconsider M as
ManySortedFunction of
[:A, B:];
take M;
let x;
thus thesis by
A1;
end;
suppose A
<>
{} & B
<>
{} ;
then
reconsider A1 = A, B1 = B as non
empty
functional
set;
deffunc
F(
Element of A1,
Element of B1) = ($1
* $2);
consider M be
ManySortedSet of
[:A1, B1:] such that
A2: for i be
Element of A1, j be
Element of B1 holds (M
. (i,j))
=
F(i,j) from
MSSLambda2D;
M is
Function-yielding
proof
let x be
object;
assume x
in (
dom M);
then
A3: x
in
[:A1, B1:];
then
A4: (x
`1 )
in A1 & (x
`2 )
in B1 by
MCART_1: 10;
then
reconsider f = (x
`1 ), g = (x
`2 ) as
Function;
(M
. x)
= (M
. (f,g)) by
A3,
MCART_1: 22
.= (f
* g) by
A2,
A4;
hence thesis;
end;
then
reconsider M as
ManySortedFunction of
[:A, B:];
take M;
let x;
assume x
in (
dom M);
then
A5: x
in
[:A1, B1:];
then
A6: (x
`1 )
in A1 & (x
`2 )
in B1 by
MCART_1: 10;
then
reconsider f = (x
`1 ), g = (x
`2 ) as
Function;
take g, f;
thus x
=
[f, g] by
A5,
MCART_1: 22;
thus (M
. x)
= (M
. (f,g)) by
A5,
MCART_1: 22
.= (f
* g) by
A2,
A6;
end;
end;
end
::$Canceled
theorem ::
ALTCAT_1:11
Th5: for A,B be
functional
set holds for F be
compositional
ManySortedSet of
[:A, B:], g,f be
Function st g
in A & f
in B holds (F
. (g,f))
= (g
* f)
proof
let A,B be
functional
set;
let F be
compositional
ManySortedSet of
[:A, B:], g,f be
Function such that
A1: g
in A & f
in B;
(
dom F)
=
[:A, B:] by
PARTFUN1:def 2;
then
[g, f]
in (
dom F) by
A1,
ZFMISC_1: 87;
then
consider ff,gg be
Function such that
A2:
[g, f]
=
[gg, ff] and
A3: (F
.
[g, f])
= (gg
* ff) by
Def9;
g
= gg by
A2,
XTUPLE_0: 1;
hence thesis by
A2,
A3,
XTUPLE_0: 1;
end;
definition
let A,B be
functional
set;
::
ALTCAT_1:def10
func
FuncComp (A,B) ->
compositional
ManySortedFunction of
[:B, A:] means
:
Def10: not contradiction;
uniqueness
proof
let M1,M2 be
compositional
ManySortedFunction of
[:B, A:];
now
let i, j;
assume i
in B & j
in A;
then
A1:
[i, j]
in
[:B, A:] by
ZFMISC_1: 87;
then
[i, j]
in (
dom M1) by
PARTFUN1:def 2;
then
consider f1,g1 be
Function such that
A2:
[i, j]
=
[g1, f1] and
A3: (M1
.
[i, j])
= (g1
* f1) by
Def9;
[i, j]
in (
dom M2) by
A1,
PARTFUN1:def 2;
then
consider f2,g2 be
Function such that
A4:
[i, j]
=
[g2, f2] and
A5: (M2
.
[i, j])
= (g2
* f2) by
Def9;
g1
= g2 by
A2,
A4,
XTUPLE_0: 1;
hence (M1
. (i,j))
= (M2
. (i,j)) by
A2,
A3,
A4,
A5,
XTUPLE_0: 1;
end;
hence M1
= M2 by
Th2;
end;
correctness ;
end
theorem ::
ALTCAT_1:12
Th6: for A,B,C be
set holds (
rng (
FuncComp ((
Funcs (A,B)),(
Funcs (B,C)))))
c= (
Funcs (A,C))
proof
let A,B,C be
set;
let i be
object;
set F = (
FuncComp ((
Funcs (A,B)),(
Funcs (B,C))));
assume i
in (
rng F);
then
consider j be
object such that
A1: j
in (
dom F) and
A2: i
= (F
. j) by
FUNCT_1:def 3;
consider f,g be
Function such that
A3: j
=
[g, f] and
A4: (F
. j)
= (g
* f) by
A1,
Def9;
g
in (
Funcs (B,C)) & f
in (
Funcs (A,B)) by
A1,
A3,
ZFMISC_1: 87;
hence thesis by
A2,
A4,
FUNCT_2: 128;
end;
theorem ::
ALTCAT_1:13
Th7: for o be
set holds (
FuncComp (
{(
id o)},
{(
id o)}))
= (((
id o),(
id o))
:-> (
id o))
proof
let o be
set;
A1: (
dom (
FuncComp (
{(
id o)},
{(
id o)})))
=
[:
{(
id o)},
{(
id o)}:] by
PARTFUN1:def 2;
(
rng (
FuncComp (
{(
id o)},
{(
id o)})))
c=
{(
id o)}
proof
let i be
object;
assume i
in (
rng (
FuncComp (
{(
id o)},
{(
id o)})));
then
consider j be
object such that
A2: j
in
[:
{(
id o)},
{(
id o)}:] and
A3: i
= ((
FuncComp (
{(
id o)},
{(
id o)}))
. j) by
A1,
FUNCT_1:def 3;
consider f,g be
Function such that
A4: j
=
[g, f] and
A5: ((
FuncComp (
{(
id o)},
{(
id o)}))
. j)
= (g
* f) by
A1,
A2,
Def9;
f
in
{(
id o)} by
A2,
A4,
ZFMISC_1: 87;
then
A6: f
= (
id o) by
TARSKI:def 1;
g
in
{(
id o)} by
A2,
A4,
ZFMISC_1: 87;
then (o
/\ o)
= o & g
= (
id o) by
TARSKI:def 1;
then i
= (
id o) by
A3,
A5,
A6,
FUNCT_1: 22;
hence thesis by
TARSKI:def 1;
end;
then (
FuncComp (
{(
id o)},
{(
id o)})) is
Function of
[:
{(
id o)},
{(
id o)}:],
{(
id o)} by
A1,
RELSET_1: 4;
hence thesis by
FUNCOP_1:def 10;
end;
theorem ::
ALTCAT_1:14
Th8: for A,B be
functional
set, A1 be
Subset of A, B1 be
Subset of B holds (
FuncComp (A1,B1))
= ((
FuncComp (A,B))
|
[:B1, A1:] qua
set)
proof
let A,B be
functional
set, A1 be
Subset of A, B1 be
Subset of B;
set f = ((
FuncComp (A,B))
|
[:B1, A1:] qua
set);
A1: (
dom (
FuncComp (A,B)))
=
[:B, A:] by
PARTFUN1:def 2;
then
A2: (
dom f)
=
[:B1, A1:] by
RELAT_1: 62;
then
reconsider f as
ManySortedFunction of
[:B1, A1:] by
PARTFUN1:def 2;
f is
compositional
proof
let i;
assume
A3: i
in (
dom f);
then (f
. i)
= ((
FuncComp (A,B))
. i) by
FUNCT_1: 49;
hence thesis by
A1,
A2,
A3,
Def9;
end;
hence thesis by
Def10;
end;
definition
let C be non
empty
AltCatStr;
::
ALTCAT_1:def11
attr C is
quasi-functional means for a1,a2 be
Object of C holds
<^a1, a2^>
c= (
Funcs (a1,a2));
::
ALTCAT_1:def12
attr C is
semi-functional means for a1,a2,a3 be
Object of C st
<^a1, a2^>
<>
{} &
<^a2, a3^>
<>
{} &
<^a1, a3^>
<>
{} holds for f be
Morphism of a1, a2, g be
Morphism of a2, a3, f9,g9 be
Function st f
= f9 & g
= g9 holds (g
* f)
= (g9
* f9);
::
ALTCAT_1:def13
attr C is
pseudo-functional means
:
Def13: for o1,o2,o3 be
Object of C holds (the
Comp of C
. (o1,o2,o3))
= ((
FuncComp ((
Funcs (o1,o2)),(
Funcs (o2,o3))))
|
[:
<^o2, o3^>,
<^o1, o2^>:] qua
set);
end
registration
let X be non
empty
set, A be
ManySortedSet of
[:X, X:], C be
BinComp of A;
cluster
AltCatStr (# X, A, C #) -> non
empty;
coherence ;
end
registration
cluster
strict
pseudo-functional for non
empty
AltCatStr;
existence
proof
A1:
{
[
0 ,
0 ,
0 ]}
=
[:
{
0 },
{
0 },
{
0 }:] by
MCART_1: 35;
then
reconsider c = (
[
0 ,
0 ,
0 ]
.--> (
FuncComp ((
Funcs (
0 ,
0 )),(
Funcs (
0 ,
0 ))))) as
ManySortedSet of
[:
{
0 },
{
0 },
{
0 }:];
reconsider c as
ManySortedFunction of
[:
{
0 },
{
0 },
{
0 }:];
(
dom (
[
0 ,
0 ]
.--> (
Funcs (
0 ,
0 ))))
=
{
[
0 ,
0 ]}
.=
[:
{
0 },
{
0 }:] by
ZFMISC_1: 29;
then
reconsider m = (
[
0 ,
0 ]
.--> (
Funcs (
0 ,
0 ))) as
ManySortedSet of
[:
{
0 },
{
0 }:];
A2: (m
. (
0 ,
0 ))
= (
Funcs (
0 ,
0 )) by
FUNCOP_1: 72;
A3:
0
in
{
0 } by
TARSKI:def 1;
now
let i;
reconsider ci = (c
. i) as
Function;
assume i
in
[:
{
0 },
{
0 },
{
0 }:];
then
A4: i
=
[
0 ,
0 ,
0 ] by
A1,
TARSKI:def 1;
then
A5: (c
. i)
= (
FuncComp ((
Funcs (
0 ,
0 )),(
Funcs (
0 ,
0 )))) by
FUNCOP_1: 72;
then
A6: (
dom ci)
=
[:(m
. (
0 ,
0 )), (m
. (
0 ,
0 )):] by
A2,
PARTFUN1:def 2
.= (
{|m, m|}
. (
0 ,
0 ,
0 )) by
A3,
Def4
.= (
{|m, m|}
. i) by
A4,
MULTOP_1:def 1;
A7: (
{|m|}
. i)
= (
{|m|}
. (
0 ,
0 ,
0 )) by
A4,
MULTOP_1:def 1
.= (m
. (
0 ,
0 )) by
A3,
Def3;
then (
rng ci)
c= (
{|m|}
. i) by
A2,
A5,
Th6;
hence (c
. i) is
Function of (
{|m, m|}
. i), (
{|m|}
. i) by
A2,
A6,
A7,
FUNCT_2:def 1,
RELSET_1: 4;
end;
then
reconsider c as
BinComp of m by
PBOOLE:def 15;
take C =
AltCatStr (#
{
0 }, m, c #);
thus C is
strict;
let o1,o2,o3 be
Object of C;
A8: o3
=
0 by
TARSKI:def 1;
A9: o1
=
0 & o2
=
0 by
TARSKI:def 1;
then
A10: (
dom (
FuncComp ((
Funcs (
0 ,
0 )),(
Funcs (
0 ,
0 )))))
=
[:
<^o2, o3^>,
<^o1, o2^>:] by
A2,
A8,
PARTFUN1:def 2;
thus (the
Comp of C
. (o1,o2,o3))
= (c
.
[o1, o2, o3]) by
MULTOP_1:def 1
.= (
FuncComp ((
Funcs (
0 ,
0 )),(
Funcs (
0 ,
0 )))) by
A9,
A8,
FUNCOP_1: 72
.= ((
FuncComp ((
Funcs (o1,o2)),(
Funcs (o2,o3))))
|
[:
<^o2, o3^>,
<^o1, o2^>:] qua
set) by
A9,
A8,
A10;
end;
end
theorem ::
ALTCAT_1:15
for C be non
empty
AltCatStr, a1,a2,a3 be
Object of C holds (the
Comp of C
. (a1,a2,a3)) is
Function of
[:
<^a2, a3^>,
<^a1, a2^>:],
<^a1, a3^>;
theorem ::
ALTCAT_1:16
Th10: for C be
pseudo-functional non
empty
AltCatStr holds for a1,a2,a3 be
Object of C st
<^a1, a2^>
<>
{} &
<^a2, a3^>
<>
{} &
<^a1, a3^>
<>
{} holds for f be
Morphism of a1, a2, g be
Morphism of a2, a3, f9,g9 be
Function st f
= f9 & g
= g9 holds (g
* f)
= (g9
* f9)
proof
let C be
pseudo-functional non
empty
AltCatStr;
let a1,a2,a3 be
Object of C such that
A1:
<^a1, a2^>
<>
{} &
<^a2, a3^>
<>
{} and
A2:
<^a1, a3^>
<>
{} ;
let f be
Morphism of a1, a2, g be
Morphism of a2, a3, f9,g9 be
Function such that
A3: f
= f9 & g
= g9;
A4:
[g, f]
in
[:
<^a2, a3^>,
<^a1, a2^>:] by
A1,
ZFMISC_1: 87;
A5: (the
Comp of C
. (a1,a2,a3))
= ((
FuncComp ((
Funcs (a1,a2)),(
Funcs (a2,a3))))
|
[:
<^a2, a3^>,
<^a1, a2^>:] qua
set) by
Def13;
(
dom ((
FuncComp ((
Funcs (a1,a2)),(
Funcs (a2,a3))))
|
[:
<^a2, a3^>,
<^a1, a2^>:] qua
set))
c= (
dom (
FuncComp ((
Funcs (a1,a2)),(
Funcs (a2,a3))))) & (
dom (the
Comp of C
. (a1,a2,a3)))
=
[:
<^a2, a3^>,
<^a1, a2^>:] by
A2,
FUNCT_2:def 1,
RELAT_1: 60;
then
consider f99,g99 be
Function such that
A6:
[g, f]
=
[g99, f99] and
A7: ((
FuncComp ((
Funcs (a1,a2)),(
Funcs (a2,a3))))
.
[g, f])
= (g99
* f99) by
A5,
A4,
Def9;
A8: g
= g99 & f
= f99 by
A6,
XTUPLE_0: 1;
thus (g
* f)
= ((the
Comp of C
. (a1,a2,a3))
. (g,f)) by
A1,
Def8
.= (g9
* f9) by
A5,
A3,
A4,
A7,
A8,
FUNCT_1: 49;
end;
definition
let A be non
empty
set;
::
ALTCAT_1:def14
func
EnsCat A ->
strict
pseudo-functional non
empty
AltCatStr means
:
Def14: the
carrier of it
= A & for a1,a2 be
Object of it holds
<^a1, a2^>
= (
Funcs (a1,a2));
existence
proof
deffunc
F(
set,
set,
set) = (
FuncComp ((
Funcs ($1,$2)),(
Funcs ($2,$3))));
consider M be
ManySortedSet of
[:A, A:] such that
A1: for i,j be
set st i
in A & j
in A holds (M
. (i,j))
= (
Funcs (i,j)) from
MSSLambda2;
consider c be
ManySortedSet of
[:A, A, A:] such that
A2: for i,j,k be
set st i
in A & j
in A & k
in A holds (c
. (i,j,k))
=
F(i,j,k) from
MSSLambda3;
c is
Function-yielding
proof
let i be
object;
assume i
in (
dom c);
then i
in
[:A, A, A:];
then
consider x1,x2,x3 be
object such that
A3: x1
in A & x2
in A & x3
in A and
A4: i
=
[x1, x2, x3] by
MCART_1: 68;
reconsider x1, x2, x3 as
set by
TARSKI: 1;
(c
. i)
= (c
. (x1,x2,x3)) by
A4,
MULTOP_1:def 1
.= (
FuncComp ((
Funcs (x1,x2)),(
Funcs (x2,x3)))) by
A2,
A3;
hence thesis;
end;
then
reconsider c as
ManySortedFunction of
[:A, A, A:];
now
let i;
reconsider ci = (c
. i) as
Function;
assume i
in
[:A, A, A:];
then
consider x1,x2,x3 be
object such that
A5: x1
in A and
A6: x2
in A and
A7: x3
in A and
A8: i
=
[x1, x2, x3] by
MCART_1: 68;
A9: (
{|M|}
. i)
= (
{|M|}
. (x1,x2,x3)) by
A8,
MULTOP_1:def 1
.= (M
. (x1,x3)) by
A5,
A6,
A7,
Def3;
reconsider x1, x2, x3 as
set by
TARSKI: 1;
A10: (c
. i)
= (c
. (x1,x2,x3)) by
A8,
MULTOP_1:def 1
.= (
FuncComp ((
Funcs (x1,x2)),(
Funcs (x2,x3)))) by
A2,
A5,
A6,
A7;
(M
. (x1,x2))
= (
Funcs (x1,x2)) & (M
. (x2,x3))
= (
Funcs (x2,x3)) by
A1,
A5,
A6,
A7;
then
A11:
[:(
Funcs (x2,x3)), (
Funcs (x1,x2)):]
= (
{|M, M|}
. (x1,x2,x3)) by
A5,
A6,
A7,
Def4
.= (
{|M, M|}
. i) by
A8,
MULTOP_1:def 1;
(M
. (x1,x3))
= (
Funcs (x1,x3)) by
A1,
A5,
A7;
then
A12: (
rng ci)
c= (
{|M|}
. i) by
A10,
A9,
Th6;
(
dom ci)
=
[:(
Funcs (x2,x3)), (
Funcs (x1,x2)):] by
A10,
PARTFUN1:def 2;
hence (c
. i) is
Function of (
{|M, M|}
. i), (
{|M|}
. i) by
A11,
A12,
FUNCT_2: 2;
end;
then
reconsider c as
BinComp of M by
PBOOLE:def 15;
set C =
AltCatStr (# A, M, c #);
C is
pseudo-functional
proof
let o1,o2,o3 be
Object of C;
<^o1, o2^>
= (
Funcs (o1,o2)) &
<^o2, o3^>
= (
Funcs (o2,o3)) by
A1;
then
A13: (
dom (
FuncComp ((
Funcs (o1,o2)),(
Funcs (o2,o3)))))
=
[:
<^o2, o3^>,
<^o1, o2^>:] by
PARTFUN1:def 2;
thus (the
Comp of C
. (o1,o2,o3))
= (
FuncComp ((
Funcs (o1,o2)),(
Funcs (o2,o3)))) by
A2
.= ((
FuncComp ((
Funcs (o1,o2)),(
Funcs (o2,o3))))
|
[:
<^o2, o3^>,
<^o1, o2^>:] qua
set) by
A13;
end;
then
reconsider C as
strict
pseudo-functional non
empty
AltCatStr;
take C;
thus the
carrier of C
= A;
let a1,a2 be
Object of C;
thus thesis by
A1;
end;
uniqueness
proof
let C1,C2 be
strict
pseudo-functional non
empty
AltCatStr such that
A14: the
carrier of C1
= A and
A15: for a1,a2 be
Object of C1 holds
<^a1, a2^>
= (
Funcs (a1,a2)) and
A16: the
carrier of C2
= A and
A17: for a1,a2 be
Object of C2 holds
<^a1, a2^>
= (
Funcs (a1,a2));
A18:
now
let i, j;
assume
A19: i
in A & j
in A;
then
reconsider a1 = i, a2 = j as
Object of C1 by
A14;
reconsider b1 = i, b2 = j as
Object of C2 by
A16,
A19;
thus (the
Arrows of C1
. (i,j))
=
<^a1, a2^>
.= (
Funcs (a1,a2)) by
A15
.=
<^b1, b2^> by
A17
.= (the
Arrows of C2
. (i,j));
end;
A20:
now
let i, j, k;
assume
A21: i
in A & j
in A & k
in A;
then
reconsider a1 = i, a2 = j, a3 = k as
Object of C1 by
A14;
reconsider b1 = i, b2 = j, b3 = k as
Object of C2 by
A16,
A21;
<^a2, a3^>
=
<^b2, b3^> &
<^a1, a2^>
=
<^b1, b2^> by
A14,
A18;
hence (the
Comp of C1
. (i,j,k))
= ((
FuncComp ((
Funcs (b1,b2)),(
Funcs (b2,b3))))
|
[:
<^b2, b3^>,
<^b1, b2^>:] qua
set) by
Def13
.= (the
Comp of C2
. (i,j,k)) by
Def13;
end;
the
Arrows of C1
= the
Arrows of C2 by
A14,
A16,
A18,
Th2;
hence thesis by
A14,
A16,
A20,
Th4;
end;
end
definition
let C be non
empty
AltCatStr;
::
ALTCAT_1:def15
attr C is
associative means
:
Def15: the
Comp of C is
associative;
::
ALTCAT_1:def16
attr C is
with_units means
:
Def16: the
Comp of C is
with_left_units
with_right_units;
end
Lm1: for A be non
empty
set holds (
EnsCat A) is
transitive
associative
with_units
proof
let A be non
empty
set;
set G = the
Arrows of (
EnsCat A), C = the
Comp of (
EnsCat A);
thus
A1: (
EnsCat A) is
transitive
proof
let o1,o2,o3 be
Object of (
EnsCat A);
assume
<^o1, o2^>
<>
{} &
<^o2, o3^>
<>
{} ;
then (
Funcs (o1,o2))
<>
{} & (
Funcs (o2,o3))
<>
{} by
Def14;
then (
Funcs (o1,o3))
<>
{} by
FUNCT_2: 129;
hence thesis by
Def14;
end;
thus (
EnsCat A) is
associative
proof
let i,j,k,l be
Element of (
EnsCat A);
reconsider i9 = i, j9 = j, k9 = k, l9 = l as
Object of (
EnsCat A);
let f,g,h be
set such that
A2: f
in (G
. (i,j)) and
A3: g
in (G
. (j,k)) and
A4: h
in (G
. (k,l));
reconsider h99 = h as
Morphism of k9, l9 by
A4;
reconsider g99 = g as
Morphism of j9, k9 by
A3;
A5:
<^k9, l9^>
= (
Funcs (k,l)) by
Def14;
<^i9, j9^>
= (
Funcs (i,j)) &
<^j9, k9^>
= (
Funcs (j,k)) by
Def14;
then
reconsider f9 = f, g9 = g, h9 = h as
Function by
A2,
A3,
A4,
A5;
A6: (G
. (k,l))
=
<^k9, l9^>;
A7:
<^j9, k9^>
<>
{} by
A3;
then
A8:
<^j9, l9^>
<>
{} by
A1,
A4,
A6;
then
A9: (h99
* g99)
= (h9
* g9) by
A3,
A4,
Th10;
reconsider f99 = f as
Morphism of i9, j9 by
A2;
(G
. (i,j))
=
<^i9, j9^>;
then
A10:
<^i9, k9^>
<>
{} by
A1,
A2,
A7;
then
A11: (g99
* f99)
= (g9
* f9) by
A2,
A3,
Th10;
A12:
<^i9, l9^>
<>
{} by
A1,
A4,
A6,
A10;
A13: ((C
. (j,k,l))
. (h,g))
= (h99
* g99) by
A3,
A4,
Def8;
((C
. (i,j,k))
. (g,f))
= (g99
* f99) by
A2,
A3,
Def8;
hence ((C
. (i,k,l))
. (h,((C
. (i,j,k))
. (g,f))))
= (h99
* (g99
* f99)) by
A4,
A10,
Def8
.= (h9
* (g9
* f9)) by
A4,
A10,
A12,
A11,
Th10
.= ((h9
* g9)
* f9) by
RELAT_1: 36
.= ((h99
* g99)
* f99) by
A2,
A8,
A12,
A9,
Th10
.= ((C
. (i,j,l))
. (((C
. (j,k,l))
. (h,g)),f)) by
A2,
A8,
A13,
Def8;
end;
thus the
Comp of (
EnsCat A) is
with_left_units
proof
let i be
Element of (
EnsCat A);
reconsider i9 = i as
Object of (
EnsCat A);
take (
id i);
A14:
<^i9, i9^>
= (
Funcs (i,i)) by
Def14;
hence (
id i)
in (G
. (i,i)) by
FUNCT_2: 126;
reconsider I = (
id i) as
Morphism of i9, i9 by
A14,
FUNCT_2: 126;
let j be
Element of (
EnsCat A), f be
set;
reconsider j9 = j as
Object of (
EnsCat A);
assume
A15: f
in (G
. (j,i));
then
reconsider f99 = f as
Morphism of j9, i9;
<^j9, i9^>
= (
Funcs (j,i)) by
Def14;
then
reconsider f9 = f as
Function of j, i by
A15,
FUNCT_2: 66;
thus ((C
. (j,i,i))
. ((
id i),f))
= (I
* f99) by
A14,
A15,
Def8
.= ((
id i)
* f9) by
A14,
A15,
Th10
.= f by
FUNCT_2: 17;
end;
let i be
Element of (
EnsCat A);
reconsider i9 = i as
Object of (
EnsCat A);
take (
id i);
A16:
<^i9, i9^>
= (
Funcs (i,i)) by
Def14;
hence (
id i)
in (G
. (i,i)) by
FUNCT_2: 126;
reconsider I = (
id i) as
Morphism of i9, i9 by
A16,
FUNCT_2: 126;
let j be
Element of (
EnsCat A), f be
set;
reconsider j9 = j as
Object of (
EnsCat A);
assume
A17: f
in (G
. (i,j));
then
reconsider f99 = f as
Morphism of i9, j9;
<^i9, j9^>
= (
Funcs (i,j)) by
Def14;
then
reconsider f9 = f as
Function of i, j by
A17,
FUNCT_2: 66;
thus ((C
. (i,i,j))
. (f,(
id i)))
= (f99
* I) by
A16,
A17,
Def8
.= (f9
* (
id i)) by
A16,
A17,
Th10
.= f by
FUNCT_2: 17;
end;
registration
cluster
transitive
associative
with_units
strict for non
empty
AltCatStr;
existence
proof
take (
EnsCat
{
{} });
thus thesis by
Lm1;
end;
end
theorem ::
ALTCAT_1:17
for C be
transitive non
empty
AltCatStr, a1,a2,a3 be
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
let C be
transitive non
empty
AltCatStr, a1,a2,a3 be
Object of C;
<^a1, a3^>
=
{} implies
<^a1, a2^>
=
{} or
<^a2, a3^>
=
{} by
Def2;
then
<^a1, a3^>
=
{} implies
[:
<^a2, a3^>,
<^a1, a2^>:]
=
{} ;
hence thesis by
FUNCT_2:def 1,
RELAT_1:def 19;
end;
theorem ::
ALTCAT_1:18
Th12: for C be
with_units non
empty
AltCatStr holds for o be
Object of C holds
<^o, o^>
<>
{}
proof
let C be
with_units non
empty
AltCatStr;
let o be
Object of C;
the
Comp of C is
with_left_units by
Def16;
then ex e be
set st e
in (the
Arrows of C
. (o,o)) & for o9 be
Element of C, f be
set st f
in (the
Arrows of C
. (o9,o)) holds ((the
Comp of C
. (o9,o,o))
. (e,f))
= f;
hence thesis;
end;
registration
let A be non
empty
set;
cluster (
EnsCat A) ->
transitive
associative
with_units;
coherence by
Lm1;
end
registration
cluster
quasi-functional
semi-functional
transitive ->
pseudo-functional for non
empty
AltCatStr;
coherence
proof
let C be non
empty
AltCatStr;
assume
A1: C is
quasi-functional
semi-functional
transitive;
let o1,o2,o3 be
Object of C;
set c = (the
Comp of C
. (o1,o2,o3)), f = ((
FuncComp ((
Funcs (o1,o2)),(
Funcs (o2,o3))))
|
[:
<^o2, o3^>,
<^o1, o2^>:] qua
set);
per cases ;
suppose
A2:
<^o2, o3^>
=
{} or
<^o1, o2^>
=
{} ;
hence c
=
{}
.= f by
A2;
end;
suppose
A3:
<^o2, o3^>
<>
{} &
<^o1, o2^>
<>
{} ;
then
A4:
<^o1, o3^>
<>
{} by
A1;
then
A5: (
dom c)
=
[:
<^o2, o3^>,
<^o1, o2^>:] by
FUNCT_2:def 1;
A6:
<^o2, o3^>
c= (
Funcs (o2,o3)) &
<^o1, o2^>
c= (
Funcs (o1,o2)) by
A1;
(
dom (
FuncComp ((
Funcs (o1,o2)),(
Funcs (o2,o3)))))
=
[:(
Funcs (o2,o3)), (
Funcs (o1,o2)):] by
PARTFUN1:def 2;
then (
dom f)
= (
[:(
Funcs (o2,o3)), (
Funcs (o1,o2)):]
/\
[:
<^o2, o3^>,
<^o1, o2^>:]) by
RELAT_1: 61;
then
A7: (
dom c)
= (
dom f) by
A6,
A5,
XBOOLE_1: 28,
ZFMISC_1: 96;
now
let i be
object;
assume
A8: i
in (
dom c);
then
consider i1,i2 be
object such that
A9: i1
in
<^o2, o3^> and
A10: i2
in
<^o1, o2^> and
A11: i
=
[i1, i2] by
ZFMISC_1: 84;
reconsider a2 = i2 as
Morphism of o1, o2 by
A10;
reconsider a1 = i1 as
Morphism of o2, o3 by
A9;
reconsider g = i1, h = i2 as
Function by
A6,
A9,
A10;
thus (c
. i)
= ((the
Comp of C
. (o1,o2,o3))
. (a1,a2)) by
A11
.= (a1
* a2) by
A3,
Def8
.= (g
* h) by
A1,
A3,
A4
.= ((
FuncComp ((
Funcs (o1,o2)),(
Funcs (o2,o3))))
. (g,h)) by
A6,
A9,
A10,
Th5
.= (f
. i) by
A7,
A8,
A11,
FUNCT_1: 47;
end;
hence thesis by
A7,
FUNCT_1: 2;
end;
end;
cluster
with_units
pseudo-functional
transitive ->
quasi-functional
semi-functional for non
empty
AltCatStr;
coherence
proof
let C be non
empty
AltCatStr such that
A12: C is
with_units
pseudo-functional
transitive;
thus C is
quasi-functional
proof
let a1,a2 be
Object of C;
per cases ;
suppose
<^a1, a2^>
=
{} ;
hence thesis;
end;
suppose
A13:
<^a1, a2^>
<>
{} ;
set c = (the
Comp of C
. (a1,a1,a2)), f = (
FuncComp ((
Funcs (a1,a1)),(
Funcs (a1,a2))));
A14: (
dom c)
=
[:
<^a1, a2^>,
<^a1, a1^>:] by
A13,
FUNCT_2:def 1;
(
dom f)
=
[:(
Funcs (a1,a2)), (
Funcs (a1,a1)):] & c
= (f
|
[:
<^a1, a2^>,
<^a1, a1^>:] qua
set) by
A12,
PARTFUN1:def 2;
then
A15:
[:
<^a1, a2^>,
<^a1, a1^>:]
c=
[:(
Funcs (a1,a2)), (
Funcs (a1,a1)):] by
A14,
RELAT_1: 60;
<^a1, a1^>
<>
{} by
A12,
Th12;
hence thesis by
A15,
ZFMISC_1: 114;
end;
end;
let a1,a2,a3 be
Object of C;
thus thesis by
A12,
Th10;
end;
end
definition
mode
category is
transitive
associative
with_units non
empty
AltCatStr;
end
begin
definition
let C be
with_units non
empty
AltCatStr;
let o be
Object of C;
::
ALTCAT_1:def17
func
idm o ->
Morphism of o, o means
:
Def17: for o9 be
Object of C st
<^o, o9^>
<>
{} holds for a be
Morphism of o, o9 holds (a
* it )
= a;
existence
proof
the
Comp of C is
with_right_units by
Def16;
then
consider e be
set such that
A1: e
in (the
Arrows of C
. (o,o)) and
A2: for o9 be
Element of C, f be
set st f
in (the
Arrows of C
. (o,o9)) holds ((the
Comp of C
. (o,o,o9))
. (f,e))
= f;
reconsider e as
Morphism of o, o by
A1;
take e;
let o9 be
Object of C such that
A3:
<^o, o9^>
<>
{} ;
let a be
Morphism of o, o9;
thus (a
* e)
= ((the
Comp of C
. (o,o,o9))
. (a,e)) by
A1,
A3,
Def8
.= a by
A2,
A3;
end;
uniqueness
proof
the
Comp of C is
with_left_units by
Def16;
then
consider d be
set such that
A4: d
in (the
Arrows of C
. (o,o)) and
A5: for o9 be
Element of C, f be
set st f
in (the
Arrows of C
. (o9,o)) holds ((the
Comp of C
. (o9,o,o))
. (d,f))
= f;
reconsider d as
Morphism of o, o by
A4;
let a1,a2 be
Morphism of o, o such that
A6: for o9 be
Object of C st
<^o, o9^>
<>
{} holds for a be
Morphism of o, o9 holds (a
* a1)
= a and
A7: for o9 be
Object of C st
<^o, o9^>
<>
{} holds for a be
Morphism of o, o9 holds (a
* a2)
= a;
A8:
<^o, o^>
<>
{} by
Th12;
hence a1
= ((the
Comp of C
. (o,o,o))
. (d,a1)) by
A5
.= (d
* a1) by
A8,
Def8
.= d by
A6,
Th12
.= (d
* a2) by
A7,
Th12
.= ((the
Comp of C
. (o,o,o))
. (d,a2)) by
A8,
Def8
.= a2 by
A5,
A8;
end;
end
theorem ::
ALTCAT_1:19
Th13: for C be
with_units non
empty
AltCatStr holds for o be
Object of C holds (
idm o)
in
<^o, o^>
proof
let C be
with_units non
empty
AltCatStr;
let o be
Object of C;
<^o, o^>
<>
{} by
Th12;
hence thesis;
end;
theorem ::
ALTCAT_1:20
for C be
with_units non
empty
AltCatStr holds for o1,o2 be
Object of C st
<^o1, o2^>
<>
{} holds for a be
Morphism of o1, o2 holds ((
idm o2)
* a)
= a
proof
let C be
with_units non
empty
AltCatStr;
let o1,o2 be
Object of C such that
A1:
<^o1, o2^>
<>
{} ;
let a be
Morphism of o1, o2;
the
Comp of C is
with_left_units by
Def16;
then
consider d be
set such that
A2: d
in (the
Arrows of C
. (o2,o2)) and
A3: for o9 be
Element of C, f be
set st f
in (the
Arrows of C
. (o9,o2)) holds ((the
Comp of C
. (o9,o2,o2))
. (d,f))
= f;
reconsider d as
Morphism of o2, o2 by
A2;
(
idm o2)
in
<^o2, o2^> by
Th13;
then d
= (d
* (
idm o2)) by
Def17
.= ((the
Comp of C
. (o2,o2,o2))
. (d,(
idm o2))) by
A2,
Def8
.= (
idm o2) by
A3,
Th13;
hence ((
idm o2)
* a)
= ((the
Comp of C
. (o1,o2,o2))
. (d,a)) by
A1,
A2,
Def8
.= a by
A1,
A3;
end;
theorem ::
ALTCAT_1:21
for C be
associative
transitive non
empty
AltCatStr holds for o1,o2,o3,o4 be
Object of C st
<^o1, o2^>
<>
{} &
<^o2, o3^>
<>
{} &
<^o3, o4^>
<>
{} holds for a be
Morphism of o1, o2, b be
Morphism of o2, o3, c be
Morphism of o3, o4 holds (c
* (b
* a))
= ((c
* b)
* a)
proof
let C be
associative
transitive non
empty
AltCatStr;
let o1,o2,o3,o4 be
Object of C such that
A1:
<^o1, o2^>
<>
{} and
A2:
<^o2, o3^>
<>
{} and
A3:
<^o3, o4^>
<>
{} ;
let a be
Morphism of o1, o2, b be
Morphism of o2, o3, c be
Morphism of o3, o4;
A4:
<^o2, o4^>
<>
{} & (c
* b)
= ((the
Comp of C
. (o2,o3,o4))
. (c,b)) by
A2,
A3,
Def2,
Def8;
A5: the
Comp of C is
associative by
Def15;
<^o1, o3^>
<>
{} & (b
* a)
= ((the
Comp of C
. (o1,o2,o3))
. (b,a)) by
A1,
A2,
Def2,
Def8;
hence (c
* (b
* a))
= ((the
Comp of C
. (o1,o3,o4))
. (c,((the
Comp of C
. (o1,o2,o3))
. (b,a)))) by
A3,
Def8
.= ((the
Comp of C
. (o1,o2,o4))
. (((the
Comp of C
. (o2,o3,o4))
. (c,b)),a)) by
A1,
A2,
A3,
A5
.= ((c
* b)
* a) by
A1,
A4,
Def8;
end;
begin
definition
let C be
AltCatStr;
::
ALTCAT_1:def18
attr C is
quasi-discrete means
:
Def18: for i,j be
Object of C st
<^i, j^>
<>
{} holds i
= j;
::
ALTCAT_1:def19
attr C is
pseudo-discrete means for i be
Object of C holds
<^i, i^> is
trivial;
end
theorem ::
ALTCAT_1:22
for C be
with_units non
empty
AltCatStr holds C is
pseudo-discrete iff for o be
Object of C holds
<^o, o^>
=
{(
idm o)}
proof
let C be
with_units non
empty
AltCatStr;
hereby
assume
A1: C is
pseudo-discrete;
let o be
Object of C;
now
let j be
object;
hereby
(
idm o)
in
<^o, o^> &
<^o, o^> is
trivial by
A1,
Th13;
then
consider i be
object such that
A2:
<^o, o^>
=
{i} by
ZFMISC_1: 131;
assume j
in
<^o, o^>;
then j
= i by
A2,
TARSKI:def 1;
hence j
= (
idm o) by
A2,
TARSKI:def 1;
end;
thus j
= (
idm o) implies j
in
<^o, o^> by
Th13;
end;
hence
<^o, o^>
=
{(
idm o)} by
TARSKI:def 1;
end;
assume
A3: for o be
Object of C holds
<^o, o^>
=
{(
idm o)};
let o be
Object of C;
<^o, o^>
=
{(
idm o)} by
A3;
hence thesis;
end;
registration
cluster 1
-element ->
quasi-discrete for
AltCatStr;
coherence by
STRUCT_0:def 10;
end
theorem ::
ALTCAT_1:23
Th17: (
EnsCat
{
0 }) is
pseudo-discrete1
-element
proof
A1: the
carrier of (
EnsCat
{
0 })
=
{
0 } by
Def14;
hereby
let i be
Object of (
EnsCat
{
0 });
i
=
0 by
A1,
TARSKI:def 1;
hence
<^i, i^> is
trivial by
Def14,
FUNCT_2: 127;
end;
thus the
carrier of (
EnsCat
{
0 }) is 1
-element by
A1;
end;
registration
cluster
pseudo-discrete
trivial
strict for
category;
existence by
Th17;
end
registration
cluster
quasi-discrete
pseudo-discrete
trivial
strict for
category;
existence by
Th17;
end
definition
mode
discrete_category is
quasi-discrete
pseudo-discrete
category;
end
definition
let A be non
empty
set;
::
ALTCAT_1:def20
func
DiscrCat A ->
quasi-discrete
strict non
empty
AltCatStr means
:
Def20: the
carrier of it
= A & for i be
Object of it holds
<^i, i^>
=
{(
id i)};
existence
proof
deffunc
F(
Element of A,
set,
set) = (
IFEQ ($1,$2,(
IFEQ ($2,$3,(
[(
id $1), (
id $1)]
.--> (
id $1)),
{} )),
{} ));
deffunc
F(
Element of A,
set) = (
IFEQ ($1,$2,
{(
id $1)},
{} ));
consider M be
ManySortedSet of
[:A, A:] such that
A1: for i,j be
Element of A holds (M
. (i,j))
=
F(i,j) from
MSSLambda2D;
consider c be
ManySortedSet of
[:A, A, A:] such that
A2: for i,j,k be
Element of A holds (c
. (i,j,k))
=
F(i,j,k) from
MSSLambda3D;
A3:
now
let i;
assume i
in
[:A, A, A:];
then
consider i1,i2,i3 be
object such that
A4: i1
in A & i2
in A & i3
in A and
A5: i
=
[i1, i2, i3] by
MCART_1: 68;
reconsider i1, i2, i3 as
Element of A by
A4;
per cases ;
suppose that
A6: i1
= i2 and
A7: i2
= i3;
A8: (M
. (i1,i1))
= (
IFEQ (i1,i1,
{(
id i1)},
{} )) by
A1
.=
{(
id i1)} by
FUNCOP_1:def 8;
A9: (c
. i)
= (c
. (i1,i2,i3)) by
A5,
MULTOP_1:def 1
.= (
IFEQ (i1,i2,(
IFEQ (i2,i3,(
[(
id i1), (
id i1)]
.--> (
id i1)),
{} )),
{} )) by
A2
.= (
IFEQ (i2,i3,(
[(
id i1), (
id i1)]
.--> (
id i1)),
{} )) by
A6,
FUNCOP_1:def 8
.= (
[(
id i1), (
id i1)]
.--> (
id i1)) by
A7,
FUNCOP_1:def 8;
A10: (
{|M|}
. i)
= (
{|M|}
. (i1,i1,i1)) by
A5,
A6,
A7,
MULTOP_1:def 1
.=
{(
id i1)} by
A8,
Def3;
A11: (
{|M, M|}
. i)
= (
{|M, M|}
. (i1,i1,i1)) by
A5,
A6,
A7,
MULTOP_1:def 1
.=
[:
{(
id i1)},
{(
id i1)}:] by
A8,
Def4
.=
{
[(
id i1), (
id i1)]} by
ZFMISC_1: 29
.= (
dom (
[(
id i1), (
id i1)]
.--> (
id i1)));
thus (c
. i) is
Function of (
{|M, M|}
. i), (
{|M|}
. i) by
A9,
A10,
A11;
end;
suppose
A12: i1
<> i2 or i2
<> i3;
A13:
now
per cases by
A12;
suppose
A14: i1
<> i2;
thus (c
. i)
= (c
. (i1,i2,i3)) by
A5,
MULTOP_1:def 1
.= (
IFEQ (i1,i2,(
IFEQ (i2,i3,(
[(
id i1), (
id i1)]
.--> (
id i1)),
{} )),
{} )) by
A2
.=
{} by
A14,
FUNCOP_1:def 8;
end;
suppose that
A15: i1
= i2 and
A16: i2
<> i3;
thus (c
. i)
= (c
. (i1,i2,i3)) by
A5,
MULTOP_1:def 1
.= (
IFEQ (i1,i2,(
IFEQ (i2,i3,(
[(
id i1), (
id i1)]
.--> (
id i1)),
{} )),
{} )) by
A2
.= (
IFEQ (i2,i3,(
[(
id i1), (
id i1)]
.--> (
id i1)),
{} )) by
A15,
FUNCOP_1:def 8
.=
{} by
A16,
FUNCOP_1:def 8;
end;
end;
(M
. (i1,i2))
= (
IFEQ (i1,i2,
{(
id i1)},
{} )) & (M
. (i2,i3))
= (
IFEQ (i2,i3,
{(
id i2)},
{} )) by
A1;
then
A17: (M
. (i1,i2))
=
{} or (M
. (i2,i3))
=
{} by
A12,
FUNCOP_1:def 8;
(
{|M, M|}
. i)
= (
{|M, M|}
. (i1,i2,i3)) by
A5,
MULTOP_1:def 1
.=
[:(M
. (i2,i3)), (M
. (i1,i2)):] by
Def4
.=
{} by
A17;
hence (c
. i) is
Function of (
{|M, M|}
. i), (
{|M|}
. i) by
A13,
FUNCT_2: 2,
RELAT_1: 38,
XBOOLE_1: 2;
end;
end;
c is
Function-yielding
proof
let i be
object;
assume i
in (
dom c);
then i
in
[:A, A, A:];
hence thesis by
A3;
end;
then
reconsider c as
ManySortedFunction of
[:A, A, A:];
reconsider c as
BinComp of M by
A3,
PBOOLE:def 15;
set C =
AltCatStr (# A, M, c #);
C is
quasi-discrete
proof
let o1,o2 be
Object of C;
assume that
A18:
<^o1, o2^>
<>
{} and
A19: o1
<> o2;
<^o1, o2^>
= (
IFEQ (o1,o2,
{(
id o1)},
{} )) by
A1
.=
{} by
A19,
FUNCOP_1:def 8;
hence contradiction by
A18;
end;
then
reconsider C =
AltCatStr (# A, M, c #) as
quasi-discrete
strict non
empty
AltCatStr;
take C;
thus the
carrier of C
= A;
let i be
Object of C;
thus
<^i, i^>
= (
IFEQ (i,i,
{(
id i)},
{} )) by
A1
.=
{(
id i)} by
FUNCOP_1:def 8;
end;
correctness
proof
let C1,C2 be
quasi-discrete
strict non
empty
AltCatStr such that
A20: the
carrier of C1
= A and
A21: for i be
Object of C1 holds
<^i, i^>
=
{(
id i)} and
A22: the
carrier of C2
= A and
A23: for i be
Object of C2 holds
<^i, i^>
=
{(
id i)};
A24:
now
let i, j, k;
assume that
A25: i
in A and
A26: j
in A & k
in A;
reconsider i2 = i as
Object of C2 by
A22,
A25;
reconsider i1 = i as
Object of C1 by
A20,
A25;
per cases ;
suppose
A27: i
= j & j
= k;
A28:
<^i2, i2^>
=
{(
id i2)} & (the
Comp of C2
. (i2,i2,i2)) is
Function of
[:
<^i2, i2^>,
<^i2, i2^>:],
<^i2, i2^> by
A23;
reconsider ii = i as
set by
TARSKI: 1;
<^i1, i1^>
=
{(
id i1)} & (the
Comp of C1
. (i1,i1,i1)) is
Function of
[:
<^i1, i1^>,
<^i1, i1^>:],
<^i1, i1^> by
A21;
hence (the
Comp of C1
. (i,j,k))
= (((
id ii),(
id ii))
:-> (
id ii)) by
A27,
FUNCOP_1:def 10
.= (the
Comp of C2
. (i,j,k)) by
A27,
A28,
FUNCOP_1:def 10;
end;
suppose
A29: i
<> j or j
<> k;
reconsider j1 = j, k1 = k as
Object of C1 by
A20,
A26;
A30:
<^i1, j1^>
=
{} or
<^j1, k1^>
=
{} by
A29,
Def18;
reconsider j2 = j, k2 = k as
Object of C2 by
A22,
A26;
A31: (the
Comp of C2
. (i2,j2,k2)) is
Function of
[:
<^j2, k2^>,
<^i2, j2^>:],
<^i2, k2^> & (the
Comp of C1
. (i1,j1,k1)) is
Function of
[:
<^j1, k1^>,
<^i1, j1^>:],
<^i1, k1^>;
<^i2, j2^>
=
{} or
<^j2, k2^>
=
{} by
A29,
Def18;
hence (the
Comp of C1
. (i,j,k))
= (the
Comp of C2
. (i,j,k)) by
A30,
A31;
end;
end;
now
let i,j be
Element of A;
reconsider i2 = i as
Object of C2 by
A22;
reconsider i1 = i as
Object of C1 by
A20;
per cases ;
suppose
A32: i
= j;
hence (the
Arrows of C1
. (i,j))
=
<^i1, i1^>
.=
{(
id i)} by
A21
.=
<^i2, i2^> by
A23
.= (the
Arrows of C2
. (i,j)) by
A32;
end;
suppose
A33: i
<> j;
reconsider j2 = j as
Object of C2 by
A22;
reconsider j1 = j as
Object of C1 by
A20;
thus (the
Arrows of C1
. (i,j))
=
<^i1, j1^>
.=
{} by
A33,
Def18
.=
<^i2, j2^> by
A33,
Def18
.= (the
Arrows of C2
. (i,j));
end;
end;
then the
Arrows of C1
= the
Arrows of C2 by
A20,
A22,
Th3;
hence thesis by
A20,
A22,
A24,
Th4;
end;
end
registration
cluster
quasi-discrete ->
transitive for
AltCatStr;
coherence ;
end
theorem ::
ALTCAT_1:24
Th18: for A be non
empty
set, o1,o2,o3 be
Object of (
DiscrCat A) st o1
<> o2 or o2
<> o3 holds (the
Comp of (
DiscrCat A)
. (o1,o2,o3))
=
{}
proof
let A be non
empty
set, o1,o2,o3 be
Object of (
DiscrCat A);
assume o1
<> o2 or o2
<> o3;
then
<^o1, o2^>
=
{} or
<^o2, o3^>
=
{} by
Def18;
hence thesis;
end;
theorem ::
ALTCAT_1:25
Th19: for A be non
empty
set, o be
Object of (
DiscrCat A) holds (the
Comp of (
DiscrCat A)
. (o,o,o))
= (((
id o),(
id o))
:-> (
id o))
proof
let A be non
empty
set, o be
Object of (
DiscrCat A);
<^o, o^>
=
{(
id o)} by
Def20;
hence thesis by
FUNCOP_1:def 10;
end;
registration
let A be non
empty
set;
cluster (
DiscrCat A) ->
pseudo-functional
pseudo-discrete
with_units
associative;
coherence
proof
set C = (
DiscrCat A);
thus C is
pseudo-functional
proof
let o1,o2,o3 be
Object of C;
A1: (
id o1)
in (
Funcs (o1,o1)) by
FUNCT_2: 126;
per cases ;
suppose
A2: o1
= o2 & o2
= o3;
then
A3:
<^o2, o3^>
=
{(
id o1)} by
Def20;
then
A4:
<^o1, o2^>
c= (
Funcs (o1,o2)) by
A1,
A2,
ZFMISC_1: 31;
thus (the
Comp of C
. (o1,o2,o3))
= (((
id o1),(
id o1))
:-> (
id o1)) by
A2,
Th19
.= (
FuncComp (
{(
id o1)},
{(
id o1)})) by
Th7
.= ((
FuncComp ((
Funcs (o1,o2)),(
Funcs (o2,o3))))
|
[:
<^o2, o3^>,
<^o1, o2^>:] qua
set) by
A2,
A3,
A4,
Th8;
end;
suppose
A5: o1
<> o2 or o2
<> o3;
then
A6:
<^o2, o3^>
=
{} or
<^o1, o2^>
=
{} by
Def18;
thus (the
Comp of C
. (o1,o2,o3))
=
{} by
A5,
Th18
.= ((
FuncComp ((
Funcs (o1,o2)),(
Funcs (o2,o3))))
|
[:
<^o2, o3^>,
<^o1, o2^>:] qua
set) by
A6;
end;
end;
thus C is
pseudo-discrete
proof
let i be
Object of C;
<^i, i^>
=
{(
id i)} by
Def20;
hence thesis;
end;
thus C is
with_units
proof
thus the
Comp of C is
with_left_units
proof
let j be
Element of C;
reconsider j9 = j as
Object of C;
take (
id j9);
(the
Arrows of C
. (j,j))
=
<^j9, j9^>
.=
{(
id j9)} by
Def20;
hence (
id j9)
in (the
Arrows of C
. (j,j)) by
TARSKI:def 1;
let i be
Element of C, f be
set such that
A7: f
in (the
Arrows of C
. (i,j));
reconsider i9 = i as
Object of C;
A8: (the
Arrows of C
. (i,j))
=
<^i9, j9^>;
then
A9: i9
= j9 by
A7,
Def18;
then f
in
{(
id i9)} by
A7,
A8,
Def20;
then
A10: f
= (
id i9) by
TARSKI:def 1;
thus ((the
Comp of C
. (i,j,j))
. ((
id j9),f))
= ((((
id i9),(
id i9))
:-> (
id i9))
. ((
id j9),f)) by
A9,
Th19
.= f by
A9,
A10,
FUNCT_4: 80;
end;
let j be
Element of C;
reconsider j9 = j as
Object of C;
take (
id j9);
(the
Arrows of C
. (j,j))
=
<^j9, j9^>
.=
{(
id j9)} by
Def20;
hence (
id j9)
in (the
Arrows of C
. (j,j)) by
TARSKI:def 1;
let i be
Element of C, f be
set such that
A11: f
in (the
Arrows of C
. (j,i));
reconsider i9 = i as
Object of C;
A12: (the
Arrows of C
. (j,i))
=
<^j9, i9^>;
then
A13: i9
= j9 by
A11,
Def18;
then f
in
{(
id i9)} by
A11,
A12,
Def20;
then
A14: f
= (
id i9) by
TARSKI:def 1;
thus ((the
Comp of C
. (j,j,i))
. (f,(
id j9)))
= ((((
id i9),(
id i9))
:-> (
id i9))
. (f,(
id j9))) by
A13,
Th19
.= f by
A13,
A14,
FUNCT_4: 80;
end;
thus C is
associative
proof
let i,j,k,l be
Element of C;
set G = the
Arrows of C, c = the
Comp of C;
reconsider i9 = i, j9 = j, k9 = k, l9 = l as
Object of C;
let f,g,h be
set;
assume that
A15: f
in (G
. (i,j)) and
A16: g
in (G
. (j,k)) and
A17: h
in (G
. (k,l));
f
in
<^i9, j9^> by
A15;
then
A18: i9
= j9 by
Def18;
A19:
<^i9, i9^>
=
{(
id i9)} by
Def20;
then
A20: f
= (
id i9) by
A15,
A18,
TARSKI:def 1;
g
in
<^j9, k9^> by
A16;
then
A21: j9
= k9 by
Def18;
then
A22: g
= (
id i9) by
A16,
A18,
A19,
TARSKI:def 1;
A23: (c
. (i9,i9,i9))
= (((
id i9),(
id i9))
:-> (
id i9)) by
Th19;
h
in
<^k9, l9^> by
A17;
then
A24: k9
= l9 by
Def18;
then h
= (
id i9) by
A17,
A18,
A21,
A19,
TARSKI:def 1;
hence thesis by
A18,
A21,
A24,
A20,
A22,
A23,
FUNCT_4: 80;
end;
end;
end