deffunc H1( Function) -> set = commute $1;
let X be non empty set ; for S, T being non empty Poset ex F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) st
( F is commuting & F is isomorphic )
let S, T be non empty Poset; ex F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) st
( F is commuting & F is isomorphic )
consider F being ManySortedSet of the carrier of (UPS (S,(T |^ X))) such that
A1:
for f being Element of (UPS (S,(T |^ X))) holds F . f = H1(f)
from PBOOLE:sch 5();
A2:
dom F = the carrier of (UPS (S,(T |^ X)))
by PARTFUN1:def 2;
A3:
rng F c= the carrier of ((UPS (S,T)) |^ X)
proof
let g be
object ;
TARSKI:def 3 ( not g in rng F or g in the carrier of ((UPS (S,T)) |^ X) )
assume
g in rng F
;
g in the carrier of ((UPS (S,T)) |^ X)
then consider f being
object such that A4:
f in dom F
and A5:
g = F . f
by FUNCT_1:def 3;
reconsider f =
f as
directed-sups-preserving Function of
S,
(T |^ X) by A4, Def4;
g = commute f
by A1, A4, A5;
then reconsider g =
g as
Function of
X, the
carrier of
(UPS (S,T)) by Th39;
A6:
rng g c= the
carrier of
(UPS (S,T))
;
dom g = X
by FUNCT_2:def 1;
then
g in Funcs (
X, the
carrier of
(UPS (S,T)))
by A6, FUNCT_2:def 2;
hence
g in the
carrier of
((UPS (S,T)) |^ X)
by YELLOW_1:28;
verum
end;
then reconsider F = F as Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) by A2, FUNCT_2:2;
take
F
; ( F is commuting & F is isomorphic )
consider G being ManySortedSet of the carrier of ((UPS (S,T)) |^ X) such that
A7:
for f being Element of ((UPS (S,T)) |^ X) holds G . f = H1(f)
from PBOOLE:sch 5();
A8:
dom G = the carrier of ((UPS (S,T)) |^ X)
by PARTFUN1:def 2;
A9:
rng G c= the carrier of (UPS (S,(T |^ X)))
proof
let g be
object ;
TARSKI:def 3 ( not g in rng G or g in the carrier of (UPS (S,(T |^ X))) )
assume
g in rng G
;
g in the carrier of (UPS (S,(T |^ X)))
then consider f being
object such that A10:
f in dom G
and A11:
g = G . f
by FUNCT_1:def 3;
the
carrier of
((UPS (S,T)) |^ X) = Funcs (
X, the
carrier of
(UPS (S,T)))
by YELLOW_1:28;
then reconsider f =
f as
Function of
X, the
carrier of
(UPS (S,T)) by A10, FUNCT_2:66;
g = commute f
by A7, A10, A11;
then
g is
directed-sups-preserving Function of
S,
(T |^ X)
by Th40;
hence
g in the
carrier of
(UPS (S,(T |^ X)))
by Def4;
verum
end;
then reconsider G = G as Function of ((UPS (S,T)) |^ X),(UPS (S,(T |^ X))) by A8, FUNCT_2:2;
A12:
G is commuting
A13:
the carrier of (T |^ X) = Funcs (X, the carrier of T)
by YELLOW_1:28;
UPS (S,T) is full SubRelStr of T |^ the carrier of S
by Def4;
then A14:
(UPS (S,T)) |^ X is full SubRelStr of (T |^ the carrier of S) |^ X
by YELLOW16:39;
A15:
UPS (S,(T |^ X)) is full SubRelStr of (T |^ X) |^ the carrier of S
by Def4;
then A16:
G is monotone
by A12, A14, Th19;
thus A17:
F is commuting
F is isomorphic
then A18:
F is monotone
by A15, A14, Th19;
the carrier of ((UPS (S,T)) |^ X) = Funcs (X, the carrier of (UPS (S,T)))
by YELLOW_1:28;
then
the carrier of ((UPS (S,T)) |^ X) c= Funcs (X,(Funcs ( the carrier of S, the carrier of T)))
by Th22, FUNCT_5:56;
then A19:
F * G = id ((UPS (S,T)) |^ X)
by A2, A8, A9, A17, A12, Th3;
the carrier of (UPS (S,(T |^ X))) c= Funcs ( the carrier of S, the carrier of (T |^ X))
by Th22;
then
G * F = id (UPS (S,(T |^ X)))
by A2, A3, A8, A17, A12, A13, Th3;
hence
F is isomorphic
by A19, A18, A16, YELLOW16:15; verum