:: by Grzegorz Bancerek

::

:: Received August 1, 2001

:: Copyright (c) 2001-2018 Association of Mizar Users

definition

let a be object ;

( ( a is 1-sorted implies a is 1-sorted ) & ( a is not 1-sorted implies the 1-sorted is 1-sorted ) ) ;

consistency

for b_{1} being 1-sorted holds verum
;

end;
func a as_1-sorted -> 1-sorted equals :Def1: :: YELLOW21:def 1

a if a is 1-sorted

otherwise the 1-sorted ;

coherence a if a is 1-sorted

otherwise the 1-sorted ;

( ( a is 1-sorted implies a is 1-sorted ) & ( a is not 1-sorted implies the 1-sorted is 1-sorted ) ) ;

consistency

for b

:: deftheorem Def1 defines as_1-sorted YELLOW21:def 1 :

for a being object holds

( ( a is 1-sorted implies a as_1-sorted = a ) & ( a is not 1-sorted implies a as_1-sorted = the 1-sorted ) );

for a being object holds

( ( a is 1-sorted implies a as_1-sorted = a ) & ( a is not 1-sorted implies a as_1-sorted = the 1-sorted ) );

definition

let W be set ;

defpred S_{1}[ object ] means ( $1 is strict Poset & the carrier of ($1 as_1-sorted) in W );

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) & ( for x being object holds

( x in b_{2} iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) )

end;
defpred S

func POSETS W -> set means :Def2: :: YELLOW21:def 2

for x being object holds

( x in it iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) );

uniqueness for x being object holds

( x in it iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) );

for b

( x in b

( x in b

b

proof end;

existence ex b

for x being object holds

( x in b

proof end;

:: deftheorem Def2 defines POSETS YELLOW21:def 2 :

for W, b_{2} being set holds

( b_{2} = POSETS W iff for x being object holds

( x in b_{2} iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) );

for W, b

( b

( x in b

registration
end;

registration
end;

definition

let C be category;

end;
attr C is carrier-underlaid means :Def3: :: YELLOW21:def 3

for a being Object of C ex S being 1-sorted st

( a = S & the_carrier_of a = the carrier of S );

for a being Object of C ex S being 1-sorted st

( a = S & the_carrier_of a = the carrier of S );

:: deftheorem Def3 defines carrier-underlaid YELLOW21:def 3 :

for C being category holds

( C is carrier-underlaid iff for a being Object of C ex S being 1-sorted st

( a = S & the_carrier_of a = the carrier of S ) );

for C being category holds

( C is carrier-underlaid iff for a being Object of C ex S being 1-sorted st

( a = S & the_carrier_of a = the carrier of S ) );

definition

let C be category;

end;
attr C is lattice-wise means :Def4: :: YELLOW21:def 4

( C is semi-functional & C is set-id-inheriting & ( for a being Object of C holds a is LATTICE ) & ( for a, b being Object of C

for A, B being LATTICE st A = a & B = b holds

<^a,b^> c= MonFuncs (A,B) ) );

( C is semi-functional & C is set-id-inheriting & ( for a being Object of C holds a is LATTICE ) & ( for a, b being Object of C

for A, B being LATTICE st A = a & B = b holds

<^a,b^> c= MonFuncs (A,B) ) );

:: deftheorem Def4 defines lattice-wise YELLOW21:def 4 :

for C being category holds

( C is lattice-wise iff ( C is semi-functional & C is set-id-inheriting & ( for a being Object of C holds a is LATTICE ) & ( for a, b being Object of C

for A, B being LATTICE st A = a & B = b holds

<^a,b^> c= MonFuncs (A,B) ) ) );

for C being category holds

( C is lattice-wise iff ( C is semi-functional & C is set-id-inheriting & ( for a being Object of C holds a is LATTICE ) & ( for a, b being Object of C

for A, B being LATTICE st A = a & B = b holds

<^a,b^> c= MonFuncs (A,B) ) ) );

definition

let C be category;

end;
attr C is with_complete_lattices means :Def5: :: YELLOW21:def 5

( C is lattice-wise & ( for a being Object of C holds a is complete LATTICE ) );

( C is lattice-wise & ( for a being Object of C holds a is complete LATTICE ) );

:: deftheorem Def5 defines with_complete_lattices YELLOW21:def 5 :

for C being category holds

( C is with_complete_lattices iff ( C is lattice-wise & ( for a being Object of C holds a is complete LATTICE ) ) );

for C being category holds

( C is with_complete_lattices iff ( C is lattice-wise & ( for a being Object of C holds a is complete LATTICE ) ) );

registration

coherence

for b_{1} being category st b_{1} is with_complete_lattices holds

b_{1} is lattice-wise
;

for b_{1} being category st b_{1} is lattice-wise holds

( b_{1} is concrete & b_{1} is carrier-underlaid )

end;
for b

b

cluster non empty transitive V121() with_units lattice-wise -> concrete carrier-underlaid for category;

coherence for b

( b

proof end;

scheme :: YELLOW21:sch 1

localCLCatEx{ F_{1}() -> non empty set , P_{1}[ object , object , object ] } :

localCLCatEx{ F

ex C being strict category st

( C is lattice-wise & the carrier of C = F_{1}() & ( for a, b being LATTICE

for f being monotone Function of a,b holds

( f in the Arrows of C . (a,b) iff ( a in F_{1}() & b in F_{1}() & P_{1}[a,b,f] ) ) ) )

provided( C is lattice-wise & the carrier of C = F

for f being monotone Function of a,b holds

( f in the Arrows of C . (a,b) iff ( a in F

A1:
for a being Element of F_{1}() holds a is LATTICE
and

A2: for a, b, c being LATTICE st a in F_{1}() & b in F_{1}() & c in F_{1}() holds

for f being Function of a,b

for g being Function of b,c st P_{1}[a,b,f] & P_{1}[b,c,g] holds

P_{1}[a,c,g * f]
and

A3: for a being LATTICE st a in F_{1}() holds

P_{1}[a,a, id a]

A2: for a, b, c being LATTICE st a in F

for f being Function of a,b

for g being Function of b,c st P

P

A3: for a being LATTICE st a in F

P

proof end;

registration

ex b_{1} being category st

( b_{1} is strict & b_{1} is with_complete_lattices )
end;

cluster non empty transitive strict V121() with_units reflexive with_complete_lattices for category;

existence ex b

( b

proof end;

theorem :: YELLOW21:1

for C being carrier-underlaid category

for a being Object of C holds the_carrier_of a = the carrier of (a as_1-sorted)

for a being Object of C holds the_carrier_of a = the carrier of (a as_1-sorted)

proof end;

theorem Th2: :: YELLOW21:2

for C being set-id-inheriting carrier-underlaid category

for a being Object of C holds idm a = id (a as_1-sorted)

for a being Object of C holds idm a = id (a as_1-sorted)

proof end;

notation
end;

definition

let C be lattice-wise category;

let a be Object of C;

coherence

a as_1-sorted is LATTICE

for b_{1} being LATTICE holds

( b_{1} = a as_1-sorted iff b_{1} = a )

end;
let a be Object of C;

coherence

a as_1-sorted is LATTICE

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines latt YELLOW21:def 6 :

for C being lattice-wise category

for a being Object of C holds latt a = a;

for C being lattice-wise category

for a being Object of C holds latt a = a;

notation
end;

definition

let C be with_complete_lattices category;

let a be Object of C;

:: original: as_1-sorted

redefine func latt a -> complete LATTICE;

coherence

a as_1-sorted is complete LATTICE by Def5;

end;
let a be Object of C;

:: original: as_1-sorted

redefine func latt a -> complete LATTICE;

coherence

a as_1-sorted is complete LATTICE by Def5;

definition

let C be lattice-wise category;

let a, b be Object of C;

assume A1: <^a,b^> <> {} ;

let f be Morphism of a,b;

coherence

f is monotone Function of (latt a),(latt b)

end;
let a, b be Object of C;

assume A1: <^a,b^> <> {} ;

let f be Morphism of a,b;

coherence

f is monotone Function of (latt a),(latt b)

proof end;

:: deftheorem Def7 defines @ YELLOW21:def 7 :

for C being lattice-wise category

for a, b being Object of C st <^a,b^> <> {} holds

for f being Morphism of a,b holds @ f = f;

for C being lattice-wise category

for a, b being Object of C st <^a,b^> <> {} holds

for f being Morphism of a,b holds @ f = f;

theorem Th3: :: YELLOW21:3

for C being lattice-wise category

for a, b, c being Object of C st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = (@ g) * (@ f)

for a, b, c being Object of C st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds g * f = (@ g) * (@ f)

proof end;

scheme :: YELLOW21:sch 2

CLCatEx1{ F_{1}() -> non empty set , P_{1}[ set , set , set ] } :

CLCatEx1{ F

ex C being strict lattice-wise category st

( the carrier of C = F_{1}() & ( for a, b being Object of C

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{1}[ latt a, latt b,f] ) ) )

provided( the carrier of C = F

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

A1:
for a being Element of F_{1}() holds a is LATTICE
and

A2: for a, b, c being LATTICE st a in F_{1}() & b in F_{1}() & c in F_{1}() holds

for f being Function of a,b

for g being Function of b,c st P_{1}[a,b,f] & P_{1}[b,c,g] holds

P_{1}[a,c,g * f]
and

A3: for a being LATTICE st a in F_{1}() holds

P_{1}[a,a, id a]

A2: for a, b, c being LATTICE st a in F

for f being Function of a,b

for g being Function of b,c st P

P

A3: for a being LATTICE st a in F

P

proof end;

scheme :: YELLOW21:sch 3

CLCatEx2{ F_{1}() -> non empty set , P_{1}[ object ], P_{2}[ set , set , set ] } :

CLCatEx2{ F

ex C being strict lattice-wise category st

( ( for x being LATTICE holds

( x is Object of C iff ( x is strict & P_{1}[x] & the carrier of x in F_{1}() ) ) ) & ( for a, b being Object of C

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{2}[ latt a, latt b,f] ) ) )

provided( ( for x being LATTICE holds

( x is Object of C iff ( x is strict & P

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

A1:
ex x being strict LATTICE st

( P_{1}[x] & the carrier of x in F_{1}() )
and

A2: for a, b, c being LATTICE st P_{1}[a] & P_{1}[b] & P_{1}[c] holds

for f being Function of a,b

for g being Function of b,c st P_{2}[a,b,f] & P_{2}[b,c,g] holds

P_{2}[a,c,g * f]
and

A3: for a being LATTICE st P_{1}[a] holds

P_{2}[a,a, id a]

( P

A2: for a, b, c being LATTICE st P

for f being Function of a,b

for g being Function of b,c st P

P

A3: for a being LATTICE st P

P

proof end;

scheme :: YELLOW21:sch 4

CLCatUniq1{ F_{1}() -> non empty set , P_{1}[ set , set , set ] } :

CLCatUniq1{ F

for C1, C2 being lattice-wise category st the carrier of C1 = F_{1}() & ( for a, b being Object of C1

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{1}[a,b,f] ) ) & the carrier of C2 = F_{1}() & ( for a, b being Object of C2

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{1}[a,b,f] ) ) holds

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

proof end;

scheme :: YELLOW21:sch 5

CLCatUniq2{ F_{1}() -> non empty set , P_{1}[ object ], P_{2}[ set , set , set ] } :

CLCatUniq2{ F

for C1, C2 being lattice-wise category st ( for x being LATTICE holds

( x is Object of C1 iff ( x is strict & P_{1}[x] & the carrier of x in F_{1}() ) ) ) & ( for a, b being Object of C1

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{2}[a,b,f] ) ) & ( for x being LATTICE holds

( x is Object of C2 iff ( x is strict & P_{1}[x] & the carrier of x in F_{1}() ) ) ) & ( for a, b being Object of C2

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{2}[a,b,f] ) ) holds

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

( x is Object of C1 iff ( x is strict & P

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

( x is Object of C2 iff ( x is strict & P

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)

proof end;

scheme :: YELLOW21:sch 6

CLCovariantFunctorEx{ P_{1}[ set , set , set ], P_{2}[ set , set , set ], F_{1}() -> lattice-wise category, F_{2}() -> lattice-wise category, F_{3}( set ) -> LATTICE, F_{4}( set , set , set ) -> Function } :

CLCovariantFunctorEx{ P

ex F being strict covariant Functor of F_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}((latt a)) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{4}((latt a),(latt b),(@ f)) ) )

provided( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

A1:
for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F_{1}() . (a,b) iff ( a in the carrier of F_{1}() & b in the carrier of F_{1}() & P_{1}[a,b,f] ) )
and

A2: for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F_{2}() . (a,b) iff ( a in the carrier of F_{2}() & b in the carrier of F_{2}() & P_{2}[a,b,f] ) )
and

A3: for a being LATTICE st a in the carrier of F_{1}() holds

F_{3}(a) in the carrier of F_{2}()
and

A4: for a, b being LATTICE

for f being Function of a,b st P_{1}[a,b,f] holds

( F_{4}(a,b,f) is Function of F_{3}(a),F_{3}(b) & P_{2}[F_{3}(a),F_{3}(b),F_{4}(a,b,f)] )
and

A5: for a being LATTICE st a in the carrier of F_{1}() holds

F_{4}(a,a,(id a)) = id F_{3}(a)
and

A6: for a, b, c being LATTICE

for f being Function of a,b

for g being Function of b,c st P_{1}[a,b,f] & P_{1}[b,c,g] holds

F_{4}(a,c,(g * f)) = F_{4}(b,c,g) * F_{4}(a,b,f)

for f being Function of a,b holds

( f in the Arrows of F

A2: for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F

A3: for a being LATTICE st a in the carrier of F

F

A4: for a, b being LATTICE

for f being Function of a,b st P

( F

A5: for a being LATTICE st a in the carrier of F

F

A6: for a, b, c being LATTICE

for f being Function of a,b

for g being Function of b,c st P

F

proof end;

scheme :: YELLOW21:sch 7

CLContravariantFunctorEx{ P_{1}[ set , set , set ], P_{2}[ set , set , set ], F_{1}() -> lattice-wise category, F_{2}() -> lattice-wise category, F_{3}( set ) -> LATTICE, F_{4}( set , set , set ) -> Function } :

CLContravariantFunctorEx{ P

ex F being strict contravariant Functor of F_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}((latt a)) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{4}((latt a),(latt b),(@ f)) ) )

provided( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

A1:
for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F_{1}() . (a,b) iff ( a in the carrier of F_{1}() & b in the carrier of F_{1}() & P_{1}[a,b,f] ) )
and

A2: for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F_{2}() . (a,b) iff ( a in the carrier of F_{2}() & b in the carrier of F_{2}() & P_{2}[a,b,f] ) )
and

A3: for a being LATTICE st a in the carrier of F_{1}() holds

F_{3}(a) in the carrier of F_{2}()
and

A4: for a, b being LATTICE

for f being Function of a,b st P_{1}[a,b,f] holds

( F_{4}(a,b,f) is Function of F_{3}(b),F_{3}(a) & P_{2}[F_{3}(b),F_{3}(a),F_{4}(a,b,f)] )
and

A5: for a being LATTICE st a in the carrier of F_{1}() holds

F_{4}(a,a,(id a)) = id F_{3}(a)
and

A6: for a, b, c being LATTICE

for f being Function of a,b

for g being Function of b,c st P_{1}[a,b,f] & P_{1}[b,c,g] holds

F_{4}(a,c,(g * f)) = F_{4}(a,b,f) * F_{4}(b,c,g)

for f being Function of a,b holds

( f in the Arrows of F

A2: for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F

A3: for a being LATTICE st a in the carrier of F

F

A4: for a, b being LATTICE

for f being Function of a,b st P

( F

A5: for a being LATTICE st a in the carrier of F

F

A6: for a, b, c being LATTICE

for f being Function of a,b

for g being Function of b,c st P

F

proof end;

scheme :: YELLOW21:sch 8

CLCatIsomorphism{ P_{1}[ set , set , set ], P_{2}[ set , set , set ], F_{1}() -> lattice-wise category, F_{2}() -> lattice-wise category, F_{3}( set ) -> LATTICE, F_{4}( set , set , set ) -> Function } :

provided

CLCatIsomorphism{ P

provided

A1:
for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F_{1}() . (a,b) iff ( a in the carrier of F_{1}() & b in the carrier of F_{1}() & P_{1}[a,b,f] ) )
and

A2: for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F_{2}() . (a,b) iff ( a in the carrier of F_{2}() & b in the carrier of F_{2}() & P_{2}[a,b,f] ) )
and

A3: ex F being covariant Functor of F_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}(a) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{4}(a,b,f) ) )
and

A4: for a, b being LATTICE st a in the carrier of F_{1}() & b in the carrier of F_{1}() & F_{3}(a) = F_{3}(b) holds

a = b and

A5: for a, b being LATTICE

for f, g being Function of a,b st P_{1}[a,b,f] & P_{1}[a,b,g] & F_{4}(a,b,f) = F_{4}(a,b,g) holds

f = g and

A6: for a, b being LATTICE

for f being Function of a,b st P_{2}[a,b,f] holds

ex c, d being LATTICE ex g being Function of c,d st

( c in the carrier of F_{1}() & d in the carrier of F_{1}() & P_{1}[c,d,g] & a = F_{3}(c) & b = F_{3}(d) & f = F_{4}(c,d,g) )

for f being Function of a,b holds

( f in the Arrows of F

A2: for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F

A3: ex F being covariant Functor of F

( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

A4: for a, b being LATTICE st a in the carrier of F

a = b and

A5: for a, b being LATTICE

for f, g being Function of a,b st P

f = g and

A6: for a, b being LATTICE

for f being Function of a,b st P

ex c, d being LATTICE ex g being Function of c,d st

( c in the carrier of F

proof end;

scheme :: YELLOW21:sch 9

CLCatAntiIsomorphism{ P_{1}[ set , set , set ], P_{2}[ set , set , set ], F_{1}() -> lattice-wise category, F_{2}() -> lattice-wise category, F_{3}( set ) -> LATTICE, F_{4}( set , set , set ) -> Function } :

provided

CLCatAntiIsomorphism{ P

provided

A1:
for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F_{1}() . (a,b) iff ( a in the carrier of F_{1}() & b in the carrier of F_{1}() & P_{1}[a,b,f] ) )
and

A2: for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F_{2}() . (a,b) iff ( a in the carrier of F_{2}() & b in the carrier of F_{2}() & P_{2}[a,b,f] ) )
and

A3: ex F being contravariant Functor of F_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}(a) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{4}(a,b,f) ) )
and

A4: for a, b being LATTICE st a in the carrier of F_{1}() & b in the carrier of F_{1}() & F_{3}(a) = F_{3}(b) holds

a = b and

A5: for a, b being LATTICE

for f, g being Function of a,b st F_{4}(a,b,f) = F_{4}(a,b,g) holds

f = g and

A6: for a, b being LATTICE

for f being Function of a,b st P_{2}[a,b,f] holds

ex c, d being LATTICE ex g being Function of c,d st

( c in the carrier of F_{1}() & d in the carrier of F_{1}() & P_{1}[c,d,g] & b = F_{3}(c) & a = F_{3}(d) & f = F_{4}(c,d,g) )

for f being Function of a,b holds

( f in the Arrows of F

A2: for a, b being LATTICE

for f being Function of a,b holds

( f in the Arrows of F

A3: ex F being contravariant Functor of F

( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

A4: for a, b being LATTICE st a in the carrier of F

a = b and

A5: for a, b being LATTICE

for f, g being Function of a,b st F

f = g and

A6: for a, b being LATTICE

for f being Function of a,b st P

ex c, d being LATTICE ex g being Function of c,d st

( c in the carrier of F

proof end;

definition

let C be lattice-wise category;

end;
attr C is with_all_isomorphisms means :Def8: :: YELLOW21:def 8

for a, b being Object of C

for f being Function of (latt a),(latt b) st f is isomorphic holds

f in <^a,b^>;

for a, b being Object of C

for f being Function of (latt a),(latt b) st f is isomorphic holds

f in <^a,b^>;

:: deftheorem Def8 defines with_all_isomorphisms YELLOW21:def 8 :

for C being lattice-wise category holds

( C is with_all_isomorphisms iff for a, b being Object of C

for f being Function of (latt a),(latt b) st f is isomorphic holds

f in <^a,b^> );

for C being lattice-wise category holds

( C is with_all_isomorphisms iff for a, b being Object of C

for f being Function of (latt a),(latt b) st f is isomorphic holds

f in <^a,b^> );

registration

ex b_{1} being strict lattice-wise category st b_{1} is with_all_isomorphisms
end;

cluster non empty transitive strict semi-functional V121() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise with_all_isomorphisms for category;

existence ex b

proof end;

theorem :: YELLOW21:4

for C being lattice-wise with_all_isomorphisms category

for a, b being Object of C

for f being Morphism of a,b st @ f is isomorphic holds

f is iso

for a, b being Object of C

for f being Morphism of a,b st @ f is isomorphic holds

f is iso

proof end;

theorem :: YELLOW21:5

for C being lattice-wise category

for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds

for f being Morphism of a,b st f is iso holds

@ f is isomorphic

for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds

for f being Morphism of a,b st f is iso holds

@ f is isomorphic

proof end;

scheme :: YELLOW21:sch 10

CLCatEquivalence{ P_{1}[ set , set , set ], P_{2}[ set , set , set ], F_{1}() -> lattice-wise category, F_{2}() -> lattice-wise category, F_{3}( set ) -> LATTICE, F_{4}( set ) -> LATTICE, F_{5}( set , set , set ) -> Function, F_{6}( set , set , set ) -> Function, F_{7}( set ) -> Function, F_{8}( set ) -> Function } :

provided

CLCatEquivalence{ P

provided

A1:
for a, b being Object of F_{1}()

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{1}[ latt a, latt b,f] )
and

A2: for a, b being Object of F_{2}()

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{2}[ latt a, latt b,f] )
and

A3: ex F being covariant Functor of F_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}(a) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{5}(a,b,f) ) )
and

A4: ex G being covariant Functor of F_{2}(),F_{1}() st

( ( for a being Object of F_{2}() holds G . a = F_{4}(a) ) & ( for a, b being Object of F_{2}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds G . f = F_{6}(a,b,f) ) )
and

A5: for a being LATTICE st a in the carrier of F_{1}() holds

ex f being monotone Function of F_{4}(F_{3}(a)),a st

( f = F_{7}(a) & f is isomorphic & P_{1}[F_{4}(F_{3}(a)),a,f] & P_{1}[a,F_{4}(F_{3}(a)),f " ] )
and

A6: for a being LATTICE st a in the carrier of F_{2}() holds

ex f being monotone Function of a,F_{3}(F_{4}(a)) st

( f = F_{8}(a) & f is isomorphic & P_{2}[a,F_{3}(F_{4}(a)),f] & P_{2}[F_{3}(F_{4}(a)),a,f " ] )
and

A7: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F_{7}(b) * F_{6}(F_{3}(a),F_{3}(b),F_{5}(a,b,f)) = (@ f) * F_{7}(a)
and

A8: for a, b being Object of F_{2}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F_{5}(F_{4}(a),F_{4}(b),F_{6}(a,b,f)) * F_{8}(a) = F_{8}(b) * (@ f)

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

A2: for a, b being Object of F

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

A3: ex F being covariant Functor of F

( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

A4: ex G being covariant Functor of F

( ( for a being Object of F

for f being Morphism of a,b holds G . f = F

A5: for a being LATTICE st a in the carrier of F

ex f being monotone Function of F

( f = F

A6: for a being LATTICE st a in the carrier of F

ex f being monotone Function of a,F

( f = F

A7: for a, b being Object of F

for f being Morphism of a,b holds F

A8: for a, b being Object of F

for f being Morphism of a,b holds F

proof end;

definition

let R be Relation;

end;
attr R is upper-bounded means :: YELLOW21:def 9

ex x being set st

for y being set st y in field R holds

[y,x] in R;

ex x being set st

for y being set st y in field R holds

[y,x] in R;

:: deftheorem defines upper-bounded YELLOW21:def 9 :

for R being Relation holds

( R is upper-bounded iff ex x being set st

for y being set st y in field R holds

[y,x] in R );

for R being Relation holds

( R is upper-bounded iff ex x being set st

for y being set st y in field R holds

[y,x] in R );

Lm1: for x, X being set holds

( x in X iff X = (X \ {x}) \/ {x} )

by ZFMISC_1:31, XBOOLE_1:7, XBOOLE_1:45;

registration

for b_{1} being Relation st b_{1} is well-ordering holds

( b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric & b_{1} is connected & b_{1} is well_founded )
;

end;

cluster Relation-like well-ordering -> well_founded reflexive antisymmetric connected transitive for Relation;

coherence for b

( b

theorem Th6: :: YELLOW21:6

for x, y being object

for f being one-to-one Function

for R being Relation holds

( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) )

for f being one-to-one Function

for R being Relation holds

( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) )

proof end;

registration

let f be one-to-one Function;

let R be reflexive Relation;

coherence

(f * R) * (f ") is reflexive

end;
let R be reflexive Relation;

coherence

(f * R) * (f ") is reflexive

proof end;

registration

let f be one-to-one Function;

let R be antisymmetric Relation;

coherence

(f * R) * (f ") is antisymmetric

end;
let R be antisymmetric Relation;

coherence

(f * R) * (f ") is antisymmetric

proof end;

registration

let f be one-to-one Function;

let R be transitive Relation;

coherence

(f * R) * (f ") is transitive

end;
let R be transitive Relation;

coherence

(f * R) * (f ") is transitive

proof end;

theorem Th7: :: YELLOW21:7

for X being set

for A being Ordinal st X,A are_equipotent holds

ex R being Order of X st

( R well_orders X & order_type_of R = A )

for A being Ordinal st X,A are_equipotent holds

ex R being Order of X st

( R well_orders X & order_type_of R = A )

proof end;

registration

let X be non empty set ;

ex b_{1} being Order of X st

( b_{1} is upper-bounded & b_{1} is well-ordering )

end;
cluster Relation-like X -defined X -valued well-ordering reflexive antisymmetric transitive V24(X) quasi_total upper-bounded for Order of ;

existence ex b

( b

proof end;

theorem Th8: :: YELLOW21:8

for P being non empty reflexive RelStr holds

( P is upper-bounded iff the InternalRel of P is upper-bounded )

( P is upper-bounded iff the InternalRel of P is upper-bounded )

proof end;

theorem Th9: :: YELLOW21:9

for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds

( P is connected & P is complete & P is continuous )

( P is connected & P is complete & P is continuous )

proof end;

theorem Th10: :: YELLOW21:10

for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds

for x, y being Element of P st y < x holds

ex z being Element of P st

( z is compact & y <= z & z <= x )

for x, y being Element of P st y < x holds

ex z being Element of P st

( z is compact & y <= z & z <= x )

proof end;

theorem Th11: :: YELLOW21:11

for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds

P is algebraic

P is algebraic

proof end;

registration

let X be non empty set ;

let R be well-ordering upper-bounded Order of X;

coherence

( RelStr(# X,R #) is complete & RelStr(# X,R #) is connected & RelStr(# X,R #) is continuous & RelStr(# X,R #) is algebraic )

end;
let R be well-ordering upper-bounded Order of X;

coherence

( RelStr(# X,R #) is complete & RelStr(# X,R #) is connected & RelStr(# X,R #) is continuous & RelStr(# X,R #) is algebraic )

proof end;

definition

defpred S_{1}[ LATTICE, LATTICE, Function of $1,$2] means $3 is directed-sups-preserving ;

defpred S_{2}[ LATTICE] means $1 is complete ;

let W be non empty set ;

given w being Element of W such that A1: not w is empty ;

ex b_{1} being strict lattice-wise category st

( ( for x being LATTICE holds

( x is Object of b_{1} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{1}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is directed-sups-preserving ) ) )

uniqueness

for b_{1}, b_{2} being strict lattice-wise category st ( for x being LATTICE holds

( x is Object of b_{1} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{1}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is directed-sups-preserving ) ) & ( for x being LATTICE holds

( x is Object of b_{2} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{2}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is directed-sups-preserving ) ) holds

b_{1} = b_{2};

end;
defpred S

let W be non empty set ;

given w being Element of W such that A1: not w is empty ;

func W -UPS_category -> strict lattice-wise category means :Def10: :: YELLOW21:def 10

( ( for x being LATTICE holds

( x is Object of it iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of it

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is directed-sups-preserving ) ) );

existence ( ( for x being LATTICE holds

( x is Object of it iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of it

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is directed-sups-preserving ) ) );

ex b

( ( for x being LATTICE holds

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is directed-sups-preserving ) ) )

proof end;

correctness uniqueness

for b

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is directed-sups-preserving ) ) & ( for x being LATTICE holds

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is directed-sups-preserving ) ) holds

b

proof end;

:: deftheorem Def10 defines -UPS_category YELLOW21:def 10 :

for W being non empty set st not for w being Element of W holds w is empty holds

for b_{2} being strict lattice-wise category holds

( b_{2} = W -UPS_category iff ( ( for x being LATTICE holds

( x is Object of b_{2} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{2}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is directed-sups-preserving ) ) ) );

for W being non empty set st not for w being Element of W holds w is empty holds

for b

( b

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is directed-sups-preserving ) ) ) );

registration

let W be with_non-empty_element set ;

coherence

( W -UPS_category is with_complete_lattices & W -UPS_category is with_all_isomorphisms )

end;
coherence

( W -UPS_category is with_complete_lattices & W -UPS_category is with_all_isomorphisms )

proof end;

theorem Th13: :: YELLOW21:13

for W being with_non-empty_element set

for x being set holds

( x is Object of (W -UPS_category) iff ( x is complete LATTICE & x in POSETS W ) )

for x being set holds

( x is Object of (W -UPS_category) iff ( x is complete LATTICE & x in POSETS W ) )

proof end;

theorem Th14: :: YELLOW21:14

for W being with_non-empty_element set

for L being LATTICE st the carrier of L in W holds

( L is Object of (W -UPS_category) iff ( L is strict & L is complete ) )

for L being LATTICE st the carrier of L in W holds

( L is Object of (W -UPS_category) iff ( L is strict & L is complete ) )

proof end;

theorem Th15: :: YELLOW21:15

for W being with_non-empty_element set

for a, b being Object of (W -UPS_category)

for f being set holds

( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

for a, b being Object of (W -UPS_category)

for f being set holds

( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

proof end;

registration

let W be with_non-empty_element set ;

let a, b be Object of (W -UPS_category);

coherence

not <^a,b^> is empty

end;
let a, b be Object of (W -UPS_category);

coherence

not <^a,b^> is empty

proof end;

registration

let A be set-id-inheriting category;

coherence

for b_{1} being non empty subcategory of A holds b_{1} is set-id-inheriting

end;
coherence

for b

proof end;

registration

let A be para-functional category;

coherence

for b_{1} being non empty subcategory of A holds b_{1} is para-functional

end;
coherence

for b

proof end;

registration

let A be semi-functional category;

coherence

for b_{1} being non empty transitive SubCatStr of A holds b_{1} is semi-functional

end;
coherence

for b

proof end;

registration

let A be carrier-underlaid category;

coherence

for b_{1} being non empty subcategory of A holds b_{1} is carrier-underlaid

end;
coherence

for b

proof end;

registration

let A be lattice-wise category;

coherence

for b_{1} being non empty subcategory of A holds b_{1} is lattice-wise

end;
coherence

for b

proof end;

registration

let A be lattice-wise with_all_isomorphisms category;

for b_{1} being non empty subcategory of A st b_{1} is full holds

b_{1} is with_all_isomorphisms

end;
cluster non empty transitive full id-inheriting -> non empty with_all_isomorphisms for subcategory of ;

coherence for b

b

proof end;

registration

let A be with_complete_lattices category;

coherence

for b_{1} being non empty subcategory of A holds b_{1} is with_complete_lattices

end;
coherence

for b

proof end;

definition

let W be with_non-empty_element set ;

defpred S_{1}[ Object of (W -UPS_category)] means latt $1 is continuous ;

consider a being non empty set such that

A1: a in W by SETFAM_1:def 10;

set r = the well-ordering upper-bounded Order of a;

set b = RelStr(# a, the well-ordering upper-bounded Order of a #);

ex b_{1} being non empty strict full subcategory of W -UPS_category st

for a being Object of (W -UPS_category) holds

( a is Object of b_{1} iff latt a is continuous )

uniqueness

for b_{1}, b_{2} being non empty strict full subcategory of W -UPS_category st ( for a being Object of (W -UPS_category) holds

( a is Object of b_{1} iff latt a is continuous ) ) & ( for a being Object of (W -UPS_category) holds

( a is Object of b_{2} iff latt a is continuous ) ) holds

b_{1} = b_{2};

end;
defpred S

consider a being non empty set such that

A1: a in W by SETFAM_1:def 10;

set r = the well-ordering upper-bounded Order of a;

set b = RelStr(# a, the well-ordering upper-bounded Order of a #);

func W -CONT_category -> non empty strict full subcategory of W -UPS_category means :Def11: :: YELLOW21:def 11

for a being Object of (W -UPS_category) holds

( a is Object of it iff latt a is continuous );

existence for a being Object of (W -UPS_category) holds

( a is Object of it iff latt a is continuous );

ex b

for a being Object of (W -UPS_category) holds

( a is Object of b

proof end;

correctness uniqueness

for b

( a is Object of b

( a is Object of b

b

proof end;

:: deftheorem Def11 defines -CONT_category YELLOW21:def 11 :

for W being with_non-empty_element set

for b_{2} being non empty strict full subcategory of W -UPS_category holds

( b_{2} = W -CONT_category iff for a being Object of (W -UPS_category) holds

( a is Object of b_{2} iff latt a is continuous ) );

for W being with_non-empty_element set

for b

( b

( a is Object of b

definition

let W be with_non-empty_element set ;

defpred S_{1}[ Object of (W -CONT_category)] means latt $1 is algebraic ;

consider a being non empty set such that

A1: a in W by SETFAM_1:def 10;

set r = the well-ordering upper-bounded Order of a;

set b = RelStr(# a, the well-ordering upper-bounded Order of a #);

ex b_{1} being non empty strict full subcategory of W -CONT_category st

for a being Object of (W -CONT_category) holds

( a is Object of b_{1} iff latt a is algebraic )

uniqueness

for b_{1}, b_{2} being non empty strict full subcategory of W -CONT_category st ( for a being Object of (W -CONT_category) holds

( a is Object of b_{1} iff latt a is algebraic ) ) & ( for a being Object of (W -CONT_category) holds

( a is Object of b_{2} iff latt a is algebraic ) ) holds

b_{1} = b_{2};

end;
defpred S

consider a being non empty set such that

A1: a in W by SETFAM_1:def 10;

set r = the well-ordering upper-bounded Order of a;

set b = RelStr(# a, the well-ordering upper-bounded Order of a #);

func W -ALG_category -> non empty strict full subcategory of W -CONT_category means :Def12: :: YELLOW21:def 12

for a being Object of (W -CONT_category) holds

( a is Object of it iff latt a is algebraic );

existence for a being Object of (W -CONT_category) holds

( a is Object of it iff latt a is algebraic );

ex b

for a being Object of (W -CONT_category) holds

( a is Object of b

proof end;

correctness uniqueness

for b

( a is Object of b

( a is Object of b

b

proof end;

:: deftheorem Def12 defines -ALG_category YELLOW21:def 12 :

for W being with_non-empty_element set

for b_{2} being non empty strict full subcategory of W -CONT_category holds

( b_{2} = W -ALG_category iff for a being Object of (W -CONT_category) holds

( a is Object of b_{2} iff latt a is algebraic ) );

for W being with_non-empty_element set

for b

( b

( a is Object of b

theorem Th16: :: YELLOW21:16

for W being with_non-empty_element set

for L being LATTICE st the carrier of L in W holds

( L is Object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) )

for L being LATTICE st the carrier of L in W holds

( L is Object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) )

proof end;

theorem :: YELLOW21:17

for W being with_non-empty_element set

for L being LATTICE st the carrier of L in W holds

( L is Object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) )

for L being LATTICE st the carrier of L in W holds

( L is Object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) )

proof end;

theorem Th18: :: YELLOW21:18

for W being with_non-empty_element set

for a, b being Object of (W -CONT_category)

for f being set holds

( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

for a, b being Object of (W -CONT_category)

for f being set holds

( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

proof end;

theorem Th19: :: YELLOW21:19

for W being with_non-empty_element set

for a, b being Object of (W -ALG_category)

for f being set holds

( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

for a, b being Object of (W -ALG_category)

for f being set holds

( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

proof end;

registration

let W be with_non-empty_element set ;

let a, b be Object of (W -CONT_category);

coherence

not <^a,b^> is empty

end;
let a, b be Object of (W -CONT_category);

coherence

not <^a,b^> is empty

proof end;

registration

let W be with_non-empty_element set ;

let a, b be Object of (W -ALG_category);

coherence

not <^a,b^> is empty

end;
let a, b be Object of (W -ALG_category);

coherence

not <^a,b^> is empty

proof end;