:: Many Sorted Quotient Algebra
:: by Ma{\l}gorzata Korolkiewicz
::
:: Received May 6, 1994
:: Copyright (c) 1994-2026 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;
definitions TARSKI, MSUALG_3, XBOOLE_0, FUNCOP_1;
equalities XBOOLE_0;
expansions TARSKI, MSUALG_3, XBOOLE_0, FUNCOP_1;
theorems FUNCT_1, FUNCT_2, PBOOLE, CARD_3, MSUALG_1, ZFMISC_1, RELAT_1,
RELSET_1, EQREL_1, MSUALG_3, MSAFREE, XBOOLE_0, FUNCOP_1, ORDINAL1,
PARTFUN1, FINSEQ_2;
schemes FUNCT_1, CLASSES1, EQREL_1;
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;
existence
proof
set R = the Relation;
set f = I --> R;
reconsider f as ManySortedSet of I;
take f;
for x be set st x in dom f holds f.x is Relation by FUNCOP_1:7;
hence thesis;
end;
end;
definition
let I be set, A,B be ManySortedSet of I;
mode ManySortedRelation of A,B -> ManySortedSet of I means
:Def1:
for i be set st i in I holds it.i is Relation of A.i,B.i;
existence
proof
consider R be Relation such that
A1: R = {};
set f = I --> R;
reconsider f as ManySortedSet of I;
take f;
for i be set st i in I holds f.i is Relation of A.i,B.i
proof
let i be set;
f.i = {} by A1;
hence thesis by RELSET_1:12;
end;
hence thesis;
end;
end;
registration
let I be set, A,B be ManySortedSet of I;
cluster -> Relation-yielding for ManySortedRelation of A,B;
coherence
proof
let R be ManySortedRelation of A,B;
let x be object;
assume x in dom R;
then x in I;
hence thesis by Def1;
end;
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
:Def2:
for i being object, R being 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;
let F be ManySortedRelation of A,B, i be Element of I;
redefine func F.i -> Relation of A.i,B.i; :: redefines . (FUNCT_1, definition)
coherence by Def1;
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
:Def3:
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;
existence
proof
deffunc F(Element of S) = id ((the Sorts of U1).$1);
consider f be Function such that
A1: dom f = the carrier of S & for d be Element of S holds f.d = F(d)
from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2
,RELAT_1:def 18;
for i be set st i in the carrier of S holds f.i is Relation of (the
Sorts of U1).i,(the Sorts of U1).i
proof
let i be set;
assume i in the carrier of S;
then f.i = id ((the Sorts of U1).i) by A1;
hence thesis;
end;
then reconsider
f as ManySortedRelation of the Sorts of U1,the Sorts of U1 by Def1;
reconsider f as ManySortedRelation of U1;
take f;
for i be set, R be Relation of (the Sorts of U1).i st i in the carrier
of S & f.i = R holds R is Equivalence_Relation of (the Sorts of U1).i
proof
let i be set, R be Relation of (the Sorts of U1).i;
assume i in the carrier of S & f.i = R;
then R = id ((the Sorts of U1).i) by A1;
hence thesis;
end;
then f is MSEquivalence_Relation-like;
hence thesis;
end;
end;
theorem Th1:
for R be MSEquivalence-like ManySortedRelation of U1 holds R.s is
Equivalence_Relation of (the Sorts of U1).s
by Def3,Def2;
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
:Def4:
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;
existence
proof
deffunc F(Element of S) = id ((the Sorts of U1).$1);
consider f be Function such that
A1: dom f = the carrier of S & for d be Element of S holds f.d = F(d)
from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2
,RELAT_1:def 18;
for i be set st i in the carrier of S holds f.i is Relation of (the
Sorts of U1).i,(the Sorts of U1).i
proof
let i be set;
assume i in the carrier of S;
then f.i = id ((the Sorts of U1).i) by A1;
hence thesis;
end;
then reconsider
f as ManySortedRelation of the Sorts of U1,the Sorts of U1 by Def1;
reconsider f as ManySortedRelation of U1;
for i be set, R be Relation of (the Sorts of U1).i st i in the carrier
of S & f.i = R holds R is Equivalence_Relation of (the Sorts of U1).i
proof
let i be set, R be Relation of (the Sorts of U1).i;
assume i in the carrier of S & f.i = R;
then R = id ((the Sorts of U1).i) by A1;
hence thesis;
end;
then f is MSEquivalence_Relation-like;
then reconsider f as MSEquivalence-like ManySortedRelation of U1 by Def3;
take f;
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 f.((the_arity_of o)/.n)) holds [Den(o,U1).
x,Den(o,U1).y] in f.(the_result_sort_of o)
proof
A2: dom (the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;
then
A3: dom ((the Sorts of U1)*(the ResultSort of S)) = dom (the ResultSort
of S) by PARTFUN1:def 2;
let o be OperSymbol of S, x,y be Element of Args(o,U1);
A4: dom x = dom (the_arity_of o) by MSUALG_3:6;
assume
A5: for n be Nat st n in dom x holds [x.n,y.n] in f.((the_arity_of o)/.n);
A6: for a be object st a in dom (the_arity_of o) holds x.a = y.a
proof
set ao = the_arity_of o;
let a be object;
assume
A7: a in dom (the_arity_of o);
then reconsider n = a as Nat by ORDINAL1:def 12;
ao.n in rng ao by A7,FUNCT_1:def 3;
then
A8: f.(ao.n) = id ((the Sorts of U1).(ao.n)) by A1;
((the_arity_of o)/.n) = (the_arity_of o).n by A7,PARTFUN1:def 6;
then [x.n,y.n] in f.(ao.n) by A5,A4,A7;
hence thesis by A8,RELAT_1:def 10;
end;
set r = the_result_sort_of o;
A9: f.r = id ((the Sorts of U1).r) by A1;
A10: Result(o,U1) = ((the Sorts of U1) * the ResultSort of S).o by
MSUALG_1:def 5
.= (the Sorts of U1).((the ResultSort of S).o) by A2,A3,FUNCT_1:12
.= (the Sorts of U1).r by MSUALG_1:def 2;
dom y = dom (the_arity_of o) by MSUALG_3:6;
then Den(o,U1).x = Den(o,U1).y by A4,A6,FUNCT_1:2;
hence thesis by A9,A10,RELAT_1:def 10;
end;
hence thesis;
end;
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); :: redefines . (FUNCT_1, definition)
coherence by Th1;
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
Class(R.i,x);
correctness;
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
:Def6:
for s being Element of S holds it.s = Class (R.s);
existence
proof
deffunc F(Element of S) = Class (R.$1);
consider f be Function such that
A1: dom f = the carrier of S & for d be Element of S holds f.d = F(d)
from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S
by A1,PARTFUN1:def 2,RELAT_1:def 18;
for i be object st i in the carrier of S holds f.i is non empty
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as Element of S;
consider x be object such that
A2: x in (the Sorts of U1).s by XBOOLE_0:def 1;
reconsider y = x as Element of (the Sorts of U1).s by A2;
f.s = Class (R.s) by A1;
then Class(R.s,y) in f.s by EQREL_1:def 3;
hence thesis;
end;
then reconsider f as non-empty ManySortedSet of the carrier of S by
PBOOLE:def 13;
take f;
thus thesis by A1;
end;
uniqueness
proof
let C,D be non-empty ManySortedSet of the carrier of S;
assume that
A3: for s being Element of S holds C.s = Class (R.s) and
A4: for s being Element of S holds D.s = Class (R.s);
now
let i be object;
assume i in the carrier of S;
then reconsider s = i as Element of S;
C.s = Class (R.s) by A3;
hence C.i = D.i by A4;
end;
hence thesis by PBOOLE:3;
end;
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; :: redefines . (FUNCT_1, definition)
coherence by PBOOLE:def 15;
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;
coherence
proof
rng p c= I;
then rng p c= dom X by PARTFUN1:def 2;
then dom (X * p) = dom p by RELAT_1:27;
then reconsider Xp = (X * p) as ManySortedSet of (dom p) by PARTFUN1:def 2
,RELAT_1:def 18;
Xp is ManySortedSet of (dom p);
hence thesis;
end;
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;
coherence
proof
rng p c= I;
then rng p c= dom X by PARTFUN1:def 2;
then dom (X * p) = dom p by RELAT_1:27;
then reconsider Xp = (X * p) as ManySortedSet of (dom p) by PARTFUN1:def 2;
Xp is ManySortedSet of (dom p);
hence thesis;
end;
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
:Def7:
for n be Nat st n in dom (the_arity_of o) holds it.n = Class(R.((the_arity_of o
)/.n),x.n);
existence
proof
defpred P[object,object] means
for n be Nat st n = $1 holds $2 = Class(R.((
the_arity_of o)/.n),x.n);
set ar = the_arity_of o, da = dom ar;
A1: for y be object st y in da ex u be object st P[y,u]
proof
let y be object;
assume y in da;
then reconsider n = y as Nat by ORDINAL1:def 12;
take Class(R.((the_arity_of o)/.n),x.n);
thus thesis;
end;
consider f be Function such that
A2: dom f = da & for x be object st x in da holds P[x,f.x] from CLASSES1:
sch 1(A1);
A3: dom ((Class R) * ar) = da by PARTFUN1:def 2;
for y be object st y in dom ((Class R) * ar)
holds f.y in ((Class R) * ar ).y
proof
let y be object;
assume
A4: y in dom ((Class R) * ar);
then reconsider n = y as Nat by ORDINAL1:def 12;
ar.y in rng ar by A3,A4,FUNCT_1:def 3;
then reconsider s = ar.y as Element of S;
A5: y in dom ((the Sorts of A) * ar) by A3,A4,PARTFUN1:def 2;
then ((the Sorts of A) * ar).y = (the Sorts of A).(ar.y) by FUNCT_1:12;
then
A6: x.y in (the Sorts of A).s by A5,MSUALG_3:6;
f.n = Class(R.(ar/.n),x.n) & ar/.n = ar.n by A2,A3,A4,PARTFUN1:def 6;
then
A7: f.y in Class (R.s) by A6,EQREL_1:def 3;
((Class R) * ar).y = (Class R).(ar.y) by A4,FUNCT_1:12;
hence thesis by A7,Def6;
end;
then reconsider f as Element of product ((Class R) * ar) by A2,A3,CARD_3:9;
take f;
let n be Nat;
assume n in da;
hence thesis by A2;
end;
uniqueness
proof
let F,G be Element of product ((Class R) * (the_arity_of o));
assume that
A8: for n be Nat st n in dom (the_arity_of o) holds F.n = Class(R.((
the_arity_of o)/.n),x.n) and
A9: for n be Nat st n in dom (the_arity_of o) holds G.n = Class(R.((
the_arity_of o)/.n),x.n);
A10: for y be object st y in dom (the_arity_of o) holds F.y = G.y
proof
let y be object;
assume
A11: y in dom (the_arity_of o);
then reconsider n = y as Nat by ORDINAL1:def 12;
F.n = Class(R.((the_arity_of o)/.n),x.n) by A8,A11;
hence thesis by A9,A11;
end;
A12: dom G = dom (the_arity_of o) by PARTFUN1:def 2;
dom F = dom (the_arity_of o) by PARTFUN1:def 2;
hence thesis by A12,A10,FUNCT_1:2;
end;
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
:Def8:
for x being Element of (the
Sorts of A).(the_result_sort_of o) holds it.x = Class(R,x);
existence
proof
set rs = (the_result_sort_of o), D = (the Sorts of A).rs;
deffunc F(Element of D)=Class(R,$1);
consider f be Function such that
A1: dom f = D & for d be Element of D holds f.d = F(d) from FUNCT_1:
sch 4;
A2: for x be object st x in D holds f.x in (Class R).rs
proof
let x be object;
assume x in D;
then reconsider x1 = x as Element of D;
f.x1 = Class(R,x1) by A1;
then f.x1 in Class (R.rs) by EQREL_1:def 3;
hence thesis by Def6;
end;
o in the carrier' of S;
then o in dom ((the Sorts of A)*(the ResultSort of S)) by PARTFUN1:def 2;
then
A3: ((the Sorts of A) * the ResultSort of S).o = (the Sorts of A).((the
ResultSort of S).o) by FUNCT_1:12
.= D by MSUALG_1:def 2;
A4: dom (the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;
then dom ((Class R) * the ResultSort of S) = dom (the ResultSort of S) by
PARTFUN1:def 2;
then
((Class R) * the ResultSort of S).o = (Class R).((the ResultSort of S)
.o) by A4,FUNCT_1:12
.= (Class R).rs by MSUALG_1:def 2;
then reconsider
f as Function of ((the Sorts of A) * the ResultSort of S).o, ((
Class R) * the ResultSort of S).o by A1,A3,A2,FUNCT_2:3;
take f;
thus thesis by A1;
end;
uniqueness
proof
set SA = the Sorts of A, RS = the ResultSort of S, rs = the_result_sort_of
o;
let f,g be Function of ((the Sorts of A) * the ResultSort of S).o, ((Class
R) * the ResultSort of S).o;
assume that
A5: for x being Element of SA.rs holds f.x = Class(R,x) and
A6: for x being Element of SA.rs holds g.x = Class(R,x);
A7: now
let x be object;
assume x in SA.rs;
then reconsider x1 = x as Element of SA.rs;
f.x1 = Class(R,x1) by A5;
hence f.x = g.x by A6;
end;
o in the carrier' of S;
then o in dom (SA*RS) by PARTFUN1:def 2;
then (SA * RS).o = SA.(RS.o) by FUNCT_1:12
.= SA.rs by MSUALG_1:def 2;
then dom f = SA.rs & dom g = SA.rs by FUNCT_2:def 1;
hence thesis by A7,FUNCT_1:2;
end;
func QuotArgs(R,o) -> Function of ((the Sorts of A)# * the Arity of S).o, ((
Class R)# * the Arity of S).o means
for x be Element of Args(o,A) holds it.x = R # x;
existence
proof
set ao = the_arity_of o;
set D = Args(o,A);
deffunc F(Element of D)=R#$1;
consider f be Function such that
A8: dom f = D & for d be Element of D holds f.d = F(d) from FUNCT_1:
sch 4;
A9: o in the carrier' of S;
then o in dom ((the Sorts of A)# * the Arity of S) by PARTFUN1:def 2;
then
A10: ((the Sorts of A)# * the Arity of S).o = (the Sorts of A)#.((the
Arity of S).o) by FUNCT_1:12
.= ((the Sorts of A)#.(the_arity_of o)) by MSUALG_1:def 1;
A11: for x be object st x in (the Sorts of A)#.ao holds f.x in (Class R)#.ao
proof
let x be object;
assume x in (the Sorts of A)#.ao;
then reconsider x1 = x as Element of D by A10,MSUALG_1:def 4;
f.x1 = R#x1 & (Class R)#.ao = product((Class R)*ao) by A8,FINSEQ_2:def 5;
hence thesis;
end;
o in dom ((Class R)# * the Arity of S) by A9,PARTFUN1:def 2;
then ((Class R)# * the Arity of S).o = (Class R)#.((the Arity of S).o) by
FUNCT_1:12
.= (Class R)#.ao by MSUALG_1:def 1;
then reconsider
f as Function of ((the Sorts of A)# * the Arity of S).o, ((
Class R)# * the Arity of S).o by A8,A10,A11,FUNCT_2:3,MSUALG_1:def 4;
take f;
thus thesis by A8;
end;
uniqueness
proof
set ao = the_arity_of o;
let f,g be Function of ((the Sorts of A)# * the Arity of S).o, ((Class R)#
* the Arity of S).o;
assume that
A12: for x be Element of Args(o,A) holds f.x = R#x and
A13: for x be Element of Args(o,A) holds g.x = R#x;
o in the carrier' of S;
then o in dom ((the Sorts of A)# * the Arity of S) by PARTFUN1:def 2;
then
A14: ((the Sorts of A)# * the Arity of S).o = (the Sorts of A)#.((the
Arity of S).o) by FUNCT_1:12
.= ((the Sorts of A)#.(the_arity_of o)) by MSUALG_1:def 1;
A15: now
let x be object;
assume x in (the Sorts of A)#.ao;
then reconsider x1 = x as Element of Args(o,A) by A14,MSUALG_1:def 4;
f.x1 = R#x1 by A12;
hence f.x = g.x by A13;
end;
dom f = (the Sorts of A)#.ao & dom g = (the Sorts of A)#.ao by A14,
FUNCT_2:def 1;
hence thesis by A15,FUNCT_1:2;
end;
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
for o being OperSymbol of S holds it.o = QuotRes(R,o);
existence
proof
defpred P[object,object] means
for o be OperSymbol of S st o = $1 holds $2 =
QuotRes(R,o);
set O = the carrier' of S;
A1: for x be object st x in O ex y be object st P[x,y]
proof
let x be object;
assume x in O;
then reconsider x1 = x as OperSymbol of S;
take QuotRes(R,x1);
thus thesis;
end;
consider f be Function such that
A2: dom f = O & for x be object st x in O holds P[x,f.x] from CLASSES1:
sch 1( A1);
reconsider f as ManySortedSet of O by A2,PARTFUN1:def 2,RELAT_1:def 18;
for x be object st x in dom f holds f.x is Function
proof
let x be object;
assume x in dom f;
then reconsider x1 = x as OperSymbol of S;
f.x1 = QuotRes(R,x1) by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of O by FUNCOP_1:def 6;
for i be object st i in O holds f.i is Function of ((the Sorts of A) *
the ResultSort of S).i, ((Class R) * the ResultSort of S).i
proof
let i be object;
assume i in O;
then reconsider i1 = i as OperSymbol of S;
f.i1 = QuotRes(R,i1) by A2;
hence thesis;
end;
then reconsider
f as ManySortedFunction of ((the Sorts of A) * the ResultSort
of S), ((Class R) * the ResultSort of S) by PBOOLE:def 15;
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be ManySortedFunction of ((the Sorts of A) * the ResultSort of S),
((Class R) * the ResultSort of S);
assume that
A3: for o being OperSymbol of S holds f.o = QuotRes(R,o) and
A4: for o being OperSymbol of S holds g.o = QuotRes(R,o);
now
let i be object;
assume i in the carrier' of S;
then reconsider i1 = i as OperSymbol of S;
f.i1 = QuotRes(R,i1) by A3;
hence f.i = g. i by A4;
end;
hence thesis by PBOOLE:3;
end;
func QuotArgs R -> ManySortedFunction of (the Sorts of A)# * the Arity of S,
(Class R)# * the Arity of S means
for o be OperSymbol of S holds it.o = QuotArgs(R,o);
existence
proof
defpred P[object,object] means
for o be OperSymbol of S st o = $1 holds $2 = QuotArgs(R,o);
set O = the carrier' of S;
A5: for x be object st x in O ex y be object st P[x,y]
proof
let x be object;
assume x in O;
then reconsider x1 = x as OperSymbol of S;
take QuotArgs(R,x1);
thus thesis;
end;
consider f be Function such that
A6: dom f = O & for x be object st x in O holds P[x,f.x] from CLASSES1:
sch 1( A5);
reconsider f as ManySortedSet of O by A6,PARTFUN1:def 2,RELAT_1:def 18;
for x be object st x in dom f holds f.x is Function
proof
let x be object;
assume x in dom f;
then reconsider x1 = x as OperSymbol of S;
f.x1 = QuotArgs(R,x1) by A6;
hence thesis;
end;
then reconsider f as ManySortedFunction of O by FUNCOP_1:def 6;
for i be object st i in O holds f.i is Function of ((the Sorts of A)# *
the Arity of S).i, ((Class R)# * the Arity of S).i
proof
let i be object;
assume i in O;
then reconsider i1 = i as OperSymbol of S;
f.i1 = QuotArgs(R,i1) by A6;
hence thesis;
end;
then reconsider
f as ManySortedFunction of ((the Sorts of A)# * the Arity of S)
, ((Class R)# * the Arity of S) by PBOOLE:def 15;
take f;
thus thesis by A6;
end;
uniqueness
proof
let f,g be ManySortedFunction of ((the Sorts of A)# * the Arity of S), ((
Class R)# * the Arity of S);
assume that
A7: for o being OperSymbol of S holds f.o = QuotArgs(R,o) and
A8: for o being OperSymbol of S holds g.o = QuotArgs(R,o);
now
let i be object;
assume i in the carrier' of S;
then reconsider i1 = i as OperSymbol of S;
f.i1 = QuotArgs(R,i1) by A7;
hence f.i = g.i by A8;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem Th2:
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
proof
let A be non-empty MSAlgebra over S, R be MSCongruence of A, x be set;
assume
A1: x in ((Class R)# * the Arity of S).o;
set ar = the_arity_of o;
A2: ar = (the Arity of S).o by MSUALG_1:def 1;
then ((Class R)# * the Arity of S).o = product ((Class R) * ar) by MSAFREE:1;
then consider f be Function such that
A3: f = x and
A4: dom f = dom ((Class R) * ar) and
A5: for y be object st y in dom ((Class R) * ar) holds f.y in ((Class R) *
ar).y by A1,CARD_3:def 5;
defpred P[object,object] means $2 in f.$1;
:: !!! ??? Kuratowski function
A6: dom ((Class R) * ar) = dom ar by PARTFUN1:def 2;
A7: for n be Nat st n in dom f holds f.n in Class (R.(ar/.n))
proof
let n be Nat;
reconsider s = ar/.n as Element of S;
assume
A8: n in dom f;
then ar.n = ar/.n by A4,A6,PARTFUN1:def 6;
then ((Class R) * ar).n = (Class R).s by A4,A8,FUNCT_1:12
.= Class (R.s) by Def6;
hence thesis by A4,A5,A8;
end;
A9: for a be object st a in dom f ex b be object st P[a,b]
proof
let a be object;
reconsider s = ar/.a as Element of S;
assume
A10: a in dom f;
then reconsider n = a as Nat by A4,ORDINAL1:def 12;
f.n in Class (R.s) by A7,A10;
then consider a1 be object such that
A11: a1 in (the Sorts of A).s & f.n = Class(R.s,a1) by EQREL_1:def 3;
take a1;
thus thesis by A11,EQREL_1:20;
end;
consider g be Function such that
A12: dom g = dom f & for a be object st a in dom f holds P[a,g.a] from
CLASSES1:sch 1(A9);
dom (the Sorts of A) = the carrier of S by PARTFUN1:def 2;
then rng ar c= dom (the Sorts of A);
then
A13: dom g = dom ((the Sorts of A) * ar) by A4,A6,A12,RELAT_1:27;
A14: for y be object st y in dom ((the Sorts of A) * ar) holds g.y in ((the
Sorts of A) * ar).y
proof
let y be object;
assume
A15: y in dom ((the Sorts of A) * ar);
then
A16: g.y in f.y & f.y in ((Class R) * ar).y by A4,A5,A12,A13;
reconsider n = y as Nat by A15,ORDINAL1:def 12;
reconsider s = ar/.n as Element of S;
A17: ar.n = ar/.n by A4,A6,A12,A13,A15,PARTFUN1:def 6;
then ((Class R) * ar).y = (Class R).s by A4,A12,A13,A15,FUNCT_1:12
.= Class (R.s) by Def6;
then g.n in (the Sorts of A).s by A16;
hence thesis by A15,A17,FUNCT_1:12;
end;
Args(o,A) = ((the Sorts of A)# * (the Arity of S)).o by MSUALG_1:def 4
.= product ((the Sorts of A) * ar) by A2,MSAFREE:1;
then reconsider g as Element of Args(o,A) by A13,A14,CARD_3:9;
A18: now
let x be object;
assume
A19: x in dom ar;
then reconsider n = x as Nat by ORDINAL1:def 12;
reconsider s = ar/.n as Element of S;
f.n in Class (R.s) by A4,A6,A7,A19;
then consider a1 be object such that
A20: a1 in (the Sorts of A).s and
A21: f.n = Class(R.s,a1) by EQREL_1:def 3;
g.n in f.n by A4,A6,A12,A19;
then Class(R.s,g.n) = Class(R.s,a1) by A20,A21,EQREL_1:23;
hence f.x = (R # g).x by A19,A21,Def7;
end;
take g;
dom (R # g) = dom ((Class R) * ar) by CARD_3:9;
hence thesis by A3,A4,A6,A18,FUNCT_1:2;
end;
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
:Def12:
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;
existence
proof
defpred P[object,object] means
for a be Element of Args(o,A) st $1 = R # a holds
$2 = ((QuotRes(R,o)) * (Den(o,A))).a;
set Ca = ((Class R)# * the Arity of S).o, Cr = ((Class R) * the ResultSort
of S).o;
A1: for x be object st x in Ca ex y be object st y in Cr & P[x,y]
proof
set ro = the_result_sort_of o, ar = the_arity_of o;
let x be object;
assume x in Ca;
then consider a be Element of Args(o,A) such that
A2: x = R # a by Th2;
take y = ((QuotRes(R,o)) * (Den(o,A))).a;
A3: o in the carrier' of S;
then o in dom ((Class R) * the ResultSort of S) by PARTFUN1:def 2;
then
A4: ((Class R) * the ResultSort of S).o = (Class R).((the ResultSort of
S).o) by FUNCT_1:12
.= (Class R).ro by MSUALG_1:def 2;
o in dom ((the Sorts of A) * the ResultSort of S) by A3,PARTFUN1:def 2;
then
A5: ((the Sorts of A) * the ResultSort of S).o = (the Sorts of A).((the
ResultSort of S).o) by FUNCT_1:12
.= (the Sorts of A).ro by MSUALG_1:def 2;
then
A6: dom (QuotRes(R,o)) = (the Sorts of A).ro & Result(o,A) = (the Sorts
of A).ro by FUNCT_2:def 1,MSUALG_1:def 5;
rng Den(o,A) c= Result(o,A);
then
A7: dom Den(o,A) = Args(o,A) & dom (QuotRes(R,o) * Den(o,A)) = dom Den(
o,A) by A6,FUNCT_2:def 1,RELAT_1:27;
QuotRes(R,o).(Den(o,A).a) in rng (QuotRes(R,o)) by A6,FUNCT_1:def 3;
then QuotRes(R,o).(Den(o,A).a) in (Class R).ro by A4;
hence y in Cr by A4,A7,FUNCT_1:12;
let b be Element of Args(o,A);
reconsider da = (Den(o,A)).a, db = (Den(o,A)).b as Element of (the Sorts
of A).ro by A5,MSUALG_1:def 5;
A8: ((QuotRes(R,o)) * (Den(o,A))).b = (QuotRes(R,o)).db by A7,FUNCT_1:12
.= Class(R,db) by Def8
.= Class(R.ro,db);
assume
A9: x = R # b;
for n be Nat st n in dom a holds [a.n,b.n] in R.(ar/.n)
proof
let n be Nat;
A10: dom a = dom ar by MSUALG_3:6;
assume
A11: n in dom a;
then
A12: (R#a).n = Class(R.(ar/.n),a.n) & (R#b).n = Class(R.(ar/.n),b.n)
by A10,Def7;
dom (the Sorts of A) = the carrier of S by PARTFUN1:def 2;
then rng ar c= dom (the Sorts of A);
then
A13: dom ((the Sorts of A) * ar) = dom ar by RELAT_1:27;
then
A14: a.n in ((the Sorts of A) * ar).n by A11,A10,MSUALG_3:6;
((the Sorts of A) * ar).n = (the Sorts of A).(ar.n) by A13,A11,A10,
FUNCT_1:12
.= (the Sorts of A).(ar/.n) by A11,A10,PARTFUN1:def 6;
hence thesis by A2,A9,A14,A12,EQREL_1:35;
end;
then
A15: [da,db] in R.ro by Def4;
y = (QuotRes(R,o)).((Den(o,A)).a) by A7,FUNCT_1:12
.= Class(R, da) by Def8
.= Class (R.ro, da);
hence thesis by A8,A15,EQREL_1:35;
end;
consider f be Function such that
A16: dom f = Ca & rng f c= Cr & for x be object st x in Ca holds P[x,f.x]
from FUNCT_1:sch 6(A1);
reconsider f as Function of ((Class R)# * the Arity of S).o, ((Class R) *
the ResultSort of S).o by A16,FUNCT_2:2;
take f;
thus thesis by A16;
end;
uniqueness
proof
set ao = the_arity_of o;
let F,G be Function of ((Class R)# * the Arity of S).o, ((Class R) * the
ResultSort of S).o;
assume that
A17: for a be Element of Args(o,A) st R # a in ((Class R)# * the Arity
of S).o holds F.(R # a) = ((QuotRes(R,o)) * (Den(o,A))).a and
A18: for a be Element of Args(o,A) st R # a in ((Class R)# * the Arity
of S).o holds G.(R # a) = ((QuotRes(R,o)) * (Den(o,A))).a;
A19: dom (the Arity of S) = the carrier' of S by FUNCT_2:def 1;
then dom ((Class R)# * the Arity of S) = dom (the Arity of S) by
PARTFUN1:def 2;
then
A20: ((Class R)# * the Arity of S).o = (Class R)#.((the Arity of S).o) by A19,
FUNCT_1:12
.= (Class R)#.ao by MSUALG_1:def 1;
A21: now
let x be object;
assume
A22: x in (Class R)#.ao;
then consider a be Element of Args(o,A) such that
A23: x = R # a by A20,Th2;
F.x = (QuotRes(R,o) * Den(o,A)).a by A17,A20,A22,A23;
hence F.x = G.x by A18,A20,A22,A23;
end;
dom F = (Class R)#.ao & dom G = (Class R)#.ao by A20,FUNCT_2:def 1;
hence thesis by A21,FUNCT_1:2;
end;
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
:Def13:
for o be OperSymbol of S holds it. o = QuotCharact(R,o);
existence
proof
defpred P[object,object] means
for o be OperSymbol of S st o = $1 holds $2 =
QuotCharact(R,o);
set O = the carrier' of S;
A1: for x be object st x in O ex y be object st P[x,y]
proof
let x be object;
assume x in O;
then reconsider x1 = x as OperSymbol of S;
take QuotCharact(R,x1);
thus thesis;
end;
consider f be Function such that
A2: dom f = O & for x be object st x in O holds P[x,f.x] from CLASSES1:
sch 1( A1);
reconsider f as ManySortedSet of O by A2,PARTFUN1:def 2,RELAT_1:def 18;
for x be object st x in dom f holds f.x is Function
proof
let x be object;
assume x in dom f;
then reconsider x1 = x as OperSymbol of S;
f.x1 = QuotCharact(R,x1) by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of O by FUNCOP_1:def 6;
for i be object st i in O holds f.i is Function of ((Class R)# * the
Arity of S).i, ((Class R) * the ResultSort of S).i
proof
let i be object;
assume i in O;
then reconsider i1 = i as OperSymbol of S;
f.i1 = QuotCharact(R,i1) by A2;
hence thesis;
end;
then reconsider
f as ManySortedFunction of ((Class R)# * the Arity of S), ((
Class R) * the ResultSort of S) by PBOOLE:def 15;
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be ManySortedFunction of ((Class R)# * the Arity of S), ((Class R)
* the ResultSort of S);
assume that
A3: for o being OperSymbol of S holds f.o = QuotCharact(R,o) and
A4: for o being OperSymbol of S holds g.o = QuotCharact(R,o);
now
let i be object;
assume i in the carrier' of S;
then reconsider i1 = i as OperSymbol of S;
f.i1 = QuotCharact(R,i1) by A3;
hence f.i = g.i by A4;
end;
hence thesis by PBOOLE:3;
end;
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
MSAlgebra(# Class R,
QuotCharact R #);
coherence;
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;
coherence by MSUALG_1:def 3;
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
:Def15:
for x be set st x in (the Sorts of U1).s holds it.x = Class(R.s,x);
existence
proof
deffunc F(object) = Class(R.s,$1);
consider f being Function such that
A1: dom f = (the Sorts of U1).s &
for x be object st x in (the Sorts of
U1).s holds f.x = F(x) from FUNCT_1:sch 3;
for x be object st x in (the Sorts of U1).s holds f.x in (Class R).s
proof
let x be object;
assume
A2: x in (the Sorts of U1).s;
then Class(R.s,x) in Class (R.s) by EQREL_1:def 3;
then f.x in Class (R.s) by A1,A2;
hence thesis by Def6;
end;
then reconsider f as Function of (the Sorts of U1).s,(Class R).s by A1,
FUNCT_2:3;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f,g be Function of (the Sorts of U1).s,(Class R).s;
assume that
A3: for x be set st x in (the Sorts of U1).s holds f.x = Class(R.s,x) and
A4: for x be set st x in (the Sorts of U1).s holds g.x = Class(R.s,x);
A5: now
let x be object;
assume
A6: x in (the Sorts of U1).s;
then f.x = Class(R.s,x) by A3;
hence f.x = g.x by A4,A6;
end;
dom f = (the Sorts of U1).s & dom g = (the Sorts of U1).s by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:2;
end;
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
:
Def16: for s be SortSymbol of S holds it.s = MSNat_Hom(U1,R,s);
existence
proof
deffunc F(Element of S) = MSNat_Hom(U1,R,$1);
consider f be Function such that
A1: dom f = the carrier of S & for d be Element of S holds f.d = F(d)
from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2
,RELAT_1:def 18;
for x be object st x in dom f holds f.x is Function
proof
let x be object;
assume x in dom f;
then reconsider y = x as Element of S;
f.y = MSNat_Hom(U1,R,y) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of the carrier of S by
FUNCOP_1:def 6;
for i be object st i in the carrier of S holds f.i is Function of (the
Sorts of U1).i, (Class R).i
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as Element of S;
f.s = MSNat_Hom(U1,R,s) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of the Sorts of U1,Class R by
PBOOLE:def 15;
reconsider f as ManySortedFunction of U1,QuotMSAlg (U1,R);
take f;
thus thesis by A1;
end;
uniqueness
proof
let F,G be ManySortedFunction of U1, QuotMSAlg (U1,R);
assume that
A2: for s be SortSymbol of S holds F.s = MSNat_Hom(U1,R,s) and
A3: for s be SortSymbol of S holds G.s = MSNat_Hom(U1,R,s);
now
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
F.s = MSNat_Hom(U1,R,s) by A2;
hence F.i = G.i by A3;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem
for U1 be non-empty MSAlgebra over S, R be MSCongruence of U1 holds
MSNat_Hom(U1,R) is_epimorphism U1, QuotMSAlg (U1,R)
proof
let U1 be non-empty MSAlgebra over S, R be MSCongruence of U1;
set F = MSNat_Hom(U1,R), QA = QuotMSAlg (U1,R), S1 = the Sorts of U1;
for o be OperSymbol of S st Args (o,U1) <> {} for x be Element of Args(o
,U1) holds (F.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,QA).(F#x)
proof
let o be OperSymbol of S such that
Args (o,U1) <> {};
let x be Element of Args(o,U1);
set ro = the_result_sort_of o, ar = the_arity_of o;
(the Arity of S).o = ar by MSUALG_1:def 1;
then
A1: ((Class R)# * the Arity of S).o = product ((Class R) * ar) by MSAFREE:1;
A2: dom x = dom ar by MSUALG_3:6;
A3: for a be object st a in dom ar holds (F#x).a = (R#x).a
proof
let a be object;
assume
A4: a in dom ar;
then reconsider n = a as Nat by ORDINAL1:def 12;
set Fo = MSNat_Hom(U1,R,ar/.n), s = (ar/.n);
A5: n in dom ((the Sorts of U1) * ar) by A4,PARTFUN1:def 2;
then ((the Sorts of U1) * ar).n = (the Sorts of U1).(ar.n) by FUNCT_1:12
.= S1.s by A4,PARTFUN1:def 6;
then reconsider xn = x.n as Element of S1.s by A5,MSUALG_3:6;
thus (F#x).a = (F.(ar/.n)).(x.n) by A2,A4,MSUALG_3:def 6
.= Fo.xn by Def16
.= Class(R.s,x.n) by Def15
.= (R#x).a by A4,Def7;
end;
dom (the Sorts of U1) = the carrier of S by PARTFUN1:def 2;
then rng (the ResultSort of S) c= dom (the Sorts of U1);
then
dom (the ResultSort of S) = the carrier' of S & dom ((the Sorts of U1
) * the ResultSort of S) = dom (the ResultSort of S) by FUNCT_2:def 1
,RELAT_1:27;
then
A6: ((the Sorts of U1) * the ResultSort of S).o = (the Sorts of U1).((the
ResultSort of S).o) by FUNCT_1:12
.= (the Sorts of U1).ro by MSUALG_1:def 2;
then reconsider dx = (Den(o,U1)).x as Element of S1.ro by MSUALG_1:def 5;
rng Den(o,U1) c= Result(o,U1) & Result(o,U1) = S1.ro by A6,MSUALG_1:def 5;
then rng Den(o,U1) c= dom QuotRes(R,o) by A6,FUNCT_2:def 1;
then
A7: dom Den(o,U1) = Args(o,U1) & dom ((QuotRes(R,o)) * Den(o,U1)) = dom
Den(o,U1 ) by FUNCT_2:def 1,RELAT_1:27;
dom (Class R) = the carrier of S by PARTFUN1:def 2;
then dom (R # x) = dom ((Class R) * (the_arity_of o)) & rng ar c= dom (
Class R) by CARD_3:9;
then dom (F#x) = dom ar & dom (R#x) = dom ar by MSUALG_3:6,RELAT_1:27;
then
A8: F # x = R # x by A3,FUNCT_1:2;
Den(o,QA) = (QuotCharact R).o by MSUALG_1:def 6
.= QuotCharact(R,o) by Def13;
then Den(o,QA).(F#x) = ((QuotRes(R,o)) * (Den(o,U1))).x by A1,A8,Def12
.= (QuotRes(R,o)) . dx by A7,FUNCT_1:12
.= Class (R, dx) by Def8
.= (MSNat_Hom(U1,R,ro)).dx by Def15
.= (F.ro).((Den(o,U1)).x) by Def16;
hence thesis;
end;
hence F is_homomorphism U1,QA;
for i be set st i in the carrier of S holds rng (F.i) = (the Sorts of QA).i
proof
let i be set;
assume i in the carrier of S;
then reconsider s = i as Element of S;
reconsider f = F.i as Function of S1.s, (the Sorts of QA).s by
PBOOLE:def 15;
A9: dom f = S1.s by FUNCT_2:def 1;
A10: (the Sorts of QA).s = Class (R.s) by Def6;
for x be object st x in (the Sorts of QA).i holds x in rng f
proof
let x be object;
A11: f = MSNat_Hom(U1,R,s) by Def16;
assume x in (the Sorts of QA).i;
then consider a1 be object such that
A12: a1 in S1.s and
A13: x = Class(R.s,a1) by A10,EQREL_1:def 3;
f.a1 in rng f by A9,A12,FUNCT_1:def 3;
hence thesis by A12,A13,A11,Def15;
end;
then (the Sorts of QA).i c= rng f;
hence thesis;
end;
hence thesis;
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;
func MSCng(F,s) -> Equivalence_Relation of (the Sorts of U1).s means
:Def17:
for x,y be Element of (the Sorts of U1).s holds [x,y] in it iff (F.s).x = (F.s)
.y;
existence
proof
defpred P[object,object] means (F.s).$1 = (F.s).$2;
set S1 = (the Sorts of U1).s;
A1: for x,y be object st P[x,y] holds P[y,x];
A2: for x,y,z be object st P[x,y] & P[y,z] holds P[x,z];
A3: for x be object st x in S1 holds P[x,x];
consider R being Equivalence_Relation of S1 such that
A4: for x,y be object holds [x,y] in R iff x in S1 & y in S1 & P[x,y]
from EQREL_1:sch 1(A3,A1,A2);
take R;
let x,y be Element of (the Sorts of U1).s;
thus thesis by A4;
end;
uniqueness
proof
let R,S be Equivalence_Relation of (the Sorts of U1).s;
assume that
A5: for x,y be Element of (the Sorts of U1).s holds [x,y] in R iff (F.
s).x = (F.s).y and
A6: for x,y be Element of (the Sorts of U1).s holds [x,y] in S iff (F.
s).x = (F.s).y;
now
let x,y be object;
thus [x,y] in R implies [x,y] in S
proof
assume
A7: [x,y] in R;
then reconsider a = x,b = y as Element of (the Sorts of U1).s by
ZFMISC_1:87;
(F.s).a = (F.s).b by A5,A7;
hence thesis by A6;
end;
assume
A8: [x,y] in S;
then reconsider a = x,b = y as Element of (the Sorts of U1).s by
ZFMISC_1:87;
(F.s).a = (F.s).b by A6,A8;
hence [x,y] in R by A5;
end;
hence thesis by RELAT_1:def 2;
end;
end;
definition
let S;
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume
A1: F is_homomorphism U1,U2;
func MSCng(F) -> MSCongruence of U1 means
:Def18:
for s be SortSymbol of S holds it.s = MSCng(F,s);
existence
proof
deffunc F(Element of S) = MSCng(F,$1);
consider f be Function such that
A2: dom f = the carrier of S & for d be Element of S holds f.d = F(d)
from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S
by A2,PARTFUN1:def 2,RELAT_1:def 18;
for i be set st i in the carrier of S holds f.i is Relation of (the
Sorts of U1).i,(the Sorts of U1).i
proof
let i be set;
assume i in the carrier of S;
then reconsider s = i as Element of S;
f.i = MSCng(F,s) by A2;
hence thesis;
end;
then reconsider f as ManySortedRelation of the Sorts of U1 by Def1;
reconsider f as ManySortedRelation of U1;
for i be set, R be Relation of (the Sorts of U1).i st i in the carrier
of S & f.i = R holds R is Equivalence_Relation of (the Sorts of U1).i
proof
let i be set, R be Relation of (the Sorts of U1).i;
assume that
A3: i in the carrier of S and
A4: f.i = R;
reconsider s = i as Element of S by A3;
R = MSCng(F,s) by A2,A4;
hence thesis;
end;
then f is MSEquivalence_Relation-like;
then reconsider f as MSEquivalence-like ManySortedRelation of U1 by Def3;
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 f.((the_arity_of o)/.n)) holds [Den(o,U1).
x,Den(o,U1).y] in f.(the_result_sort_of o)
proof
let o be OperSymbol of S, x,y be Element of Args(o,U1);
set ao = the_arity_of o, ro = the_result_sort_of o, S1 = the Sorts of U1;
A5: dom x = dom (the_arity_of o) by MSUALG_3:6;
A6: dom y = dom (the_arity_of o) by MSUALG_3:6;
assume
A7: for n be Nat st n in dom x holds [x.n,y.n] in f.((the_arity_of o)/.n);
A8: now
let n be object;
assume
A9: n in dom (the_arity_of o);
then reconsider m = n as Nat by ORDINAL1:def 12;
A10: (F#x).m = (F.(ao/.m)).(x.m) & (F#y).m = (F.(ao/.m)).(y.m) by A5,A6,A9,
MSUALG_3:def 6;
ao.m in rng ao by A9,FUNCT_1:def 3;
then reconsider s = ao.m as SortSymbol of S;
A11: n in dom (S1*ao) by A9,PARTFUN1:def 2;
then x.m in (S1*ao).n & y.m in (S1*ao).n by MSUALG_3:6;
then reconsider x1 = x.m, y1 = y.m as Element of S1.s by A11,FUNCT_1:12
;
A12: [x1,y1] in f.(ao/.m) by A7,A5,A9;
A13: ao/.m = ao.m by A9,PARTFUN1:def 6;
then f.(ao/.m) = MSCng(F,s) by A2;
hence (F#x).n = (F#y).n by A10,A13,A12,Def17;
end;
dom (F#x) = dom (the_arity_of o) & dom (F#y) = dom (the_arity_of o)
by MSUALG_3:6;
then
A14: F#x = F#y by A8,FUNCT_1:2;
reconsider ro as SortSymbol of S;
A15: dom (the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;
then
A16: dom ((the Sorts of U1)*(the ResultSort of S)) = dom (the ResultSort
of S) by PARTFUN1:def 2;
Result(o,U1) = ((the Sorts of U1) * the ResultSort of S).o by
MSUALG_1:def 5
.= (the Sorts of U1).((the ResultSort of S).o) by A15,A16,FUNCT_1:12
.= (the Sorts of U1).ro by MSUALG_1:def 2;
then reconsider
Dx = Den(o,U1).x, Dy = Den(o,U1).y as Element of (the Sorts
of U1).ro;
A17: (F.ro).Dy = Den(o,U2).(F#y) by A1;
f.ro = MSCng(F,ro) & (F.ro).Dx = Den(o,U2).(F#x) by A1,A2;
hence thesis by A14,A17,Def17;
end;
then reconsider f as MSCongruence of U1 by Def4;
take f;
thus thesis by A2;
end;
uniqueness
proof
let C1,C2 be MSCongruence of U1;
assume that
A18: for s be SortSymbol of S holds C1.s = MSCng(F,s) and
A19: for s be SortSymbol of S holds C2.s = MSCng(F,s);
now
let i be object;
assume i in the carrier of S;
then reconsider s = i as Element of S;
C1.s = MSCng(F,s) by A18;
hence C1.i = C2.i by A19;
end;
hence thesis by PBOOLE:3;
end;
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
A1: 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
:Def19:
for x be Element of (the Sorts of U1).s
holds it.(Class(MSCng(F,s),x)) = (F.s).x;
existence
proof
set qa = QuotMSAlg (U1,MSCng F), cqa = the Sorts of qa, S1 = the Sorts of
U1, S2 = the Sorts of U2;
defpred P[object,object] means
for a be Element of S1.s st $1 = Class(MSCng(F,s)
,a) holds $2 = (F.s).a;
A2: cqa.s = Class ((MSCng(F)).s) by Def6
.= Class (MSCng(F,s)) by A1,Def18;
A3: for x be object st x in cqa.s ex y be object st y in S2.s & P[x,y]
proof
let x be object;
assume
A4: x in cqa.s;
then reconsider x1 = x as Subset of S1.s by A2;
consider a be object such that
A5: a in S1.s and
A6: x1 = Class(MSCng(F,s),a) by A2,A4,EQREL_1:def 3;
reconsider a as Element of S1.s by A5;
take y = (F.s).a;
thus y in S2.s;
let b be Element of S1.s;
assume x = Class(MSCng(F,s),b);
then b in Class(MSCng(F,s),a) by A6,EQREL_1:23;
then [b,a] in MSCng(F,s) by EQREL_1:19;
hence thesis by Def17;
end;
consider G being Function such that
A7: dom G = cqa.s & rng G c= S2.s & for x be object st x in cqa.s holds
P[x,G.x] from FUNCT_1:sch 6(A3);
reconsider G as Function of cqa.s,S2.s by A7,FUNCT_2:def 1,RELSET_1:4;
take G;
let a be Element of S1.s;
Class(MSCng(F,s),a) in Class MSCng(F,s) by EQREL_1:def 3;
hence thesis by A2,A7;
end;
uniqueness
proof
set qa = QuotMSAlg (U1, MSCng F), cqa = the Sorts of qa, u1 = the Sorts of
U1, u2 = the Sorts of U2;
let H,G be Function of cqa.s,u2.s;
assume that
A8: for a be Element of u1.s holds H.(Class(MSCng(F,s),a)) = (F.s).a and
A9: for a be Element of u1.s holds G.(Class(MSCng(F,s),a)) = (F.s).a;
A10: cqa.s = Class ((MSCng(F)).s) by Def6
.= Class (MSCng(F,s)) by A1,Def18;
for x be object st x in cqa.s holds H.x = G.x
proof
let x be object;
assume
A11: x in cqa.s;
then reconsider x1 = x as Subset of u1.s by A10;
consider a be object such that
A12: a in u1.s and
A13: x1 = Class(MSCng(F,s),a) by A10,A11,EQREL_1:def 3;
reconsider a as Element of u1.s by A12;
thus H.x = (F.s).a by A8,A13
.= G.x by A9,A13;
end;
hence thesis by FUNCT_2:12;
end;
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
:Def20:
for s be SortSymbol of S holds it.s = MSHomQuot(F,s);
existence
proof
deffunc G(Element of S)= MSHomQuot(F,$1);
consider f be Function such that
A1: dom f = the carrier of S & for d be Element of S holds f.d = G(d)
from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2
,RELAT_1:def 18;
for x be object st x in dom f holds f.x is Function
proof
let x be object;
assume x in dom f;
then reconsider y = x as Element of S;
f.y = MSHomQuot(F,y) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of the carrier of S by
FUNCOP_1:def 6;
for i be object st i in the carrier of S holds f.i is Function of (the
Sorts of QuotMSAlg (U1, MSCng F)).i, (the Sorts of U2).i
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as Element of S;
f.s = MSHomQuot(F,s) by A1;
hence thesis;
end;
then reconsider
f as ManySortedFunction of the Sorts of QuotMSAlg (U1,MSCng F),
the Sorts of U2 by PBOOLE:def 15;
reconsider f as ManySortedFunction of QuotMSAlg (U1,MSCng F),U2;
take f;
thus thesis by A1;
end;
uniqueness
proof
let H,G be ManySortedFunction of QuotMSAlg (U1,MSCng F),U2;
assume that
A2: for s be SortSymbol of S holds H.s = MSHomQuot(F,s) and
A3: for s be SortSymbol of S holds G.s = MSHomQuot(F,s);
now
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
H.s = MSHomQuot(F,s) by A2;
hence H.i = G.i by A3;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem Th4:
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
proof
let U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1,U2;
set mc = MSCng(F), qa = QuotMSAlg (U1,mc), qh = MSHomQuot(F), S1 = the Sorts
of U1;
assume
A1: F is_homomorphism U1,U2;
for o be OperSymbol of S st Args (o,qa) <> {} for x be Element of Args(o
,qa) holds (qh.(the_result_sort_of o)).(Den(o,qa).x) = Den(o,U2).(qh#x)
proof
let o be OperSymbol of S such that
Args (o,qa) <> {};
let x be Element of Args(o,qa);
set ro = the_result_sort_of o, ar = the_arity_of o;
A2: dom x = dom ar by MSUALG_3:6;
Args(o,qa) = ((Class mc)# * (the Arity of S)).o by MSUALG_1:def 4;
then consider a be Element of Args(o,U1) such that
A3: x = mc # a by Th2;
A4: dom a = dom ar by MSUALG_3:6;
A5: now
let y be object;
assume
A6: y in dom ar;
then reconsider n = y as Nat by ORDINAL1:def 12;
ar.n in rng ar by A6,FUNCT_1:def 3;
then reconsider s = ar.n as SortSymbol of S;
A7: ar/.n = ar.n by A6,PARTFUN1:def 6;
then x.n = Class(mc.s,a.n) by A3,A6,Def7;
then
A8: x.n = Class(MSCng(F,s),a.n) by A1,Def18;
A9: n in dom (S1 * ar) by A6,PARTFUN1:def 2;
then a.n in (S1 * ar).n by MSUALG_3:6;
then reconsider an = a.n as Element of S1.s by A9,FUNCT_1:12;
(qh # x).n = (qh.s).(x.n) by A2,A6,A7,MSUALG_3:def 6
.= MSHomQuot(F,s).(x.n) by Def20
.= (F.s).an by A1,A8,Def19
.= (F # a).n by A4,A6,A7,MSUALG_3:def 6;
hence (qh # x).y = (F # a).y;
end;
o in the carrier' of S;
then o in dom (S1 * the ResultSort of S) by PARTFUN1:def 2;
then
A10: ((the Sorts of U1) * the ResultSort of S).o = (the Sorts of U1).((the
ResultSort of S).o) by FUNCT_1:12
.= (the Sorts of U1).ro by MSUALG_1:def 2;
then rng Den(o,U1) c= Result(o,U1) & Result(o,U1) = S1.ro by MSUALG_1:def 5
;
then rng Den(o,U1) c= dom QuotRes(mc,o) by A10,FUNCT_2:def 1;
then
A11: dom Den(o,U1) = Args(o,U1) & dom ((QuotRes(mc,o)) * Den(o,U1)) = dom
Den(o, U1) by FUNCT_2:def 1,RELAT_1:27;
ar = (the Arity of S).o by MSUALG_1:def 1;
then
A12: product((Class mc) * ar) = ((Class mc)# * the Arity of S).o by MSAFREE:1;
reconsider da = (Den(o,U1)).a as Element of S1.ro by A10,MSUALG_1:def 5;
A13: qh.ro = MSHomQuot(F,ro) by Def20;
Den(o,qa) = (QuotCharact mc).o by MSUALG_1:def 6
.= QuotCharact(mc,o) by Def13;
then Den(o,qa).x = (QuotRes(mc,o) * Den(o,U1)).a by A3,A12,Def12
.= (QuotRes(mc,o)) . da by A11,FUNCT_1:12
.= Class (mc, da) by Def8
.= Class (MSCng(F,ro),da) by A1,Def18;
then
A14: (qh.ro).(Den(o,qa).x) = (F.ro).((Den(o,U1)).a) by A1,A13,Def19
.= Den(o,U2).(F#a) by A1;
dom (qh # x) = dom ar & dom (F # a) = dom ar by MSUALG_3:6;
hence thesis by A5,A14,FUNCT_1:2;
end;
hence qh is_homomorphism qa,U2;
for i be set st i in the carrier of S holds (qh.i) is one-to-one
proof
let i be set;
set f = qh.i;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A15: f = MSHomQuot(F,s) by Def20;
for x1,x2 be object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be object;
assume that
A16: x1 in dom f and
A17: x2 in dom f and
A18: f.x1 = f.x2;
x1 in (Class mc).s by A15,A16,FUNCT_2:def 1;
then x1 in Class (mc.s) by Def6;
then consider a1 be object such that
A19: a1 in S1.s and
A20: x1 = Class(mc.s,a1) by EQREL_1:def 3;
x2 in (Class mc).s by A15,A17,FUNCT_2:def 1;
then x2 in Class (mc.s) by Def6;
then consider a2 be object such that
A21: a2 in S1.s and
A22: x2 = Class(mc.s,a2) by EQREL_1:def 3;
reconsider a2 as Element of S1.s by A21;
A23: mc.s = MSCng(F,s) by A1,Def18;
then
A24: f.x2 = (F.s).a2 by A1,A15,A22,Def19;
reconsider a1 as Element of S1.s by A19;
f.x1 = (F.s).a1 by A1,A15,A23,A20,Def19;
then [a1,a2] in MSCng(F,s) by A18,A24,Def17;
hence thesis by A23,A20,A22,EQREL_1:35;
end;
hence thesis by FUNCT_1:def 4;
end;
hence thesis by MSUALG_3:1;
end;
theorem Th5:
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
proof
let U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1,U2;
set mc = MSCng(F), qa = QuotMSAlg (U1,mc), qh = MSHomQuot(F);
set Sq = the Sorts of qa, S1 = the Sorts of U1, S2 = the Sorts of U2;
assume
A1: F is_epimorphism U1,U2;
then
A2: F is_homomorphism U1,U2;
A3: F is "onto" by A1;
for i be set st i in the carrier of S holds rng (qh.i) = S2.i
proof
let i be set;
set f = qh.i;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A4: rng (F.s) = S2.s by A3;
A5: qh.i = MSHomQuot(F,s) by Def20;
hence rng f c= S2.i by RELAT_1:def 19;
let x be object;
assume x in S2.i;
then consider a be object such that
A6: a in dom (F.s) and
A7: (F.s).a = x by A4,FUNCT_1:def 3;
A8: MSCng(F,s) = (MSCng(F)).s & Sq.s = Class ((MSCng(F)).s) by A2,Def6,Def18;
reconsider a as Element of S1.s by A6;
dom f = Sq.s by A5,FUNCT_2:def 1;
then
A9: Class(MSCng(F,s),a) in dom f by A8,EQREL_1:def 3;
f.(Class(MSCng(F,s),a)) = x by A2,A5,A7,Def19;
hence thesis by A9,FUNCT_1:def 3;
end;
then
A10: qh is "onto";
qh is_monomorphism qa,U2 by A2,Th4;
then qh is_homomorphism qa,U2 & qh is "1-1";
hence thesis by A10,MSUALG_3:13;
end;
theorem
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
proof
let U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1,U2;
assume F is_epimorphism U1,U2;
then MSHomQuot(F) is_isomorphism QuotMSAlg (U1,MSCng F),U2 by Th5;
hence thesis;
end;