:: Homomorphisms of Order Sorted Algebras
:: by Josef Urban
::
:: 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;
coherence 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,b1,b1)
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,b1,b2) holds
(S1,b2,b1)
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;
existence
ex b1 being OSSubAlgebra of U1 st b1 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 b1 being OSSubAlgebra of U1 holds b1 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,() 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,() ex F2 being ManySortedFunction of (),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;