Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

### The abstract of the Mizar article:

### Homomorphisms of Many Sorted Algebras

**by****Malgorzata Korolkiewicz**- Received April 25, 1994
- MML identifier: MSUALG_3

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_1, MSUALG_1, PBOOLE, PRALG_1, FUNCT_1, RELAT_1, BOOLE, ZF_REFLE, QC_LANG1, TDGROUP, FUNCT_6, FUNCT_5, FINSEQ_4, ALG_1, CARD_3, GROUP_6, WELLORD1, MSUALG_2, UNIALG_2, MSUALG_3; notation TARSKI, XBOOLE_0, SUBSET_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, CARD_3, FINSEQ_4, FUNCT_5, FUNCT_6, PBOOLE, STRUCT_0, PRALG_1, MSUALG_1, MSUALG_2, PRALG_2; constructors FINSEQ_4, MSUALG_2, PRALG_2, MEMBERED, PARTFUN1, RELAT_2, XBOOLE_0; clusters FUNCT_1, PBOOLE, MSUALG_1, MSUALG_2, PRALG_1, RELSET_1, STRUCT_0, MEMBERED, ZFMISC_1, PARTFUN1, FUNCT_2, XBOOLE_0; requirements BOOLE, SUBSET; begin reserve S for non void non empty ManySortedSign, U1,U2 for MSAlgebra over S, o for OperSymbol of S, n for Nat; ::::::::::::::::::::::::::::::::::::::::::::::::: :: :: :: PRELIMINARIES - MANY SORTED FUNCTIONS :: :: :: ::::::::::::::::::::::::::::::::::::::::::::::::: definition let I be non empty set, A,B be ManySortedSet of I, F be ManySortedFunction of A,B, i be Element of I; redefine func F.i -> Function of A.i,B.i; end; definition let S; let U1,U2 be MSAlgebra over S; mode ManySortedFunction of U1,U2 is ManySortedFunction of the Sorts of U1, the Sorts of U2; end; definition let I be set,A be ManySortedSet of I; func id A -> ManySortedFunction of A,A means :: MSUALG_3:def 1 for i be set st i in I holds it.i = id (A.i); end; definition let IT be Function; attr IT is "1-1" means :: MSUALG_3:def 2 for i be set, f be Function st i in dom IT & IT.i = f holds f is one-to-one; end; definition let I be set; cluster "1-1" ManySortedFunction of I; end; theorem :: MSUALG_3:1 for I be set,F be ManySortedFunction of I holds F is "1-1" iff for i be set st i in I holds F.i is one-to-one; definition let I be set, A,B be ManySortedSet of I; let IT be ManySortedFunction of A,B; attr IT is "onto" means :: MSUALG_3:def 3 for i be set st i in I holds rng(IT.i) = B.i; end; definition let F,G be Function-yielding Function; func G**F -> Function-yielding Function means :: MSUALG_3:def 4 dom it = (dom F) /\ (dom G) & for i be set st i in dom it holds it.i = (G.i)*(F.i); end; theorem :: MSUALG_3:2 for I be set, A,B,C be ManySortedSet of I, F be ManySortedFunction of A,B, G be ManySortedFunction of B,C holds dom (G ** F) = I & for i be set st i in I holds (G**F).i = (G.i)*(F.i); definition let I be set, A be ManySortedSet of I, B,C be non-empty ManySortedSet of I, F be ManySortedFunction of A,B, G be ManySortedFunction of B,C; redefine func G**F -> ManySortedFunction of A,C; end; theorem :: MSUALG_3:3 for I be set,A,B be ManySortedSet of I, F be ManySortedFunction of A,B holds F**(id A) = F; theorem :: MSUALG_3:4 for I be set, A,B be ManySortedSet of I for F be ManySortedFunction of A, B holds (id B)**F = F; definition let I be set, A,B be ManySortedSet of I, F be ManySortedFunction of A,B; assume F is "1-1" & F is "onto"; func F"" -> ManySortedFunction of B,A means :: MSUALG_3:def 5 for i be set st i in I holds it.i = (F.i)"; end; theorem :: MSUALG_3:5 for I be set,A,B be non-empty ManySortedSet of I, H be ManySortedFunction of A,B, H1 be ManySortedFunction of B,A st H is "1-1" "onto" & H1 = H"" holds H**H1 = id B & H1**H = id A; definition let I be set, A be ManySortedSet of I, F be ManySortedFunction of I; func F.:.:A -> ManySortedSet of I means :: MSUALG_3:def 6 for i be set st i in I holds it.i = (F.i).:(A.i); end; definition let S; let U1 be non-empty MSAlgebra over S; let o; cluster -> Function-like Relation-like Element of Args(o,U1); end; begin ::::::::::::::::::::::::::::::::::::::::::::::: :: :: :: HOMOMORPHISMS OF MANY SORTED ALGEBRAS :: :: :: ::::::::::::::::::::::::::::::::::::::::::::::: theorem :: MSUALG_3:6 for U1 being MSAlgebra over S for x be Function st x in Args(o,U1) holds dom x = dom (the_arity_of o) & for y be set st y in dom ((the Sorts of U1) * (the_arity_of o)) holds x.y in ((the Sorts of U1) * (the_arity_of o)).y; definition let S; let U1,U2 be MSAlgebra over S; let o; let F be ManySortedFunction of U1,U2; let x be Element of Args(o,U1); assume that Args(o,U1) <> {} and Args(o,U2) <> {}; func F # x -> Element of Args(o,U2) equals :: MSUALG_3:def 7 (Frege(F*the_arity_of o)).x; end; definition let S; let U1 be non-empty MSAlgebra over S; let o; cluster Function-like Relation-like Element of Args(o,U1); end; definition let S; let U1,U2 be non-empty MSAlgebra over S; let o; let F be ManySortedFunction of U1,U2; let x be Element of Args(o,U1); redefine func F # x -> Function-like Relation-like Element of Args(o,U2 ) means :: MSUALG_3:def 8 for n st n in dom x holds it.n = (F.((the_arity_of o)/.n)).(x.n); end; theorem :: MSUALG_3:7 for S,o for U1 being MSAlgebra over S st Args(o,U1) <> {} for x be Element of Args(o,U1) holds x = ((id (the Sorts of U1))#x); theorem :: MSUALG_3:8 for U1,U2,U3 being non-empty MSAlgebra over S for H1 be ManySortedFunction of U1,U2, H2 be ManySortedFunction of U2,U3, x be Element of Args(o,U1) holds (H2**H1)#x = H2#(H1#x); definition let S; let U1,U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; pred F is_homomorphism U1,U2 means :: MSUALG_3:def 9 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,U2).(F#x); end; theorem :: MSUALG_3:9 for U1 being MSAlgebra over S holds id (the Sorts of U1) is_homomorphism U1,U1; theorem :: MSUALG_3:10 for U1,U2,U3 being non-empty MSAlgebra over S for H1 be ManySortedFunction of U1,U2, H2 be ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds H2 ** H1 is_homomorphism U1,U3; definition let S; let U1,U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; pred F is_epimorphism U1,U2 means :: MSUALG_3:def 10 F is_homomorphism U1,U2 & F is "onto"; end; theorem :: MSUALG_3:11 for U1,U2,U3 being non-empty MSAlgebra over S for F be ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds G**F is_epimorphism U1,U3; definition let S; let U1,U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; pred F is_monomorphism U1,U2 means :: MSUALG_3:def 11 F is_homomorphism U1,U2 & F is "1-1"; end; theorem :: MSUALG_3:12 for U1,U2,U3 being non-empty MSAlgebra over S for F be ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds G**F is_monomorphism U1,U3; definition let S; let U1,U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; pred F is_isomorphism U1,U2 means :: MSUALG_3:def 12 F is_epimorphism U1,U2 & F is_monomorphism U1,U2; end; theorem :: MSUALG_3:13 for F be ManySortedFunction of U1,U2 holds F is_isomorphism U1,U2 iff F is_homomorphism U1,U2 & F is "onto" & F is "1-1"; theorem :: MSUALG_3:14 for U1,U2 being non-empty MSAlgebra over S for H be ManySortedFunction of U1,U2, H1 be ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H"" holds H1 is_isomorphism U2,U1; theorem :: MSUALG_3:15 for U1,U2,U3 being non-empty MSAlgebra over S for H be ManySortedFunction of U1,U2, H1 be ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds H1 ** H is_isomorphism U1,U3; definition let S; let U1,U2 be MSAlgebra over S; pred U1,U2 are_isomorphic means :: MSUALG_3:def 13 ex F be ManySortedFunction of U1,U2 st F is_isomorphism U1,U2; end; theorem :: MSUALG_3:16 for U1 being MSAlgebra over S holds id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic; definition let S; let U1, U2 be MSAlgebra over S; redefine pred U1, U2 are_isomorphic; reflexivity; end; theorem :: MSUALG_3:17 for U1,U2 being non-empty MSAlgebra over S holds U1,U2 are_isomorphic implies U2,U1 are_isomorphic; theorem :: MSUALG_3:18 for U1,U2,U3 being non-empty MSAlgebra over S holds U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic; definition let S; let U1,U2 be non-empty MSAlgebra over S; let F be ManySortedFunction of U1,U2; assume F is_homomorphism U1,U2; func Image F -> strict non-empty MSSubAlgebra of U2 means :: MSUALG_3:def 14 the Sorts of it = F.:.:(the Sorts of U1); end; theorem :: MSUALG_3:19 for U1 being non-empty MSAlgebra over S, U2 being strict non-empty MSAlgebra over S, F be ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds F is_epimorphism U1,U2 iff Image F = U2; theorem :: MSUALG_3:20 for U1,U2 being non-empty MSAlgebra over S for F be ManySortedFunction of U1,U2, G be ManySortedFunction of U1,Image F st F = G & F is_homomorphism U1,U2 holds G is_epimorphism U1,Image F; theorem :: MSUALG_3:21 for U1,U2 being non-empty MSAlgebra over S for F be ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 ex G be ManySortedFunction of U1,Image F st F = G & G is_epimorphism U1,Image F; theorem :: MSUALG_3:22 for U1 being non-empty MSAlgebra over S for U2 be non-empty MSSubAlgebra of U1, G be ManySortedFunction of U2,U1 st G = id (the Sorts of U2) holds G is_monomorphism U2,U1; theorem :: MSUALG_3:23 for U1,U2 being non-empty MSAlgebra over S for F be ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 ex F1 be ManySortedFunction of U1,Image F, F2 be ManySortedFunction of Image F,U2 st F1 is_epimorphism U1,Image F & F2 is_monomorphism Image F,U2 & F = F2**F1; theorem :: MSUALG_3:24 for S for U1,U2 being MSAlgebra over S for o for F being ManySortedFunction of U1,U2 for x being Element of Args(o,U1), f,u being Function st x = f & x in Args(o,U1) & u in Args(o,U2) holds u = F#x iff for n st n in dom f holds u.n = (F.((the_arity_of o)/.n)).(f.n);

Back to top