Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

### The abstract of the Mizar article:

### The Correspondence Between Homomorphisms of Universal Algebra \& Many Sorted Algebra

**by****Adam Grabowski**- Received December 13, 1994
- MML identifier: MSUHOM_1

- [ Mizar article, MML identifier index ]

environ vocabulary UNIALG_1, FUNCT_1, RELAT_1, FINSEQ_1, PRALG_1, PBOOLE, TDGROUP, CARD_3, FINSEQ_2, MSUALG_1, BOOLE, CAT_1, AMI_1, ZF_REFLE, CQC_SIM1, FUNCOP_1, UNIALG_2, QC_LANG1, ALG_1, GROUP_6, MSUALG_3, MSUHOM_1, FINSEQ_4; notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, NAT_1, RELAT_1, FUNCT_1, RELSET_1, STRUCT_0, PARTFUN1, FUNCT_2, PBOOLE, CARD_3, CQC_LANG, UNIALG_1, FINSEQ_1, UNIALG_2, PRALG_1, FINSEQ_2, FINSEQ_4, TOPREAL1, ALG_1, MSUALG_3, PRE_CIRC, MSUALG_1; constructors XREAL_0, CQC_LANG, ALG_1, MSUALG_3, PRE_CIRC, FINSEQ_4, FINSEQOP, XCMPLX_0, MEMBERED, XBOOLE_0; clusters MSUALG_1, MSUALG_3, PRE_CIRC, FUNCT_1, RELSET_1, STRUCT_0, CQC_LANG, ARYTM_3, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0, SUBSET_1, NUMBERS, ORDINAL2; 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 A, n; let a be Element of A; redefine func n |-> a -> FinSequence of A; end; definition let S,S' be non empty ManySortedSign; pred S <= S' means :: MSUHOM_1:def 1 the carrier of S c= the carrier of S' & the OperSymbols of S c= the OperSymbols of S' & (the Arity of S')|the OperSymbols of S = the Arity of S & (the ResultSort of S')|the OperSymbols of S = the ResultSort of S; reflexivity; end; theorem :: MSUHOM_1:5 for S,S',S'' be non empty ManySortedSign st S <= S' & S' <= S'' holds S <= S''; theorem :: MSUHOM_1:6 for S,S' be strict non empty ManySortedSign st S <= S' & S' <= S holds S = S'; 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,S' be strict non void non empty ManySortedSign; let A be non-empty strict MSAlgebra over S'; assume S <= S'; 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 OperSymbols 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 U1,U2 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 U1, U2 implies MSAlg h is_epimorphism MSAlg U1, (MSAlg U2 Over MSSign U1); theorem :: MSUHOM_1:19 h is_monomorphism U1, U2 implies MSAlg h is_monomorphism MSAlg U1,(MSAlg U2 Over MSSign U1); theorem :: MSUHOM_1:20 h is_isomorphism U1,U2 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 U1,U2; 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 U1, U2; 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 U1, U2; 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 U1, U2; 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);

Back to top