:: The Correspondence Between Lattices of Subalgebras of Universal
:: Algebras and Many Sorted Algebras
:: by Adam Naumowicz and Agnieszka Julia Marasik
::
:: Received September 22, 1998
:: Copyright (c) 1998-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 NAT_1, PBOOLE, FUNCT_1, CARD_1, XBOOLE_0, FINSEQ_2, FINSEQ_1,
RELAT_1, TARSKI, NUMBERS, SUBSET_1, UNIALG_1, UNIALG_2, MSUALG_1,
FUNCOP_1, CQC_SIM1, STRUCT_0, MSUALG_2, MARGREL1, PARTFUN1, CARD_3,
FUNCT_2, ZFMISC_1, EQREL_1, INCPROJ, WELLORD1, GROUP_6, LATTICES,
SETLIM_2, LATTICE4;
notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, CARD_3, ORDINAL1, LATTICES,
LATTICE4, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, STRUCT_0,
PBOOLE, UNIALG_1, UNIALG_2, NUMBERS, FINSEQ_1, FINSEQ_2, MARGREL1,
MSUALG_1, MSUALG_2;
constructors BINOP_1, FINSEQOP, FILTER_1, UNIALG_2, LATTICE4, MSUALG_2,
RELSET_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSEQ_2,
RELAT_1, PBOOLE, STRUCT_0, UNIALG_1, UNIALG_2, MSUALG_1, MSUALG_2,
FINSEQ_1, MARGREL1;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, MSUALG_2, PBOOLE, LATTICE4, UNIALG_2, FUNCT_2;
equalities MSUALG_2, UNIALG_2, FUNCOP_1, FINSEQ_2, ORDINAL1;
expansions TARSKI, XBOOLE_0, MSUALG_2, PBOOLE, UNIALG_1, UNIALG_2, FUNCT_2;
theorems MSUALG_1, MSUALG_2, PBOOLE, TARSKI, UNIALG_1, UNIALG_2, FUNCT_1,
RELAT_1, FUNCOP_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3,
ZFMISC_1, CARD_3, LATTICES, MSUHOM_1, XBOOLE_0, XBOOLE_1, STRUCT_0,
MARGREL1, CARD_1;
schemes FUNCT_2;
begin
:: Preliminaries
reserve a for set,
i for Nat;
theorem Th1:
(*-->a).0 = {}
proof
thus (*-->a).0 = 0 |-> a by FINSEQ_2:def 6
.= {};
end;
theorem
(*-->a).1 = <*a*>
proof
thus (*-->a).1 = 1 |-> a by FINSEQ_2:def 6
.= <*a*> by FINSEQ_2:59;
end;
theorem
(*-->a).2 = <*a,a*>
proof
thus (*-->a).2 = 2 |-> a by FINSEQ_2:def 6
.= <*a,a*> by FINSEQ_2:61;
end;
theorem
(*-->a).3 = <*a,a,a*>
proof
thus (*-->a).3 = 3 |-> a by FINSEQ_2:def 6
.= <*a,a,a*> by FINSEQ_2:62;
end;
theorem Th5:
for f being FinSequence of {0} holds f = i |-> 0 iff len f = i
proof
let f be FinSequence of {0};
thus f = i |-> 0 implies len f = i by CARD_1:def 7;
assume len f = i;
then
A1: dom f = Seg i by FINSEQ_1:def 3;
per cases;
suppose
A2: Seg i = {};
hence f = {} by A1
.= 0 |-> 0
.= i |-> 0 by A2;
end;
suppose
A3: Seg i <> {};
rng f c= {0} by FINSEQ_1:def 4;
then rng f = {0} or rng f = {} by ZFMISC_1:33;
hence thesis by A1,A3,FUNCOP_1:9,RELAT_1:42;
end;
end;
theorem Th6:
for f be FinSequence st f = (*-->0).i holds len f = i
proof
let p be FinSequence;
assume
A1: p = (*-->0).i;
p = i |-> 0 by A1,FINSEQ_2:def 6;
hence thesis by CARD_1:def 7;
end;
begin
:: Some Properties of Subalgebras of Universal and Many Sorted Algebras
reconsider z = 0 as Element of {0} by TARSKI:def 1;
theorem Th7:
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
MSSign U1 = MSSign U2
proof
let U1,U2 be Universal_Algebra;
set ff2 = dom signature(U1)-->z, gg2 = dom signature(U2)-->z;
reconsider ff1 = (*-->0)*(signature U1) as Function of dom signature(U1), {0
}* by MSUALG_1:2;
reconsider gg1 = (*-->0)*(signature U2) as Function of dom signature(U2), {0
}* by MSUALG_1:2;
assume U1 is SubAlgebra of U2;
then
A1: U1,U2 are_similar by UNIALG_2:13;
A2: MSSign U1 = ManySortedSign (#{0},dom signature(U1),ff1,ff2#) & MSSign U2
= ManySortedSign (#{0},dom signature(U2),gg1,gg2#) by MSUALG_1:10;
thus thesis by A1,A2;
end;
theorem Th8:
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 for B
being MSSubset of MSAlg U2 st B = the Sorts of MSAlg U1 for o being OperSymbol
of MSSign U2 for a being OperSymbol of MSSign U1 st a = o holds Den(a,MSAlg U1)
= Den(o,MSAlg U2)|Args(a,MSAlg U1)
proof
let U1,U2 be Universal_Algebra such that
A1: U1 is SubAlgebra of U2;
A2: MSSign U1 = MSSign U2 by A1,Th7;
A3: MSSign U1 = MSSign U2 by A1,Th7;
let B be MSSubset of MSAlg U2 such that
A4: B = the Sorts of MSAlg U1;
let o be OperSymbol of MSSign U2;
reconsider a = o as Element of the carrier' of MSSign U1 by A1,Th7;
set X = Args(a,MSAlg U1);
set Y = dom Den(a,MSAlg U1);
the Sorts of MSAlg U2 is MSSubset of MSAlg U2 & B c= the Sorts of MSAlg
U2 by PBOOLE:def 18;
then
A5: (B# * the Arity of MSSign U1).a c= ((the Sorts of MSAlg U2)#* the Arity
of MSSign U2).o by A3,MSUALG_2:2;
dom Den(o,MSAlg U2) = Args(o,MSAlg U2) & Args(o,MSAlg U2) = ((the Sorts
of MSAlg U2)#*the Arity of MSSign U2).o by FUNCT_2:def 1,MSUALG_1:def 4;
then Args(a,MSAlg U1) c= dom Den(o,MSAlg U2) by A4,A2,A5,MSUALG_1:def 4;
then dom (Den(o,MSAlg U2)|Args(a,MSAlg U1)) = Args(a,MSAlg U1) by RELAT_1:62;
then dom (Den(o,MSAlg U2)|Args(a,MSAlg U1)) = dom Den(a,MSAlg U1) by
FUNCT_2:def 1;
then
A6: Y = dom Den(o,MSAlg U2) /\ X by RELAT_1:61;
for x being object st x in Y
holds (Den(o,MSAlg U2)).x = (Den(a,MSAlg U1 ) ) . x
proof
MSAlg U1 = MSAlgebra(#MSSorts U1,MSCharact U1#) by MSUALG_1:def 11;
then the Sorts of MSAlg U1 = 0.-->the carrier of U1 by MSUALG_1:def 9;
then rng(the Sorts of MSAlg U1) = {the carrier of U1} by FUNCOP_1:8;
then
A7: the carrier of U1 is Component of the Sorts of MSAlg U1 by TARSKI:def 1;
reconsider cc = the carrier of U1 as non empty Subset of U2 by A1,
UNIALG_2:def 7;
let x be object;
A8: MSAlg U2 = MSAlgebra(#MSSorts U2,MSCharact U2#) by MSUALG_1:def 11;
U1,U2 are_similar by A1,UNIALG_2:13;
then
A9: signature(U1)=signature(U2);
assume x in Y;
then x in X by A6,XBOOLE_0:def 4;
then x in (len the_arity_of a)-tuples_on the_sort_of MSAlg U1 by MSUALG_1:6
;
then
A10: x in (len the_arity_of a)-tuples_on the carrier of U1 by A7,
MSUALG_1:def 12;
reconsider gg1 = (*-->0)*(signature U2) as Function of dom signature(U2),
{0}* by MSUALG_1:2;
set ff1 = (*-->0)*(signature U1), ff2 = dom signature(U1)-->z, gg2 = dom
signature(U2)-->z;
reconsider ff1 as Function of dom signature(U1), {0}* by MSUALG_1:2;
consider n being Nat such that
A11: dom (signature (U2)) = Seg n by FINSEQ_1:def 2;
A12: MSSign U2 = ManySortedSign (#{0},dom signature(U2),gg1,gg2#) by
MSUALG_1:10;
then
A13: a in Seg n by A11;
A14: dom (the charact of U2) = Seg (len(the charact of U2)) by FINSEQ_1:def 3
.= Seg (len(signature (U2))) by UNIALG_1:def 4
.= dom signature(U2) by FINSEQ_1:def 3;
then reconsider op = (the charact of U2).a as operation of U2 by A12,
FUNCT_1:def 3;
reconsider a as Element of NAT by A13;
A15: rng (signature U1) c= NAT by FINSEQ_1:def 4;
U1,U2 are_similar by A1,UNIALG_2:13;
then
A16: signature(U1)=signature(U2);
then
A17: (signature U1).a in rng (signature U1) by A12,FUNCT_1:def 3;
then reconsider sig=(signature U1).a as Element of NAT by A15;
dom (*-->0) = NAT by FUNCT_2:def 1;
then MSSign U1= ManySortedSign (#{0},dom signature(U1),ff1,ff2#) & a in
dom (( *-->0)*(signature U1)) by A12,A16,A17,A15,FUNCT_1:11,MSUALG_1:10;
then (the Arity of MSSign U1).a = (*-->0).((signature U1).a) by FUNCT_1:12;
then
A18: (the Arity of MSSign U1).a = sig |-> 0 by FINSEQ_2:def 6;
reconsider ar = (the Arity of MSSign U1).a as FinSequence;
x in (len ar)-tuples_on the carrier of U1 by A10,MSUALG_1:def 1;
then x in (sig)-tuples_on the carrier of U1 by A18,CARD_1:def 7;
then
A19: x in ((arity op)-tuples_on the carrier of U1) by A12,A9,UNIALG_1:def 4;
for n being object st n in dom Opers(U2,cc)
holds (Opers(U2,cc)).n is Function;
then reconsider f = Opers(U2,cc) as Function-yielding Function
by FUNCOP_1:def 6;
cc is opers_closed by A1,UNIALG_2:def 7;
then
A20: cc is_closed_on op;
a in dom the charact of U2 by A12,A14;
then
A21: o in dom(Opers(U2,cc)) by UNIALG_2:def 6;
reconsider a as OperSymbol of MSSign U1;
MSAlg U1 = MSAlgebra(#MSSorts U1,MSCharact U1#) by MSUALG_1:def 11;
then (Den(a,MSAlg U1)).x = ((MSCharact U1).o).x by MSUALG_1:def 6
.= ((the charact of U1).o).x by MSUALG_1:def 10
.= (f.o).x by A1,UNIALG_2:def 7
.= (op/.cc).x by A21,UNIALG_2:def 6
.= (op|(arity op)-tuples_on cc).x by A20,UNIALG_2:def 5
.= ((the charact of U2).o).x by A19,FUNCT_1:49
.= ((the Charact of MSAlg U2).o).x by A8,MSUALG_1:def 10
.= (Den(o,MSAlg U2)).x by MSUALG_1:def 6;
hence thesis;
end;
hence thesis by A6,FUNCT_1:46;
end;
theorem Th9:
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
the Sorts of MSAlg U1 is MSSubset of MSAlg U2
proof
let U1,U2 be Universal_Algebra;
set gg1 = (*-->0)*(signature U2), gg2 = dom signature(U2)-->z;
reconsider gg1 as Function of dom signature(U2), {0}* by MSUALG_1:2;
A1: MSSign U2 = ManySortedSign (#{0},dom signature(U2),gg1,gg2#) by MSUALG_1:10
;
MSAlg U2 = MSAlgebra(#MSSorts U2,MSCharact U2#) by MSUALG_1:def 11;
then
A2: the Sorts of MSAlg U2 = 0 .--> the carrier of U2 by MSUALG_1:def 9;
assume
A3: U1 is SubAlgebra of U2;
then MSSign U1 = MSSign U2 by Th7;
then reconsider A = MSAlg U1 as non-empty MSAlgebra over MSSign U2;
MSAlg U1 = MSAlgebra(#MSSorts U1,MSCharact U1#) by MSUALG_1:def 11;
then
A4: the Sorts of A = 0 .--> the carrier of U1 by MSUALG_1:def 9;
A5: 0 in {0} by TARSKI:def 1;
A6: the carrier of U1 is Subset of U2 by A3,UNIALG_2:def 7;
the Sorts of A c= the Sorts of MSAlg U2
proof
let i be object;
assume i in the carrier of MSSign U2;
then
A7: i = 0 by A1,TARSKI:def 1;
(the Sorts of A).0 = the carrier of U1 & (the Sorts of MSAlg U2).0 =
the carrier of U2 by A4,A2,A5,FUNCOP_1:7;
hence thesis by A6,A7;
end;
hence thesis by PBOOLE:def 18;
end;
theorem Th10:
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 for
B being MSSubset of MSAlg U2 st B = the Sorts of MSAlg U1 holds B is
opers_closed
proof
let U1,U2 be Universal_Algebra such that
A1: U1 is SubAlgebra of U2;
let B be MSSubset of MSAlg U2 such that
A2: B = the Sorts of MSAlg U1;
let o be OperSymbol of MSSign U2;
reconsider a = o as Element of the carrier' of MSSign U1 by A1,Th7;
set S = (B * the ResultSort of MSSign U2).a;
S = ((the Sorts of MSAlg U1) * the ResultSort of MSSign U1).a by A1,A2,Th7;
then
A3: S = Result(a,MSAlg U1) by MSUALG_1:def 5;
set Z = rng ((Den(o,MSAlg U2))|((B# * the Arity of MSSign U2).a));
MSSign U1 = MSSign U2 by A1,Th7;
then
rng Den(a,MSAlg U1) c= Result(a,MSAlg U1) & Z = rng ((Den(o,MSAlg U2))|(
Args (a,MSAlg U1))) by A2,MSUALG_1:def 4,RELAT_1:def 19;
then Z c= Result (a,MSAlg U1) by A1,A2,Th8;
hence thesis by A3;
end;
theorem Th11:
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 for
B being MSSubset of MSAlg U2 st B = the Sorts of MSAlg U1 holds the Charact of
MSAlg U1 = Opers(MSAlg U2,B)
proof
let U1,U2 be Universal_Algebra such that
A1: U1 is SubAlgebra of U2;
let B be MSSubset of MSAlg U2;
set f1 = the Charact of MSAlg U1, f2 = Opers(MSAlg U2,B);
the carrier' of MSSign U1 = the carrier' of MSSign U2
proof
set ff1 = (*-->0)*(signature U1), ff2 = dom signature(U1)-->z, gg1 = (*-->
0)*(signature U2), gg2 = dom signature(U2)-->z;
reconsider ff1 as Function of dom signature(U1), {0}* by MSUALG_1:2;
reconsider gg1 as Function of dom signature(U2), {0}* by MSUALG_1:2;
A2: MSSign U2 = ManySortedSign (#{0},dom signature(U2),gg1,gg2#) by MSUALG_1:10
;
U1,U2 are_similar & MSSign U1 = ManySortedSign (#{0},dom signature(U1)
,ff1, ff2#) by A1,MSUALG_1:10,UNIALG_2:13;
hence thesis by A2;
end;
then reconsider f1 as ManySortedSet of the carrier' of MSSign U2;
assume
A3: B = the Sorts of MSAlg U1;
for x being object st x in the carrier' of MSSign U2 holds f1.x = f2. x
proof
let x be object;
assume
A4: x in (the carrier' of MSSign U2);
then reconsider y = x as OperSymbol of MSSign U2;
reconsider x as OperSymbol of MSSign U1 by A1,A4,Th7;
B is opers_closed by A1,A3,Th10;
then f2.y = y/.B & B is_closed_on y by MSUALG_2:def 8;
then
A5: f2.y = Den(y,MSAlg U2) | ((B# * the Arity of MSSign U2).y) by
MSUALG_2:def 7;
(B# * the Arity of MSSign U1).x = ((the Sorts of MSAlg U1)# * the
Arity of MSSign U1).x by A1,A3,Th7;
then f2.y = Den(y,MSAlg U2)| (((the Sorts of MSAlg U1)# * the Arity of
MSSign U1).x) by A1,A5,Th7;
then f1.x = Den(x,MSAlg U1) & f2.y = (Den(y,MSAlg U2))|(Args(x,MSAlg U1))
by MSUALG_1:def 4,def 6;
hence thesis by A1,A3,Th8;
end;
hence thesis by PBOOLE:3;
end;
theorem Th12:
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2
holds MSAlg U1 is MSSubAlgebra of MSAlg U2
proof
let U1,U2 be Universal_Algebra;
assume
A1: U1 is SubAlgebra of U2;
then MSSign U1 = MSSign U2 by Th7;
then reconsider A = MSAlg U1 as non-empty MSAlgebra over MSSign U2;
A is MSSubAlgebra of MSAlg U2
proof
thus the Sorts of A is MSSubset of MSAlg U2 by A1,Th9;
let B be MSSubset of MSAlg U2;
assume
A2: B = the Sorts of A;
hence B is opers_closed by A1,Th10;
thus thesis by A1,A2,Th11;
end;
hence thesis;
end;
theorem Th13:
for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of
MSAlg U2 holds the carrier of U1 is Subset of U2
proof
let U1,U2 be Universal_Algebra;
set MU1 = MSAlg U1, MU2 = MSAlg U2;
assume
A1: MU1 is MSSubAlgebra of MU2;
then reconsider MU1 as MSAlgebra over MSSign U2;
reconsider C = the Sorts of MU1 as MSSubset of MU2 by A1,MSUALG_2:def 9;
set gg1 = (*-->0)*(signature U2), gg2 = dom signature(U2)-->z;
reconsider gg1 as Function of dom signature(U2), {0}* by MSUALG_1:2;
reconsider C1 = C as ManySortedSet of the carrier of MSSign U2;
A2: 0 in {0} by TARSKI:def 1;
MU2 = MSAlgebra(#MSSorts U2,MSCharact U2#) by MSUALG_1:def 11;
then
A3: C1 c= MSSorts U2 by PBOOLE:def 18;
MSSign U2 = ManySortedSign (#{0},dom signature(U2),gg1,gg2#) & MSSorts
U2 = 0.-->the carrier of U2 by MSUALG_1:10,def 9;
then
MU1 = MSAlgebra(#MSSorts U1,MSCharact U1#) & C1.0 c= ({0}-->the carrier
of U2).0 by A3,MSUALG_1:def 11;
then (MSSorts U1).0 c= the carrier of U2 by A2,FUNCOP_1:7;
then (0.-->the carrier of U1).0 c= the carrier of U2 by MSUALG_1:def 9;
hence thesis by A2,FUNCOP_1:7;
end;
theorem Th14:
for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of
MSAlg U2 for B being non empty Subset of U2 st B=the carrier of U1 holds B is
opers_closed
proof
let U1,U2 be Universal_Algebra;
set MU1 = MSAlg U1, MU2 = MSAlg U2;
A1: MU2 = MSAlgebra(#MSSorts U2,MSCharact U2#) by MSUALG_1:def 11;
assume
A2: MU1 is MSSubAlgebra of MU2;
then reconsider MU1 as MSAlgebra over MSSign U2;
let B be non empty Subset of U2;
assume
A3: B = the carrier of U1;
let o be operation of U2;
reconsider C = the Sorts of MU1 as MSSubset of MU2 by A2,MSUALG_2:def 9;
A4: MU1 = MSAlgebra(#MSSorts U1,MSCharact U1#) by MSUALG_1:def 11;
set gg1 = (*-->0)*(signature U2), gg2 = dom signature(U2)-->z;
reconsider gg1 as Function of dom signature(U2), {0}* by MSUALG_1:2;
A5: MSSign U2 = ManySortedSign (#{0},dom signature(U2),gg1,gg2#) by MSUALG_1:10
;
A6: C is opers_closed by A2,MSUALG_2:def 9;
thus B is_closed_on o
proof
A7: 0 in {0} by TARSKI:def 1;
let s be FinSequence of B;
consider n being object such that
A8: n in dom the charact of U2 and
A9: o = (the charact of U2).n by FUNCT_1:def 3;
A10: dom the charact of U2 = Seg (len (the charact of U2)) & dom signature
U2 = Seg (len (signature U2)) by FINSEQ_1:def 3;
then
A11: n in dom signature U2 by A8,UNIALG_1:def 4;
reconsider n as OperSymbol of MSSign U2 by A5,A8,A10,UNIALG_1:def 4;
assume
A12: len s = arity o;
ex y being set st y in dom ((Den(n,MU2))|((C# * the Arity of MSSign
U2).n)) & ((Den(n,MU2))|((C# * the Arity of MSSign U2).n)).y = o.s
proof
take s;
thus s in dom ((Den(n,MU2))|((C# * the Arity of MSSign U2).n))
proof
(arity o) |-> 0 is FinSequence of the carrier of MSSign U2 by A5,
FINSEQ_2:63;
then reconsider
ao0 = (arity o) |-> 0 as Element of (the carrier of MSSign
U2)* by FINSEQ_1:def 11;
A13: now
assume Seg arity(o) = {};
then (arity(o) |-> 0) = <*>the carrier of MSSign U2;
hence (arity(o) |-> 0) is FinSequence of the carrier of MSSign U2;
end;
Seg arity(o) <> {} implies dom (arity(o) |-> 0) = Seg arity(o) &
rng (arity(o) |-> 0) c= the carrier of MSSign U2 by A5,FUNCOP_1:13;
then
arity(o) |-> 0 is FinSequence of the carrier of MSSign U2 by A13,
FINSEQ_1:def 4;
then reconsider
aro = arity(o) |-> 0 as Element of (the carrier of MSSign
U2)* by FINSEQ_1:def 11;
A14: dom the Arity of MSSign U2 = the carrier' of MSSign U2 by FUNCT_2:def 1
;
the Sorts of MU2 = 0.-->the carrier of U2 by A1,MSUALG_1:def 9;
then
A15: (the Sorts of MU2)*aro = arity(o) |-> the carrier of U2 by FINSEQ_2:144
.= Seg arity(o) --> the carrier of U2;
dom s = Seg arity(o) by A12,FINSEQ_1:def 3;
then
A16: dom s = dom ((the Sorts of MU2)*aro) by A15;
A17: for x being object st x in dom ((the Sorts of MU2)*aro) holds s.x in
((the Sorts of MU2)*aro).x
proof
let x be object;
rng s c= B by FINSEQ_1:def 4;
then
A18: rng s c= the carrier of U2 by XBOOLE_1:1;
assume
A19: x in dom ((the Sorts of MU2)*aro);
s.x in rng s by A16,A19,FUNCT_1:def 3;
then
A20: 0 in {0} & s.x in the carrier of U2 by A18,TARSKI:def 1;
((the Sorts of MU2)*aro).x = (the Sorts of MU2).(aro.x) by A19,
FUNCT_1:12
.= (MSSorts U2).0 by A1
.= (0 .--> the carrier of U2).0 by MSUALG_1:def 9;
hence thesis by A20,FUNCOP_1:7;
end;
dom Den (n,MU2) = Args(n,MU2) by FUNCT_2:def 1;
then
dom Den(n,MU2) = ((the Sorts of MU2)# * the Arity of MSSign U2).n
by MSUALG_1:def 4
.=(the Sorts of MU2)#.(((*-->0)*(signature U2)).n) by A5,A14,
FUNCT_1:13
.=(the Sorts of MU2)#.((*-->0).((signature U2).n)) by A11,FUNCT_1:13
.=(the Sorts of MU2)#.((*-->0).(arity(o))) by A9,A11,UNIALG_1:def 4
.=(the Sorts of MU2)#.(arity(o) |-> 0) by FINSEQ_2:def 6;
then dom Den(n,MU2) = product((the Sorts of MU2)*aro) by FINSEQ_2:def 5
;
then
A21: s in dom Den(n,MU2) by A16,A17,CARD_3:def 5;
A22: s is Element of (len s)-tuples_on B by FINSEQ_2:92;
A23: 0 in {0} by TARSKI:def 1;
A24: n in dom signature U2 by A8,A10,UNIALG_1:def 4;
A25: C = 0 .--> the carrier of U1 by A4,MSUALG_1:def 9;
then dom C = {0};
then
A26: 0 in dom C by TARSKI:def 1;
dom *-->0 = NAT & (signature U2).n = arity o by A9,A11,FUNCT_2:def 1
,UNIALG_1:def 4;
then
A27: n in dom ((*-->0)*(signature U2)) by A24,FUNCT_1:11;
then
(C# * the Arity of MSSign U2).n = C#.(((*-->0)*(signature U2)).n)
by A5,FUNCT_1:13
.= C#.((*-->0).((signature U2).n)) by A27,FUNCT_1:12
.= C#.((*-->0).(arity o)) by A9,A24,UNIALG_1:def 4
.= C#.((arity o) |-> 0) by FINSEQ_2:def 6;
then (C# * the Arity of MSSign U2).n = product(C*ao0) by FINSEQ_2:def 5
.= product(Seg (arity o) --> C.0) by A26,FUNCOP_1:17
.= product(Seg (arity o) --> B) by A3,A25,A23,FUNCOP_1:7
.= Funcs(Seg (arity o),B) by CARD_3:11
.= (arity o)-tuples_on B by FINSEQ_2:93;
then s in (dom Den(n,MU2)) /\ (C# * the Arity of MSSign U2).n by A12
,A21,A22,XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
hence ((Den(n,MU2))|((C# * the Arity of MSSign U2).n)).s = Den(n,MU2).s
by FUNCT_1:47
.= ((MSCharact U2).n).s by A1,MSUALG_1:def 6
.= o.s by A9,MSUALG_1:def 10;
end;
then
A28: o.s in rng ((Den(n,MU2))|((C# * the Arity of MSSign U2).n)) by
FUNCT_1:def 3;
C is_closed_on n by A6;
then
A29: rng ((Den(n,MU2))|((C# * the Arity of MSSign U2).n)) c= (C * the
ResultSort of MSSign U2).n;
n in dom (dom signature(U2)-->0) by A11;
then (C * the ResultSort of MSSign U2).n = C.((dom signature(U2)-->0).n)
by A5,FUNCT_1:13
.= (the Sorts of MU1).0
.= (0.-->the carrier of U1).0 by A4,MSUALG_1:def 9
.= B by A3,A7,FUNCOP_1:7;
hence thesis by A29,A28;
end;
end;
theorem Th15:
for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of
MSAlg U2 for B being non empty Subset of U2 st B=the carrier of U1 holds the
charact of U1 = Opers(U2,B)
proof
let U1,U2 be Universal_Algebra;
set MU1 = MSAlg U1, MU2 = MSAlg U2;
A1: MU2 = MSAlgebra(#MSSorts U2,MSCharact U2#) by MSUALG_1:def 11;
assume
A2: MU1 is MSSubAlgebra of MU2;
then reconsider MU1 as MSAlgebra over MSSign U2;
reconsider C = the Sorts of MU1 as MSSubset of MU2 by A2,MSUALG_2:def 9;
A3: the Charact of MU1 = Opers(MU2,C) by A2,MSUALG_2:def 9;
set gg1 = (*-->0)*(signature U2), gg2 = dom signature(U2)-->z;
reconsider gg1 as Function of dom signature(U2), {0}* by MSUALG_1:2;
A4: MSSign U2 = ManySortedSign (#{0},dom signature(U2),gg1,gg2#) by MSUALG_1:10
;
let B be non empty Subset of U2;
assume
A5: B = the carrier of U1;
then reconsider ch1 = the charact of U1 as PFuncFinSequence of B;
A6: MU1 = MSAlgebra(#MSSorts U1,MSCharact U1#) by MSUALG_1:def 11;
then
A7: dom ch1 = dom (the Charact of MU1) by MSUALG_1:def 10
.= the carrier' of MSSign U2 by PARTFUN1:def 2
.= Seg (len signature (U2)) by A4,FINSEQ_1:def 3
.= Seg (len the charact of U2) by UNIALG_1:def 4
.= dom the charact of U2 by FINSEQ_1:def 3;
A8: C is opers_closed by A2,MSUALG_2:def 9;
for n being set,o being operation of U2 st n in dom ch1 & o =(the
charact of U2).n holds ch1.n = o/.B
proof
A9: C = 0 .--> the carrier of U1 by A6,MSUALG_1:def 9;
then dom C = {0};
then
A10: 0 in dom C by TARSKI:def 1;
let n be set;
let o be operation of U2;
assume that
A11: n in dom ch1 and
A12: o =(the charact of U2).n;
n in dom the Charact of MU2 by A1,A7,A11,MSUALG_1:def 10;
then reconsider N=n as OperSymbol of MSSign U2 by PARTFUN1:def 2;
A13: dom the charact of U2 = Seg (len (the charact of U2)) & dom signature
U2 = Seg (len (signature U2)) by FINSEQ_1:def 3;
then
A14: N in dom signature U2 by A7,A11,UNIALG_1:def 4;
(arity o) |-> 0 is FinSequence of the carrier of MSSign U2 by A4,
FINSEQ_2:63;
then reconsider
ao0 = (arity o) |-> 0 as Element of (the carrier of MSSign U2)*
by FINSEQ_1:def 11;
A15: C is_closed_on N by A8;
B is opers_closed by A2,A5,Th14;
then
A16: B is_closed_on o;
A17: 0 in {0} by TARSKI:def 1;
N in dom signature U2 by A7,A11,A13,UNIALG_1:def 4;
then dom *-->0 = NAT & (signature U2).N = arity o by A12,FUNCT_2:def 1
,UNIALG_1:def 4;
then
A18: N in dom ((*-->0)*(signature U2)) by A14,FUNCT_1:11;
then (C# * the Arity of MSSign U2).N = C#.(((*-->0)*(signature U2)).N) by
A4,FUNCT_1:13
.= C#.((*-->0).((signature U2).N)) by A18,FUNCT_1:12
.= C#.((*-->0).(arity o)) by A12,A14,UNIALG_1:def 4
.= C#.((arity o) |-> 0) by FINSEQ_2:def 6;
then
A19: (C# * the Arity of MSSign U2).N = product(C*ao0) by FINSEQ_2:def 5
.= product(Seg (arity o) --> C.0) by A10,FUNCOP_1:17
.= product(Seg (arity o) --> B) by A5,A9,A17,FUNCOP_1:7
.= Funcs(Seg (arity o),B) by CARD_3:11
.= (arity o)-tuples_on B by FINSEQ_2:93;
ch1.N = (the Charact of MU1).N by A6,MSUALG_1:def 10
.= N/.C by A3,MSUALG_2:def 8
.= (Den(N,MU2)) | ((C# * the Arity of MSSign U2).N) by A15,MSUALG_2:def 7
.= ((MSCharact U2).N) | ((C# * the Arity of MSSign U2).N) by A1,
MSUALG_1:def 6
.= o|((arity o)-tuples_on B) by A12,A19,MSUALG_1:def 10;
hence thesis by A16,UNIALG_2:def 5;
end;
hence thesis by A7,UNIALG_2:def 6;
end;
theorem Th16:
for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of
MSAlg U2 holds U1 is SubAlgebra of U2
proof
let U1,U2 be Universal_Algebra;
assume
A1: MSAlg U1 is MSSubAlgebra of MSAlg U2;
hence the carrier of U1 is Subset of U2 by Th13;
let B be non empty Subset of U2;
assume B=the carrier of U1;
hence thesis by A1,Th14,Th15;
end;
reserve MS for segmental non void 1-element ManySortedSign,
A for non-empty MSAlgebra over MS;
theorem Th17:
for B being non-empty MSSubAlgebra of A holds the carrier of
1-Alg B is Subset of 1-Alg A
proof
let B be non-empty MSSubAlgebra of A;
the Sorts of B is MSSubset of A by MSUALG_2:def 9;
then
A1: the Sorts of B c= the Sorts of A by PBOOLE:def 18;
1-Alg B = UAStr(#the_sort_of B, the_charact_of B#) by MSUALG_1:def 14;
then reconsider
c = the carrier of 1-Alg B as Component of the Sorts of B by MSUALG_1:def 12;
1-Alg A = UAStr(#the_sort_of A, the_charact_of A#) by MSUALG_1:def 14;
then reconsider
d = the carrier of 1-Alg A as Component of the Sorts of A by MSUALG_1:def 12;
A2: dom the Sorts of A = the carrier of MS by PARTFUN1:def 2;
then consider dr being object such that
A3: dr in the carrier of MS and
A4: d = (the Sorts of A).dr by FUNCT_1:def 3;
dom the Sorts of A = dom the Sorts of B by A2,PARTFUN1:def 2;
then consider cr being object such that
A5: cr in the carrier of MS and
A6: c = (the Sorts of B).cr by A2,FUNCT_1:def 3;
cr = dr by A5,A3,STRUCT_0:def 10;
hence thesis by A1,A5,A6,A4;
end;
theorem Th18:
for B being non-empty MSSubAlgebra of A holds for S being non
empty Subset of 1-Alg A st S = the carrier of 1-Alg B holds S is opers_closed
proof
let B be non-empty MSSubAlgebra of A;
reconsider C = the Sorts of B as MSSubset of A by MSUALG_2:def 9;
A1: C is opers_closed by MSUALG_2:def 9;
A2: 1-Alg B = UAStr(#the_sort_of B, the_charact_of B#) by MSUALG_1:def 14;
let S be non empty Subset of 1-Alg A such that
A3: S = the carrier of 1-Alg B;
set 1A = 1-Alg A;
A4: 1-Alg A = UAStr(#the_sort_of A, the_charact_of A#) by MSUALG_1:def 14;
let o be operation of 1A;
A5: dom the Sorts of A = the carrier of MS by PARTFUN1:def 2;
then
A6: dom the Sorts of A = dom the Sorts of B by PARTFUN1:def 2;
thus S is_closed_on o
proof
reconsider com = S as Component of the Sorts of B by A2,A3,MSUALG_1:def 12;
consider n being object such that
A7: n in dom the charact of 1A and
A8: o = (the charact of 1A).n by FUNCT_1:def 3;
n in dom the Charact of A by A4,A7,MSUALG_1:def 13;
then reconsider n as OperSymbol of MS by PARTFUN1:def 2;
reconsider crn = C.((the ResultSort of MS).n) as Component of the Sorts of
B by A5,A6,FUNCT_1:def 3;
let s be FinSequence of S;
A9: dom the Arity of MS = the carrier' of MS by FUNCT_2:def 1;
assume
A10: len s = arity o;
ex y being set st y in dom ((Den(n,A))|((C# * the Arity of MS).n)) &
((Den(n,A))|((C# * the Arity of MS).n)).y = o.s
proof
take s;
A11: (the Charact of A).n = (the charact of 1A).n by A4,MSUALG_1:def 13;
thus s in dom ((Den(n,A))|((C# * the Arity of MS).n))
proof
rng s c= S by FINSEQ_1:def 4;
then rng s c= the carrier of 1A by XBOOLE_1:1;
then reconsider s1=s as FinSequence of the carrier of 1A by
FINSEQ_1:def 4;
reconsider An=(the Arity of MS).n as Element of (the carrier of MS)*;
set f = (the Sorts of A)*An;
consider d being object such that
A12: d in dom o by XBOOLE_0:def 1;
o in PFuncs((the carrier of 1A)*,the carrier of 1A) by PARTFUN1:45;
then ex o1 being Function st o1=o & dom o1 c= (the carrier of 1A)* &
rng o1 c= the carrier of 1A by PARTFUN1:def 3;
then reconsider d as FinSequence of the carrier of 1A by A12,
FINSEQ_1:def 11;
A13: dom Den(n,A) = Args(n,A) by FUNCT_2:def 1
.= (len the_arity_of n)-tuples_on the carrier of 1A by A4,MSUALG_1:6;
dom Den (n,A) = Args(n,A) by FUNCT_2:def 1;
then dom Den(n,A) = ((the Sorts of A)# * the Arity of MS).n by
MSUALG_1:def 4
.=(the Sorts of A)#.((the Arity of MS).n) by A9,FUNCT_1:13;
then
A14: dom Den(n,A) = product((the Sorts of A)*(An)) by FINSEQ_2:def 5;
A15: o = (the Charact of A).n by A4,A8,MSUALG_1:def 13
.= Den(n,A) by MSUALG_1:def 6;
len d = len s1 by A10,A12,MARGREL1:def 25;
then len s = len the_arity_of n by A12,A15,A13,CARD_1:def 7;
then
A16: dom s = Seg len the_arity_of n by FINSEQ_1:def 3
.= dom the_arity_of n by FINSEQ_1:def 3
.= dom An by MSUALG_1:def 1;
A17: dom s c= dom (C*An)
proof
let x be object;
assume
A18: x in dom s;
then rng An c= the carrier of MS & An.x in rng An by A16,
FINSEQ_1:def 4,FUNCT_1:def 3;
then An.x in the carrier of MS;
then An.x in dom C by PARTFUN1:def 2;
hence thesis by A16,A18,FUNCT_1:11;
end;
dom (C*An) c= dom s by A16,RELAT_1:25;
then
A19: dom s = dom (C*An) by A17;
A20: for x being object st x in dom s holds s.x in (C*An).x
proof
let x be object;
A21: rng s c= S by FINSEQ_1:def 4;
assume
A22: x in dom s;
then
A23: s.x in rng s by FUNCT_1:def 3;
dom s c= dom An by A19,RELAT_1:25;
then rng An c= the carrier of MS & An.x in rng An by A22,
FINSEQ_1:def 4,FUNCT_1:def 3;
then An.x in the carrier of MS;
then
A24: An.x in dom C by PARTFUN1:def 2;
(C*An).x = C.(An.x) by A17,A22,FUNCT_1:12;
then reconsider canx = (C*An).x as Component of C by A24,
FUNCT_1:def 3;
(C*An).x = canx .= S by A2,A3,MSUALG_1:def 12;
hence thesis by A23,A21;
end;
A25: dom f c= dom s
by A16,FUNCT_1:11;
A26: for x being object st x in dom f holds s.x in f.x
proof
let x be object;
A27: rng s c= S by FINSEQ_1:def 4;
assume
A28: x in dom f;
then f.x in rng f by FUNCT_1:def 3;
then reconsider fx=f.x as Component of the Sorts of A by FUNCT_1:14;
s.x in rng s by A25,A28,FUNCT_1:def 3;
then fx = the_sort_of A & s.x in S by A27,MSUALG_1:def 12;
hence thesis by A4;
end;
dom the Arity of MS = the carrier' of MS by FUNCT_2:def 1;
then (C# * the Arity of MS).n =C#.An by FUNCT_1:13
.=product(C*An) by FINSEQ_2:def 5;
then
A29: s in (C# * the Arity of MS).n by A19,A20,CARD_3:9;
dom s c= dom f
proof
let x be object;
assume
A30: x in dom s;
then rng An c= the carrier of MS & An.x in rng An by A16,
FINSEQ_1:def 4,FUNCT_1:def 3;
then An.x in the carrier of MS;
then An.x in dom (the Sorts of A) by PARTFUN1:def 2;
hence thesis by A16,A30,FUNCT_1:11;
end;
then dom s = dom f by A25;
then s in dom Den(n,A) by A14,A26,CARD_3:9;
then s in dom Den(n,A)/\(C# * the Arity of MS).n by A29,XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
hence ((Den(n,A))|((C# * the Arity of MS).n)).s = Den(n,A).s by
FUNCT_1:47
.= o.s by A8,A11,MSUALG_1:def 6;
end;
then
A31: o.s in rng ((Den(n,A))|((C# * the Arity of MS).n)) by FUNCT_1:def 3;
dom the ResultSort of MS = the carrier' of MS by FUNCT_2:def 1;
then
A32: (C * the ResultSort of MS).n = crn by FUNCT_1:13
.= com by MSUALG_1:5;
C is_closed_on n by A1;
then
rng ((Den(n,A))|((C# * the Arity of MS).n)) c= (C * the ResultSort of
MS).n;
hence thesis by A31,A32;
end;
end;
theorem Th19:
for B being non-empty MSSubAlgebra of A holds for S being non
empty Subset of 1-Alg A st S = the carrier of 1-Alg B holds the charact of(
1-Alg B) = Opers(1-Alg A,S)
proof
let B be non-empty MSSubAlgebra of A;
reconsider C = the Sorts of B as MSSubset of A by MSUALG_2:def 9;
A1: the Charact of B = Opers(A,C) by MSUALG_2:def 9;
set 1B = 1-Alg B,1A = 1-Alg A;
A2: 1-Alg A = UAStr(#the_sort_of A, the_charact_of A#) by MSUALG_1:def 14;
set f1 = the charact of 1B;
let S be non empty Subset of 1-Alg A such that
A3: S = the carrier of 1-Alg B;
reconsider f1 as PFuncFinSequence of S by A3;
A4: 1-Alg B = UAStr(#the_sort_of B, the_charact_of B#) by MSUALG_1:def 14;
then
A5: f1 = the Charact of B by MSUALG_1:def 13;
A6: C is opers_closed by MSUALG_2:def 9;
A7: for n being set,o being operation of 1A st n in dom f1 & o =(the charact
of(1A)).n holds f1.n = o/.S
proof
let n be set,o be operation of 1A;
assume that
A8: n in dom f1 and
A9: o =(the charact of(1A)).n;
reconsider y = n as OperSymbol of MS by A5,A8,PARTFUN1:def 2;
o = (the Charact of A).y by A2,A9,MSUALG_1:def 13
.= Den(y,A) by MSUALG_1:def 6;
then
A10: dom o = Args(y,A) by FUNCT_2:def 1
.= (len the_arity_of y)-tuples_on the_sort_of A by MSUALG_1:6;
now
set a = the Element of (len the_arity_of y)-tuples_on the_sort_of A;
a in dom o by A10;
hence ex x being FinSequence st x in dom o;
let x be FinSequence;
assume x in dom o;
then ex s being Element of (the_sort_of A)* st x=s & len s = len
the_arity_of y by A10;
hence (len the_arity_of y) = len x;
end;
then
A11: arity o = len the_arity_of y by MARGREL1:def 25;
S is opers_closed by A3,Th18;
then
A12: S is_closed_on o;
A13: C is_closed_on y by A6;
A14: (C# * the Arity of MS).y = Args(y,B) by MSUALG_1:def 4
.= (arity o)-tuples_on S by A4,A3,A11,MSUALG_1:6;
f1.n = (the Charact of B).y by A4,MSUALG_1:def 13
.= y/.C by A1,MSUALG_2:def 8
.= (Den(y,A)) | ((C# * the Arity of MS).y) by A13,MSUALG_2:def 7
.= ((the Charact of A).y) | ((C# * the Arity of MS).y) by MSUALG_1:def 6
.= o | ((arity o)-tuples_on S) by A2,A9,A14,MSUALG_1:def 13;
hence thesis by A12,UNIALG_2:def 5;
end;
dom f1 = the carrier' of MS by A5,PARTFUN1:def 2
.= dom the Charact of A by PARTFUN1:def 2
.= dom the charact of(1A) by A2,MSUALG_1:def 13;
hence thesis by A7,UNIALG_2:def 6;
end;
theorem Th20:
for B being non-empty MSSubAlgebra of A holds 1-Alg B is
SubAlgebra of 1-Alg A
proof
let B be non-empty MSSubAlgebra of A;
the carrier of 1-Alg B is Subset of 1-Alg A & for S being non empty
Subset of 1-Alg A st S = the carrier of 1-Alg B holds the charact of(1-Alg B) =
Opers( 1-Alg A,S) & S is opers_closed by Th17,Th18,Th19;
hence thesis by UNIALG_2:def 7;
end;
theorem Th21:
for S being non empty non void ManySortedSign, A,B being
MSAlgebra over S holds A is MSSubAlgebra of B iff A is MSSubAlgebra of the
MSAlgebra of B
proof
let S be non empty non void ManySortedSign, A,B be MSAlgebra over S;
thus A is MSSubAlgebra of B implies A is MSSubAlgebra of the MSAlgebra of B
proof
assume
A1: A is MSSubAlgebra of B;
hence the Sorts of A is MSSubset of the MSAlgebra of B by MSUALG_2:def 9;
thus for BB be MSSubset of the MSAlgebra of B st BB = the Sorts of A holds
BB is opers_closed & the Charact of A = Opers(the MSAlgebra of B,BB)
proof
let BB be MSSubset of the MSAlgebra of B such that
A2: BB = the Sorts of A;
reconsider bb = BB as MSSubset of B;
A3: bb is opers_closed by A1,A2,MSUALG_2:def 9;
A4: BB is opers_closed
proof
let o be OperSymbol of S;
A5: Den(o,B) = (the Charact of the MSAlgebra of B).o by MSUALG_1:def 6
.= Den(o,the MSAlgebra of B) by MSUALG_1:def 6;
bb is_closed_on o by A3;
then
rng ((Den(o,the MSAlgebra of B))|((BB# * the Arity of S).o) ) c= (
BB * the ResultSort of S).o by A5;
hence thesis;
end;
for o be object st o in the carrier' of S holds (the Charact of A).o =
(Opers(the MSAlgebra of B,BB)).o
proof
let o be object;
assume o in the carrier' of S;
then reconsider o as OperSymbol of S;
A6: Den(o,B) = (the Charact of the MSAlgebra of B).o by MSUALG_1:def 6
.= Den(o,the MSAlgebra of B) by MSUALG_1:def 6;
A7: bb is_closed_on o by A3;
A8: BB is_closed_on o by A4;
(Opers(B,bb)).o = o/.bb by MSUALG_2:def 8
.= (Den(o,the MSAlgebra of B))|((BB# * the Arity of S).o) by A6,A7,
MSUALG_2:def 7
.= o/.BB by A8,MSUALG_2:def 7
.= (Opers(the MSAlgebra of B,BB)).o by MSUALG_2:def 8;
hence thesis by A1,A2,MSUALG_2:def 9;
end;
hence thesis by A4;
end;
end;
assume
A9: A is MSSubAlgebra of the MSAlgebra of B;
hence the Sorts of A is MSSubset of B by MSUALG_2:def 9;
let C be MSSubset of B such that
A10: C = the Sorts of A;
reconsider CC = C as MSSubset of the MSAlgebra of B;
A11: CC is opers_closed by A9,A10,MSUALG_2:def 9;
A12: C is opers_closed
proof
let o be OperSymbol of S;
A13: Den(o,B) = (the Charact of the MSAlgebra of B).o by MSUALG_1:def 6
.= Den(o,the MSAlgebra of B) by MSUALG_1:def 6;
CC is_closed_on o by A11;
then rng ((Den(o,B))|((C# * the Arity of S).o)) c= (C * the ResultSort of
S).o by A13;
hence thesis;
end;
for o be object st o in the carrier' of S holds (the Charact of A).o = (
Opers(B,C)).o
proof
let o be object;
assume o in the carrier' of S;
then reconsider o as OperSymbol of S;
A14: Den(o,B) = (the Charact of the MSAlgebra of B).o by MSUALG_1:def 6
.= Den(o,the MSAlgebra of B) by MSUALG_1:def 6;
A15: CC is_closed_on o by A11;
A16: C is_closed_on o by A12;
(Opers(the MSAlgebra of B,CC)).o = o/.CC by MSUALG_2:def 8
.= (Den(o,B))|((C# * the Arity of S).o) by A14,A15,MSUALG_2:def 7
.= o/.C by A16,MSUALG_2:def 7
.= (Opers(B,C)).o by MSUALG_2:def 8;
hence thesis by A9,A10,MSUALG_2:def 9;
end;
hence thesis by A12;
end;
theorem
for A,B being Universal_Algebra holds signature A = signature B iff
MSSign A = MSSign B
proof
A1: for A, B be Universal_Algebra st MSSign A = MSSign B holds signature A =
signature B
proof
let A,B be Universal_Algebra;
reconsider ff1 = (*-->0)*(signature A) as Function of dom signature A, {0}
* by MSUALG_1:2;
reconsider gg1 = (*-->0)*(signature B) as Function of dom signature B, {0}
* by MSUALG_1:2;
A2: MSSign A = ManySortedSign (#{0},dom signature(A),ff1,dom signature(A)
-->z#) & MSSign B = ManySortedSign (#{0},dom signature(B),gg1,dom signature(B)
-->z#) by MSUALG_1:10;
assume
A3: MSSign A = MSSign B;
now
let i be Nat;
assume
A4: i in dom signature A;
then reconsider k= (signature A).i as Element of NAT by PARTFUN1:4;
A5: i in dom ((*-->0)*(signature A)) by A4,FINSEQ_3:120;
then
A6: (*-->0).((signature B).i)= ((*-->0)*(signature A)).i
by A3,A2,FINSEQ_3:120
.= (*-->0).((signature A).i) by A5,FINSEQ_3:120;
reconsider m = (signature B).i as Element of NAT by A3,A2,A4,PARTFUN1:4;
reconsider q = (*-->0).m as FinSequence;
reconsider p = (*-->0).k as FinSequence;
thus (signature A).i = len p by Th6
.= len q by A6
.= (signature B).i by Th6;
end;
hence thesis by A3,A2,FINSEQ_1:13;
end;
for A,B be Universal_Algebra st signature A = signature B holds MSSign A
= MSSign B
by UNIALG_2:def 1,MSUHOM_1:10;
hence thesis by A1;
end;
theorem Th23:
for A being non-empty MSAlgebra over MS st the carrier of MS = {
0} holds MSSign 1-Alg A = the ManySortedSign of MS
proof
let A be non-empty MSAlgebra over MS;
reconsider ff1 = (*-->0)*(signature 1-Alg A) as Function of dom signature
1-Alg A, {0}* by MSUALG_1:2;
A1: MSSign 1-Alg A = ManySortedSign (#{0},dom signature(1-Alg A),ff1,dom
signature(1-Alg A)-->z#) by MSUALG_1:10;
dom (the ResultSort of MS) = the carrier' of MS by FUNCT_2:def 1;
then
A2: rng (the ResultSort of MS) <> {} by RELAT_1:42;
consider k be Nat such that
A3: the carrier' of MS = Seg k by MSUALG_1:def 7;
A4: 1-Alg A = UAStr(#the_sort_of A, the_charact_of A#) by MSUALG_1:def 14;
A5: len signature (1-Alg A) = len the charact of 1-Alg A by UNIALG_1:def 4;
then
A6: dom signature (1-Alg A) = dom (the charact of 1-Alg A) by FINSEQ_3:29
.= dom the Charact of A by A4,MSUALG_1:def 13
.= the carrier' of MS by PARTFUN1:def 2;
then
A7: the carrier' of MS = dom ff1 by FUNCT_2:def 1;
assume
A8: the carrier of MS = {0};
A9: for x being object st x in the carrier' of MS holds ((*-->0)*(signature (
1-Alg A))).x = (the Arity of MS).x
proof
let x be object;
assume x in the carrier' of MS;
then reconsider x as OperSymbol of MS;
x in Seg k by A3;
then reconsider n = x as Nat;
n in dom(signature (1-Alg A)) by A6;
then
A10: n in dom the charact of 1-Alg A by A5,FINSEQ_3:29;
reconsider
h = (the charact of 1-Alg A).n as PartFunc of (the carrier of
1-Alg A)*,the carrier of 1-Alg A;
reconsider h as homogeneous quasi_total non empty PartFunc of (the carrier
of 1-Alg A)*,the carrier of 1-Alg A by A10,MARGREL1:def 24;
set aa = the Element of dom h;
set ah = arity h;
dom h c= (the carrier of 1-Alg A)* by RELAT_1:def 18;
then aa in (the carrier of 1-Alg A)*;
then reconsider bb = aa as FinSequence of the carrier of 1-Alg A by
FINSEQ_1:def 11;
A11: bb in dom h;
h = (the Charact of A).x by A4,MSUALG_1:def 13
.= Den(x,A) by MSUALG_1:def 6;
then bb in Args(x,A) by A11,FUNCT_2:def 1;
then bb in (len the_arity_of x)-tuples_on the_sort_of A by MSUALG_1:6;
then
A12: len the_arity_of x = len bb by CARD_1:def 7
.= ah by MARGREL1:def 25;
((*-->0)*(signature (1-Alg A))).x = (*-->0).((signature (1-Alg A)).x)
by A6,FUNCT_1:13
.= (*-->0).ah by A6,UNIALG_1:def 4
.= ah |-> 0 by FINSEQ_2:def 6
.= the_arity_of x by A8,A12,Th5
.= (the Arity of MS).x by MSUALG_1:def 1;
hence thesis;
end;
rng (the ResultSort of MS) c= {0} by A8,RELAT_1:def 19;
then the carrier' of MS = dom (the ResultSort of MS) & rng (the ResultSort
of MS) = {0} by A2,FUNCT_2:def 1,ZFMISC_1:33;
then the carrier' of MS = dom the Arity of MS & the ResultSort of MSSign
1-Alg A = the ResultSort of MS by A1,A6,FUNCOP_1:9,FUNCT_2:def 1;
hence thesis by A8,A1,A7,A9,FUNCT_1:2;
end;
theorem Th24:
for A,B being non-empty MSAlgebra over MS st 1-Alg A = 1-Alg B
holds the MSAlgebra of A = the MSAlgebra of B
proof
let A,B be non-empty MSAlgebra over MS such that
A1: 1-Alg A = 1-Alg B;
A2: 1-Alg B = UAStr(#the_sort_of B, the_charact_of B#) by MSUALG_1:def 14;
A3: 1-Alg A = UAStr(#the_sort_of A, the_charact_of A#) by MSUALG_1:def 14;
A4: now
let i be object such that
A5: i in the carrier of MS;
A6: ex c being Component of the Sorts of B st (the Sorts of B).i = c
proof
reconsider c = (the Sorts of B).i as Component of the Sorts of B by A5,
PBOOLE:139;
take c;
thus thesis;
end;
ex c being Component of the Sorts of A st (the Sorts of A).i = c
proof
reconsider c = (the Sorts of A).i as Component of the Sorts of A by A5,
PBOOLE:139;
take c;
thus thesis;
end;
then (the Sorts of A).i = the_sort_of B by A1,A3,A2,MSUALG_1:def 12
.= (the Sorts of B).i by A6,MSUALG_1:def 12;
hence (the Sorts of A).i = (the Sorts of B).i;
end;
the Charact of A = the charact of 1-Alg A by A3,MSUALG_1:def 13
.= the Charact of B by A1,A2,MSUALG_1:def 13;
hence thesis by A4,PBOOLE:3;
end;
theorem
for A being non-empty MSAlgebra over MS st the carrier of MS = {0}
holds the Sorts of A = the Sorts of MSAlg (1-Alg A)
proof
let A be non-empty MSAlgebra over MS;
assume
A1: the carrier of MS = {0};
A2: now
let i be object;
assume
A3: i in the carrier of MS;
A4: ex c being Component of the Sorts of A st (the Sorts of A).i = c
proof
reconsider c = (the Sorts of A).i as Component of the Sorts of A by A3,
PBOOLE:139;
take c;
thus thesis;
end;
({0} --> (the_sort_of A)).i = the_sort_of A by A1,A3,FUNCOP_1:7;
hence (the Sorts of A).i = ({0} --> (the_sort_of A)).i by A4,
MSUALG_1:def 12;
end;
1-Alg A = UAStr(#the_sort_of A, the_charact_of A#) by MSUALG_1:def 14;
then
A5: MSAlg (1-Alg A) = MSAlgebra(#MSSorts (1-Alg A),MSCharact (1-Alg A)#) &
MSSorts (1-Alg A) = 0.--> (the_sort_of A) by MSUALG_1:def 9,def 11;
{0} --> (the_sort_of A) is ManySortedSet of the carrier of MS by A1;
hence thesis by A5,A2,PBOOLE:3;
end;
theorem Th26:
for A being non-empty MSAlgebra over MS st the carrier of MS = {
0} holds MSAlg (1-Alg A) = the MSAlgebra of A
proof
let A be non-empty MSAlgebra over MS;
reconsider c = the_sort_of MSAlg (1-Alg A) as Component of the Sorts of
MSAlg (1-Alg A) by MSUALG_1:def 12;
assume the carrier of MS = {0};
then MSSign 1-Alg A = the ManySortedSign of MS by Th23;
then reconsider M1A = MSAlg (1-Alg A) as strict MSAlgebra over MS;
reconsider M1A as non-empty strict MSAlgebra over MS by MSUALG_1:def 3;
A1: 1-Alg M1A = UAStr(#the_sort_of M1A, the_charact_of M1A#) by MSUALG_1:def 14
;
reconsider c as Component of the Sorts of M1A;
A2: 1-Alg(MSAlg (1-Alg A)) = UAStr(#the_sort_of (MSAlg (1-Alg A)),
the_charact_of (MSAlg (1-Alg A))#) by MSUALG_1:def 14;
then
A3: the charact of 1-Alg A = the_charact_of MSAlg (1-Alg A) by MSUALG_1:9
.= the Charact of M1A by MSUALG_1:def 13
.= the charact of 1-Alg M1A by A1,MSUALG_1:def 13;
c = the_sort_of M1A by MSUALG_1:def 12;
then the carrier of 1-Alg A = the carrier of 1-Alg M1A by A2,A1,MSUALG_1:9;
hence thesis by A3,Th24;
end;
theorem
for A being Universal_Algebra, B being strict non-empty MSSubAlgebra
of MSAlg A st the carrier of MSSign A = {0} holds 1-Alg B is SubAlgebra of A
proof
let A be Universal_Algebra , B be strict non-empty MSSubAlgebra of MSAlg A;
assume the carrier of MSSign A = {0};
then MSAlg (1-Alg B) = the MSAlgebra of B by Th26;
hence thesis by Th16;
end;
begin
:: The Correspondence Between Lattices of Subalgebras of
:: Universal and Many Sorted Algebras
theorem Th28:
for A being Universal_Algebra, a1,b1 being strict SubAlgebra of
A, a2,b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 =
MSAlg b1 holds (the Sorts of a2) (\/) (the Sorts of b2)
= 0 .--> ((the carrier of a1) \/ (the carrier of b1))
proof
let A be Universal_Algebra;
let a1,b1 be strict SubAlgebra of A;
let a2,b2 be strict non-empty MSSubAlgebra of MSAlg A such that
A1: a2 = MSAlg a1 and
A2: b2 = MSAlg b1;
a2 = MSAlgebra(#MSSorts a1,MSCharact a1#) by A1,MSUALG_1:def 11;
then
A3: the Sorts of a2 = 0 .--> (the carrier of a1) by MSUALG_1:def 9;
reconsider ff1 = (*-->0)*(signature A) as Function of dom signature A, {0}*
by MSUALG_1:2;
A4: MSSign A = ManySortedSign (#{0},dom signature(A),ff1,dom signature(A)-->
z#) by MSUALG_1:10;
then reconsider W = 0 .--> ((the carrier of a1) \/ (the carrier of b1)) as
ManySortedSet of the carrier of MSSign A;
A5: b2 = MSAlgebra(#MSSorts b1,MSCharact b1#) by A2,MSUALG_1:def 11;
now
let x be object;
assume
A6: x in the carrier of MSSign A;
then
A7: x = 0 by A4,TARSKI:def 1;
W.x = (0 .--> ((the carrier of a1) \/ (the carrier of b1))).0 by A4,A6,
TARSKI:def 1
.= (the carrier of a1) \/ (the carrier of b1) by FUNCOP_1:72
.= (0 .--> the carrier of a1).0 \/ ( the carrier of b1) by FUNCOP_1:72
.= (0 .--> the carrier of a1).0 \/ (0 .--> the carrier of b1).0 by
FUNCOP_1:72
.= (the Sorts of a2).x \/ (the Sorts of b2).x by A3,A5,A7,MSUALG_1:def 9;
hence W.x = (the Sorts of a2).x \/ (the Sorts of b2).x;
end;
hence thesis by PBOOLE:def 4;
end;
theorem Th29:
for A being Universal_Algebra, a1,b1 being strict non-empty
SubAlgebra of A, a2,b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 =
MSAlg a1 & b2 = MSAlg b1 holds
(the Sorts of a2) (/\) (the Sorts of b2) = 0 .-->
((the carrier of a1) /\ (the carrier of b1))
proof
let A be Universal_Algebra;
let a1,b1 be strict non-empty SubAlgebra of A;
let a2,b2 be strict non-empty MSSubAlgebra of MSAlg A such that
A1: a2 = MSAlg a1 and
A2: b2 = MSAlg b1;
a2 = MSAlgebra(#MSSorts a1,MSCharact a1#) by A1,MSUALG_1:def 11;
then
A3: the Sorts of a2 = 0 .--> (the carrier of a1) by MSUALG_1:def 9;
reconsider ff1 = (*-->0)*(signature A) as Function of dom signature A, {0}*
by MSUALG_1:2;
A4: MSSign A = ManySortedSign (#{0},dom signature(A),ff1,dom signature(A)-->
z#) by MSUALG_1:10;
then reconsider W = 0 .--> ((the carrier of a1) /\ (the carrier of b1)) as
ManySortedSet of the carrier of MSSign A;
A5: b2 = MSAlgebra(#MSSorts b1,MSCharact b1#) by A2,MSUALG_1:def 11;
now
let x be object;
assume x in the carrier of MSSign A;
then
A6: x = 0 by A4,TARSKI:def 1;
then W.x = (the carrier of a1) /\ (the carrier of b1) by FUNCOP_1:72
.= (0 .--> the carrier of a1).0 /\ ( the carrier of b1) by FUNCOP_1:72
.= (0 .--> the carrier of a1).0 /\ (0 .--> the carrier of b1).0 by
FUNCOP_1:72
.= (the Sorts of a2).x /\ (the Sorts of b2).x by A3,A5,A6,MSUALG_1:def 9;
hence W.x = (the Sorts of a2).x /\ (the Sorts of b2).x;
end;
hence thesis by PBOOLE:def 5;
end;
theorem Th30:
for A being strict Universal_Algebra, a1,b1 be strict non-empty
SubAlgebra of A, a2,b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 =
MSAlg a1 & b2 = MSAlg b1 holds MSAlg (a1 "\/" b1) = a2 "\/" b2
proof
let A be strict Universal_Algebra;
let a1,b1 be strict non-empty SubAlgebra of A;
reconsider MSA = MSAlg (a1"\/"b1) as MSSubAlgebra of MSAlg A by Th12;
let a2,b2 be strict non-empty MSSubAlgebra of MSAlg A such that
A1: a2 = MSAlg a1 and
A2: b2 = MSAlg b1;
MSSign (a1"\/"b1) = MSSign A by Th7;
then reconsider MSA as strict non-empty MSSubAlgebra of MSAlg A;
for B be MSSubset of MSAlg A st B = (the Sorts of a2) (\/) (the Sorts of
b2) holds MSA = GenMSAlg(B)
proof
the carrier of a1 is Subset of A & the carrier of b1 is Subset of A by
UNIALG_2:def 7;
then reconsider
K = (the carrier of a1) \/ (the carrier of b1) as non empty
Subset of A by XBOOLE_1:8;
reconsider ff1 = (*-->0)*(signature A) as Function of dom signature A, {0}
* by MSUALG_1:2;
set X = MSA;
reconsider M1 = the Sorts of X as ManySortedSet of the carrier of MSSign A;
A3: MSSign A = ManySortedSign (#{0},dom signature(A),ff1,dom signature(A)
-->z#) by MSUALG_1:10;
then reconsider x = 0 as Element of MSSign A;
let B be MSSubset of MSAlg A such that
A4: B = (the Sorts of a2) (\/) (the Sorts of b2);
A5: for U1 be MSSubAlgebra of MSAlg A st B is MSSubset of U1 holds X is
MSSubAlgebra of U1
proof
let U1 be MSSubAlgebra of MSAlg A;
assume
A6: B is MSSubset of U1;
per cases;
suppose
U1 is non-empty;
then reconsider U11=U1 as non-empty MSSubAlgebra of MSAlg A;
A7: 1-Alg U11 is SubAlgebra of 1-Alg MSAlg A by Th20;
then reconsider A1 = 1-Alg U11 as strict SubAlgebra of A by MSUALG_1:9;
B c= the Sorts of U11 by A6,PBOOLE:def 18;
then
A8: B.x c= (the Sorts of U11).x;
the MSAlgebra of U11 = MSAlg (1-Alg U11) & MSAlg (1-Alg U11) =
MSAlgebra(# MSSorts (1-Alg U11),MSCharact (1-Alg U11)#) by A3,Th26,
MSUALG_1:def 11;
then
A9: (the Sorts of U11).0 = (0 .--> the carrier of 1-Alg U11).0 by
MSUALG_1:def 9;
B.0 = (0.--> K).0 by A1,A2,A4,Th28
.= K by FUNCOP_1:72;
then (the carrier of a1) \/ the carrier of b1 c= the carrier of A1 by
A8,A9,FUNCOP_1:72;
then GenUnivAlg K is SubAlgebra of 1-Alg U11 by UNIALG_2:def 12;
then a1"\/"b1 is SubAlgebra of 1-Alg U11 by UNIALG_2:def 13;
then
A10: MSA is MSSubAlgebra of MSAlg(1-Alg U11) by Th12;
1-Alg U11 is SubAlgebra of A by A7,MSUALG_1:9;
then MSSign A = MSSign 1-Alg U11 by Th7;
then X is MSSubAlgebra of the MSAlgebra of U11 by A3,A10,Th26;
hence thesis by Th21;
end;
suppose
not U1 is non-empty;
then the Sorts of U1 is non non-empty by MSUALG_1:def 3;
then
A11: ex i be object st i in the carrier of MSSign A & (the Sorts of U1).i
is empty;
reconsider
0a1=0.-->the carrier of a1 as ManySortedSet of the carrier
of MSSign A by A3;
set e = the Element of a1;
B c= the Sorts of U1 by A6,PBOOLE:def 18;
then
A12: B.x c= (the Sorts of U1).x;
a2=MSAlgebra(#MSSorts a1,MSCharact a1#) by A1,MSUALG_1:def 11;
then B = 0a1 (\/) (the Sorts of b2) by A4,MSUALG_1:def 9;
then
A13: B.x = 0a1.x \/ (the Sorts of b2).x by PBOOLE:def 4;
x in {0} by TARSKI:def 1;
then 0a1.x = the carrier of a1 by FUNCOP_1:7;
then e in B.x by A13,XBOOLE_0:def 3;
hence thesis by A3,A11,A12,TARSKI:def 1;
end;
end;
X = MSAlgebra(#MSSorts (a1"\/"b1),MSCharact (a1"\/"b1)#) by MSUALG_1:def 11
;
then
A14: the Sorts of X = 0 .--> the carrier of a1"\/"b1 by MSUALG_1:def 9;
(the Sorts of a2) (\/) (the Sorts of b2) c= M1
proof
let x be object;
A15: a1"\/"b1 = GenUnivAlg K by UNIALG_2:def 13;
assume
A16: x in the carrier of MSSign A;
then
A17: M1.x = (0 .--> the carrier of a1"\/"b1).0 by A14,A3,TARSKI:def 1
.= the carrier of a1"\/"b1 by FUNCOP_1:72;
((the Sorts of a2) (\/) (the Sorts of b2)).x = ((the Sorts of a2) (\/)
(the Sorts of b2)).0 by A3,A16,TARSKI:def 1
.= (0 .--> ((the carrier of a1) \/ (the carrier of b1))).0 by A1,A2
,Th28
.= (the carrier of a1) \/ (the carrier of b1) by FUNCOP_1:72;
hence thesis by A17,A15,UNIALG_2:def 12;
end;
then B is MSSubset of X by A4,PBOOLE:def 18;
hence thesis by A5,MSUALG_2:def 17;
end;
hence thesis by MSUALG_2:def 18;
end;
registration
let A be with_const_op Universal_Algebra;
cluster MSSign(A) -> non void strict segmental trivial all-with_const_op;
coherence
proof
reconsider ff1 = (*-->0)*(signature A) as Function of dom signature A, {0}
* by MSUALG_1:2;
A1: MSSign(A) = ManySortedSign (#{0},dom signature(A),ff1,dom signature(A)
-->z#) by MSUALG_1:10;
MSSign(A) is all-with_const_op
proof
let s be SortSymbol of MSSign(A);
consider OO being operation of A such that
A2: arity OO=0 by UNIALG_2:def 11;
Seg len the charact of A = dom the charact of A by FINSEQ_1:def 3;
then consider i being Nat such that
A3: i in Seg len the charact of A and
A4: (the charact of A).i = OO by FINSEQ_2:10;
A5: len signature(A) = len the charact of A by UNIALG_1:def 4;
then
A6: i in dom signature(A) by A3,FINSEQ_1:def 3;
reconsider i as OperSymbol of MSSign(A) by A1,A3,A5,FINSEQ_1:def 3;
take i;
(*-->0).((signature A).i) = (*-->0).0 by A2,A4,A6,UNIALG_1:def 4
.= {} by Th1;
hence (the Arity of MSSign(A)).i = {} by A1,FUNCT_1:13;
thus (the ResultSort of MSSign(A)).i = s by A1,TARSKI:def 1;
end;
hence thesis;
end;
end;
theorem Th31:
for A being with_const_op Universal_Algebra, a1,b1 being strict
non-empty SubAlgebra of A, a2,b2 being strict non-empty MSSubAlgebra of MSAlg A
st a2 = MSAlg a1 & b2 = MSAlg b1 holds MSAlg (a1 /\ b1) = a2 /\ b2
proof
let A be with_const_op Universal_Algebra;
let a1,b1 be strict non-empty SubAlgebra of A;
reconsider ff1 = (*-->0)*(signature A) as Function of dom signature A, {0}*
by MSUALG_1:2;
A1: MSSign A = ManySortedSign (#{0},dom signature(A),ff1,dom signature(A)-->
z#) by MSUALG_1:10;
MSAlg (a1/\b1) = MSAlgebra(#MSSorts (a1/\b1),MSCharact (a1/\b1)#) by
MSUALG_1:def 11;
then
A2: the Sorts of MSAlg (a1/\b1) = 0 .--> the carrier of a1/\b1 by
MSUALG_1:def 9;
then dom the Sorts of MSAlg (a1/\b1) = the carrier of MSSign A by A1;
then reconsider
D = the Sorts of MSAlg (a1 /\ b1) as ManySortedSet of the carrier
of MSSign A by PARTFUN1:def 2,RELAT_1:def 18;
let a2,b2 be strict non-empty MSSubAlgebra of MSAlg A such that
A3: a2 = MSAlg a1 & b2 = MSAlg b1;
now
let x be object;
A4: (the carrier of a1) meets (the carrier of b1) by UNIALG_2:17;
assume
A5: x in the carrier of MSSign A;
hence D.x = ( 0 .--> the carrier of a1/\ b1).0 by A2,A1,TARSKI:def 1
.= the carrier of a1 /\ b1 by FUNCOP_1:72
.= (the carrier of a1) /\ (the carrier of b1) by A4,UNIALG_2:def 9
.= (0 .--> ((the carrier of a1) /\ (the carrier of b1))).0 by FUNCOP_1:72
.= ((the Sorts of a2) (/\) (the Sorts of b2)).0 by A3,Th29
.= ((the Sorts of a2) (/\) (the Sorts of b2)).x by A1,A5,TARSKI:def 1;
end;
then
A6: D = (the Sorts of a2) (/\) (the Sorts of b2);
MSSign (a1/\ b1) = MSSign A by Th7;
then reconsider
AA = MSAlg (a1 /\ b1) as strict non-empty MSSubAlgebra of MSAlg A
by Th12;
for B be MSSubset of MSAlg A st B = the Sorts of AA holds B is
opers_closed & the Charact of AA = Opers(MSAlg A,B) by MSUALG_2:def 9;
hence thesis by A6,MSUALG_2:def 16;
end;
registration
let A be quasi_total UAStr;
cluster the UAStr of A -> quasi_total;
coherence;
end;
registration
let A be partial UAStr;
cluster the UAStr of A -> partial;
coherence;
end;
registration
let A be non-empty UAStr;
cluster the UAStr of A -> non-empty;
coherence;
end;
registration
let A be with_const_op Universal_Algebra;
cluster the UAStr of A -> with_const_op;
coherence
proof
consider o be operation of A such that
A1: arity o = 0 by UNIALG_2:def 11;
reconsider oo = o as operation of the UAStr of A;
take oo;
thus thesis by A1;
end;
end;
theorem
for A being with_const_op Universal_Algebra holds UnSubAlLattice the
UAStr of A, MSSubAlLattice MSAlg the UAStr of A are_isomorphic
proof
let Z be with_const_op Universal_Algebra;
set A = the UAStr of Z;
reconsider ff1 = (*-->0)*(signature A) as Function of dom signature A, {0}*
by MSUALG_1:2;
A1: MSSign A = ManySortedSign (#{0},dom signature(A),ff1,dom signature(A)-->
z#) by MSUALG_1:10;
defpred P[set,set] means ex A1 be strict SubAlgebra of A st A1= $1 & $2=
MSAlg A1;
A2: for x being Element of Sub A ex y being Element of MSSub MSAlg A st P[x, y]
proof
let x be Element of Sub A;
reconsider B = x as strict SubAlgebra of A by UNIALG_2:def 14;
MSSign A = MSSign B by Th7;
then MSAlg B is strict non-empty MSSubAlgebra of MSAlg A by Th12;
then reconsider y = MSAlg B as Element of MSSub MSAlg A by MSUALG_2:def 19;
take y, B;
thus thesis;
end;
consider f being Function of Sub A,MSSub MSAlg A such that
A3: for x being Element of Sub A holds P[x,f.x] from FUNCT_2:sch 3(A2);
reconsider f as Function of the carrier of UnSubAlLattice A, the carrier of
MSSubAlLattice MSAlg A;
f is Homomorphism of UnSubAlLattice A, MSSubAlLattice MSAlg A
proof
AA: f is "\/"-preserving
proof
let a1,b1 be Element of UnSubAlLattice A;
reconsider a2=a1,b2=b1 as Element of Sub A;
reconsider a3=a2,b3=b2 as strict non-empty SubAlgebra of A
by UNIALG_2:def 14;
reconsider s=a3"\/"b3 as Element of Sub A by UNIALG_2:def 14;
reconsider m= a3 /\ b3 as Element of Sub A by UNIALG_2:def 14;
A4: ex A1 be strict non-empty SubAlgebra of A st A1= s & f.s = MSAlg A1 by A3;
MSSign b3 = MSSign A by Th7;
then reconsider
g2 = MSAlg b3 as strict non-empty MSSubAlgebra of MSAlg A by Th12;
consider A4 be strict non-empty SubAlgebra of A such that
A5: A4=b3 and
A6: f.b3= MSAlg A4 by A3;
MSSign A4 = MSSign A by Th7;
then reconsider
g3= MSAlg A4 as strict non-empty MSSubAlgebra of MSAlg A by Th12;
MSSign a3 = MSSign A by Th7;
then reconsider
g1 = MSAlg a3 as strict non-empty MSSubAlgebra of MSAlg A by Th12;
consider A3 be strict non-empty SubAlgebra of A such that
A7: A3=a3 and
A8: f.a3= MSAlg A3 by A3;
MSSign A3 = MSSign A by Th7;
then reconsider
g4= MSAlg A3 as strict non-empty MSSubAlgebra of MSAlg A by Th12;
thus f.(a1 "\/" b1) = f.((UniAlg_join A).(a2,b2)) by LATTICES:def 1
.= MSAlg (a3"\/"b3) by A4,UNIALG_2:def 15
.= g4 "\/" g3 by A7,A5,Th30
.= (the L_join of MSSubAlLattice MSAlg A).(f.a1,f.b1) by A8,A6,
MSUALG_2:def 20
.= f.a1 "\/" f.b1 by LATTICES:def 1;
end;
f is "/\"-preserving
proof
let a1,b1 be Element of UnSubAlLattice A;
reconsider a2=a1,b2=b1 as Element of Sub A;
reconsider a3=a2,b3=b2 as strict non-empty SubAlgebra of A
by UNIALG_2:def 14;
reconsider s=a3"\/"b3 as Element of Sub A by UNIALG_2:def 14;
reconsider m= a3 /\ b3 as Element of Sub A by UNIALG_2:def 14;
MSSign b3 = MSSign A by Th7;
then reconsider
g2 = MSAlg b3 as strict non-empty MSSubAlgebra of MSAlg A by Th12;
consider A4 be strict non-empty SubAlgebra of A such that
A5: A4=b3 and
A6: f.b3= MSAlg A4 by A3;
MSSign A4 = MSSign A by Th7;
then reconsider
g3= MSAlg A4 as strict non-empty MSSubAlgebra of MSAlg A by Th12;
MSSign a3 = MSSign A by Th7;
then reconsider
g1 = MSAlg a3 as strict non-empty MSSubAlgebra of MSAlg A by Th12;
consider A3 be strict non-empty SubAlgebra of A such that
A7: A3=a3 and
A8: f.a3= MSAlg A3 by A3;
MSSign A3 = MSSign A by Th7;
then reconsider
g4= MSAlg A3 as strict non-empty MSSubAlgebra of MSAlg A by Th12;
A9: ex A1 be strict non-empty SubAlgebra of A st A1=m & f.m = MSAlg A1 by A3;
thus f.(a1 "/\" b1) = f.((UniAlg_meet A).(a2,b2)) by LATTICES:def 2
.= MSAlg (a3 /\ b3) by A9,UNIALG_2:def 16
.= g1 /\ g2 by Th31
.= (the L_meet of MSSubAlLattice MSAlg A).(f.a1,f.b1) by A7,A8,A5,A6,
MSUALG_2:def 21
.= (f.a1) "/\" (f.b1) by LATTICES:def 2;
end;
hence thesis by AA;
end;
then reconsider
f as Homomorphism of UnSubAlLattice A, MSSubAlLattice MSAlg A;
take f;
now
let x1,x2 be object such that
A11: x1 in dom f & x2 in dom f and
A12: f.x1 = f.x2;
reconsider y1 = x1, y2 = x2 as Element of Sub A by A11,FUNCT_2:def 1;
consider A1 be strict SubAlgebra of A such that
A13: A1= y1 and
A14: f.y1= MSAlg A1 by A3;
consider A2 be strict SubAlgebra of A such that
A15: A2= y2 & f.y2= MSAlg A2 by A3;
A16: MSSign A1 = MSSign A by Th7
.= MSSign A2 by Th7;
thus x1 = 1-Alg MSAlg A1 by A13,MSUALG_1:9
.= x2 by A12,A14,A15,A16,MSUALG_1:9;
end;
hence f is one-to-one by FUNCT_1:def 4;
A17: dom f = Sub A by FUNCT_2:def 1;
thus rng f = the carrier of MSSubAlLattice MSAlg A
proof
thus rng f c= the carrier of MSSubAlLattice MSAlg A by RELAT_1:def 19;
let x be object;
assume x in the carrier of MSSubAlLattice MSAlg A;
then reconsider y = x as strict MSSubAlgebra of MSAlg A by MSUALG_2:def 19;
reconsider C=Constants(MSAlg A) as MSSubset of y by MSUALG_2:10;
C c= the Sorts of y by PBOOLE:def 18;
then (the Sorts of y) is non-empty by PBOOLE:131;
then reconsider y as strict non-empty MSSubAlgebra of MSAlg A by
MSUALG_1:def 3;
1-Alg y is SubAlgebra of 1-Alg MSAlg A by Th20;
then 1-Alg y is SubAlgebra of A by MSUALG_1:9;
then reconsider y1=(1-Alg y) as Element of Sub A by UNIALG_2:def 14;
ex A1 be strict SubAlgebra of A st A1= y1 & f.y1 = MSAlg A1 by A3;
then
A18: f.(1-Alg y) = x by A1,Th26;
y1 in dom f by A17;
hence thesis by A18,FUNCT_1:def 3;
end;
end;