:: Examples of Category Structures
:: by Adam Grabowski
::
:: Received June 11, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

definition
let A be non empty set ;
func MSSCat A ->  non empty strict AltCatStr  means :Def1: :: MSINST_1:def 1
( the carrier of it = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of it . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of it st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being 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)] ) );
existence
 ex b1 being non empty strict AltCatStr st
( the carrier of b1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b1 . (i,j) & [g1,g2] in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) )
proofend;
uniqueness
 for b1, b2 being non empty strict AltCatStr st the carrier of b1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b1 . (i,j) & [g1,g2] in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) & the carrier of b2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b2 . (i,j) & [g1,g2] in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines MSSCat MSINST_1:def_1_:_
 for A being non empty set
for b2 being non empty strict AltCatStr holds
( b2 = MSSCat A iff ( the carrier of b2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b2 . (i,j) & [g1,g2] in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ) );

registration
let A be non empty set ;
cluster MSSCat A ->  non empty transitive strict associative with_units ;
coherence
 ( MSSCat A is transitive & MSSCat A is associative & MSSCat A is with_units )
proofend;
end;

theorem :: MSINST_1:1
for A being non empty set
for C being category st C = MSSCat A holds
for o being object of C holds o is non empty non void ManySortedSign
proofend;

registration
let S be non empty non void ManySortedSign ;
cluster strict feasible for MSAlgebra over S;
existence
 ex b1 being MSAlgebra over S st
( b1 is strict & b1 is feasible )
proofend;
end;

definition
let S be non empty non void ManySortedSign ;
let A be non empty set ;
func MSAlg_set (S,A) ->  set  means :Def2: :: MSINST_1:def 2
 for x being set holds
( x in it iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) & ( for x being set holds
( x in b2 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines MSAlg_set MSINST_1:def_2_:_
 for S being non empty non void ManySortedSign
for A being non empty set
for b3 being set holds
( b3 = MSAlg_set (S,A) iff for x being set holds
( x in b3 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) );

registration
let S be non empty non void ManySortedSign ;
let A be non empty set ;
cluster MSAlg_set (S,A) ->  non empty ;
coherence
 not MSAlg_set (S,A) is empty
proofend;
end;

begin

theorem :: MSINST_1:2
for A being non empty set
for S being non empty non void ManySortedSign
for x being 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))) )
proofend;

theorem Th3: :: MSINST_1:3
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 &amp; Args (o,U1) <> {} holds
Args (o,U2) <> {}
proofend;

theorem Th4: :: MSINST_1:4
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2, U3 being feasible MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) st Args (o,U1) <> {} &amp; the Sorts of U1 is_transformable_to the Sorts of U2 &amp; the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F &amp; GF # x = G # (F # x) )
proofend;

theorem Th5: :: MSINST_1:5
for S being non empty non void ManySortedSign
for U1, U2, U3 being feasible MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 &amp; the Sorts of U2 is_transformable_to the Sorts of U3 &amp; F is_homomorphism U1,U2 &amp; G is_homomorphism U2,U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F &amp; GF is_homomorphism U1,U3 )
proofend;

definition
let S be non empty non void ManySortedSign ;
let A be non empty set ;
let i, j be set ;
assume that
A1: i in MSAlg_set (S,A) and
A2: j in MSAlg_set (S,A) ;
func MSAlg_morph (S,A,i,j) ->  set  means :Def3: :: MSINST_1:def 3
 for x being set holds
( x in it iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i &amp; N = j &amp; f = x &amp; the Sorts of M is_transformable_to the Sorts of N &amp; f is_homomorphism M,N ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i &amp; N = j &amp; f = x &amp; the Sorts of M is_transformable_to the Sorts of N &amp; f is_homomorphism M,N ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i &amp; N = j &amp; f = x &amp; the Sorts of M is_transformable_to the Sorts of N &amp; f is_homomorphism M,N ) ) ) &amp; ( for x being set holds
( x in b2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i &amp; N = j &amp; f = x &amp; the Sorts of M is_transformable_to the Sorts of N &amp; f is_homomorphism M,N ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines MSAlg_morph MSINST_1:def_3_:_
 for S being non empty non void ManySortedSign
for A being non empty set
for i, j being set st i in MSAlg_set (S,A) &amp; j in MSAlg_set (S,A) holds
for b5 being set holds
( b5 = MSAlg_morph (S,A,i,j) iff for x being set holds
( x in b5 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i &amp; N = j &amp; f = x &amp; the Sorts of M is_transformable_to the Sorts of N &amp; f is_homomorphism M,N ) ) );

definition
let S be non empty non void ManySortedSign ;
let A be non empty set ;
func MSAlgCat (S,A) ->  non empty strict AltCatStr  means :Def4: :: MSINST_1:def 4
( the carrier of it = MSAlg_set (S,A) &amp; ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of it . (i,j) = MSAlg_morph (S,A,i,j) ) &amp; ( for i, j, k being object of it
for f, g being Function-yielding Function st f in the Arrows of it . (i,j) &amp; g in the Arrows of it . (j,k) holds
( the Comp of it . (i,j,k)) . (g,f) = g ** f ) );
existence
 ex b1 being non empty strict AltCatStr st
( the carrier of b1 = MSAlg_set (S,A) &amp; ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b1 . (i,j) = MSAlg_morph (S,A,i,j) ) &amp; ( for i, j, k being object of b1
for f, g being Function-yielding Function st f in the Arrows of b1 . (i,j) &amp; g in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . (g,f) = g ** f ) )
proofend;
uniqueness
 for b1, b2 being non empty strict AltCatStr st the carrier of b1 = MSAlg_set (S,A) &amp; ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b1 . (i,j) = MSAlg_morph (S,A,i,j) ) &amp; ( for i, j, k being object of b1
for f, g being Function-yielding Function st f in the Arrows of b1 . (i,j) &amp; g in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . (g,f) = g ** f ) &amp; the carrier of b2 = MSAlg_set (S,A) &amp; ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b2 . (i,j) = MSAlg_morph (S,A,i,j) ) &amp; ( for i, j, k being object of b2
for f, g being Function-yielding Function st f in the Arrows of b2 . (i,j) &amp; g in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . (g,f) = g ** f ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines MSAlgCat MSINST_1:def_4_:_
 for S being non empty non void ManySortedSign
for A being non empty set
for b3 being non empty strict AltCatStr holds
( b3 = MSAlgCat (S,A) iff ( the carrier of b3 = MSAlg_set (S,A) &amp; ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b3 . (i,j) = MSAlg_morph (S,A,i,j) ) &amp; ( for i, j, k being object of b3
for f, g being Function-yielding Function st f in the Arrows of b3 . (i,j) &amp; g in the Arrows of b3 . (j,k) holds
( the Comp of b3 . (i,j,k)) . (g,f) = g ** f ) ) );

registration
let S be non empty non void ManySortedSign ;
let A be non empty set ;
cluster MSAlgCat (S,A) ->  non empty transitive strict associative with_units ;
coherence
 ( MSAlgCat (S,A) is transitive &amp; MSAlgCat (S,A) is associative &amp; MSAlgCat (S,A) is with_units )
proofend;
end;

theorem :: MSINST_1:6
for A being non empty set
for S being non empty non void ManySortedSign
for C being category st C = MSAlgCat (S,A) holds
for o being object of C holds o is strict feasible MSAlgebra over S
proofend;