:: Examples of Category Structures :: by Adam Grabowski :: :: Received June 11, 1996 :: Copyright (c) 1996-2021 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;