:: The Correspondence Between Homomorphisms of Universal Algebra &
:: Many Sorted Algebra
:: by Adam Grabowski
::
:: Received December 13, 1994
:: Copyright (c) 1994-2019 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 UNIALG_1, NAT_1, XBOOLE_0, FUNCT_1, RELAT_1, TARSKI, SUBSET_1,
FINSEQ_1, FUNCOP_1, PBOOLE, CARD_3, MSUALG_1, XXREAL_0, STRUCT_0,
FINSEQ_2, PARTFUN1, CQC_SIM1, CARD_1, UNIALG_2, MARGREL1, NUMBERS,
MSUALG_3, MEMBER_1, MSUHOM_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, CARD_3, FUNCOP_1, FINSEQ_1,
STRUCT_0, UNIALG_1, UNIALG_2, FINSEQ_2, ALG_1, MSUALG_3, MSUALG_1,
XXREAL_0;
constructors FINSEQOP, ALG_1, MSUALG_3, XREAL_0, RELSET_1, NAT_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1,
XREAL_0, PRE_CIRC, STRUCT_0, MSUALG_1, MSUALG_3, RELAT_1, PBOOLE,
FINSEQ_1;
requirements NUMERALS, SUBSET, BOOLE;
begin
reserve U1,U2,U3 for Universal_Algebra,
m,n for Nat,
a for set,
A for non empty set,
h for Function of U1,U2;
theorem :: MSUHOM_1:1
for f,g be Function, C be set st rng f c= C holds (g|C)*f = g*f;
theorem :: MSUHOM_1:2
for I be set, C be Subset of I holds C* c= I*;
theorem :: MSUHOM_1:3
for f be Function, C be set st f is Function-yielding holds f|C is
Function-yielding;
theorem :: MSUHOM_1:4
for I be set, C be Subset of I, M be ManySortedSet of I holds (M|
C)# = M#|(C*);
definition
let S,S9 be non empty ManySortedSign;
pred S <= S9 means
:: MSUHOM_1:def 1
the carrier of S c= the carrier of S9 & the
carrier' of S c= the carrier' of S9 & (the Arity of S9)|the carrier' of S = the
Arity of S & (the ResultSort of S9)|the carrier' of S = the ResultSort of S;
reflexivity;
end;
theorem :: MSUHOM_1:5
for S,S9,S99 be non empty ManySortedSign st S <= S9 & S9 <= S99 holds
S <= S99;
theorem :: MSUHOM_1:6
for S,S9 be strict non empty ManySortedSign st S <= S9 & S9 <= S holds S = S9
;
theorem :: MSUHOM_1:7
for g be Function, a be Element of A for k be Nat st 1 <= k & k <= n
holds (a .--> g).((n |-> a)/.k) = g;
theorem :: MSUHOM_1:8
for I be set,I0 be Subset of I, A,B be ManySortedSet of I, F be
ManySortedFunction of A,B for A0,B0 be ManySortedSet of I0 st A0 = A | I0 & B0
= B | I0 holds F|I0 is ManySortedFunction of A0,B0;
definition
let S,S9 be strict non void non empty ManySortedSign;
let A be non-empty strict MSAlgebra over S9;
assume
S <= S9;
func A Over S -> non-empty strict MSAlgebra over S means
:: MSUHOM_1:def 2
the Sorts of
it = (the Sorts of A)|the carrier of S & the Charact of it = (the Charact of A)
|the carrier' of S;
end;
theorem :: MSUHOM_1:9
for S be strict non void non empty ManySortedSign, A be non-empty
strict MSAlgebra over S holds A = A Over S;
theorem :: MSUHOM_1:10
for U1,U2 st U1,U2 are_similar holds MSSign U1 = MSSign U2;
definition
let U1,U2 be Universal_Algebra, h be Function of U1,U2;
assume
MSSign U1 = MSSign U2;
func MSAlg h -> ManySortedFunction of MSAlg U1, ((MSAlg U2) Over MSSign U1)
equals
:: MSUHOM_1:def 3
0 .--> h;
end;
theorem :: MSUHOM_1:11
for U1,U2,h st U1,U2 are_similar for o be OperSymbol of MSSign
U1 holds ((MSAlg h).(the_result_sort_of o)) = h;
theorem :: MSUHOM_1:12
for o be OperSymbol of MSSign U1 holds Den(o,MSAlg U1) = (the
charact of U1).o;
theorem :: MSUHOM_1:13
for o be OperSymbol of MSSign U1 holds Den(o,MSAlg U1) is operation of U1;
theorem :: MSUHOM_1:14
for o be OperSymbol of MSSign U1 for y be Element of Args(o,
MSAlg U1) holds y is FinSequence of the carrier of U1;
theorem :: MSUHOM_1:15
for U1,U2,h st U1,U2 are_similar for o be OperSymbol of MSSign
U1,y be Element of Args(o,MSAlg U1) holds (MSAlg h)#y = h * y;
theorem :: MSUHOM_1:16
h is_homomorphism implies MSAlg h is_homomorphism MSAlg U1
,(MSAlg U2 Over MSSign U1);
theorem :: MSUHOM_1:17
U1,U2 are_similar implies MSAlg h is ManySortedSet of {0};
theorem :: MSUHOM_1:18
h is_epimorphism implies MSAlg h is_epimorphism MSAlg U1,
(MSAlg U2 Over MSSign U1);
theorem :: MSUHOM_1:19
h is_monomorphism implies MSAlg h is_monomorphism MSAlg
U1,(MSAlg U2 Over MSSign U1);
theorem :: MSUHOM_1:20
h is_isomorphism implies MSAlg h is_isomorphism MSAlg U1,(MSAlg
U2 Over MSSign U1);
theorem :: MSUHOM_1:21
for U1,U2,h st U1,U2 are_similar holds MSAlg h is_homomorphism
MSAlg U1,(MSAlg U2 Over MSSign U1) implies h is_homomorphism;
theorem :: MSUHOM_1:22
for U1,U2,h st U1, U2 are_similar holds MSAlg h is_epimorphism
MSAlg U1, (MSAlg U2 Over MSSign U1) implies h is_epimorphism;
theorem :: MSUHOM_1:23
for U1, U2, h st U1, U2 are_similar holds MSAlg h
is_monomorphism MSAlg U1, (MSAlg U2 Over MSSign U1) implies h is_monomorphism
;
theorem :: MSUHOM_1:24
for U1, U2, h st U1, U2 are_similar holds MSAlg h is_isomorphism MSAlg
U1, (MSAlg U2 Over MSSign U1) implies h is_isomorphism;
theorem :: MSUHOM_1:25
MSAlg (id the carrier of U1) = (id the Sorts of MSAlg U1);
theorem :: MSUHOM_1:26
for U1,U2,U3 st U1,U2 are_similar & U2,U3 are_similar for h1 be
Function of U1,U2, h2 be Function of U2,U3 holds (MSAlg h2) ** (MSAlg h1) =
MSAlg (h2*h1);