:: by Adam Grabowski

::

:: Received June 11, 1996

:: Copyright (c) 1996-2021 Association of Mizar Users

definition

let A be non empty set ;

ex b_{1} being non empty strict AltCatStr st

( the carrier of b_{1} = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b_{1} . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of b_{1} 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 b_{1} . (i,j) & [g1,g2] in the Arrows of b_{1} . (j,k) holds

( the Comp of b_{1} . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) )

for b_{1}, b_{2} being non empty strict AltCatStr st the carrier of b_{1} = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b_{1} . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of b_{1} 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 b_{1} . (i,j) & [g1,g2] in the Arrows of b_{1} . (j,k) holds

( the Comp of b_{1} . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) & the carrier of b_{2} = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b_{2} . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of b_{2} 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 b_{2} . (i,j) & [g1,g2] in the Arrows of b_{2} . (j,k) holds

( the Comp of b_{2} . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) holds

b_{1} = b_{2}

end;
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 ( 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)] ) );

ex b

( the carrier of b

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b

( the Comp of b

proof end;

uniqueness for b

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b

( the Comp of b

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b

( the Comp of b

b

proof end;

:: deftheorem Def1 defines MSSCat MSINST_1:def 1 :

for A being non empty set

for b_{2} being non empty strict AltCatStr holds

( b_{2} = MSSCat A iff ( the carrier of b_{2} = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b_{2} . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of b_{2} 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 b_{2} . (i,j) & [g1,g2] in the Arrows of b_{2} . (j,k) holds

( the Comp of b_{2} . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ) );

for A being non empty set

for b

( b

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b

( the Comp of b

registration

let A be non empty set ;

coherence

( MSSCat A is transitive & MSSCat A is associative & MSSCat A is with_units )

end;
coherence

( MSSCat A is transitive & MSSCat A is associative & MSSCat A is with_units )

proof 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

for C being category st C = MSSCat A holds

for o being Object of C holds o is non empty non void ManySortedSign

proof end;

registration

let S be non empty non void ManySortedSign ;

existence

ex b_{1} being MSAlgebra over S st

( b_{1} is strict & b_{1} is feasible )

end;
existence

ex b

( b

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be non empty set ;

ex b_{1} being set st

for x being object holds

( x in b_{1} 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 b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} 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 object holds

( x in b_{2} 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

b_{1} = b_{2}

end;
let A be non empty set ;

func MSAlg_set (S,A) -> set means :Def2: :: MSINST_1:def 2

for x being object 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 for x being object 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 ) ) );

ex b

for x being object holds

( x in b

( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) )

proof end;

uniqueness for b

( x in b

( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) & ( for x being object holds

( x in b

( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) holds

b

proof 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 b_{3} being set holds

( b_{3} = MSAlg_set (S,A) iff for x being object holds

( x in b_{3} 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 S being non empty non void ManySortedSign

for A being non empty set

for b

( b

( x in b

( 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 ;

coherence

not MSAlg_set (S,A) is empty

end;
let A be non empty set ;

coherence

not MSAlg_set (S,A) is empty

proof end;

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))) )

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))) )

proof end;

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 & Args (o,U1) <> {} holds

Args (o,U2) <> {}

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 & Args (o,U1) <> {} holds

Args (o,U2) <> {}

proof end;

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) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds

ex GF being ManySortedFunction of U1,U3 st

( GF = G ** F & GF # x = G # (F # x) )

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) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds

ex GF being ManySortedFunction of U1,U3 st

( GF = G ** F & GF # x = G # (F # x) )

proof end;

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 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds

ex GF being ManySortedFunction of U1,U3 st

( GF = G ** F & GF is_homomorphism U1,U3 )

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 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds

ex GF being ManySortedFunction of U1,U3 st

( GF = G ** F & GF is_homomorphism U1,U3 )

proof end;

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) ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex M, N being strict feasible MSAlgebra over S ex f being 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 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex M, N being strict feasible MSAlgebra over S ex f being 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 ) ) ) & ( for x being set holds

( x in b_{2} iff ex M, N being strict feasible MSAlgebra over S ex f being 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 ) ) ) holds

b_{1} = b_{2}

end;
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 & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) );

existence 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 & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) );

ex b

for x being set holds

( x in b

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) )

proof end;

uniqueness for b

( x in b

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) & ( for x being set holds

( x in b

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) holds

b

proof 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) & j in MSAlg_set (S,A) holds

for b_{5} being set holds

( b_{5} = MSAlg_morph (S,A,i,j) iff for x being set holds

( x in b_{5} iff ex M, N being strict feasible MSAlgebra over S ex f being 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 ) ) );

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) & j in MSAlg_set (S,A) holds

for b

( b

( x in b

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) );

definition

let S be non empty non void ManySortedSign ;

let A be non empty set ;

ex b_{1} being non empty strict AltCatStr st

( the carrier of b_{1} = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b_{1} . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of b_{1}

for f, g being Function-yielding Function st f in the Arrows of b_{1} . (i,j) & g in the Arrows of b_{1} . (j,k) holds

( the Comp of b_{1} . (i,j,k)) . (g,f) = g ** f ) )

for b_{1}, b_{2} being non empty strict AltCatStr st the carrier of b_{1} = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b_{1} . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of b_{1}

for f, g being Function-yielding Function st f in the Arrows of b_{1} . (i,j) & g in the Arrows of b_{1} . (j,k) holds

( the Comp of b_{1} . (i,j,k)) . (g,f) = g ** f ) & the carrier of b_{2} = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b_{2} . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of b_{2}

for f, g being Function-yielding Function st f in the Arrows of b_{2} . (i,j) & g in the Arrows of b_{2} . (j,k) holds

( the Comp of b_{2} . (i,j,k)) . (g,f) = g ** f ) holds

b_{1} = b_{2}

end;
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) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of it . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of it

for f, g being 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 ) );

existence ( the carrier of it = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of it . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of it

for f, g being 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 ) );

ex b

( the carrier of b

for f, g being Function-yielding Function st f in the Arrows of b

( the Comp of b

proof end;

uniqueness for b

for f, g being Function-yielding Function st f in the Arrows of b

( the Comp of b

for f, g being Function-yielding Function st f in the Arrows of b

( the Comp of b

b

proof end;

:: deftheorem Def4 defines MSAlgCat MSINST_1:def 4 :

for S being non empty non void ManySortedSign

for A being non empty set

for b_{3} being non empty strict AltCatStr holds

( b_{3} = MSAlgCat (S,A) iff ( the carrier of b_{3} = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b_{3} . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of b_{3}

for f, g being Function-yielding Function st f in the Arrows of b_{3} . (i,j) & g in the Arrows of b_{3} . (j,k) holds

( the Comp of b_{3} . (i,j,k)) . (g,f) = g ** f ) ) );

for S being non empty non void ManySortedSign

for A being non empty set

for b

( b

for f, g being Function-yielding Function st f in the Arrows of b

( the Comp of b

registration

let S be non empty non void ManySortedSign ;

let A be non empty set ;

coherence

( MSAlgCat (S,A) is transitive & MSAlgCat (S,A) is associative & MSAlgCat (S,A) is with_units )

end;
let A be non empty set ;

coherence

( MSAlgCat (S,A) is transitive & MSAlgCat (S,A) is associative & MSAlgCat (S,A) is with_units )

proof 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

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

proof end;