:: Categories without Uniqueness of { \bf cod } and { \bf dom }
:: by Andrzej Trybulec
::
:: Received February 28, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, SUBSET_1, RELAT_1, FUNCT_2, XBOOLE_0, TARSKI, PBOOLE,
ZFMISC_1, MCART_1, FUNCOP_1, STRUCT_0, CAT_1, RELAT_2, BINOP_1, CARD_1,
ALTCAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, DOMAIN_1,
RELAT_1, CARD_1, ORDINAL1, NUMBERS, RELSET_1, STRUCT_0, FUNCT_1, FUNCT_2,
BINOP_1, MULTOP_1, FUNCOP_1, PBOOLE;
constructors PARTFUN1, BINOP_1, MULTOP_1, PBOOLE, REALSET2, RELSET_1,
XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
STRUCT_0, RELSET_1, ZFMISC_1, CARD_1, XTUPLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, STRUCT_0, FUNCOP_1;
equalities TARSKI, FUNCOP_1, BINOP_1, XTUPLE_0, ORDINAL1;
expansions TARSKI;
theorems FUNCT_1, ZFMISC_1, PBOOLE, DOMAIN_1, MULTOP_1, MCART_1, FUNCT_2,
TARSKI, FUNCOP_1, RELAT_1, STRUCT_0, RELSET_1, XBOOLE_1, PARTFUN1,
XTUPLE_0, FUNCT_4;
schemes FUNCT_1;
begin :: Preliminaries
reserve i,j,k,x for object;
::$CT 4
theorem
for A,B being set, F being ManySortedSet of [:B,A:], C being Subset of
A, D being Subset of B, x,y being 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
MSSLambda2{ A,B() -> set, F(object,object) -> object }:
ex M being ManySortedSet of [:A(),B():]
st for i,j being set st i in A() & j in B() holds M.(i,j) = F(i,j) proof
deffunc F(object) = F($1`1,$1`2);
consider f being Function such that
A1: dom f = [:A(),B():] and
A2: for x being 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
MSSLambda2D{ A,B() -> non empty set, F(object,object) -> object }:
ex M being
ManySortedSet of [:A(),B():] st for i being Element of A(), j being Element of
B() holds M.(i,j) = F(i,j) proof
consider M being ManySortedSet of [:A(),B():] such that
A1: for i,j being 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
MSSLambda3{ A,B,C() -> set, F(object,object,object) -> object }:
ex M being ManySortedSet of [:A(),B(),C():] st
for i,j,k being set st i in A() & j in B() & k in C()
holds M.(i,j,k) = F(i,j,k) proof
deffunc F(object) = F($1`1`1,$1`1`2,$1`2);
consider f being Function such that
A1: dom f = [:A(),B(),C():] and
A2: for x being 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
MSSLambda3D{ A,B,C() -> non empty set, F(object,object,object) -> object }:
ex M being
ManySortedSet of [:A(),B(),C():] st for i being Element of A(), j being Element
of B(), k being Element of C() holds M.(i,j,k) = F(i,j,k) proof
consider M being ManySortedSet of [:A(),B(),C():] such that
A1: for i,j,k being 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 Th2:
for A,B being set, N,M being 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 being Element of A1, j being 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 Th3:
for A,B being non empty set, N,M being ManySortedSet of [:A,B:]
st for i being Element of A, j being 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 being Element of A, j being 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 Th4:
for A being set, N,M being 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 being 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 :: Alternative Graphs
definition
struct(1-sorted) AltGraph (# carrier -> set, Arrows -> ManySortedSet of [:
the carrier, the carrier:] #);
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
(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;
attr G is transitive means
:Def2:
for o1,o2,o3 being Object of G st <^o1,o2
^> <> {} & <^o2,o3^> <> {} holds <^o1,o3^> <> {};
end;
begin :: Binary Compositions
definition
let I be set;
let G be ManySortedSet of [:I,I:];
func {|G|} -> ManySortedSet of [:I,I,I:] means
:Def3:
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
proof
deffunc F(object,object,object) = G.($1,$3);
consider M being ManySortedSet of [:I,I,I:] such that
A1: for i,j,k being 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 being 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 being 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:];
func {|G,H|} -> ManySortedSet of [:I,I,I:] means
:Def4:
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
proof
deffunc F(object,object,object) = [:H.($2,$3),G.($1,$2):];
consider M being ManySortedSet of [:I,I,I:] such that
A5: for i,j,k being 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 being 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 being 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;
redefine func o.(i,j,k) -> Function of [:G.(j,k),G.(i,j):], G.(i,k); :: redefines . (MULTOP_1, definition)
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;
attr IT is associative means
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
for i being Element of I ex e being
set st e in G.(i,i) & for j being Element of I, f be set st f in G.(i,j) holds
IT.(i,i,j).(f,e) = f;
attr IT is with_left_units means
for j being Element of I ex e being
set st e in G.(j,j) & for i being Element of I, f be set st f in G.(i,j) holds
IT.(i,j,j).(e,f) = f;
end;
begin :: Alternative categories
definition
struct(AltGraph) AltCatStr (# carrier -> set, Arrows -> ManySortedSet of [:
the carrier, the carrier:], Comp -> BinComp of the Arrows #);
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 such that
A1: <^o1,o2^> <> {} & <^o2,o3^> <> {};
let f be Morphism of o1,o2, g be Morphism of o2,o3;
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;
attr IT is compositional means
:Def9:
x in dom IT implies ex f,g being 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 being ManySortedSet of [:A1,B1:] such that
A2: for i being Element of A1, j being 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;
::$CT 2
theorem Th5:
for A,B being functional set for F being compositional
ManySortedSet of [:A,B:], g,f being 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 being 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;
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 being 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 being 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 Th6:
for A,B,C being 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 being object such that
A1: j in dom F and
A2: i = F.j by FUNCT_1:def 3;
consider f,g being 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 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 being 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 being 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 Th8:
for A,B being functional set, A1 being Subset of A, B1 being
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;
:: Kategorie przeksztalcen, Semadeni Wiweger, 1.2.2, str.15
definition
let C be non empty AltCatStr;
attr C is quasi-functional means
for a1,a2 being Object of C holds <^a1,a2^> c= Funcs(a1,a2);
attr C is semi-functional means
for a1,a2,a3 being Object of C st <^
a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} for f being Morphism of a1,a2
, g being Morphism of a2,a3, f9,g9 being Function st f = f9 & g = g9 holds g*f
=g9*f9;
attr C is pseudo-functional means
:Def13:
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^>:] 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
for C being non empty AltCatStr, 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:
for C being pseudo-functional non empty AltCatStr for a1,a2,a3
being Object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} for f
being Morphism of a1,a2, g being Morphism of a2,a3, f9,g9 being 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 being 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;
:: Kategorie EnsCat(A), Semadeni Wiweger 1.2.3, str. 15
:: ale bez parametryzacji
definition
let A be non empty set;
func EnsCat A -> strict pseudo-functional non empty AltCatStr means
:Def14
:
the carrier of it = A & for a1,a2 being 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 being ManySortedSet of [:A,A:] such that
A1: for i,j being set st i in A & j in A holds M.(i,j) = Funcs(i,j) from
MSSLambda2;
consider c being ManySortedSet of [:A,A,A:] such that
A2: for i,j,k being 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 being 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 being 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 being Object of C1 holds <^a1,a2^> = Funcs(a1,a2) and
A16: the carrier of C2 = A and
A17: for a1,a2 being 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;
attr C is associative means
:Def15:
the Comp of C is associative;
attr C is with_units means
:Def16:
the Comp of C is with_left_units with_right_units;
end;
Lm1: for A being 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
for C being transitive non empty AltCatStr, 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
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 Th12:
for C being with_units non empty AltCatStr for o being 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 being set st e in (the Arrows of C).(o,o) & for o9 being 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 being 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;
:: Definicja kategorii, Semadeni Wiweger 1.3.1, str. 16-17
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;
func idm o -> Morphism of o,o means
:Def17:
for o9 being Object of C st <^o,
o9^> <> {} for a being Morphism of o,o9 holds a*it = a;
existence
proof
the Comp of C is with_right_units by Def16;
then consider e being set such that
A1: e in (the Arrows of C).(o,o) and
A2: for o9 being 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 being set such that
A4: d in (the Arrows of C).(o,o) and
A5: for o9 being 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 being Object of C st <^o,o9^> <> {} for a being Morphism of
o,o9 holds a*a1 = a and
A7: for o9 being Object of C st <^o,o9^> <> {} for a being 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 Th13:
for C being with_units non empty AltCatStr for o being 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
for C being with_units non empty AltCatStr for o1,o2 being Object of
C st <^o1,o2^> <> {} for a being 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 being set such that
A2: d in (the Arrows of C).(o2,o2) and
A3: for o9 being 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
for C being associative transitive non empty AltCatStr for o1,o2,o3,
o4 being Object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} for
a being Morphism of o1,o2, b being Morphism of o2,o3, c being 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
:: kategoria dyskretna, Semadeni Wiweger, 1.3.1, str.18
definition
let C be AltCatStr;
attr C is quasi-discrete means
:Def18:
for i,j being Object of C st <^i,j^> <> {} holds i = j;
:: to sa po prostu zbiory monoidow
attr C is pseudo-discrete means
for i being Object of C holds <^i,i ^> is trivial;
end;
theorem
for C being with_units non empty AltCatStr holds C is
pseudo-discrete iff for o being 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 being 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 Th17:
EnsCat {0} is pseudo-discrete 1-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;
func DiscrCat A -> quasi-discrete strict non empty AltCatStr means
:Def20:
the carrier of it = A & for i being 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 being ManySortedSet of [:A,A:] such that
A1: for i,j being Element of A holds M.(i,j) = F(i,j) from MSSLambda2D;
consider c being ManySortedSet of [:A,A,A:] such that
A2: for i,j,k being 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 being 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 being Object of C1 holds <^i,i^> = { id i } and
A22: the carrier of C2 = A and
A23: for i being 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 Th18:
for A being non empty set, o1,o2,o3 being 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 Th19:
for A being non empty set, o being 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;