:: Many Sorted Quotient Algebra
:: by Ma{\l}gorzata Korolkiewicz
::
:: Received May 6, 1994
:: Copyright (c) 1994-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 STRUCT_0, XBOOLE_0, MSUALG_1, FUNCT_1, RELAT_1, PBOOLE, FUNCOP_1,
EQREL_1, SUBSET_1, NAT_1, MARGREL1, PARTFUN1, FINSEQ_1, TARSKI, CARD_3,
MSUALG_3, WELLORD1, MSUALG_4;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
EQREL_1, STRUCT_0, ORDINAL1, NAT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, CARD_3,
PBOOLE, FUNCOP_1, MSUALG_1, MSUALG_3;
constructors EQREL_1, PRALG_2, MSUALG_3, RELSET_1;
registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1, PBOOLE, STRUCT_0,
MSUALG_1, MSUALG_3, CARD_3, RELSET_1, FINSEQ_2, FINSEQ_1;
requirements SUBSET, BOOLE;
begin
reserve S for non void non empty ManySortedSign,
U1 for MSAlgebra over S,
o for OperSymbol of S,
s for SortSymbol of S;
registration
let I be set;
cluster Relation-yielding for ManySortedSet of I;
end;
definition
let I be set, A,B be ManySortedSet of I;
mode ManySortedRelation of A,B -> ManySortedSet of I means
:: MSUALG_4:def 1
for i be set st i in I holds it.i is Relation of A.i,B.i;
end;
registration
let I be set, A,B be ManySortedSet of I;
cluster -> Relation-yielding for ManySortedRelation of A,B;
end;
definition
let I be set, A be ManySortedSet of I;
mode ManySortedRelation of A is ManySortedRelation of A,A;
end;
definition
let I be set, A be ManySortedSet of I;
let IT be ManySortedRelation of A;
attr IT is MSEquivalence_Relation-like means
:: MSUALG_4:def 2
for i be set, R be
Relation of A.i st i in I & IT.i = R holds R is Equivalence_Relation of A.i;
end;
definition
let I be non empty set, A,B be ManySortedSet of I, F be ManySortedRelation
of A,B, i be Element of I;
redefine func F.i -> Relation of A.i,B.i;
end;
definition
let S be non empty ManySortedSign, U1 be MSAlgebra over S;
mode ManySortedRelation of U1 is ManySortedRelation of the Sorts of U1;
end;
definition
let S be non empty ManySortedSign, U1 be MSAlgebra over S;
let IT be ManySortedRelation of U1;
attr IT is MSEquivalence-like means
:: MSUALG_4:def 3
IT is MSEquivalence_Relation-like;
end;
registration
let S be non void non empty ManySortedSign, U1 be MSAlgebra over S;
cluster MSEquivalence-like for ManySortedRelation of U1;
end;
theorem :: MSUALG_4:1
for R be MSEquivalence-like ManySortedRelation of U1 holds R.s is
Equivalence_Relation of (the Sorts of U1).s;
definition
let S be non void non empty ManySortedSign, U1 be non-empty MSAlgebra over S
, R be MSEquivalence-like ManySortedRelation of U1;
attr R is MSCongruence-like means
:: MSUALG_4:def 4
for o be OperSymbol of S, x,y be
Element of Args(o,U1) st (for n be Nat st n in dom x holds [x.n,y.n] in R.((
the_arity_of o)/.n)) holds [Den(o,U1).x,Den(o,U1).y] in R.(the_result_sort_of o
);
end;
registration
let S be non void non empty ManySortedSign, U1 be non-empty MSAlgebra over S;
cluster MSCongruence-like for MSEquivalence-like ManySortedRelation of U1;
end;
definition
let S be non void non empty ManySortedSign, U1 be non-empty MSAlgebra over S;
mode MSCongruence of U1 is MSCongruence-like MSEquivalence-like
ManySortedRelation of U1;
end;
definition
let S be non void non empty ManySortedSign, U1 be MSAlgebra over S, R be
MSEquivalence-like (ManySortedRelation of U1), i be Element of S;
redefine func R.i -> Equivalence_Relation of ((the Sorts of U1).i);
end;
definition
let S be non void non empty ManySortedSign, U1 be MSAlgebra over S, R be
MSEquivalence-like (ManySortedRelation of U1), i be Element of S,
x be Element of (the Sorts of U1).i;
func Class(R,x) -> Subset of (the Sorts of U1).i equals
:: MSUALG_4:def 5
Class(R.i,x);
end;
definition
let S;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
func Class R -> non-empty ManySortedSet of the carrier of S means
:: MSUALG_4:def 6
for s being Element of S holds it.s = Class (R.s);
end;
begin :: Many Sorted Quotient Algebra
definition
let S;
let M1,M2 be ManySortedSet of the carrier' of S;
let F be ManySortedFunction of M1,M2;
let o be OperSymbol of S;
redefine func F.o -> Function of M1.o,M2.o;
end;
registration
let I be non empty set, p be FinSequence of I, X be ManySortedSet of I;
cluster X * p -> dom p-defined for Function;
end;
registration
let I be non empty set, p be FinSequence of I, X be ManySortedSet of I;
cluster X * p -> total for dom p-defined Function;
end;
definition
let S,o;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
let x be Element of Args(o,A);
func R # x -> Element of product ((Class R) * (the_arity_of o)) means
:: MSUALG_4:def 7
for n be Nat st n in dom (the_arity_of o) holds it.n = Class(R.((the_arity_of o
)/.n),x.n);
end;
definition
let S,o;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotRes(R,o) -> Function of ((the Sorts of A) * the ResultSort of S).o,
((Class R) * the ResultSort of S).o means
:: MSUALG_4:def 8
for x being Element of (the
Sorts of A).(the_result_sort_of o) holds it.x = Class(R,x);
func QuotArgs(R,o) -> Function of ((the Sorts of A)# * the Arity of S).o, ((
Class R)# * the Arity of S).o means
:: MSUALG_4:def 9
for x be Element of Args(o,A) holds it.x = R # x;
end;
definition
let S;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotRes R -> ManySortedFunction of ((the Sorts of A) * the ResultSort
of S), ((Class R) * the ResultSort of S) means
:: MSUALG_4:def 10
for o being OperSymbol of S holds it.o = QuotRes(R,o);
func QuotArgs R -> ManySortedFunction of (the Sorts of A)# * the Arity of S,
(Class R)# * the Arity of S means
:: MSUALG_4:def 11
for o be OperSymbol of S holds it.o = QuotArgs(R,o);
end;
theorem :: MSUALG_4:2
for A be non-empty MSAlgebra over S, R be MSCongruence of A, x be
set st x in ((Class R)# * the Arity of S).o ex a be Element of Args(o,A) st x =
R # a;
definition
let S,o;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotCharact(R,o) -> Function of ((Class R)# * the Arity of S).o, ((
Class R) * the ResultSort of S).o means
:: MSUALG_4:def 12
for a be Element of Args(o,A)
st R # a in ((Class R)# * the Arity of S).o holds it.(R # a) = ((QuotRes(R,o))
* (Den(o,A))).a;
end;
definition
let S;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotCharact R -> ManySortedFunction of (Class R)# * the Arity of S, (
Class R) * the ResultSort of S means
:: MSUALG_4:def 13
for o be OperSymbol of S holds it. o = QuotCharact(R,o);
end;
definition
let S;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
func QuotMSAlg(U1,R) -> MSAlgebra over S equals
:: MSUALG_4:def 14
MSAlgebra(# Class R,
QuotCharact R #);
end;
registration
let S;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
cluster QuotMSAlg (U1,R) -> strict non-empty;
end;
definition
let S;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
let s be SortSymbol of S;
func MSNat_Hom(U1,R,s) -> Function of (the Sorts of U1).s,(Class R).s means
:: MSUALG_4:def 15
for x be set st x in (the Sorts of U1).s holds it.x = Class(R.s,x);
end;
definition
let S;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
func MSNat_Hom(U1,R) -> ManySortedFunction of U1, QuotMSAlg (U1,R) means
:: MSUALG_4:def 16
for s be SortSymbol of S holds it.s = MSNat_Hom(U1,R,s);
end;
theorem :: MSUALG_4:3
for U1 be non-empty MSAlgebra over S, R be MSCongruence of U1 holds
MSNat_Hom(U1,R) is_epimorphism U1, QuotMSAlg (U1,R);
definition
let S;
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
let s be SortSymbol of S;
func MSCng(F,s) -> Equivalence_Relation of (the Sorts of U1).s means
:: MSUALG_4:def 17
for x,y be Element of (the Sorts of U1).s holds [x,y] in it iff (F.s).x = (F.s)
.y;
end;
definition
let S;
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume
F is_homomorphism U1,U2;
func MSCng(F) -> MSCongruence of U1 means
:: MSUALG_4:def 18
for s be SortSymbol of S holds it.s = MSCng(F,s);
end;
definition
let S;
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
let s be SortSymbol of S;
assume
F is_homomorphism U1,U2;
func MSHomQuot(F,s) -> Function of (the Sorts of (QuotMSAlg (U1,MSCng F))).s
,(the Sorts of U2).s means
:: MSUALG_4:def 19
for x be Element of (the Sorts of U1).s
holds it.(Class(MSCng(F,s),x)) = (F.s).x;
end;
definition
let S;
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
func MSHomQuot(F) -> ManySortedFunction of (QuotMSAlg (U1, MSCng F)),U2
means
:: MSUALG_4:def 20
for s be SortSymbol of S holds it.s = MSHomQuot(F,s);
end;
theorem :: MSUALG_4:4
for U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction
of U1,U2 st F is_homomorphism U1,U2 holds MSHomQuot(F) is_monomorphism
QuotMSAlg (U1,MSCng F),U2;
theorem :: MSUALG_4:5
for U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction
of U1,U2 st F is_epimorphism U1,U2 holds MSHomQuot(F) is_isomorphism QuotMSAlg
(U1,MSCng F),U2;
theorem :: MSUALG_4:6
for U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1
,U2 st F is_epimorphism U1,U2 holds QuotMSAlg (U1,MSCng F),U2 are_isomorphic;