:: On the Trivial Many Sorted Algebras and Many Sorted Congruences
:: by Artur Korni\l owicz
::
:: Received June 11, 1996
:: Copyright (c) 1996-2016 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 XBOOLE_0, STRUCT_0, MSUALG_1, PBOOLE, FINSET_1, SUBSET_1,
CLOSURE2, TARSKI, RELAT_1, FUNCT_1, FINSEQ_1, MARGREL1, NAT_1, PRALG_2,
CARD_3, RLVECT_2, MSAFREE, PRELAMB, ZFMISC_1, PRALG_1, MCART_1, EQREL_1,
FUNCOP_1, MSUALG_3, TREES_4, LANG1, NUMBERS, MSUALG_2, MEMBER_1, GROUP_6,
WELLORD1, PARTFUN1, FUNCT_6, FINSEQ_4, PZFMISC1, CARD_1, MSUALG_4,
MSUALG_5, SETFAM_1, FUNCT_4, RELAT_2, MSUALG_9;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
RELAT_2, STRUCT_0, SETFAM_1, FUNCT_1, PBOOLE, EQREL_1, RELSET_1,
PARTFUN1, FUNCT_2, FINSEQ_1, LANG1, XTUPLE_0, MCART_1, FINSET_1, CARD_3,
NAT_1, TREES_4, FUNCT_6, DTCONSTR, MSUALG_1, MSUALG_2, PRALG_1, MSUALG_3,
MSAFREE, PRALG_2, FUNCOP_1, MSAFREE2, MSUALG_4, PZFMISC1, MSSUBFAM,
CLOSURE2, MSUALG_5;
constructors BINOP_1, PZFMISC1, MSUALG_3, MSUALG_5, CLOSURE1, CLOSURE2,
PRALG_3, RELSET_1, CIRCUIT1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, RELAT_1, ORDINAL1, FUNCT_2, FUNCOP_1, FINSET_1,
EQREL_1, PRE_CIRC, PZFMISC1, MSSUBFAM, STRUCT_0, FUNCT_1, MSUALG_1,
MSUALG_2, PRALG_2, MSUALG_3, MSAFREE, MSUALG_4, MSUALG_5, CLOSURE2,
CARD_3, RELSET_1, PRALG_1, PBOOLE, XTUPLE_0;
requirements SUBSET, BOOLE;
begin :: Preliminaries
reserve a, I for set,
S for non empty non void ManySortedSign;
registration
let I be set, M be ManySortedSet of I;
cluster finite-yielding for Element of Bool M;
end;
registration
let I be set, M be non-empty ManySortedSet of I;
cluster non-empty finite-yielding for ManySortedSubset of M;
end;
registration
let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S,
o be OperSymbol of S;
cluster -> FinSequence-like for Element of Args(o,A);
end;
registration
let S be non void non empty ManySortedSign, I be set, s be SortSymbol of S,
F be MSAlgebra-Family of I, S;
cluster -> Function-like Relation-like for Element of (SORTS F).s;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
cluster FreeGen X -> free non-empty;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
cluster FreeMSA X -> free;
end;
registration
let S be non empty non void ManySortedSign, A, B be non-empty MSAlgebra over
S;
cluster [:A,B:] -> non-empty;
end;
theorem :: MSUALG_9:1
for X, Y being set, f being Function st a in dom f & f.a in [:X,Y:]
holds f.a = [(pr1 f).a, (pr2 f).a];
theorem :: MSUALG_9:2
for X being non empty set, Y being set, f being Function of X, {Y
} holds rng f = {Y};
theorem :: MSUALG_9:3
Class(nabla I) c= {I};
theorem :: MSUALG_9:4
for I being non empty set holds Class(nabla I) = {I};
theorem :: MSUALG_9:5
ex A being ManySortedSet of I st {A} = I --> {a};
theorem :: MSUALG_9:6
for A being ManySortedSet of I ex B being non-empty ManySortedSet of I
st A c= B;
theorem :: MSUALG_9:7
for M being non-empty ManySortedSet of I for B being finite-yielding
ManySortedSubset of M ex C being non-empty finite-yielding ManySortedSubset of
M st B c= C;
theorem :: MSUALG_9:8
for A, B being ManySortedSet of I for F, G being ManySortedFunction of
A, {B} holds F = G;
theorem :: MSUALG_9:9
for A being non-empty ManySortedSet of I, B being ManySortedSet
of I for F being ManySortedFunction of A, {B} holds F is "onto";
theorem :: MSUALG_9:10
for A being ManySortedSet of I, B being non-empty ManySortedSet
of I for F being ManySortedFunction of {A}, B holds F is "1-1";
theorem :: MSUALG_9:11
for X being non-empty ManySortedSet of the carrier of S holds Reverse
X is "1-1";
theorem :: MSUALG_9:12
for A being non-empty finite-yielding ManySortedSet of I ex F being
ManySortedFunction of I --> NAT, A st F is "onto";
theorem :: MSUALG_9:13
for S being non empty ManySortedSign for A being non-empty MSAlgebra
over S for f, g being Element of product the Sorts of A
st for i being object
holds proj(the Sorts of A,i).f = proj(the Sorts of A,i).g holds f = g;
theorem :: MSUALG_9:14
for I being non empty set for s being Element of S for A being
MSAlgebra-Family of I,S for f, g being Element of product Carrier(A,s) st for a
being Element of I holds proj(Carrier(A,s),a).f = proj(Carrier(A,s),a).g holds
f = g;
theorem :: MSUALG_9:15
for A, B being non-empty MSAlgebra over S for C being non-empty
MSSubAlgebra of A for h1 being ManySortedFunction of B, C st h1 is_homomorphism
B, C for h2 being ManySortedFunction of B, A st h1 = h2 holds h2
is_homomorphism B, A;
theorem :: MSUALG_9:16
for A, B being non-empty MSAlgebra over S for F being
ManySortedFunction of A, B st F is_monomorphism A, B holds A, Image F
are_isomorphic;
theorem :: MSUALG_9:17
for A, B being non-empty MSAlgebra over S for F being
ManySortedFunction of A, B st F is "onto" for o being OperSymbol of S for x
being Element of Args(o,B) holds ex y being Element of Args(o,A) st F # y = x
;
theorem :: MSUALG_9:18
for A being non-empty MSAlgebra over S, o being OperSymbol of S
for x being Element of Args(o,A) holds Den(o,A).x in (the Sorts of A).(
the_result_sort_of o);
theorem :: MSUALG_9:19
for A, B, C being non-empty MSAlgebra over S for F1 being
ManySortedFunction of A, B for F2 being ManySortedFunction of A, C st F1
is_epimorphism A, B & F2 is_homomorphism A, C for G being ManySortedFunction of
B, C st G ** F1 = F2 holds G is_homomorphism B, C;
reserve A, M for ManySortedSet of I,
B, C for non-empty ManySortedSet of I;
definition
let I be set;
let A be ManySortedSet of I;
let B, C be non-empty ManySortedSet of I;
let F be ManySortedFunction of A, [|B,C|];
func Mpr1 F -> ManySortedFunction of A, B means
:: MSUALG_9:def 1
for i being set st i in I holds it.i = pr1 (F.i);
func Mpr2 F -> ManySortedFunction of A, C means
:: MSUALG_9:def 2
for i being set st i in I holds it.i = pr2 (F.i);
end;
theorem :: MSUALG_9:20
for F being ManySortedFunction of A, [| I-->{a} , I-->{a} |] holds
Mpr1 F = Mpr2 F;
theorem :: MSUALG_9:21
for F being ManySortedFunction of A, [|B,C|] st F is "onto" holds Mpr1
F is "onto";
theorem :: MSUALG_9:22
for F being ManySortedFunction of A, [|B,C|] st F is "onto" holds Mpr2
F is "onto";
theorem :: MSUALG_9:23
for F being ManySortedFunction of A, [|B,C|] st M in doms F holds for
i be set st i in I holds (F..M).i = [((Mpr1 F)..M).i, ((Mpr2 F)..M).i];
begin :: On the Trivial Many Sorted Algebras
registration
let S be non empty ManySortedSign;
cluster the Sorts of Trivial_Algebra S -> finite-yielding non-empty;
end;
registration
let S be non empty ManySortedSign;
cluster Trivial_Algebra S -> finite-yielding non-empty;
end;
theorem :: MSUALG_9:24
for A being non-empty MSAlgebra over S for F being
ManySortedFunction of A, Trivial_Algebra S for o being OperSymbol of S for x
being Element of Args(o,A) holds (F.the_result_sort_of o).(Den(o,A).x) = 0 &
Den(o,Trivial_Algebra S).(F#x) = 0;
theorem :: MSUALG_9:25
for A being non-empty MSAlgebra over S for F being
ManySortedFunction of A, Trivial_Algebra S holds F is_epimorphism A,
Trivial_Algebra S;
theorem :: MSUALG_9:26
for A being MSAlgebra over S st ex X being ManySortedSet of the
carrier of S st the Sorts of A = {X} holds A, Trivial_Algebra S are_isomorphic;
begin :: On the Many Sorted Congruences
theorem :: MSUALG_9:27
for A being non-empty MSAlgebra over S for C being MSCongruence of A
holds C is ManySortedSubset of [|the Sorts of A, the Sorts of A|];
theorem :: MSUALG_9:28
for A being non-empty MSAlgebra over S for R being Subset of CongrLatt
A for F being SubsetFamily of [|the Sorts of A, the Sorts of A|] st R = F holds
meet |:F:| is MSCongruence of A;
theorem :: MSUALG_9:29
for A being non-empty MSAlgebra over S for C being MSCongruence of A
st C = [|the Sorts of A, the Sorts of A|] holds the Sorts of QuotMSAlg (A,C) =
{the Sorts of A};
theorem :: MSUALG_9:30
for A, B being non-empty MSAlgebra over S for F being
ManySortedFunction of A, B st F is_homomorphism A, B holds MSHomQuot F **
MSNat_Hom(A,MSCng F) = F;
theorem :: MSUALG_9:31
for A being non-empty MSAlgebra over S for C being MSCongruence
of A for s being SortSymbol of S for a being Element of (the Sorts of QuotMSAlg
(A,C)).s ex x being Element of (the Sorts of A).s st a = Class(C,x);
theorem :: MSUALG_9:32
for A being MSAlgebra over S for C1, C2 being MSEquivalence-like
ManySortedRelation of A st C1 c= C2 for i being Element of S for x, y being
Element of (the Sorts of A).i st [x,y] in C1.i holds Class (C1,x) c= Class (C2,
y) & (A is non-empty implies Class (C1,y) c= Class (C2,x));
theorem :: MSUALG_9:33
for A being non-empty MSAlgebra over S, C being MSCongruence of A for
s being SortSymbol of S, x, y being Element of (the Sorts of A).s holds (
MSNat_Hom(A,C)).s.x = (MSNat_Hom(A,C)).s.y iff [x,y] in C.s;
theorem :: MSUALG_9:34
for A being non-empty MSAlgebra over S for C1, C2 being
MSCongruence of A for G being ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg
(A,C2) st for i being Element of S for x being Element of (the Sorts of
QuotMSAlg (A,C1)).i for xx being Element of (the Sorts of A).i st x = Class(C1,
xx) holds G.i.x = Class(C2,xx) holds G ** MSNat_Hom(A,C1) = MSNat_Hom(A,C2);
theorem :: MSUALG_9:35
for A being non-empty MSAlgebra over S for C1, C2 being
MSCongruence of A for G being ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg
(A,C2) st for i being Element of S for x being Element of (the Sorts of
QuotMSAlg (A,C1)).i for xx being Element of (the Sorts of A).i st x = Class(C1,
xx) holds G.i.x = Class(C2,xx) holds G is_epimorphism QuotMSAlg (A,C1),
QuotMSAlg (A,C2);
theorem :: MSUALG_9:36
for A, B being non-empty MSAlgebra over S for F being
ManySortedFunction of A, B st F is_homomorphism A, B for C1 being MSCongruence
of A st C1 c= MSCng F ex H being ManySortedFunction of QuotMSAlg (A,C1), B st H
is_homomorphism QuotMSAlg (A,C1), B & F = H ** MSNat_Hom(A,C1);