:: Homomorphisms of Order Sorted Algebras
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users

definition

let R be non empty Poset;
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;

:: deftheorem defines order-sorted OSALG_3:def 1 :
for R being non empty Poset
for F being ManySortedFunction of the carrier of R holds
( F is order-sorted iff 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 ) );

:: maybe later cluster 1-1 order-sorted (when clusterable)
:: REVISE the prf of cluster in MSUALG_3

theorem Th1: :: OSALG_3:1

for R being non empty Poset
for F being ManySortedFunction of the carrier of R st F is order-sorted holds
for s1, s2 being Element of R st s1 <= s2 holds
( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 )

proof end;

theorem Th2: :: OSALG_3:2

for R being non empty Poset
for A being OrderSortedSet of R
for B being V2() OrderSortedSet of R
for F being 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 )

proof end;

theorem :: OSALG_3:3

for R being non empty Poset
for F being ManySortedFunction of the carrier of R st F is order-sorted holds
for w1, w2 being Element of the carrier of R * st w1 <= w2 holds
(F #) . w1 c= (F #) . w2

proof end;

theorem Th4: :: OSALG_3:4

for R being non empty Poset
for A being OrderSortedSet of R holds id A is order-sorted

proof end;

registration

let R be non empty Poset;
let A be OrderSortedSet of R;

cluster id A -> order-sorted ;

coherence
id A is order-sorted by Th4;

end;

theorem Th5: :: OSALG_3:5

for R being non empty Poset
for A being OrderSortedSet of R
for B, C being V2() OrderSortedSet of R
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is order-sorted & G is order-sorted holds
G ** F is order-sorted

proof end;

theorem Th6: :: OSALG_3:6

for R being non empty Poset
for A, B being OrderSortedSet of R
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" & F is order-sorted holds
F "" is order-sorted

proof end;

:: this could be done via by cluster, when non clusterable attrs removed

theorem Th7: :: OSALG_3:7

for R being non empty Poset
for A being OrderSortedSet of R
for F being ManySortedFunction of the carrier of R st F is order-sorted holds
F .:.: A is OrderSortedSet of R

proof end;

definition

let S1 be OrderSortedSign;
let U1, U2 be OSAlgebra of S1;

pred U1,U2 are_os_isomorphic means :: OSALG_3:def 2
ex F being ManySortedFunction of U1,U2 st
( F is_isomorphism U1,U2 & F is order-sorted );

end;

:: deftheorem defines are_os_isomorphic OSALG_3:def 2 :
for S1 being OrderSortedSign
for U1, U2 being OSAlgebra of S1 holds
( U1,U2 are_os_isomorphic iff ex F being ManySortedFunction of U1,U2 st
( F is_isomorphism U1,U2 & F is order-sorted ) );

theorem Th8: :: OSALG_3:8

for S1 being OrderSortedSign
for U1 being OSAlgebra of S1 holds U1,U1 are_os_isomorphic

proof end;

theorem Th9: :: OSALG_3:9

for S1 being OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds
U2,U1 are_os_isomorphic

proof end;

definition

let S1 be OrderSortedSign;
let U1, U2 be OSAlgebra of S1;
:: original: are_os_isomorphic
redefine pred U1,U2 are_os_isomorphic ;
reflexivity
for U1 being OSAlgebra of S1 holds (S1,b₁,b₁) by Th8;

end;

definition

let S1 be OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S1;
:: original: are_os_isomorphic
redefine pred U1,U2 are_os_isomorphic ;
symmetry
for U1, U2 being non-empty OSAlgebra of S1 st (S1,b₁,b₂) holds
(S1,b₂,b₁) by Th9;

end;

:: prove for order-sorted

theorem :: OSALG_3:10

for S1 being OrderSortedSign
for U1, U2, U3 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic holds
U1,U3 are_os_isomorphic

proof end;

:: again, should be done as cluster or redefine

theorem Th11: :: OSALG_3:11

for S1 being OrderSortedSign
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

proof end;

theorem Th12: :: OSALG_3:12

for S1 being OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is order-sorted holds
for o1, o2 being OperSymbol of S1 st o1 <= o2 holds
for x being Element of Args (o1,U1)
for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1

proof end;

theorem Th13: :: OSALG_3:13

for S1 being OrderSortedSign
for U1 being non-empty monotone OSAlgebra of S1
for 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 )

proof end;

theorem Th14: :: OSALG_3:14

for S1 being OrderSortedSign
for U1 being monotone OSAlgebra of S1
for U2 being OSSubAlgebra of U1 holds U2 is monotone

proof end;

registration

let S1 be OrderSortedSign;
let U1 be monotone OSAlgebra of S1;

cluster order-sorted monotone for MSSubAlgebra of U1;

existence
ex b₁ being OSSubAlgebra of U1 st b₁ is monotone

proof end;

end;

registration

let S1 be OrderSortedSign;
let U1 be monotone OSAlgebra of S1;

cluster order-sorted -> monotone for MSSubAlgebra of U1;

coherence
for b₁ being OSSubAlgebra of U1 holds b₁ is monotone by Th14;

end;

theorem Th15: :: OSALG_3:15

for S1 being OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
ex G being ManySortedFunction of U1,(Image F) st
( F = G & G is order-sorted & G is_epimorphism U1, Image F )

proof end;

theorem :: OSALG_3:16

for S1 being OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
ex F1 being ManySortedFunction of U1,(Image F) ex F2 being 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 )

proof end;

registration

let S1 be OrderSortedSign;
let U1 be OSAlgebra of S1;

cluster MSAlgebra(# the Sorts of U1, the Charact of U1 #) -> order-sorted ;

coherence
MSAlgebra(# the Sorts of U1, the Charact of U1 #) is order-sorted

proof end;

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:17

for S1 being OrderSortedSign
for U1 being OSAlgebra of S1 holds
( U1 is monotone iff MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone )

proof end;

:: 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:18

for S1 being OrderSortedSign
for U1, U2 being strict non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds
( U1 is monotone iff U2 is monotone )

proof end;