:: Examples of Category Structures
:: by Adam Grabowski
::
:: Received June 11, 1996
:: Copyright (c) 1996-2017 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 XBOOLE_0, STRUCT_0, MSUALG_1, ALTCAT_1, MSALIMIT, SUBSET_1,
FUNCT_1, CAT_1, RELAT_1, PBOOLE, ZFMISC_1, MCART_1, PUA2MSS1, RELAT_2,
BINOP_1, TARSKI, MSUALG_6, FUNCT_2, PARTFUN1, NUMBERS, CARD_3, FUNCOP_1,
PZFMISC1, MARGREL1, MEMBER_1, FUNCT_6, FINSEQ_4, MSUALG_3, MSINST_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XTUPLE_0,
MCART_1, RELAT_1, FUNCT_1, STRUCT_0, FUNCT_2, RELSET_1, PARTFUN1,
FINSEQ_2, CARD_3, BINOP_1, MULTOP_1, FUNCT_6, FUNCOP_1, PBOOLE, PZFMISC1,
PRALG_1, MSUALG_1, MSUALG_3, ALTCAT_1, PRALG_2, PUA2MSS1, MSUALG_6,
MSALIMIT;
constructors PZFMISC1, MSUALG_3, ALTCAT_1, PUA2MSS1, CLOSURE1, MSUALG_6,
MSALIMIT, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCOP_1, RELAT_1,
STRUCT_0, MSUALG_1, ALTCAT_1, MSUALG_6, MSALIMIT, MSSUBFAM, PBOOLE,
FINSEQ_1, XTUPLE_0;
requirements SUBSET, BOOLE;
begin :: Category of Many Sorted Signatures
reserve A for non empty set,
S for non void non empty ManySortedSign;
reserve x for set;
definition
let A;
func MSSCat A -> strict non empty AltCatStr means
:: MSINST_1:def 1
the carrier of it =
MSS_set A & ( for i, j be Element of MSS_set A holds (the Arrows of it).(i,j) =
MSS_morph (i,j) ) & for i,j,k be Object of it st i in MSS_set A & j in MSS_set
A & k in MSS_set A for f1,f2,g1,g2 be Function st [f1,f2] in (the Arrows of it)
.(i,j) & [g1,g2] in (the Arrows of it).(j,k) holds (the Comp of it).(i,j,k).([
g1,g2],[f1,f2]) = [g1*f1,g2*f2];
end;
registration
let A;
cluster MSSCat A -> transitive associative with_units;
end;
theorem :: MSINST_1:1
for C be category st C = MSSCat A for o be Object of C holds o is non
empty non void ManySortedSign;
registration
let S;
cluster strict feasible for MSAlgebra over S;
end;
definition
let S, A;
func MSAlg_set (S,A) -> set means
:: MSINST_1:def 2
for x being object holds
x in it iff ex M be strict feasible MSAlgebra over S st x = M &
for C be Component of the Sorts of M holds C c= A;
end;
registration
let S, A;
cluster MSAlg_set (S,A) -> non empty;
end;
begin :: Category of Many Sorted Algebras
reserve o for OperSymbol of S;
theorem :: MSINST_1:2
for x be MSAlgebra over S st x in MSAlg_set (S,A) holds the Sorts
of x in Funcs (the carrier of S, bool A) & the Charact of x in Funcs (the
carrier' of S,PFuncs(PFuncs (NAT ,A),A));
theorem :: MSINST_1:3
for U1,U2 be MSAlgebra over S st the Sorts of U1
is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds Args (o,U2) <> {}
;
theorem :: MSINST_1:4
for U1,U2,U3 be feasible MSAlgebra over S, F be
ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3, x be Element of
Args(o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts
of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 ex GF be
ManySortedFunction of U1,U3 st GF = G ** F & GF#x = G#(F#x);
theorem :: MSINST_1:5
for U1,U2,U3 be feasible MSAlgebra over S, F be
ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3 st the Sorts of
U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to
the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 ex GF be
ManySortedFunction of U1,U3 st GF = G ** F & GF is_homomorphism U1,U3;
definition
let S, A;
let i,j be set;
assume that
i in MSAlg_set (S,A) and
j in MSAlg_set (S,A);
func MSAlg_morph (S,A,i,j) -> set means
:: MSINST_1:def 3
x in it iff
ex M,N be strict feasible MSAlgebra over S,
f be ManySortedFunction of M,N st M = i & N = j &
f = x & the Sorts of M is_transformable_to the Sorts of N &
f is_homomorphism M,N;
end;
definition
let S, A;
func MSAlgCat (S,A) -> strict non empty AltCatStr means
:: MSINST_1:def 4
the carrier
of it = MSAlg_set (S,A) & ( for i, j be Element of MSAlg_set (S,A) holds (the
Arrows of it).(i,j) = MSAlg_morph (S,A,i,j) ) & for i,j,k be Object of it, f,g
be Function-yielding Function st f in (the Arrows of it).(i,j) & g in (the
Arrows of it).(j,k) holds (the Comp of it).(i,j,k).(g,f) = ( g ** f );
end;
registration
let S, A;
cluster MSAlgCat (S,A) -> transitive associative with_units;
end;
theorem :: MSINST_1:6
for C be category st C = MSAlgCat (S,A) for o be Object of C holds o
is strict feasible MSAlgebra over S;