:: Function Spaces in the Category of Directed Suprema Preserving Maps
:: by Grzegorz Bancerek and Adam Naumowicz
::
:: Received November 26, 1999
:: Copyright (c) 1999-2011 Association of Mizar Users


begin

definition
let F be Function;
attr F is uncurrying means :Def1: :: WAYBEL27:def 1
( ( for x being set st x in dom F holds
x is Function-yielding Function ) & ( for f being Function st f in dom F holds
F . f = uncurry f ) );
attr F is currying means :Def2: :: WAYBEL27:def 2
( ( for x being set st x in dom F holds
( x is Function & proj1 x is Relation ) ) & ( for f being Function st f in dom F holds
F . f = curry f ) );
attr F is commuting means :Def3: :: WAYBEL27:def 3
( ( for x being set st x in dom F holds
x is Function-yielding Function ) & ( for f being Function st f in dom F holds
F . f = commute f ) );
end;

:: deftheorem Def1 defines uncurrying WAYBEL27:def 1 :
for F being Function holds
( F is uncurrying iff ( ( for x being set st x in dom F holds
x is Function-yielding Function ) & ( for f being Function st f in dom F holds
F . f = uncurry f ) ) );

:: deftheorem Def2 defines currying WAYBEL27:def 2 :
for F being Function holds
( F is currying iff ( ( for x being set st x in dom F holds
( x is Function & proj1 x is Relation ) ) & ( for f being Function st f in dom F holds
F . f = curry f ) ) );

:: deftheorem Def3 defines commuting WAYBEL27:def 3 :
for F being Function holds
( F is commuting iff ( ( for x being set st x in dom F holds
x is Function-yielding Function ) & ( for f being Function st f in dom F holds
F . f = commute f ) ) );

registration
cluster empty Relation-like Function-like -> uncurrying currying commuting set ;
coherence
for b1 being Function st b1 is empty holds
( b1 is uncurrying & b1 is currying & b1 is commuting )
proof end;
end;

registration
cluster Relation-like Function-like uncurrying currying commuting set ;
existence
ex b1 being Function st
( b1 is uncurrying & b1 is currying & b1 is commuting )
proof end;
end;

registration
let F be uncurrying Function;
let X be set ;
cluster F | X -> uncurrying ;
coherence
F | X is uncurrying
proof end;
end;

registration
let F be currying Function;
let X be set ;
cluster F | X -> currying ;
coherence
F | X is currying
proof end;
end;

theorem Th1: :: WAYBEL27:1
for X, Y, Z, D being set st D c= Funcs (X,(Funcs (Y,Z))) holds
ex F being ManySortedSet of D st
( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) )
proof end;

theorem Th2: :: WAYBEL27:2
for X, Y, Z, D being set st D c= Funcs ([:X,Y:],Z) holds
ex F being ManySortedSet of D st
( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) )
proof end;

registration
let X, Y, Z be set ;
cluster Relation-like Funcs (X,(Funcs (Y,Z))) -defined Function-like V24( Funcs (X,(Funcs (Y,Z)))) uncurrying set ;
existence
ex b1 being ManySortedSet of Funcs (X,(Funcs (Y,Z))) st b1 is uncurrying
proof end;
cluster Relation-like Funcs ([:X,Y:],Z) -defined Function-like V24( Funcs ([:X,Y:],Z)) currying set ;
existence
ex b1 being ManySortedSet of Funcs ([:X,Y:],Z) st b1 is currying
proof end;
end;

theorem Th3: :: WAYBEL27:3
for A, B being non empty set
for C being set
for f, g being commuting Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds
g * f = id (dom f)
proof end;

theorem Th4: :: WAYBEL27:4
for B being non empty set
for A, C being set
for f being uncurrying Function
for g being currying Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds
g * f = id (dom f)
proof end;

theorem Th5: :: WAYBEL27:5
for A, B, C being set
for f being currying Function
for g being uncurrying Function st dom f c= Funcs ([:A,B:],C) & rng f c= dom g holds
g * f = id (dom f)
proof end;

theorem Th6: :: WAYBEL27:6
for f being Function-yielding Function
for i, A being set st i in dom (commute f) holds
((commute f) . i) .: A c= pi ((f .: A),i)
proof end;

theorem Th7: :: WAYBEL27:7
for f being Function-yielding Function
for i, A being set st ( for g being Function st g in f .: A holds
i in dom g ) holds
pi ((f .: A),i) c= ((commute f) . i) .: A
proof end;

theorem Th8: :: WAYBEL27:8
for X, Y being set
for f being Function st rng f c= Funcs (X,Y) holds
for i, A being set st i in X holds
((commute f) . i) .: A = pi ((f .: A),i)
proof end;

theorem Th9: :: WAYBEL27:9
for f being Function
for i, A being set st [:A,{i}:] c= dom f holds
pi (((curry f) .: A),i) = f .: [:A,{i}:]
proof end;

registration
let T be constituted-Functions 1-sorted ;
cluster the carrier of T -> functional ;
coherence
the carrier of T is functional
proof end;
end;

registration
cluster non empty constituted-Functions strict reflexive transitive antisymmetric V209() V210() complete non void RelStr ;
existence
ex b1 being LATTICE st
( b1 is constituted-Functions & b1 is complete & b1 is strict )
proof end;
cluster non empty constituted-Functions 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is constituted-Functions & not b1 is empty )
proof end;
end;

registration
let T be non empty constituted-Functions RelStr ;
cluster non empty -> non empty constituted-Functions SubRelStr of T;
coherence
for b1 being non empty SubRelStr of T holds b1 is constituted-Functions
proof end;
end;

theorem Th10: :: WAYBEL27:10
for S, T being complete LATTICE
for f being idempotent Function of T,T
for h being Function of S,(Image f) holds f * h = h
proof end;

theorem :: WAYBEL27:11
for S, T, T1 being non empty RelStr st T is SubRelStr of T1 holds
for f being Function of S,T
for f1 being Function of S,T1 st f is monotone & f = f1 holds
f1 is monotone
proof end;

theorem Th12: :: WAYBEL27:12
for S, T, T1 being non empty RelStr st T is full SubRelStr of T1 holds
for f being Function of S,T
for f1 being Function of S,T1 st f1 is monotone & f = f1 holds
f is monotone
proof end;

theorem Th13: :: WAYBEL27:13
for X being set
for V being Subset of X holds
( (chi (V,X)) " {1} = V & (chi (V,X)) " {0} = X \ V )
proof end;

begin

definition
let X be non empty set ;
let T be non empty RelStr ;
let f be Element of (T |^ X);
let x be Element of X;
:: original: .
redefine func f . x -> Element of T;
coherence
f . x is Element of T
proof end;
end;

theorem Th14: :: WAYBEL27:14
for X being non empty set
for T being non empty RelStr
for f, g being Element of (T |^ X) holds
( f <= g iff for x being Element of X holds f . x <= g . x )
proof end;

theorem Th15: :: WAYBEL27:15
for X being set
for L, S being non empty RelStr st RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) holds
L |^ X = S |^ X
proof end;

theorem :: WAYBEL27:16
for S1, S2, T1, T2 being non empty TopSpace st TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) & TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds
oContMaps (S1,T1) = oContMaps (S2,T2)
proof end;

theorem Th17: :: WAYBEL27:17
for X being set ex f being Function of (BoolePoset X),((BoolePoset 1) |^ X) st
( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )
proof end;

theorem Th18: :: WAYBEL27:18
for X being set holds BoolePoset X,(BoolePoset 1) |^ X are_isomorphic
proof end;

theorem Th19: :: WAYBEL27:19
for X, Y being non empty set
for T being non empty Poset
for S1 being non empty full SubRelStr of (T |^ X) |^ Y
for S2 being non empty full SubRelStr of (T |^ Y) |^ X
for F being Function of S1,S2 st F is commuting holds
F is monotone
proof end;

theorem Th20: :: WAYBEL27:20
for X, Y being non empty set
for T being non empty Poset
for S1 being non empty full SubRelStr of (T |^ Y) |^ X
for S2 being non empty full SubRelStr of T |^ [:X,Y:]
for F being Function of S1,S2 st F is uncurrying holds
F is monotone
proof end;

theorem Th21: :: WAYBEL27:21
for X, Y being non empty set
for T being non empty Poset
for S1 being non empty full SubRelStr of (T |^ Y) |^ X
for S2 being non empty full SubRelStr of T |^ [:X,Y:]
for F being Function of S2,S1 st F is currying holds
F is monotone
proof end;

begin

definition
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric RelStr ;
func UPS (S,T) -> strict RelStr means :Def4: :: WAYBEL27:def 4
( it is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of it iff x is directed-sups-preserving Function of S,T ) ) );
existence
ex b1 being strict RelStr st
( b1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b1 iff x is directed-sups-preserving Function of S,T ) ) )
proof end;
uniqueness
for b1, b2 being strict RelStr st b1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b1 iff x is directed-sups-preserving Function of S,T ) ) & b2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b2 iff x is directed-sups-preserving Function of S,T ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines UPS WAYBEL27:def 4 :
for S being non empty RelStr
for T being non empty reflexive antisymmetric RelStr
for b3 being strict RelStr holds
( b3 = UPS (S,T) iff ( b3 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b3 iff x is directed-sups-preserving Function of S,T ) ) ) );

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric RelStr ;
cluster UPS (S,T) -> non empty constituted-Functions strict reflexive antisymmetric ;
coherence
( not UPS (S,T) is empty & UPS (S,T) is reflexive & UPS (S,T) is antisymmetric & UPS (S,T) is constituted-Functions )
proof end;
end;

registration
let S be non empty RelStr ;
let T be non empty Poset;
cluster UPS (S,T) -> strict transitive ;
coherence
UPS (S,T) is transitive
proof end;
end;

theorem Th22: :: WAYBEL27:22
for S being non empty RelStr
for T being non empty reflexive antisymmetric RelStr holds the carrier of (UPS (S,T)) c= Funcs ( the carrier of S, the carrier of T)
proof end;

definition
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric RelStr ;
let f be Element of (UPS (S,T));
let s be Element of S;
:: original: .
redefine func f . s -> Element of T;
coherence
f . s is Element of T
proof end;
end;

theorem Th23: :: WAYBEL27:23
for S being non empty RelStr
for T being non empty reflexive antisymmetric RelStr
for f, g being Element of (UPS (S,T)) holds
( f <= g iff for s being Element of S holds f . s <= g . s )
proof end;

theorem Th24: :: WAYBEL27:24
for S, T being complete Scott TopLattice holds UPS (S,T) = SCMaps (S,T)
proof end;

theorem Th25: :: WAYBEL27:25
for S, S9 being non empty RelStr
for T, T9 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) holds
UPS (S,T) = UPS (S9,T9)
proof end;

registration
let S, T be complete LATTICE;
cluster UPS (S,T) -> strict complete ;
coherence
UPS (S,T) is complete
proof end;
end;

theorem Th26: :: WAYBEL27:26
for S, T being complete LATTICE holds UPS (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S
proof end;

theorem Th27: :: WAYBEL27:27
for S, T being complete LATTICE
for A being Subset of (UPS (S,T)) holds sup A = "\/" (A,(T |^ the carrier of S))
proof end;

definition
let S1, S2, T1, T2 be non empty reflexive antisymmetric RelStr ;
let f be Function of S1,S2;
assume A1: f is directed-sups-preserving ;
let g be Function of T1,T2;
assume A2: g is directed-sups-preserving ;
func UPS (f,g) -> Function of (UPS (S2,T1)),(UPS (S1,T2)) means :Def5: :: WAYBEL27:def 5
for h being directed-sups-preserving Function of S2,T1 holds it . h = (g * h) * f;
existence
ex b1 being Function of (UPS (S2,T1)),(UPS (S1,T2)) st
for h being directed-sups-preserving Function of S2,T1 holds b1 . h = (g * h) * f
proof end;
uniqueness
for b1, b2 being Function of (UPS (S2,T1)),(UPS (S1,T2)) st ( for h being directed-sups-preserving Function of S2,T1 holds b1 . h = (g * h) * f ) & ( for h being directed-sups-preserving Function of S2,T1 holds b2 . h = (g * h) * f ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines UPS WAYBEL27:def 5 :
for S1, S2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of S1,S2 st f is directed-sups-preserving holds
for g being Function of T1,T2 st g is directed-sups-preserving holds
for b7 being Function of (UPS (S2,T1)),(UPS (S1,T2)) holds
( b7 = UPS (f,g) iff for h being directed-sups-preserving Function of S2,T1 holds b7 . h = (g * h) * f );

theorem Th28: :: WAYBEL27:28
for S1, S2, S3, T1, T2, T3 being non empty Poset
for f1 being directed-sups-preserving Function of S2,S3
for f2 being directed-sups-preserving Function of S1,S2
for g1 being directed-sups-preserving Function of T1,T2
for g2 being directed-sups-preserving Function of T2,T3 holds (UPS (f2,g2)) * (UPS (f1,g1)) = UPS ((f1 * f2),(g2 * g1))
proof end;

theorem Th29: :: WAYBEL27:29
for S, T being non empty reflexive antisymmetric RelStr holds UPS ((id S),(id T)) = id (UPS (S,T))
proof end;

theorem Th30: :: WAYBEL27:30
for S1, S2, T1, T2 being complete LATTICE
for f being directed-sups-preserving Function of S1,S2
for g being directed-sups-preserving Function of T1,T2 holds UPS (f,g) is directed-sups-preserving
proof end;

theorem Th31: :: WAYBEL27:31
Omega Sierpinski_Space is Scott
proof end;

theorem :: WAYBEL27:32
for S being complete Scott TopLattice holds oContMaps (S,Sierpinski_Space) = UPS (S,(BoolePoset 1))
proof end;

theorem Th33: :: WAYBEL27:33
for S being complete LATTICE ex F being Function of (UPS (S,(BoolePoset 1))),(InclPoset (sigma S)) st
( F is isomorphic & ( for f being directed-sups-preserving Function of S,(BoolePoset 1) holds F . f = f " {1} ) )
proof end;

theorem Th34: :: WAYBEL27:34
for S being complete LATTICE holds UPS (S,(BoolePoset 1)), InclPoset (sigma S) are_isomorphic
proof end;

theorem Th35: :: WAYBEL27:35
for S1, S2, T1, T2 being complete LATTICE
for f being Function of S1,S2
for g being Function of T1,T2 st f is isomorphic & g is isomorphic holds
UPS (f,g) is isomorphic
proof end;

theorem Th36: :: WAYBEL27:36
for S1, S2, T1, T2 being complete LATTICE st S1,S2 are_isomorphic & T1,T2 are_isomorphic holds
UPS (S2,T1), UPS (S1,T2) are_isomorphic
proof end;

theorem Th37: :: WAYBEL27:37
for S, T being complete LATTICE
for f being directed-sups-preserving projection Function of T,T holds Image (UPS ((id S),f)) = UPS (S,(Image f))
proof end;

Lm1: now
let M be non empty set ; :: thesis: for X, Y being non empty Poset
for f being directed-sups-preserving Function of X,(Y |^ M) holds
( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

let X, Y be non empty Poset; :: thesis: for f being directed-sups-preserving Function of X,(Y |^ M) holds
( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

let f be directed-sups-preserving Function of X,(Y |^ M); :: thesis: ( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )
the carrier of (Y |^ M) = Funcs (M, the carrier of Y) by YELLOW_1:28;
then A1: rng f c= Funcs (M, the carrier of Y) ;
dom f = the carrier of X by FUNCT_2:def 1;
hence f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) by A1, FUNCT_2:def 2; :: thesis: ( rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )
then commute f in Funcs (M,(Funcs ( the carrier of X, the carrier of Y))) by FUNCT_6:85;
then ex g being Function st
( commute f = g & dom g = M & rng g c= Funcs ( the carrier of X, the carrier of Y) ) by FUNCT_2:def 2;
hence ( rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M ) ; :: thesis: verum
end;

theorem Th38: :: WAYBEL27:38
for X being non empty set
for S, T being non empty Poset
for f being directed-sups-preserving Function of S,(T |^ X)
for i being Element of X holds (commute f) . i is directed-sups-preserving Function of S,T
proof end;

theorem Th39: :: WAYBEL27:39
for X being non empty set
for S, T being non empty Poset
for f being directed-sups-preserving Function of S,(T |^ X) holds commute f is Function of X, the carrier of (UPS (S,T))
proof end;

theorem Th40: :: WAYBEL27:40
for X being non empty set
for S, T being non empty Poset
for f being Function of X, the carrier of (UPS (S,T)) holds commute f is directed-sups-preserving Function of S,(T |^ X)
proof end;

theorem Th41: :: WAYBEL27:41
for X being 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 )
proof end;

theorem Th42: :: WAYBEL27:42
for X being non empty set
for S, T being non empty Poset holds UPS (S,(T |^ X)),(UPS (S,T)) |^ X are_isomorphic
proof end;

theorem :: WAYBEL27:43
for S, T being complete continuous LATTICE holds UPS (S,T) is continuous
proof end;

theorem :: WAYBEL27:44
for S, T being complete algebraic LATTICE holds UPS (S,T) is algebraic
proof end;

theorem Th45: :: WAYBEL27:45
for R, S, T being complete LATTICE
for f being directed-sups-preserving Function of R,(UPS (S,T)) holds uncurry f is directed-sups-preserving Function of [:R,S:],T
proof end;

theorem Th46: :: WAYBEL27:46
for R, S, T being complete LATTICE
for f being directed-sups-preserving Function of [:R,S:],T holds curry f is directed-sups-preserving Function of R,(UPS (S,T))
proof end;

theorem :: WAYBEL27:47
for R, S, T being complete LATTICE ex f being Function of (UPS (R,(UPS (S,T)))),(UPS ([:R,S:],T)) st
( f is uncurrying & f is isomorphic )
proof end;