Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### Homomorphisms of Order Sorted Algebras

**by****Josef Urban**- Received September 19, 2002
- MML identifier: OSALG_3

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_1, MSUALG_1, PBOOLE, PRALG_1, FUNCT_1, RELAT_1, BOOLE, ZF_REFLE, CARD_3, QC_LANG1, TDGROUP, FINSEQ_1, FINSEQ_4, ALG_1, SEQM_3, GROUP_6, MSUALG_2, UNIALG_2, MSUALG_3, OSALG_1, ORDERS_1, OSALG_2, OSALG_3; notation TARSKI, XBOOLE_0, SUBSET_1, NAT_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FINSEQ_1, CARD_3, FINSEQ_4, STRUCT_0, ORDERS_1, PRALG_1, MSUALG_1, MSUALG_2, YELLOW18, OSALG_1, OSALG_2, MSUALG_3; constructors ORDERS_3, FINSEQ_4, OSALG_2, MSUALG_3, YELLOW18, MEMBERED; clusters DTCONSTR, FINSEQ_1, MSAFREE, MSUALG_1, ORDERS_3, OSALG_1, PRALG_1, RELSET_1, STRUCT_0, MSUALG_9, PARTFUN1; requirements BOOLE, SUBSET; begin reserve R for non empty Poset, S1 for OrderSortedSign; definition let R; let F be ManySortedFunction of the carrier of R; attr F is order-sorted means :: OSALG_3:def 1 for s1,s2 being Element of R st s1 <= s2 holds for a1 being set st a1 in dom (F.s1) holds a1 in dom (F.s2) & (F.s1).a1 = (F.s2).a1; end; :: maybe later cluster 1-1 order-sorted (when clusterable) :: REVISE the prf of cluster in MSUALG_3 canceled; theorem :: OSALG_3:2 for F being ManySortedFunction of the carrier of R st F is order-sorted for s1,s2 being Element of R st s1 <= s2 holds dom (F.s1) c= dom (F.s2) & F.s1 c= F.s2; theorem :: OSALG_3:3 for A be OrderSortedSet of R, B be non-empty OrderSortedSet of R, F be ManySortedFunction of A,B holds F is order-sorted iff for s1,s2 being Element of R st s1 <= s2 holds for a1 being set st a1 in A.s1 holds (F.s1).a1 = (F.s2).a1; theorem :: OSALG_3:4 for F being ManySortedFunction of the carrier of R st F is order-sorted for w1,w2 being Element of (the carrier of R)* st w1 <= w2 holds F#.w1 c= F#.w2; theorem :: OSALG_3:5 for A being OrderSortedSet of R holds id A is order-sorted; definition let R; let A be OrderSortedSet of R; cluster id A -> order-sorted; end; theorem :: OSALG_3:6 for A be OrderSortedSet of R for B,C be non-empty OrderSortedSet of R, F be ManySortedFunction of A,B, G be ManySortedFunction of B,C holds F is order-sorted & G is order-sorted implies G**F is order-sorted; theorem :: OSALG_3:7 for A,B being OrderSortedSet of R, F being ManySortedFunction of A,B st F is "1-1" & F is "onto" & F is order-sorted holds F"" is order-sorted; :: this could be done via by cluster, when non clusterable attrs removed theorem :: OSALG_3:8 for A being OrderSortedSet of R, F being ManySortedFunction of the carrier of R st F is order-sorted holds F.:.:A is OrderSortedSet of R; definition let S1; let U1,U2 be OSAlgebra of S1; pred U1,U2 are_os_isomorphic means :: OSALG_3:def 2 ex F be ManySortedFunction of U1,U2 st F is_isomorphism U1,U2 & F is order-sorted; end; theorem :: OSALG_3:9 for U1 being OSAlgebra of S1 holds U1,U1 are_os_isomorphic; theorem :: OSALG_3:10 for U1,U2 being non-empty OSAlgebra of S1 holds U1,U2 are_os_isomorphic implies U2,U1 are_os_isomorphic; definition let S1; let U1, U2 be OSAlgebra of S1; redefine pred U1, U2 are_os_isomorphic; reflexivity; end; definition let S1; let U1, U2 be non-empty OSAlgebra of S1; redefine pred U1, U2 are_os_isomorphic; symmetry; end; :: prove for order-sorted theorem :: OSALG_3:11 for U1,U2,U3 being non-empty OSAlgebra of S1 holds U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic implies U1,U3 are_os_isomorphic; :: again, should be done as cluster or redefine theorem :: OSALG_3:12 for U1,U2 being non-empty OSAlgebra of S1 for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds Image F is order-sorted; theorem :: OSALG_3:13 for U1,U2 being non-empty OSAlgebra of S1 for F being ManySortedFunction of U1,U2 st F is order-sorted for o1,o2 being OperSymbol of S1 st o1 <= o2 for x being Element of Args(o1,U1), x1 be Element of Args(o2,U1) st x = x1 holds F # x = F # x1; theorem :: OSALG_3:14 for U1 being monotone non-empty OSAlgebra of S1, U2 being non-empty OSAlgebra of S1 for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds Image F is order-sorted & Image F is monotone OSAlgebra of S1; theorem :: OSALG_3:15 for U1 being monotone OSAlgebra of S1, U2 being OSSubAlgebra of U1 holds U2 is monotone; definition let S1; let U1 be monotone OSAlgebra of S1; cluster monotone OSSubAlgebra of U1; end; definition let S1; let U1 be monotone OSAlgebra of S1; cluster -> monotone OSSubAlgebra of U1; end; theorem :: OSALG_3:16 for U1,U2 being non-empty OSAlgebra of S1 for F be ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted ex G be ManySortedFunction of U1,Image F st F = G & G is order-sorted & G is_epimorphism U1,Image F; theorem :: OSALG_3:17 for U1,U2 being non-empty OSAlgebra of S1 for F be ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted 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 & F1 is order-sorted & F2 is order-sorted; definition let S1; let U1 be OSAlgebra of S1; cluster MSAlgebra(# the Sorts of U1, the Charact of U1 #) -> order-sorted; end; :: very strange, the "strict" attribute is quite unfriendly :: could Grzegorz's suggestion for struct implementation fix this? :: hard to generalize to some useful scheme theorem :: OSALG_3:18 for U1 being OSAlgebra of S1 holds (U1 is monotone iff MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone); :: proving the non strict version is painful, I'll do it only :: if it is necessary, see TWiki.StructureImplementation for some suggestions theorem :: OSALG_3:19 for U1,U2 being strict non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds U1 is monotone iff U2 is monotone;

Back to top