:: Categories without Uniqueness of { \bf cod } and { \bf dom }
:: by Andrzej Trybulec
::
:: Received February 28, 1995
:: Copyright (c) 1995-2019 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, NUMERALS;
begin :: Preliminaries
reserve i,j,k,x for object;
::$CT 4
theorem :: ALTCAT_1:5
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);
scheme :: ALTCAT_1:sch 1
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);
scheme :: ALTCAT_1:sch 2
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);
scheme :: ALTCAT_1:sch 3
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);
scheme :: ALTCAT_1:sch 4
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);
theorem :: ALTCAT_1:6
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;
theorem :: ALTCAT_1:7
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;
theorem :: ALTCAT_1:8
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;
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
:: ALTCAT_1:def 1
(the Arrows of G).(o1,o2);
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
:: ALTCAT_1:def 2
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
:: ALTCAT_1:def 3
for i,j,k being object st i in I & j in I & k in I
holds it.(i,j,k) = G.(i,k);
let H be ManySortedSet of [:I,I:];
func {|G,H|} -> ManySortedSet of [:I,I,I:] means
:: ALTCAT_1:def 4
for i,j,k being object st i in I & j in I & k in I
holds it.(i,j,k) = [:H.(j,k),G.(i,j):];
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);
end;
definition
let I be non empty set;
let G be ManySortedSet of [:I,I:];
let IT be BinComp of G;
attr IT is associative means
:: ALTCAT_1:def 5
for i,j,k,l being Element of I for f,g,h
being set st f in G.(i,j) & g in G.(j,k) & h in G.(k,l) holds IT.(i,k,l).(h,IT.
(i,j,k).(g,f)) = IT.(i,j,l).(IT.(j,k,l).(h,g),f);
attr IT is with_right_units means
:: ALTCAT_1:def 6
for i being Element of I ex e being
set st e in G.(i,i) & for j being Element of I, f be set st f in G.(i,j) holds
IT.(i,i,j).(f,e) = f;
attr IT is with_left_units means
:: ALTCAT_1:def 7
for j being Element of I ex e being
set st e in G.(j,j) & for i being Element of I, 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;
end;
definition
let C be non empty AltCatStr;
let o1,o2,o3 be Object of C such that
<^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
:: ALTCAT_1:def 8
(the Comp of C).(o1,o2,o3).(g,f
);
end;
definition
let IT be Function;
attr IT is compositional means
:: ALTCAT_1:def 9
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:];
end;
::$CT 2
theorem :: ALTCAT_1:11
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;
definition
let A,B be functional set;
func FuncComp(A,B) -> compositional ManySortedFunction of [:B,A:] means
:: ALTCAT_1:def 10
not contradiction;
end;
theorem :: ALTCAT_1:12
for A,B,C being set holds rng FuncComp(Funcs(A,B),Funcs(B,C)) c= Funcs(A,C);
theorem :: ALTCAT_1:13
for o be set holds FuncComp({id o},{id o}) = (id o,id o) :-> id o;
theorem :: ALTCAT_1:14
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);
:: Kategorie przeksztalcen, Semadeni Wiweger, 1.2.2, str.15
definition
let C be non empty AltCatStr;
attr C is quasi-functional means
:: ALTCAT_1:def 11
for a1,a2 being Object of C holds <^a1,a2^> c= Funcs(a1,a2);
attr C is semi-functional means
:: ALTCAT_1:def 12
for a1,a2,a3 being Object of C st <^
a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} 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
:: ALTCAT_1:def 13
for o1,o2,o3 being Object of C
holds (the Comp of C).(o1,o2,o3) = FuncComp(Funcs(o1,o2),Funcs(o2,o3))|([:<^o2,
o3^>,<^o1,o2^>:] 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;
end;
registration
cluster strict pseudo-functional for non empty AltCatStr;
end;
theorem :: ALTCAT_1:15
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 :: ALTCAT_1:16
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;
:: 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
:: ALTCAT_1:def 14
the carrier of it = A & for a1,a2 being Object of it holds <^a1,a2^> = Funcs(
a1,a2);
end;
definition
let C be non empty AltCatStr;
attr C is associative means
:: ALTCAT_1:def 15
the Comp of C is associative;
attr C is with_units means
:: ALTCAT_1:def 16
the Comp of C is with_left_units with_right_units;
end;
registration
cluster transitive associative with_units strict for non empty AltCatStr;
end;
theorem :: ALTCAT_1:17
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^>;
theorem :: ALTCAT_1:18
for C being with_units non empty AltCatStr for o being Object
of C holds <^o,o^> <> {};
registration
let A be non empty set;
cluster EnsCat A -> transitive associative with_units;
end;
registration
cluster quasi-functional semi-functional transitive -> pseudo-functional for
non empty AltCatStr;
cluster with_units pseudo-functional transitive -> quasi-functional
semi-functional for non empty AltCatStr;
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
:: ALTCAT_1:def 17
for o9 being Object of C st <^o,
o9^> <> {} for a being Morphism of o,o9 holds a*it = a;
end;
theorem :: ALTCAT_1:19
for C being with_units non empty AltCatStr for o being Object
of C holds idm o in <^o,o^>;
theorem :: ALTCAT_1:20
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;
theorem :: ALTCAT_1:21
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;
begin
:: kategoria dyskretna, Semadeni Wiweger, 1.3.1, str.18
definition
let C be AltCatStr;
attr C is quasi-discrete means
:: ALTCAT_1:def 18
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
:: ALTCAT_1:def 19
for i being Object of C holds <^i,i ^> is trivial;
end;
theorem :: ALTCAT_1:22
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 };
registration
cluster 1-element -> quasi-discrete for AltCatStr;
end;
theorem :: ALTCAT_1:23
EnsCat {0} is pseudo-discrete 1-element;
registration
cluster pseudo-discrete trivial strict for category;
end;
registration
cluster quasi-discrete pseudo-discrete trivial strict for category;
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
:: ALTCAT_1:def 20
the carrier of it = A & for i being Object of it holds <^i,i^> = { id i };
end;
registration
cluster quasi-discrete -> transitive for AltCatStr;
end;
theorem :: ALTCAT_1:24
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) = {};
theorem :: ALTCAT_1:25
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;
registration
let A be non empty set;
cluster DiscrCat A -> pseudo-functional pseudo-discrete with_units
associative;
end;