yellow18.miz
begin
scheme ::
YELLOW18:sch1
AltCatStrLambda { A() -> non
empty
set , B(
object,
object) ->
set , C(
object,
object,
object,
object,
object) ->
object } :
ex C be
strict non
empty
transitive
AltCatStr st the
carrier of C
= A() & (for a,b be
Object of C holds
<^a, b^>
= B(a,b)) & for a,b,c be
Object of C st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= C(a,b,c,f,g)
provided
A1: for a,b,c be
Element of A(), f,g be
set st f
in B(a,b) & g
in B(b,c) holds C(a,b,c,f,g)
in B(a,c);
consider B be
ManySortedSet of
[:A(), A():] such that
A2: for a,b be
Element of A() holds (B
. (a,b))
= B(a,b) from
ALTCAT_1:sch 2;
defpred
P[
object,
object] means ex a,b,c be
Element of A(), F be
Function of (
{|B, B|}
. (a,b,c)), (
{|B|}
. (a,b,c)) st $1
=
[a, b, c] & $2
= F & for f,g be
object st f
in B(a,b) & g
in B(b,c) holds (F
.
[g, f])
= C(a,b,c,f,g);
A3: for i be
object st i
in
[:A(), A(), A():] holds ex j be
object st
P[i, j]
proof
let i be
object;
assume i
in
[:A(), A(), A():];
then
consider a,b,c be
object such that
A4: a
in A() and
A5: b
in A() and
A6: c
in A() and
A7: i
=
[a, b, c] by
MCART_1: 68;
reconsider a, b, c as
Element of A() by
A4,
A5,
A6;
defpred
P[
object,
object] means ex f,g be
object st $1
=
[g, f] & $2
= C(a,b,c,f,g);
A8: for x be
object st x
in
[:B(b,c), B(a,b):] holds ex y be
object st y
in B(a,c) &
P[x, y]
proof
let x be
object;
assume x
in
[:B(b,c), B(a,b):];
then
consider x1,x2 be
object such that
A9: x1
in B(b,c) and
A10: x2
in B(a,b) and
A11: x
=
[x1, x2] by
ZFMISC_1:def 2;
take y = C(a,b,c,x2,x1);
thus y
in B(a,c) by
A1,
A9,
A10;
thus thesis by
A11;
end;
consider F be
Function such that
A12: (
dom F)
=
[:B(b,c), B(a,b):] & (
rng F)
c= B(a,c) and
A13: for x be
object st x
in
[:B(b,c), B(a,b):] holds
P[x, (F
. x)] from
FUNCT_1:sch 6(
A8);
A14: (B
. (a,b))
= B(a,b) by
A2;
A15: (B
. (b,c))
= B(b,c) by
A2;
A16: (B
. (a,c))
= B(a,c) by
A2;
A17: (
{|B, B|}
. (a,b,c))
=
[:B(b,c), B(a,b):] by
A14,
A15,
ALTCAT_1:def 4;
(
{|B|}
. (a,b,c))
= B(a,c) by
A16,
ALTCAT_1:def 3;
then
reconsider F as
Function of (
{|B, B|}
. (a,b,c)), (
{|B|}
. (a,b,c)) by
A12,
A17,
FUNCT_2: 2;
take j = F, a, b, c, F;
thus i
=
[a, b, c] & j
= F by
A7;
let f,g be
object;
assume that
A18: f
in B(a,b) and
A19: g
in B(b,c);
[g, f]
in
[:B(b,c), B(a,b):] by
A18,
A19,
ZFMISC_1: 87;
then
consider f9,g9 be
object such that
A20:
[g, f]
=
[g9, f9] and
A21: (F
.
[g, f])
= C(a,b,c,f9,g9) by
A13;
g
= g9 by
A20,
XTUPLE_0: 1;
hence thesis by
A20,
A21,
XTUPLE_0: 1;
end;
consider C be
Function such that
A22: (
dom C)
=
[:A(), A(), A():] and
A23: for i be
object st i
in
[:A(), A(), A():] holds
P[i, (C
. i)] from
CLASSES1:sch 1(
A3);
reconsider C as
ManySortedSet of
[:A(), A(), A():] by
A22,
PARTFUN1:def 2,
RELAT_1:def 18;
now
let i be
object;
assume i
in
[:A(), A(), A():];
then
consider a,b,c be
Element of A(), F be
Function of (
{|B, B|}
. (a,b,c)), (
{|B|}
. (a,b,c)) such that
A24: i
=
[a, b, c] and
A25: (C
. i)
= F and for f,g be
object st f
in B(a,b) & g
in B(b,c) holds (F
.
[g, f])
= C(a,b,c,f,g) by
A23;
A26: (
{|B|}
. (a,b,c))
= (
{|B|}
. i) by
A24,
MULTOP_1:def 1;
(
{|B, B|}
. (a,b,c))
= (
{|B, B|}
. i) by
A24,
MULTOP_1:def 1;
hence (C
. i) is
Function of (
{|B, B|}
. i), (
{|B|}
. i) by
A25,
A26;
end;
then
reconsider C as
ManySortedFunction of
{|B, B|},
{|B|} by
PBOOLE:def 15;
set alt =
AltCatStr (# A(), B, C #);
alt is
transitive
proof
let o1,o2,o3 be
Object of alt;
reconsider a = o1, b = o2, c = o3 as
Element of A();
set f = the
Element of
<^o1, o2^>, g = the
Element of
<^o2, o3^>;
assume that
A27:
<^o1, o2^>
<>
{} and
A28:
<^o2, o3^>
<>
{} ;
A29: f
in
<^o1, o2^> by
A27;
A30: g
in
<^o2, o3^> by
A28;
A31: f
in B(a,b) by
A2,
A29;
g
in B(b,c) by
A2,
A30;
then C(a,b,c,f,g)
in B(a,c) by
A1,
A31;
hence thesis by
A2;
end;
then
reconsider alt as
strict
transitive non
empty
AltCatStr;
take alt;
thus the
carrier of alt
= A();
thus for a,b be
Object of alt holds
<^a, b^>
= B(a,b) by
A2;
let a,b,c be
Object of alt such that
A32:
<^a, b^>
<>
{} and
A33:
<^b, c^>
<>
{} ;
[a, b, c]
in
[:A(), A(), A():] by
MCART_1: 69;
then
consider a9,b9,c9 be
Element of A(), F be
Function of (
{|B, B|}
. (a9,b9,c9)), (
{|B|}
. (a9,b9,c9)) such that
A34:
[a, b, c]
=
[a9, b9, c9] and
A35: (C
.
[a, b, c])
= F and
A36: for f,g be
object st f
in B(a9,b9) & g
in B(b9,c9) holds (F
.
[g, f])
= C(a9,b9,c9,f,g) by
A23;
A37: a
= a9 by
A34,
XTUPLE_0: 3;
A38: b
= b9 by
A34,
XTUPLE_0: 3;
A39: c
= c9 by
A34,
XTUPLE_0: 3;
let f be
Morphism of a, b, g be
Morphism of b, c;
A40:
<^a, b^>
= B(a,b) by
A2;
<^b, c^>
= B(b,c) by
A2;
then
A41: (F
.
[g, f])
= C(a,b,c,f,g) by
A32,
A33,
A36,
A37,
A38,
A39,
A40;
thus (g
* f)
= ((the
Comp of alt
. (a,b,c))
. (g,f)) by
A32,
A33,
ALTCAT_1:def 8
.= C(a,b,c,f,g) by
A35,
A41,
MULTOP_1:def 1;
end;
scheme ::
YELLOW18:sch2
CatAssocSch { A() -> non
empty
transitive
AltCatStr , C(
object,
object,
object,
object,
object) ->
object } :
A() is
associative
provided
A1: for a,b,c be
Object of A() st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= C(a,b,c,f,g)
and
A2: for a,b,c,d be
Object of A(), f,g,h be
set st f
in
<^a, b^> & g
in
<^b, c^> & h
in
<^c, d^> holds C(a,c,d,C,h)
= C(a,b,d,f,C);
let i,j,k,l be
Element of A();
set alt = A(), IT = the
Comp of alt;
set B = the
Arrows of alt;
reconsider i9 = i, j9 = j, k9 = k, l9 = l as
Object of alt;
let f,g,h be
set such that
A3: f
in (B
. (i,j)) and
A4: g
in (B
. (j,k)) and
A5: h
in (B
. (k,l));
A6: (B
. (i,j))
=
<^i9, j9^>;
reconsider f9 = f as
Morphism of i9, j9 by
A3;
A7: (B
. (j,k))
=
<^j9, k9^>;
reconsider g9 = g as
Morphism of j9, k9 by
A4;
A8: (B
. (k,l))
=
<^k9, l9^>;
reconsider h9 = h as
Morphism of k9, l9 by
A5;
A9:
<^i9, k9^>
<>
{} by
A3,
A4,
A6,
A7,
ALTCAT_1:def 2;
A10:
<^j9, l9^>
<>
{} by
A4,
A5,
A7,
A8,
ALTCAT_1:def 2;
thus ((IT
. (i,k,l))
. (h,((IT
. (i,j,k))
. (g,f))))
= ((IT
. (i,k,l))
. (h,(g9
* f9))) by
A3,
A4,
ALTCAT_1:def 8
.= (h9
* (g9
* f9)) by
A5,
A9,
ALTCAT_1:def 8
.= C(i,k,l,*,h9) by
A1,
A5,
A9
.= C(i,k,l,C,h) by
A1,
A3,
A4
.= C(i9,j9,l9,f,C) by
A2,
A3,
A4,
A5,
A6,
A7,
A8
.= C(i9,j9,l9,f,*) by
A1,
A4,
A5
.= ((h9
* g9)
* f9) by
A1,
A3,
A10
.= ((IT
. (i,j,l))
. ((h9
* g9),f)) by
A3,
A10,
ALTCAT_1:def 8
.= ((IT
. (i,j,l))
. (((IT
. (j,k,l))
. (h,g)),f)) by
A4,
A5,
ALTCAT_1:def 8;
end;
scheme ::
YELLOW18:sch3
CatUnitsSch { A() -> non
empty
transitive
AltCatStr , C(
object,
object,
object,
object,
object) ->
object } :
A() is
with_units
provided
A1: for a,b,c be
Object of A() st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= C(a,b,c,f,g)
and
A2: for a be
Object of A() holds ex f be
set st f
in
<^a, a^> & for b be
Object of A(), g be
set st g
in
<^a, b^> holds C(a,a,b,f,g)
= g
and
A3: for a be
Object of A() holds ex f be
set st f
in
<^a, a^> & for b be
Object of A(), g be
set st g
in
<^b, a^> holds C(b,a,a,g,f)
= g;
set alt = A(), IT = the
Comp of alt, I = the
carrier of alt;
set G = the
Arrows of alt;
hereby
let j be
Element of I;
reconsider j9 = j as
Object of alt;
consider f be
set such that
A4: f
in
<^j9, j9^> and
A5: for b be
Element of A(), g be
set st g
in
<^b, j9^> holds C(b,j9,j9,g,f)
= g by
A3;
take f;
thus f
in (G
. (j,j)) by
A4;
let i be
Element of I, g be
set such that
A6: g
in (G
. (i,j));
reconsider i9 = i as
Object of alt;
(G
. (i,j))
=
<^i9, j9^>;
then
A7: C(i,j,j,g,f)
= g by
A5,
A6;
reconsider f9 = f as
Morphism of j9, j9 by
A4;
reconsider g9 = g as
Morphism of i9, j9 by
A6;
thus ((IT
. (i,j,j))
. (f,g))
= (f9
* g9) by
A4,
A6,
ALTCAT_1:def 8
.= g by
A1,
A4,
A6,
A7;
end;
let i be
Element of I;
reconsider i9 = i as
Object of alt;
consider e be
set such that
A8: e
in
<^i9, i9^> and
A9: for b be
Element of A(), g be
set st g
in
<^i9, b^> holds C(i,i,b,e,g)
= g by
A2;
take e;
thus e
in (G
. (i,i)) by
A8;
reconsider e9 = e as
Morphism of i9, i9 by
A8;
let j be
Element of I, f be
set such that
A10: f
in (G
. (i,j));
reconsider j9 = j as
Object of alt;
(G
. (i,j))
=
<^i9, j9^>;
then
A11: C(i,i,j,e,f)
= f by
A9,
A10;
reconsider f9 = f as
Morphism of i9, j9 by
A10;
thus ((IT
. (i,i,j))
. (f,e))
= (f9
* e9) by
A8,
A10,
ALTCAT_1:def 8
.= f by
A1,
A8,
A10,
A11;
end;
scheme ::
YELLOW18:sch4
CategoryLambda { A() -> non
empty
set , B(
object,
object) ->
set , C(
object,
object,
object,
object,
object) ->
object } :
ex C be
strict
category st the
carrier of C
= A() & (for a,b be
Object of C holds
<^a, b^>
= B(a,b)) & for a,b,c be
Object of C st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= C(a,b,c,f,g)
provided
A1: for a,b,c be
Element of A(), f,g be
set st f
in B(a,b) & g
in B(b,c) holds C(a,b,c,f,g)
in B(a,c)
and
A2: for a,b,c,d be
Element of A(), f,g,h be
set st f
in B(a,b) & g
in B(b,c) & h
in B(c,d) holds C(a,c,d,C,h)
= C(a,b,d,f,C)
and
A3: for a be
Element of A() holds ex f be
set st f
in B(a,a) & for b be
Element of A(), g be
set st g
in B(a,b) holds C(a,a,b,f,g)
= g
and
A4: for a be
Element of A() holds ex f be
set st f
in B(a,a) & for b be
Element of A(), g be
set st g
in B(b,a) holds C(b,a,a,g,f)
= g;
A5: for a,b,c be
Element of A(), f,g be
set st f
in B(a,b) & g
in B(b,c) holds C(a,b,c,f,g)
in B(a,c) by
A1;
consider C be
strict non
empty
transitive
AltCatStr such that
A6: the
carrier of C
= A() and
A7: for a,b be
Object of C holds
<^a, b^>
= B(a,b) and
A8: for a,b,c be
Object of C st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= C(a,b,c,f,g) from
AltCatStrLambda(
A5);
A9: for a,b,c,d be
Object of C, f,g,h be
set st f
in
<^a, b^> & g
in
<^b, c^> & h
in
<^c, d^> holds C(a,c,d,C,h)
= C(a,b,d,f,C)
proof
let a,b,c,d be
Object of C, f,g,h be
set such that
A10: f
in
<^a, b^> and
A11: g
in
<^b, c^> and
A12: h
in
<^c, d^>;
A13:
<^a, b^>
= B(a,b) by
A7;
A14:
<^b, c^>
= B(b,c) by
A7;
<^c, d^>
= B(c,d) by
A7;
hence thesis by
A2,
A6,
A10,
A11,
A12,
A13,
A14;
end;
A15: for a be
Object of C holds ex f be
set st f
in
<^a, a^> & for b be
Object of C, g be
set st g
in
<^a, b^> holds C(a,a,b,f,g)
= g
proof
let a be
Object of C;
consider f be
set such that
A16: f
in B(a,a) and
A17: for b be
Element of A(), g be
set st g
in B(a,b) holds C(a,a,b,f,g)
= g by
A3,
A6;
take f;
thus f
in
<^a, a^> by
A7,
A16;
let b be
Object of C;
<^a, b^>
= B(a,b) by
A7;
hence thesis by
A6,
A17;
end;
A18: for a be
Object of C holds ex f be
set st f
in
<^a, a^> & for b be
Object of C, g be
set st g
in
<^b, a^> holds C(b,a,a,g,f)
= g
proof
let a be
Object of C;
consider f be
set such that
A19: f
in B(a,a) and
A20: for b be
Element of A(), g be
set st g
in B(b,a) holds C(b,a,a,g,f)
= g by
A4,
A6;
take f;
thus f
in
<^a, a^> by
A7,
A19;
let b be
Object of C;
<^b, a^>
= B(b,a) by
A7;
hence thesis by
A6,
A20;
end;
A21: C is
associative from
CatAssocSch(
A8,
A9);
C is
with_units from
CatUnitsSch(
A8,
A15,
A18);
hence thesis by
A6,
A7,
A8,
A21;
end;
scheme ::
YELLOW18:sch5
CategoryLambdaUniq { A() -> non
empty
set , B(
object,
object) ->
object , C(
object,
object,
object,
object,
object) ->
object } :
for C1,C2 be non
empty
transitive
AltCatStr st the
carrier of C1
= A() & (for a,b be
Object of C1 holds
<^a, b^>
= B(a,b)) & (for a,b,c be
Object of C1 st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= C(a,b,c,f,g)) & the
carrier of C2
= A() & (for a,b be
Object of C2 holds
<^a, b^>
= B(a,b)) & (for a,b,c be
Object of C2 st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= C(a,b,c,f,g)) holds the AltCatStr of C1
= the AltCatStr of C2;
let C1,C2 be non
empty
transitive
AltCatStr such that
A1: the
carrier of C1
= A() and
A2: for a,b be
Object of C1 holds
<^a, b^>
= B(a,b) and
A3: for a,b,c be
Object of C1 st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= C(a,b,c,f,g) and
A4: the
carrier of C2
= A() and
A5: for a,b be
Object of C2 holds
<^a, b^>
= B(a,b) and
A6: for a,b,c be
Object of C2 st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= C(a,b,c,f,g);
A7:
now
let i be
object;
assume i
in
[:A(), A():];
then
consider a,b be
object such that
A8: a
in A() and
A9: b
in A() and
A10: i
=
[a, b] by
ZFMISC_1:def 2;
reconsider a1 = a, b1 = b as
Object of C1 by
A1,
A8,
A9;
reconsider a2 = a, b2 = b as
Object of C2 by
A4,
A8,
A9;
thus (the
Arrows of C1
. i)
=
<^a1, b1^> by
A10
.= B(a1,b1) by
A2
.=
<^a2, b2^> by
A5
.= (the
Arrows of C2
. i) by
A10;
end;
then
A11: the
Arrows of C1
= the
Arrows of C2 by
A1,
A4,
PBOOLE: 3;
now
let i be
object;
assume i
in
[:A(), A(), A():];
then
consider a,b,c be
object such that
A12: a
in A() and
A13: b
in A() and
A14: c
in A() and
A15: i
=
[a, b, c] by
MCART_1: 68;
reconsider a1 = a, b1 = b, c1 = c as
Object of C1 by
A1,
A12,
A13,
A14;
reconsider a2 = a, b2 = b, c2 = c as
Object of C2 by
A4,
A12,
A13,
A14;
A16: (the
Comp of C1
. i)
= (the
Comp of C1
. (a1,b1,c1)) by
A15,
MULTOP_1:def 1;
A17: (the
Comp of C2
. i)
= (the
Comp of C2
. (a2,b2,c2)) by
A15,
MULTOP_1:def 1;
A18:
now
assume
A19:
[:
<^b1, c1^>,
<^a1, b1^>:]
<>
{} ;
then
A20:
<^b1, c1^>
<>
{} by
ZFMISC_1: 90;
<^a1, b1^>
<>
{} by
A19,
ZFMISC_1: 90;
hence
<^a1, c1^>
<>
{} by
A20,
ALTCAT_1:def 2;
end;
then
A21: (
dom (the
Comp of C1
. (a1,b1,c1)))
=
[:
<^b1, c1^>,
<^a1, b1^>:] by
FUNCT_2:def 1;
A22: (
dom (the
Comp of C2
. (a2,b2,c2)))
=
[:
<^b1, c1^>,
<^a1, b1^>:] by
A11,
A18,
FUNCT_2:def 1;
now
let j be
object;
assume j
in
[:
<^b1, c1^>,
<^a1, b1^>:];
then
consider j1,j2 be
object such that
A23: j1
in
<^b1, c1^> and
A24: j2
in
<^a1, b1^> and
A25: j
=
[j1, j2] by
ZFMISC_1:def 2;
reconsider j1 as
Morphism of b1, c1 by
A23;
reconsider j2 as
Morphism of a1, b1 by
A24;
reconsider f1 = j1 as
Morphism of b2, c2 by
A1,
A4,
A7,
PBOOLE: 3;
reconsider f2 = j2 as
Morphism of a2, b2 by
A1,
A4,
A7,
PBOOLE: 3;
thus ((the
Comp of C1
. (a1,b1,c1))
. j)
= ((the
Comp of C1
. (a1,b1,c1))
. (j1,j2)) by
A25
.= (j1
* j2) by
A23,
A24,
ALTCAT_1:def 8
.= C(a1,b1,c1,j2,j1) by
A3,
A23,
A24
.= (f1
* f2) by
A6,
A11,
A23,
A24
.= ((the
Comp of C2
. (a2,b2,c2))
. (f1,f2)) by
A11,
A23,
A24,
ALTCAT_1:def 8
.= ((the
Comp of C2
. (a2,b2,c2))
. j) by
A25;
end;
hence (the
Comp of C1
. i)
= (the
Comp of C2
. i) by
A16,
A17,
A21,
A22;
end;
hence thesis by
A1,
A4,
A11,
PBOOLE: 3;
end;
scheme ::
YELLOW18:sch6
CategoryQuasiLambda { A() -> non
empty
set , P[
object,
object,
object], B(
object,
object) ->
set , C(
object,
object,
object,
object,
object) ->
object } :
ex C be
strict
category st the
carrier of C
= A() & (for a,b be
Object of C holds for f be
set holds f
in
<^a, b^> iff f
in B(a,b) & P[a, b, f]) & for a,b,c be
Object of C st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= C(a,b,c,f,g)
provided
A1: for a,b,c be
Element of A(), f,g be
set st f
in B(a,b) & P[a, b, f] & g
in B(b,c) & P[b, c, g] holds C(a,b,c,f,g)
in B(a,c) & P[a, c, C(a,b,c,f,g)]
and
A2: for a,b,c,d be
Element of A(), f,g,h be
set st f
in B(a,b) & P[a, b, f] & g
in B(b,c) & P[b, c, g] & h
in B(c,d) & P[c, d, h] holds C(a,c,d,C,h)
= C(a,b,d,f,C)
and
A3: for a be
Element of A() holds ex f be
set st f
in B(a,a) & P[a, a, f] & for b be
Element of A(), g be
set st g
in B(a,b) & P[a, b, g] holds C(a,a,b,f,g)
= g
and
A4: for a be
Element of A() holds ex f be
set st f
in B(a,a) & P[a, a, f] & for b be
Element of A(), g be
set st g
in B(b,a) & P[b, a, g] holds C(b,a,a,g,f)
= g;
deffunc
F(
object) = B(`1,`2);
defpred
Q[
object,
object] means P[($1
`1 ), ($1
`2 ), $2];
consider P be
Function such that (
dom P)
=
[:A(), A():] and
A5: for i be
object st i
in
[:A(), A():] holds for x be
object holds x
in (P
. i) iff x
in
F(i) &
Q[i, x] from
CARD_3:sch 2;
deffunc
b(
set,
set) = (P
. ($1,$2));
A6:
now
let a,b be
Element of A();
let x be
set;
A7: (
[a, b]
`1 )
= a;
A8: (
[a, b]
`2 )
= b;
[a, b]
in
[:A(), A():] by
ZFMISC_1:def 2;
hence x
in (P
. (a,b)) iff x
in B(a,b) & P[a, b, x] by
A5,
A7,
A8;
end;
A9:
now
let a,b,c be
Element of A(), f,g be
set;
assume that
A10: f
in
b(a,b) and
A11: g
in
b(b,c);
A12: f
in B(a,b) by
A6,
A10;
A13: P[a, b, f] by
A6,
A10;
A14: g
in B(b,c) by
A6,
A11;
A15: P[b, c, g] by
A6,
A11;
then
A16: C(a,b,c,f,g)
in B(a,c) by
A1,
A12,
A13,
A14;
P[a, c, C(a,b,c,f,g)] by
A1,
A12,
A13,
A14,
A15;
hence C(a,b,c,f,g)
in
b(a,c) by
A6,
A16;
end;
A17:
now
let a,b,c,d be
Element of A(), f,g,h be
set;
assume that
A18: f
in
b(a,b) and
A19: g
in
b(b,c) and
A20: h
in
b(c,d);
A21: f
in B(a,b) by
A6,
A18;
A22: P[a, b, f] by
A6,
A18;
A23: g
in B(b,c) by
A6,
A19;
A24: P[b, c, g] by
A6,
A19;
A25: h
in B(c,d) by
A6,
A20;
P[c, d, h] by
A6,
A20;
hence C(a,c,d,C,h)
= C(a,b,d,f,C) by
A2,
A21,
A22,
A23,
A24,
A25;
end;
A26:
now
let a be
Element of A();
consider f be
set such that
A27: f
in B(a,a) and
A28: P[a, a, f] and
A29: for b be
Element of A(), g be
set st g
in B(a,b) & P[a, b, g] holds C(a,a,b,f,g)
= g by
A3;
take f;
thus f
in
b(a,a) by
A6,
A27,
A28;
let b be
Element of A(), g be
set;
assume
A30: g
in
b(a,b);
then
A31: g
in B(a,b) by
A6;
P[a, b, g] by
A6,
A30;
hence C(a,a,b,f,g)
= g by
A29,
A31;
end;
A32:
now
let a be
Element of A();
consider f be
set such that
A33: f
in B(a,a) and
A34: P[a, a, f] and
A35: for b be
Element of A(), g be
set st g
in B(b,a) & P[b, a, g] holds C(b,a,a,g,f)
= g by
A4;
take f;
thus f
in
b(a,a) by
A6,
A33,
A34;
let b be
Element of A(), g be
set;
assume
A36: g
in
b(b,a);
then
A37: g
in B(b,a) by
A6;
P[b, a, g] by
A6,
A36;
hence C(b,a,a,g,f)
= g by
A35,
A37;
end;
consider C be
strict
category such that
A38: the
carrier of C
= A() and
A39: for a,b be
Object of C holds
<^a, b^>
=
b(a,b) and
A40: for a,b,c be
Object of C st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= C(a,b,c,f,g) from
CategoryLambda(
A9,
A17,
A26,
A32);
take C;
thus the
carrier of C
= A() by
A38;
hereby
let a,b be
Object of C, f be
set;
<^a, b^>
= (P
. (a,b)) by
A39;
hence f
in
<^a, b^> iff f
in B(a,b) & P[a, b, f] by
A6,
A38;
end;
thus thesis by
A40;
end;
registration
let f be
Function-yielding
Function;
let a,b,c be
set;
cluster (f
. (a,b,c)) ->
Relation-like
Function-like;
coherence
proof
(f
. (a,b,c))
= (f
.
[a, b, c]) by
MULTOP_1:def 1;
hence thesis;
end;
end
scheme ::
YELLOW18:sch7
SubcategoryEx { A() ->
category , P[
object], Q[
object,
object,
object] } :
ex B be
strict non
empty
subcategory of A() st (for a be
Object of A() holds a is
Object of B iff P[a]) & for a,b be
Object of A(), a9,b9 be
Object of B st a9
= a & b9
= b &
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds f
in
<^a9, b9^> iff Q[a, b, f]
provided
A1: ex a be
Object of A() st P[a]
and
A2: for a,b,c be
Object of A() st P[a] & P[b] & P[c] &
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c st Q[a, b, f] & Q[b, c, g] holds Q[a, c, (g
* f)]
and
A3: for a be
Object of A() st P[a] holds Q[a, a, (
idm a)];
consider X be
set such that
A4: for x be
object holds x
in X iff x
in the
carrier of A() & P[x] from
XBOOLE_0:sch 1;
reconsider X as non
empty
set by
A1,
A4;
A5: X
c= the
carrier of A() by
A4;
deffunc
B(
set,
set) = (the
Arrows of A()
. ($1,$2));
deffunc
C(
set,
set,
set,
set,
set) = ((the
Comp of A()
. ($1,$2,$3))
. ($5,$4));
A6:
now
let a,b,c be
Element of X, f,g be
set such that
A7: f
in
B(a,b) and
A8: Q[a, b, f] and
A9: g
in
B(b,c) and
A10: Q[b, c, g];
reconsider a9 = a, b9 = b, c9 = c as
Object of A() by
A4;
A11:
B(a,b)
=
<^a9, b9^>;
reconsider f9 = f as
Morphism of a9, b9 by
A7;
A12:
B(b,c)
=
<^b9, c9^>;
reconsider g9 = g as
Morphism of b9, c9 by
A9;
A13:
C(a,b,c,f,g)
= (g9
* f9) by
A7,
A9,
ALTCAT_1:def 8;
<^a9, c9^>
<>
{} by
A7,
A9,
A11,
A12,
ALTCAT_1:def 2;
hence
C(a,b,c,f,g)
in
B(a,c) by
A13;
A14: P[a9] by
A4;
A15: P[b9] by
A4;
P[c9] by
A4;
hence Q[a, c,
C(a,b,c,f,g)] by
A2,
A7,
A8,
A9,
A10,
A13,
A14,
A15;
end;
A16:
now
let a,b,c,d be
Element of X, f,g,h be
set such that
A17: f
in
B(a,b) and Q[a, b, f] and
A18: g
in
B(b,c) and Q[b, c, g] and
A19: h
in
B(c,d) and Q[c, d, h];
reconsider a9 = a, b9 = b, c9 = c, d9 = d as
Object of A() by
A4;
A20:
B(a,b)
=
<^a9, b9^>;
reconsider f9 = f as
Morphism of a9, b9 by
A17;
A21:
B(b,c)
=
<^b9, c9^>;
reconsider g9 = g as
Morphism of b9, c9 by
A18;
A22:
B(c,d)
=
<^c9, d9^>;
reconsider h9 = h as
Morphism of c9, d9 by
A19;
A23:
<^a9, c9^>
<>
{} by
A17,
A18,
A20,
A21,
ALTCAT_1:def 2;
A24:
<^b9, d9^>
<>
{} by
A18,
A19,
A21,
A22,
ALTCAT_1:def 2;
thus
C(a,c,d,C,h)
=
C(a9,c9,d9,*,h) by
A17,
A18,
ALTCAT_1:def 8
.= (h9
* (g9
* f9)) by
A19,
A23,
ALTCAT_1:def 8
.= ((h9
* g9)
* f9) by
A17,
A18,
A19,
ALTCAT_1: 21
.=
C(a,b,d,f,*) by
A17,
A24,
ALTCAT_1:def 8
.=
C(a,b,d,f,C) by
A18,
A19,
ALTCAT_1:def 8;
end;
A25:
now
let a be
Element of X;
reconsider b = a as
Object of A() by
A4;
reconsider f = (
idm b) as
set;
take f;
P[b] by
A4;
hence f
in
B(a,a) & Q[a, a, f] by
A3;
let c be
Element of X, g be
set such that
A26: g
in
B(a,c) and Q[a, c, g];
reconsider d = c as
Object of A() by
A4;
reconsider g9 = g as
Morphism of b, d by
A26;
thus
C(a,a,c,f,g)
= (g9
* (
idm b)) by
A26,
ALTCAT_1:def 8
.= g by
A26,
ALTCAT_1:def 17;
end;
A27:
now
let a be
Element of X;
reconsider b = a as
Object of A() by
A4;
reconsider f = (
idm b) as
set;
take f;
P[b] by
A4;
hence f
in
B(a,a) & Q[a, a, f] by
A3;
let c be
Element of X, g be
set such that
A28: g
in
B(c,a) and Q[c, a, g];
reconsider d = c as
Object of A() by
A4;
reconsider g9 = g as
Morphism of d, b by
A28;
thus
C(c,a,a,g,f)
= ((
idm b)
* g9) by
A28,
ALTCAT_1:def 8
.= g by
A28,
ALTCAT_1: 20;
end;
consider C be
strict
category such that
A29: the
carrier of C
= X and
A30: for a,b be
Object of C holds for f be
set holds f
in
<^a, b^> iff f
in
B(a,b) & Q[a, b, f] and
A31: for a,b,c be
Object of C st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
=
C(a,b,c,f,g) from
CategoryQuasiLambda(
A6,
A16,
A25,
A27);
C is
SubCatStr of A()
proof
thus the
carrier of C
c= the
carrier of A() by
A5,
A29;
thus
[:the
carrier of C, the
carrier of C:]
c=
[:the
carrier of A(), the
carrier of A():] by
A5,
A29,
ZFMISC_1: 96;
hereby
let i be
set;
assume i
in
[:the
carrier of C, the
carrier of C:];
then
consider a,b be
object such that
A32: a
in the
carrier of C and
A33: b
in the
carrier of C and
A34:
[a, b]
= i by
ZFMISC_1:def 2;
reconsider a, b as
Object of C by
A32,
A33;
A35: (the
Arrows of C
. i)
=
<^a, b^> by
A34;
A36: (the
Arrows of A()
. i)
= (the
Arrows of A()
. (a,b)) by
A34;
thus (the
Arrows of C
. i)
c= (the
Arrows of A()
. i) by
A30,
A35,
A36;
end;
thus
[:the
carrier of C, the
carrier of C, the
carrier of C:]
c=
[:the
carrier of A(), the
carrier of A(), the
carrier of A():] by
A5,
A29,
MCART_1: 73;
let i be
set;
assume i
in
[:the
carrier of C, the
carrier of C, the
carrier of C:];
then
consider a,b,c be
object such that
A37: a
in the
carrier of C and
A38: b
in the
carrier of C and
A39: c
in the
carrier of C and
A40:
[a, b, c]
= i by
MCART_1: 68;
reconsider a, b, c as
Object of C by
A37,
A38,
A39;
reconsider a9 = a, b9 = b, c9 = c as
Object of A() by
A4,
A29;
let x be
object;
assume x
in (the
Comp of C
. i);
then
A41: x
in (the
Comp of C
. (a,b,c)) by
A40,
MULTOP_1:def 1;
then
consider gf,h be
object such that
A42: x
=
[gf, h] and
A43: gf
in
[:(the
Arrows of C
. (b,c)), (the
Arrows of C
. (a,b)):] and
A44: h
in (the
Arrows of C
. (a,c)) by
RELSET_1: 2;
consider g,f be
object such that
A45: g
in (the
Arrows of C
. (b,c)) and
A46: f
in (the
Arrows of C
. (a,b)) and
A47:
[g, f]
= gf by
A43,
ZFMISC_1:def 2;
reconsider f as
Morphism of a, b by
A46;
reconsider g as
Morphism of b, c by
A45;
reconsider h as
Morphism of a, c by
A44;
A48: (the
Comp of A()
. (a9,b9,c9))
= (the
Comp of A()
. i) by
A40,
MULTOP_1:def 1;
A49: g
in (the
Arrows of A()
. (b9,c9)) by
A30,
A45;
A50: f
in (the
Arrows of A()
. (a9,b9)) by
A30,
A46;
A51: h
= ((the
Comp of C
. (a,b,c))
. (g,f)) by
A41,
A42,
A47,
FUNCT_1: 1
.= (g
* f) by
A45,
A46,
ALTCAT_1:def 8
.= ((the
Comp of A()
. (a9,b9,c9))
. (g,f)) by
A31,
A45,
A46;
h
in (the
Arrows of A()
. (a9,c9)) by
A30,
A44;
then (
dom (the
Comp of A()
. (a9,b9,c9)))
=
[:(the
Arrows of A()
. (b9,c9)), (the
Arrows of A()
. (a9,b9)):] by
FUNCT_2:def 1;
then gf
in (
dom (the
Comp of A()
. (a9,b9,c9))) by
A47,
A49,
A50,
ZFMISC_1:def 2;
hence thesis by
A42,
A47,
A48,
A51,
FUNCT_1:def 2;
end;
then
reconsider C as non
empty
SubCatStr of A();
for o be
Object of C, o9 be
Object of A() st o
= o9 holds (
idm o9)
in
<^o, o^>
proof
let a be
Object of C, b be
Object of A();
assume
A52: a
= b;
then P[b] by
A4,
A29;
then Q[b, b, (
idm b)] by
A3;
hence thesis by
A30,
A52;
end;
then
reconsider C as
strict non
empty
subcategory of A() by
ALTCAT_2:def 14;
take C;
thus for a be
Object of A() holds a is
Object of C iff P[a] by
A4,
A29;
let a,b be
Object of A(), a9,b9 be
Object of C such that
A53: a9
= a and
A54: b9
= b and
A55:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
thus thesis by
A30,
A53,
A54,
A55;
end;
scheme ::
YELLOW18:sch8
CovariantFunctorLambda { A,B() ->
category , O(
object) ->
object , F(
object,
object,
object) ->
object } :
ex F be
covariant
strict
Functor of A(), B() st (for a be
Object of A() holds (F
. a)
= O(a)) & for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= F(a,b,f)
provided
A1: for a be
Object of A() holds O(a) is
Object of B()
and
A2: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds F(a,b,f)
in (the
Arrows of B()
. (O(a),O(b)))
and
A3: for a,b,c be
Object of A() st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds for a9,b9,c9 be
Object of B() st a9
= O(a) & b9
= O(b) & c9
= O(c) holds for f9 be
Morphism of a9, b9, g9 be
Morphism of b9, c9 st f9
= F(a,b,f) & g9
= F(b,c,g) holds F(a,c,*)
= (g9
* f9)
and
A4: for a be
Object of A(), a9 be
Object of B() st a9
= O(a) holds F(a,a,idm)
= (
idm a9);
consider O be
Function such that
A5: (
dom O)
= the
carrier of A() and
A6: for x be
object st x
in the
carrier of A() holds (O
. x)
= O(x) from
FUNCT_1:sch 3;
(
rng O)
c= the
carrier of B()
proof
let y be
object;
assume y
in (
rng O);
then
consider x be
object such that
A7: x
in (
dom O) and
A8: y
= (O
. x) by
FUNCT_1:def 3;
reconsider x as
Object of A() by
A5,
A7;
A9: y
= O(x) by
A6,
A8;
O(x) is
Object of B() by
A1;
hence thesis by
A9;
end;
then
reconsider O as
Function of the
carrier of A(), the
carrier of B() by
A5,
FUNCT_2: 2;
reconsider OM =
[:O, O:] as
bifunction of the
carrier of A(), the
carrier of B();
defpred
P[
object,
object,
object] means $1
= F(`1,`2,$2);
A10: for i be
object st i
in
[:the
carrier of A(), the
carrier of A():] holds for x be
object st x
in (the
Arrows of A()
. i) holds ex y be
object st y
in ((the
Arrows of B()
* OM)
. i) &
P[y, x, i]
proof
let i be
object;
assume
A11: i
in
[:the
carrier of A(), the
carrier of A():];
then
consider a,b be
object such that
A12: a
in the
carrier of A() and
A13: b
in the
carrier of A() and
A14:
[a, b]
= i by
ZFMISC_1:def 2;
reconsider a, b as
Object of A() by
A12,
A13;
let x be
object;
assume
A15: x
in (the
Arrows of A()
. i);
then
reconsider f = x as
Morphism of a, b by
A14;
take y = F(a,b,f);
A16: y
in (the
Arrows of B()
. (O(a),O(b))) by
A2,
A14,
A15;
A17: O(a)
= (O
. a) by
A6;
i
in (
dom OM) by
A5,
A11,
FUNCT_3:def 8;
then ((the
Arrows of B()
* OM)
. i)
= (the
Arrows of B()
. (OM
. (a,b))) by
A14,
FUNCT_1: 13
.= (the
Arrows of B()
. ((O
. a),(O
. b))) by
A5,
FUNCT_3:def 8;
hence y
in ((the
Arrows of B()
* OM)
. i) by
A6,
A16,
A17;
thus thesis by
A14;
end;
consider M be
ManySortedFunction of the
Arrows of A(), (the
Arrows of B()
* OM) such that
A18: for i be
object st i
in
[:the
carrier of A(), the
carrier of A():] holds ex f be
Function of (the
Arrows of A()
. i), ((the
Arrows of B()
* OM)
. i) st f
= (M
. i) & for x be
object st x
in (the
Arrows of A()
. i) holds
P[(f
. x), x, i] from
MSSUBFAM:sch 1(
A10);
reconsider M as
MSUnTrans of OM, the
Arrows of A(), the
Arrows of B() by
FUNCTOR0:def 4;
FunctorStr (# OM, M #) is
Covariant
proof
take O;
thus thesis;
end;
then
reconsider F =
FunctorStr (# OM, M #) as
Covariant
FunctorStr over A(), B();
A19:
now
let a be
Object of A();
thus (F
. a)
= (
[(O
. a), (O
. a)]
`1 ) by
A5,
FUNCT_3:def 8
.= (O
. a)
.= O(a) by
A6;
end;
A20:
now
let o1,o2 be
Object of A() such that
A21:
<^o1, o2^>
<>
{} ;
let g be
Morphism of o1, o2;
[o1, o2]
in
[:the
carrier of A(), the
carrier of A():] by
ZFMISC_1:def 2;
then
consider f be
Function of (the
Arrows of A()
.
[o1, o2]), ((the
Arrows of B()
* OM)
.
[o1, o2]) such that
A22: f
= (M
.
[o1, o2]) and
A23: for x be
object st x
in (the
Arrows of A()
.
[o1, o2]) holds
P[(f
. x), x,
[o1, o2]] by
A18;
(f
. g)
= F(`1,`2,g) by
A21,
A23
.= F(o1,`2,g)
.= F(o1,o2,g);
hence ((
Morph-Map (F,o1,o2))
. g)
= F(o1,o2,g) by
A22;
end;
A24: F is
feasible
proof
let o1,o2 be
Object of A();
set g = the
Morphism of o1, o2;
assume
A25:
<^o1, o2^>
<>
{} ;
then ((
Morph-Map (F,o1,o2))
. g)
= F(o1,o2,g) by
A20;
then ((
Morph-Map (F,o1,o2))
. g)
in (the
Arrows of B()
. (O(o1),O(o2))) by
A2,
A25;
then ((
Morph-Map (F,o1,o2))
. g)
in (the
Arrows of B()
. ((F
. o1),O(o2))) by
A19;
hence thesis by
A19;
end;
A26:
now
let o1,o2 be
Object of A();
assume
A27:
<^o1, o2^>
<>
{} ;
let g be
Morphism of o1, o2;
A28: ((
Morph-Map (F,o1,o2))
. g)
= F(o1,o2,g) by
A20,
A27;
<^(F
. o1), (F
. o2)^>
<>
{} by
A24,
A27;
hence (F
. g)
= F(o1,o2,g) by
A27,
A28,
FUNCTOR0:def 15;
end;
A29: F is
comp-preserving
proof
let o1,o2,o3 be
Object of A() such that
A30:
<^o1, o2^>
<>
{} and
A31:
<^o2, o3^>
<>
{} ;
let f be
Morphism of o1, o2, g be
Morphism of o2, o3;
set a = (O
. o1), b = (O
. o2), c = (O
. o3);
A32: a
= O(o1) by
A6;
A33: b
= O(o2) by
A6;
A34: c
= O(o3) by
A6;
reconsider f9 = F(o1,o2,f) as
Morphism of a, b by
A2,
A30,
A32,
A33;
reconsider g9 = F(o2,o3,g) as
Morphism of b, c by
A2,
A31,
A33,
A34;
A35: a
= (F
. o1) by
A19,
A32;
A36: b
= (F
. o2) by
A19,
A33;
A37: c
= (F
. o3) by
A19,
A34;
reconsider ff = f9 as
Morphism of (F
. o1), (F
. o2) by
A19,
A32,
A36;
reconsider gg = g9 as
Morphism of (F
. o2), (F
. o3) by
A19,
A34,
A36;
take ff, gg;
A38:
<^o1, o3^>
<>
{} by
A30,
A31,
ALTCAT_1:def 2;
F(o1,o3,*)
= (gg
* ff) by
A3,
A30,
A31,
A32,
A33,
A34,
A35,
A36,
A37;
hence ff
= ((
Morph-Map (F,o1,o2))
. f) & gg
= ((
Morph-Map (F,o2,o3))
. g) & ((
Morph-Map (F,o1,o3))
. (g
* f))
= (gg
* ff) by
A20,
A30,
A31,
A38;
end;
F is
Functor of A(), B()
proof
thus F is
feasible by
A24;
hereby
let o be
Object of A();
A39: (F
. o)
= O(o) by
A19;
thus ((
Morph-Map (F,o,o))
. (
idm o))
= F(o,o,idm) by
A20
.= (
idm (F
. o)) by
A4,
A39;
end;
thus thesis by
A29;
end;
then
reconsider F as
covariant
strict
Functor of A(), B() by
A29;
take F;
thus thesis by
A19,
A26;
end;
theorem ::
YELLOW18:1
Th1: for A,B be
category, F,G be
covariant
Functor of A, B st (for a be
Object of A holds (F
. a)
= (G
. a)) & (for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= (G
. f)) holds the FunctorStr of F
= the FunctorStr of G
proof
let A,B be
category, F,G be
covariant
Functor of A, B such that
A1: for a be
Object of A holds (F
. a)
= (G
. a) and
A2: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= (G
. f);
the
ObjectMap of F is
Covariant by
FUNCTOR0:def 12;
then
consider ff be
Function of the
carrier of A, the
carrier of B such that
A3: the
ObjectMap of F
=
[:ff, ff:];
the
ObjectMap of G is
Covariant by
FUNCTOR0:def 12;
then
consider gg be
Function of the
carrier of A, the
carrier of B such that
A4: the
ObjectMap of G
=
[:gg, gg:];
now
let a,b be
Element of A;
reconsider x = a, y = b as
Object of A;
A5: (
dom ff)
= the
carrier of A by
FUNCT_2:def 1;
A6: (
dom gg)
= the
carrier of A by
FUNCT_2:def 1;
A7: (the
ObjectMap of F
. (x,x))
=
[(ff
. x), (ff
. x)] by
A3,
A5,
FUNCT_3:def 8;
A8: (the
ObjectMap of F
. (y,y))
=
[(ff
. y), (ff
. y)] by
A3,
A5,
FUNCT_3:def 8;
A9: (the
ObjectMap of G
. (x,x))
=
[(gg
. x), (gg
. x)] by
A4,
A6,
FUNCT_3:def 8;
A10: (the
ObjectMap of G
. (y,y))
=
[(gg
. y), (gg
. y)] by
A4,
A6,
FUNCT_3:def 8;
A11: (F
. x)
= (ff
. x) by
A7;
A12: (F
. y)
= (ff
. y) by
A8;
A13: (G
. x)
= (gg
. x) by
A9;
A14: (G
. y)
= (gg
. y) by
A10;
A15: (F
. x)
= (G
. x) by
A1;
A16: (F
. y)
= (G
. y) by
A1;
thus (the
ObjectMap of F
. (a,b))
=
[(ff
. a), (ff
. b)] by
A3,
A5,
FUNCT_3:def 8
.= (the
ObjectMap of G
. (a,b)) by
A4,
A6,
A11,
A12,
A13,
A14,
A15,
A16,
FUNCT_3:def 8;
end;
then
A17: the
ObjectMap of F
= the
ObjectMap of G;
now
let i be
object;
assume i
in
[:the
carrier of A, the
carrier of A:];
then
consider a,b be
object such that
A18: a
in the
carrier of A and
A19: b
in the
carrier of A and
A20: i
=
[a, b] by
ZFMISC_1:def 2;
reconsider x = a, y = b as
Object of A by
A18,
A19;
A21:
<^x, y^>
<>
{} implies
<^(F
. x), (F
. y)^>
<>
{} by
FUNCTOR0:def 18;
A22:
<^x, y^>
<>
{} implies
<^(G
. x), (G
. y)^>
<>
{} by
FUNCTOR0:def 18;
A23: (
dom (
Morph-Map (F,x,y)))
=
<^x, y^> by
A21,
FUNCT_2:def 1;
A24: (
dom (
Morph-Map (G,x,y)))
=
<^x, y^> by
A22,
FUNCT_2:def 1;
now
let z be
object;
assume
A25: z
in
<^x, y^>;
then
reconsider f = z as
Morphism of x, y;
thus ((
Morph-Map (F,x,y))
. z)
= (F
. f) by
A21,
A25,
FUNCTOR0:def 15
.= (G
. f) by
A2,
A25
.= ((
Morph-Map (G,x,y))
. z) by
A22,
A25,
FUNCTOR0:def 15;
end;
hence (the
MorphMap of F
. i)
= (the
MorphMap of G
. i) by
A20,
A23,
A24;
end;
hence thesis by
A17,
PBOOLE: 3;
end;
scheme ::
YELLOW18:sch9
ContravariantFunctorLambda { A,B() ->
category , O(
object) ->
object , F(
object,
object,
object) ->
object } :
ex F be
contravariant
strict
Functor of A(), B() st (for a be
Object of A() holds (F
. a)
= O(a)) & for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= F(a,b,f)
provided
A1: for a be
Object of A() holds O(a) is
Object of B()
and
A2: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds F(a,b,f)
in (the
Arrows of B()
. (O(b),O(a)))
and
A3: for a,b,c be
Object of A() st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds for a9,b9,c9 be
Object of B() st a9
= O(a) & b9
= O(b) & c9
= O(c) holds for f9 be
Morphism of b9, a9, g9 be
Morphism of c9, b9 st f9
= F(a,b,f) & g9
= F(b,c,g) holds F(a,c,*)
= (f9
* g9)
and
A4: for a be
Object of A(), a9 be
Object of B() st a9
= O(a) holds F(a,a,idm)
= (
idm a9);
consider O be
Function such that
A5: (
dom O)
= the
carrier of A() and
A6: for x be
object st x
in the
carrier of A() holds (O
. x)
= O(x) from
FUNCT_1:sch 3;
(
rng O)
c= the
carrier of B()
proof
let y be
object;
assume y
in (
rng O);
then
consider x be
object such that
A7: x
in (
dom O) and
A8: y
= (O
. x) by
FUNCT_1:def 3;
reconsider x as
Object of A() by
A5,
A7;
A9: y
= O(x) by
A6,
A8;
O(x) is
Object of B() by
A1;
hence thesis by
A9;
end;
then
reconsider O as
Function of the
carrier of A(), the
carrier of B() by
A5,
FUNCT_2: 2;
reconsider OM = (
~
[:O, O:]) as
bifunction of the
carrier of A(), the
carrier of B();
(
dom
[:O, O:])
=
[:the
carrier of A(), the
carrier of A():] by
A5,
FUNCT_3:def 8;
then
A10: (
dom OM)
=
[:the
carrier of A(), the
carrier of A():] by
FUNCT_4: 46;
defpred
P[
object,
object,
object] means $1
= F(`1,`2,$2);
A11: for i be
object st i
in
[:the
carrier of A(), the
carrier of A():] holds for x be
object st x
in (the
Arrows of A()
. i) holds ex y be
object st y
in ((the
Arrows of B()
* OM)
. i) &
P[y, x, i]
proof
let i be
object;
assume
A12: i
in
[:the
carrier of A(), the
carrier of A():];
then
consider a,b be
object such that
A13: a
in the
carrier of A() and
A14: b
in the
carrier of A() and
A15:
[a, b]
= i by
ZFMISC_1:def 2;
reconsider a, b as
Object of A() by
A13,
A14;
let x be
object;
assume
A16: x
in (the
Arrows of A()
. i);
then
reconsider f = x as
Morphism of a, b by
A15;
take y = F(a,b,f);
A17: y
in (the
Arrows of B()
. (O(b),O(a))) by
A2,
A15,
A16;
A18: O(a)
= (O
. a) by
A6;
((the
Arrows of B()
* OM)
. i)
= (the
Arrows of B()
. (OM
. (a,b))) by
A10,
A12,
A15,
FUNCT_1: 13
.= (the
Arrows of B()
. (
[:O, O:]
. (b,a))) by
A10,
A12,
A15,
FUNCT_4: 43
.= (the
Arrows of B()
. ((O
. b),(O
. a))) by
A5,
FUNCT_3:def 8;
hence y
in ((the
Arrows of B()
* OM)
. i) by
A6,
A17,
A18;
thus thesis by
A15;
end;
consider M be
ManySortedFunction of the
Arrows of A(), (the
Arrows of B()
* OM) such that
A19: for i be
object st i
in
[:the
carrier of A(), the
carrier of A():] holds ex f be
Function of (the
Arrows of A()
. i), ((the
Arrows of B()
* OM)
. i) st f
= (M
. i) & for x be
object st x
in (the
Arrows of A()
. i) holds
P[(f
. x), x, i] from
MSSUBFAM:sch 1(
A11);
reconsider M as
MSUnTrans of OM, the
Arrows of A(), the
Arrows of B() by
FUNCTOR0:def 4;
FunctorStr (# OM, M #) is
Contravariant
proof
take O;
thus thesis;
end;
then
reconsider F =
FunctorStr (# OM, M #) as
Contravariant
FunctorStr over A(), B();
A20:
now
let a be
Object of A();
[a, a]
in (
dom OM) by
A10,
ZFMISC_1:def 2;
hence (F
. a)
= ((
[:O, O:]
. (a,a))
`1 ) by
FUNCT_4: 43
.= (
[(O
. a), (O
. a)]
`1 ) by
A5,
FUNCT_3:def 8
.= (O
. a)
.= O(a) by
A6;
end;
A21:
now
let o1,o2 be
Object of A() such that
A22:
<^o1, o2^>
<>
{} ;
let g be
Morphism of o1, o2;
[o1, o2]
in
[:the
carrier of A(), the
carrier of A():] by
ZFMISC_1:def 2;
then
consider f be
Function of (the
Arrows of A()
.
[o1, o2]), ((the
Arrows of B()
* OM)
.
[o1, o2]) such that
A23: f
= (M
.
[o1, o2]) and
A24: for x be
object st x
in (the
Arrows of A()
.
[o1, o2]) holds (f
. x)
= F(`1,`2,x) by
A19;
(f
. g)
= F(`1,`2,g) by
A22,
A24
.= F(o1,`2,g)
.= F(o1,o2,g);
hence ((
Morph-Map (F,o1,o2))
. g)
= F(o1,o2,g) by
A23;
end;
A25: F is
feasible
proof
let o1,o2 be
Object of A();
set g = the
Morphism of o1, o2;
assume
A26:
<^o1, o2^>
<>
{} ;
then ((
Morph-Map (F,o1,o2))
. g)
= F(o1,o2,g) by
A21;
then ((
Morph-Map (F,o1,o2))
. g)
in (the
Arrows of B()
. (O(o2),O(o1))) by
A2,
A26;
then ((
Morph-Map (F,o1,o2))
. g)
in (the
Arrows of B()
. ((F
. o2),O(o1))) by
A20;
hence thesis by
A20;
end;
A27:
now
let o1,o2 be
Object of A();
assume
A28:
<^o1, o2^>
<>
{} ;
let g be
Morphism of o1, o2;
A29: ((
Morph-Map (F,o1,o2))
. g)
= F(o1,o2,g) by
A21,
A28;
<^(F
. o2), (F
. o1)^>
<>
{} by
A25,
A28;
hence (F
. g)
= F(o1,o2,g) by
A28,
A29,
FUNCTOR0:def 16;
end;
A30: F is
comp-reversing
proof
let o1,o2,o3 be
Object of A() such that
A31:
<^o1, o2^>
<>
{} and
A32:
<^o2, o3^>
<>
{} ;
let f be
Morphism of o1, o2, g be
Morphism of o2, o3;
set a = (O
. o1), b = (O
. o2), c = (O
. o3);
A33: a
= O(o1) by
A6;
A34: b
= O(o2) by
A6;
A35: c
= O(o3) by
A6;
reconsider f9 = F(o1,o2,f) as
Morphism of b, a by
A2,
A31,
A33,
A34;
reconsider g9 = F(o2,o3,g) as
Morphism of c, b by
A2,
A32,
A34,
A35;
A36: a
= (F
. o1) by
A20,
A33;
A37: b
= (F
. o2) by
A20,
A34;
A38: c
= (F
. o3) by
A20,
A35;
reconsider ff = f9 as
Morphism of (F
. o2), (F
. o1) by
A20,
A33,
A37;
reconsider gg = g9 as
Morphism of (F
. o3), (F
. o2) by
A20,
A35,
A37;
take ff, gg;
A39:
<^o1, o3^>
<>
{} by
A31,
A32,
ALTCAT_1:def 2;
F(o1,o3,*)
= (ff
* gg) by
A3,
A31,
A32,
A33,
A34,
A35,
A36,
A37,
A38;
hence ff
= ((
Morph-Map (F,o1,o2))
. f) & gg
= ((
Morph-Map (F,o2,o3))
. g) & ((
Morph-Map (F,o1,o3))
. (g
* f))
= (ff
* gg) by
A21,
A31,
A32,
A39;
end;
F is
Functor of A(), B()
proof
thus F is
feasible by
A25;
hereby
let o be
Object of A();
A40: (F
. o)
= O(o) by
A20;
thus ((
Morph-Map (F,o,o))
. (
idm o))
= F(o,o,idm) by
A21
.= (
idm (F
. o)) by
A4,
A40;
end;
thus thesis by
A30;
end;
then
reconsider F as
contravariant
strict
Functor of A(), B() by
A30;
take F;
thus thesis by
A20,
A27;
end;
theorem ::
YELLOW18:2
Th2: for A,B be
category, F,G be
contravariant
Functor of A, B st (for a be
Object of A holds (F
. a)
= (G
. a)) & (for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= (G
. f)) holds the FunctorStr of F
= the FunctorStr of G
proof
let A,B be
category, F,G be
contravariant
Functor of A, B such that
A1: for a be
Object of A holds (F
. a)
= (G
. a) and
A2: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= (G
. f);
the
ObjectMap of F is
Contravariant by
FUNCTOR0:def 13;
then
consider ff be
Function of the
carrier of A, the
carrier of B such that
A3: the
ObjectMap of F
= (
~
[:ff, ff:]);
the
ObjectMap of G is
Contravariant by
FUNCTOR0:def 13;
then
consider gg be
Function of the
carrier of A, the
carrier of B such that
A4: the
ObjectMap of G
= (
~
[:gg, gg:]);
now
let a,b be
Element of A;
reconsider x = a, y = b as
Object of A;
A5: (
dom ff)
= the
carrier of A by
FUNCT_2:def 1;
A6: (
dom gg)
= the
carrier of A by
FUNCT_2:def 1;
A7: (
dom
[:ff, ff:])
=
[:the
carrier of A, the
carrier of A:] by
FUNCT_2:def 1;
then
A8:
[b, a]
in (
dom
[:ff, ff:]) by
ZFMISC_1:def 2;
A9: (
dom
[:gg, gg:])
=
[:the
carrier of A, the
carrier of A:] by
FUNCT_2:def 1;
then
A10:
[b, a]
in (
dom
[:gg, gg:]) by
ZFMISC_1:def 2;
A11:
[a, a]
in (
dom
[:gg, gg:]) by
A9,
ZFMISC_1:def 2;
A12:
[b, b]
in (
dom
[:gg, gg:]) by
A9,
ZFMISC_1:def 2;
A13: (the
ObjectMap of F
. (x,x))
= (
[:ff, ff:]
. (x,x)) by
A3,
A7,
A11,
FUNCT_4:def 2;
A14: (the
ObjectMap of F
. (y,y))
= (
[:ff, ff:]
. (y,y)) by
A3,
A7,
A12,
FUNCT_4:def 2;
A15: (the
ObjectMap of G
. (x,x))
= (
[:gg, gg:]
. (x,x)) by
A4,
A11,
FUNCT_4:def 2;
A16: (the
ObjectMap of G
. (y,y))
= (
[:gg, gg:]
. (y,y)) by
A4,
A12,
FUNCT_4:def 2;
A17: (the
ObjectMap of F
. (x,x))
=
[(ff
. x), (ff
. x)] by
A5,
A13,
FUNCT_3:def 8;
A18: (the
ObjectMap of F
. (y,y))
=
[(ff
. y), (ff
. y)] by
A5,
A14,
FUNCT_3:def 8;
A19: (the
ObjectMap of G
. (x,x))
=
[(gg
. x), (gg
. x)] by
A6,
A15,
FUNCT_3:def 8;
A20: (the
ObjectMap of G
. (y,y))
=
[(gg
. y), (gg
. y)] by
A6,
A16,
FUNCT_3:def 8;
A21: (F
. x)
= (ff
. x) by
A17;
A22: (F
. y)
= (ff
. y) by
A18;
A23: (G
. x)
= (gg
. x) by
A19;
A24: (G
. y)
= (gg
. y) by
A20;
A25: (F
. x)
= (G
. x) by
A1;
A26: (F
. y)
= (G
. y) by
A1;
thus (the
ObjectMap of F
. (a,b))
= (
[:ff, ff:]
. (b,a)) by
A3,
A8,
FUNCT_4:def 2
.=
[(ff
. b), (ff
. a)] by
A5,
FUNCT_3:def 8
.= (
[:gg, gg:]
. (b,a)) by
A6,
A21,
A22,
A23,
A24,
A25,
A26,
FUNCT_3:def 8
.= (the
ObjectMap of G
. (a,b)) by
A4,
A10,
FUNCT_4:def 2;
end;
then
A27: the
ObjectMap of F
= the
ObjectMap of G;
now
let i be
object;
assume i
in
[:the
carrier of A, the
carrier of A:];
then
consider a,b be
object such that
A28: a
in the
carrier of A and
A29: b
in the
carrier of A and
A30: i
=
[a, b] by
ZFMISC_1:def 2;
reconsider x = a, y = b as
Object of A by
A28,
A29;
A31:
<^x, y^>
<>
{} implies
<^(F
. y), (F
. x)^>
<>
{} by
FUNCTOR0:def 19;
A32:
<^x, y^>
<>
{} implies
<^(G
. y), (G
. x)^>
<>
{} by
FUNCTOR0:def 19;
A33: (
dom (
Morph-Map (F,x,y)))
=
<^x, y^> by
A31,
FUNCT_2:def 1;
A34: (
dom (
Morph-Map (G,x,y)))
=
<^x, y^> by
A32,
FUNCT_2:def 1;
now
let z be
object;
assume
A35: z
in
<^x, y^>;
then
reconsider f = z as
Morphism of x, y;
thus ((
Morph-Map (F,x,y))
. z)
= (F
. f) by
A31,
A35,
FUNCTOR0:def 16
.= (G
. f) by
A2,
A35
.= ((
Morph-Map (G,x,y))
. z) by
A32,
A35,
FUNCTOR0:def 16;
end;
hence (the
MorphMap of F
. i)
= (the
MorphMap of G
. i) by
A30,
A33,
A34;
end;
hence thesis by
A27,
PBOOLE: 3;
end;
begin
definition
let A,B,C be non
empty
set;
let f be
Function of
[:A, B:], C;
:: original:
one-to-one
redefine
::
YELLOW18:def1
attr f is
one-to-one means for a1,a2 be
Element of A, b1,b2 be
Element of B st (f
. (a1,b1))
= (f
. (a2,b2)) holds a1
= a2 & b1
= b2;
compatibility
proof
A1: (
dom f)
=
[:A, B:] by
FUNCT_2:def 1;
thus f is
one-to-one implies for a1,a2 be
Element of A, b1,b2 be
Element of B st (f
. (a1,b1))
= (f
. (a2,b2)) holds a1
= a2 & b1
= b2
proof
assume
A2: for x,y be
object st x
in (
dom f) & y
in (
dom f) & (f
. x)
= (f
. y) holds x
= y;
let a1,a2 be
Element of A, b1,b2 be
Element of B;
A3:
[a1, b1]
in
[:A, B:] by
ZFMISC_1:def 2;
[a2, b2]
in
[:A, B:] by
ZFMISC_1:def 2;
then (f
. (a1,b1))
= (f
. (a2,b2)) implies
[a1, b1]
=
[a2, b2] by
A1,
A2,
A3;
hence thesis by
XTUPLE_0: 1;
end;
assume
A4: for a1,a2 be
Element of A, b1,b2 be
Element of B st (f
. (a1,b1))
= (f
. (a2,b2)) holds a1
= a2 & b1
= b2;
let x,y be
object;
assume x
in (
dom f);
then
consider a1,b1 be
object such that
A5: a1
in A and
A6: b1
in B and
A7: x
=
[a1, b1] by
ZFMISC_1:def 2;
assume y
in (
dom f);
then
consider a2,b2 be
object such that
A8: a2
in A and
A9: b2
in B and
A10: y
=
[a2, b2] by
ZFMISC_1:def 2;
reconsider a1, a2 as
Element of A by
A5,
A8;
reconsider b1, b2 as
Element of B by
A6,
A9;
assume (f
. x)
= (f
. y);
then
A11: (f
. (a1,b1))
= (f
. (a2,b2)) by
A7,
A10;
then a1
= a2 by
A4;
hence thesis by
A4,
A7,
A10,
A11;
end;
end
scheme ::
YELLOW18:sch10
CoBijectiveSch { A,B() ->
category , F() ->
covariant
Functor of A(), B() , O(
object) ->
object , F(
object,
object,
object) ->
object } :
F() is
bijective
provided
A1: for a be
Object of A() holds (F()
. a)
= O(a)
and
A2: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F()
. f)
= F(a,b,f)
and
A3: for a,b be
Object of A() st O(a)
= O(b) holds a
= b
and
A4: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f,g be
Morphism of a, b st F(a,b,f)
= F(a,b,g) holds f
= g
and
A5: for a,b be
Object of B() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds ex c,d be
Object of A(), g be
Morphism of c, d st a
= O(c) & b
= O(d) &
<^c, d^>
<>
{} & f
= F(c,d,g);
set F = F();
thus the
ObjectMap of F is
one-to-one
proof
let x1,x2,y1,y2 be
Element of A();
reconsider a1 = x1, a2 = x2, b1 = y1, b2 = y2 as
Object of A();
assume (the
ObjectMap of F
. (x1,y1))
= (the
ObjectMap of F
. (x2,y2));
then
A6:
[(F
. a1), (F
. b1)]
= (the
ObjectMap of F
. (x2,y2)) by
FUNCTOR0: 22
.=
[(F
. a2), (F
. b2)] by
FUNCTOR0: 22;
then
A7: (F
. a1)
= (F
. a2) by
XTUPLE_0: 1;
A8: (F
. b1)
= (F
. b2) by
A6,
XTUPLE_0: 1;
A9: O(a1)
= (F
. a2) by
A1,
A7;
A10: O(b1)
= (F
. b2) by
A1,
A8;
A11: O(a1)
= O(a2) by
A1,
A9;
O(b1)
= O(b2) by
A1,
A10;
hence thesis by
A3,
A11;
end;
now
let i be
set;
assume i
in
[:the
carrier of A(), the
carrier of A():];
then
consider a,b be
object such that
A12: a
in the
carrier of A() and
A13: b
in the
carrier of A() and
A14: i
=
[a, b] by
ZFMISC_1:def 2;
reconsider a, b as
Object of A() by
A12,
A13;
A15:
<^a, b^>
<>
{} implies
<^(F
. a), (F
. b)^>
<>
{} by
FUNCTOR0:def 18;
(
Morph-Map (F,a,b)) is
one-to-one
proof
let x,y be
object;
assume that
A16: x
in (
dom (
Morph-Map (F,a,b))) and
A17: y
in (
dom (
Morph-Map (F,a,b)));
reconsider f = x, g = y as
Morphism of a, b by
A16,
A17;
A18: (F
. f)
= ((
Morph-Map (F,a,b))
. x) by
A15,
A16,
FUNCTOR0:def 15;
A19: (F
. g)
= ((
Morph-Map (F,a,b))
. y) by
A15,
A16,
FUNCTOR0:def 15;
A20: F(a,b,f)
= ((
Morph-Map (F,a,b))
. x) by
A2,
A16,
A18;
F(a,b,g)
= ((
Morph-Map (F,a,b))
. y) by
A2,
A16,
A19;
hence thesis by
A4,
A16,
A20;
end;
hence (the
MorphMap of F
. i) is
one-to-one by
A14;
end;
hence the
MorphMap of F is
"1-1" by
MSUALG_3: 1;
reconsider G = the
MorphMap of F as
ManySortedFunction of the
Arrows of A(), (the
Arrows of B()
* the
ObjectMap of F) by
FUNCTOR0:def 4;
thus F is
full
proof
take G;
thus G
= the
MorphMap of F;
let i be
set;
assume i
in
[:the
carrier of A(), the
carrier of A():];
then
reconsider ab = i as
Element of
[:the
carrier of A(), the
carrier of A():];
(G
. ab) is
Function of (the
Arrows of A()
. ab), ((the
Arrows of B()
* the
ObjectMap of F)
. ab);
hence (
rng (G
. i))
c= ((the
Arrows of B()
* the
ObjectMap of F)
. i) by
RELAT_1:def 19;
consider a,b be
object such that
A21: a
in the
carrier of A() and
A22: b
in the
carrier of A() and
A23: ab
=
[a, b] by
ZFMISC_1:def 2;
reconsider a, b as
Object of A() by
A21,
A22;
A24: (the
ObjectMap of F
. ab)
= (the
ObjectMap of F
. (a,b)) by
A23
.=
[(F
. a), (F
. b)] by
FUNCTOR0: 22;
then
A25: ((the
Arrows of B()
* the
ObjectMap of F)
. ab)
=
<^(F
. a), (F
. b)^> by
FUNCT_2: 15;
let x be
object;
assume
A26: x
in ((the
Arrows of B()
* the
ObjectMap of F)
. i);
then
reconsider f = x as
Morphism of (F
. a), (F
. b) by
A24,
FUNCT_2: 15;
consider c,d be
Object of A(), g be
Morphism of c, d such that
A27: (F
. a)
= O(c) and
A28: (F
. b)
= O(d) and
A29:
<^c, d^>
<>
{} and
A30: f
= F(c,d,g) by
A5,
A25,
A26;
A31: O(a)
= O(c) by
A1,
A27;
A32: O(b)
= O(d) by
A1,
A28;
A33: a
= c by
A3,
A31;
A34: b
= d by
A3,
A32;
A35: f
= (F
. g) by
A2,
A29,
A30
.= ((
Morph-Map (F,c,d))
. g) by
A25,
A26,
A29,
A33,
A34,
FUNCTOR0:def 15;
(
dom (
Morph-Map (F,a,b)))
=
<^a, b^> by
A25,
A26,
FUNCT_2:def 1;
hence thesis by
A23,
A29,
A33,
A34,
A35,
FUNCT_1:def 3;
end;
thus (
rng the
ObjectMap of F)
c=
[:the
carrier of B(), the
carrier of B():];
let x be
object;
assume x
in
[:the
carrier of B(), the
carrier of B():];
then
consider a,b be
object such that
A36: a
in the
carrier of B() and
A37: b
in the
carrier of B() and
A38: x
=
[a, b] by
ZFMISC_1:def 2;
reconsider a, b as
Object of B() by
A36,
A37;
consider c,c9 be
Object of A(), g be
Morphism of c, c9 such that
A39: a
= O(c) and a
= O(c9) and
<^c, c9^>
<>
{} and (
idm a)
= F(c,c9,g) by
A5;
consider d,d9 be
Object of A(), h be
Morphism of d, d9 such that
A40: b
= O(d) and b
= O(d9) and
<^d, d9^>
<>
{} and (
idm b)
= F(d,d9,h) by
A5;
[c, d]
in
[:the
carrier of A(), the
carrier of A():] by
ZFMISC_1:def 2;
then
A41:
[c, d]
in (
dom the
ObjectMap of F) by
FUNCT_2:def 1;
(the
ObjectMap of F
.
[c, d])
= (the
ObjectMap of F
. (c,d))
.=
[(F
. c), (F
. d)] by
FUNCTOR0: 22
.=
[a, (F
. d)] by
A1,
A39
.= x by
A1,
A38,
A40;
hence thesis by
A41,
FUNCT_1:def 3;
end;
scheme ::
YELLOW18:sch11
CatIsomorphism { A,B() ->
category , O(
object) ->
object , F(
object,
object,
object) ->
object } :
(A(),B())
are_isomorphic
provided
A1: ex F be
covariant
Functor of A(), B() st (for a be
Object of A() holds (F
. a)
= O(a)) & for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= F(a,b,f)
and
A2: for a,b be
Object of A() st O(a)
= O(b) holds a
= b
and
A3: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f,g be
Morphism of a, b st F(a,b,f)
= F(a,b,g) holds f
= g
and
A4: for a,b be
Object of B() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds ex c,d be
Object of A(), g be
Morphism of c, d st a
= O(c) & b
= O(d) &
<^c, d^>
<>
{} & f
= F(c,d,g);
A5: for a,b be
Object of A() st O(a)
= O(b) holds a
= b by
A2;
A6: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f,g be
Morphism of a, b st F(a,b,f)
= F(a,b,g) holds f
= g by
A3;
A7: for a,b be
Object of B() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds ex c,d be
Object of A(), g be
Morphism of c, d st a
= O(c) & b
= O(d) &
<^c, d^>
<>
{} & f
= F(c,d,g) by
A4;
consider F be
covariant
Functor of A(), B() such that
A8: for a be
Object of A() holds (F
. a)
= O(a) and
A9: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= F(a,b,f) by
A1;
take F;
thus F is
bijective from
CoBijectiveSch(
A8,
A9,
A5,
A6,
A7);
thus thesis;
end;
scheme ::
YELLOW18:sch12
ContraBijectiveSch { A,B() ->
category , F() ->
contravariant
Functor of A(), B() , O(
object) ->
object , F(
object,
object,
object) ->
object } :
F() is
bijective
provided
A1: for a be
Object of A() holds (F()
. a)
= O(a)
and
A2: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F()
. f)
= F(a,b,f)
and
A3: for a,b be
Object of A() st O(a)
= O(b) holds a
= b
and
A4: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f,g be
Morphism of a, b st F(a,b,f)
= F(a,b,g) holds f
= g
and
A5: for a,b be
Object of B() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds ex c,d be
Object of A(), g be
Morphism of c, d st b
= O(c) & a
= O(d) &
<^c, d^>
<>
{} & f
= F(c,d,g);
set F = F();
thus the
ObjectMap of F is
one-to-one
proof
let x1,x2,y1,y2 be
Element of A();
reconsider a1 = x1, a2 = x2, b1 = y1, b2 = y2 as
Object of A();
assume (the
ObjectMap of F
. (x1,y1))
= (the
ObjectMap of F
. (x2,y2));
then
A6:
[(F
. b1), (F
. a1)]
= (the
ObjectMap of F
. (x2,y2)) by
FUNCTOR0: 23
.=
[(F
. b2), (F
. a2)] by
FUNCTOR0: 23;
then
A7: (F
. a1)
= (F
. a2) by
XTUPLE_0: 1;
A8: (F
. b1)
= (F
. b2) by
A6,
XTUPLE_0: 1;
A9: O(a1)
= (F
. a2) by
A1,
A7;
A10: O(b1)
= (F
. b2) by
A1,
A8;
A11: O(a1)
= O(a2) by
A1,
A9;
O(b1)
= O(b2) by
A1,
A10;
hence thesis by
A3,
A11;
end;
now
let i be
set;
assume i
in
[:the
carrier of A(), the
carrier of A():];
then
consider a,b be
object such that
A12: a
in the
carrier of A() and
A13: b
in the
carrier of A() and
A14: i
=
[a, b] by
ZFMISC_1:def 2;
reconsider a, b as
Object of A() by
A12,
A13;
A15:
<^a, b^>
<>
{} implies
<^(F
. b), (F
. a)^>
<>
{} by
FUNCTOR0:def 19;
(
Morph-Map (F,a,b)) is
one-to-one
proof
let x,y be
object;
assume that
A16: x
in (
dom (
Morph-Map (F,a,b))) and
A17: y
in (
dom (
Morph-Map (F,a,b)));
reconsider f = x, g = y as
Morphism of a, b by
A16,
A17;
A18: (F
. f)
= ((
Morph-Map (F,a,b))
. x) by
A15,
A16,
FUNCTOR0:def 16;
A19: (F
. g)
= ((
Morph-Map (F,a,b))
. y) by
A15,
A16,
FUNCTOR0:def 16;
A20: F(a,b,f)
= ((
Morph-Map (F,a,b))
. x) by
A2,
A16,
A18;
F(a,b,g)
= ((
Morph-Map (F,a,b))
. y) by
A2,
A16,
A19;
hence thesis by
A4,
A16,
A20;
end;
hence (the
MorphMap of F
. i) is
one-to-one by
A14;
end;
hence the
MorphMap of F is
"1-1" by
MSUALG_3: 1;
reconsider G = the
MorphMap of F as
ManySortedFunction of the
Arrows of A(), (the
Arrows of B()
* the
ObjectMap of F) by
FUNCTOR0:def 4;
thus F is
full
proof
take G;
thus G
= the
MorphMap of F;
let i be
set;
assume i
in
[:the
carrier of A(), the
carrier of A():];
then
reconsider ab = i as
Element of
[:the
carrier of A(), the
carrier of A():];
(G
. ab) is
Function of (the
Arrows of A()
. ab), ((the
Arrows of B()
* the
ObjectMap of F)
. ab);
hence (
rng (G
. i))
c= ((the
Arrows of B()
* the
ObjectMap of F)
. i) by
RELAT_1:def 19;
consider a,b be
object such that
A21: a
in the
carrier of A() and
A22: b
in the
carrier of A() and
A23: ab
=
[a, b] by
ZFMISC_1:def 2;
reconsider a, b as
Object of A() by
A21,
A22;
A24: (the
ObjectMap of F
. ab)
= (the
ObjectMap of F
. (a,b)) by
A23
.=
[(F
. b), (F
. a)] by
FUNCTOR0: 23;
then
A25: ((the
Arrows of B()
* the
ObjectMap of F)
. ab)
=
<^(F
. b), (F
. a)^> by
FUNCT_2: 15;
let x be
object;
assume
A26: x
in ((the
Arrows of B()
* the
ObjectMap of F)
. i);
then
reconsider f = x as
Morphism of (F
. b), (F
. a) by
A24,
FUNCT_2: 15;
consider c,d be
Object of A(), g be
Morphism of c, d such that
A27: (F
. a)
= O(c) and
A28: (F
. b)
= O(d) and
A29:
<^c, d^>
<>
{} and
A30: f
= F(c,d,g) by
A5,
A25,
A26;
A31: O(a)
= O(c) by
A1,
A27;
A32: O(b)
= O(d) by
A1,
A28;
A33: a
= c by
A3,
A31;
A34: b
= d by
A3,
A32;
A35: f
= (F
. g) by
A2,
A29,
A30
.= ((
Morph-Map (F,c,d))
. g) by
A25,
A26,
A29,
A33,
A34,
FUNCTOR0:def 16;
(
dom (
Morph-Map (F,a,b)))
=
<^a, b^> by
A25,
A26,
FUNCT_2:def 1;
hence thesis by
A23,
A29,
A33,
A34,
A35,
FUNCT_1:def 3;
end;
thus (
rng the
ObjectMap of F)
c=
[:the
carrier of B(), the
carrier of B():];
let x be
object;
assume x
in
[:the
carrier of B(), the
carrier of B():];
then
consider a,b be
object such that
A36: a
in the
carrier of B() and
A37: b
in the
carrier of B() and
A38: x
=
[a, b] by
ZFMISC_1:def 2;
reconsider a, b as
Object of B() by
A36,
A37;
consider c,c9 be
Object of A(), g be
Morphism of c, c9 such that
A39: a
= O(c) and a
= O(c9) and
<^c, c9^>
<>
{} and (
idm a)
= F(c,c9,g) by
A5;
consider d,d9 be
Object of A(), h be
Morphism of d, d9 such that
A40: b
= O(d) and b
= O(d9) and
<^d, d9^>
<>
{} and (
idm b)
= F(d,d9,h) by
A5;
[d, c]
in
[:the
carrier of A(), the
carrier of A():] by
ZFMISC_1:def 2;
then
A41:
[d, c]
in (
dom the
ObjectMap of F) by
FUNCT_2:def 1;
(the
ObjectMap of F
.
[d, c])
= (the
ObjectMap of F
. (d,c))
.=
[(F
. c), (F
. d)] by
FUNCTOR0: 23
.=
[a, (F
. d)] by
A1,
A39
.= x by
A1,
A38,
A40;
hence thesis by
A41,
FUNCT_1:def 3;
end;
scheme ::
YELLOW18:sch13
CatAntiIsomorphism { A,B() ->
category , O(
object) ->
object , F(
object,
object,
object) ->
object } :
(A(),B())
are_anti-isomorphic
provided
A1: ex F be
contravariant
Functor of A(), B() st (for a be
Object of A() holds (F
. a)
= O(a)) & for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= F(a,b,f)
and
A2: for a,b be
Object of A() st O(a)
= O(b) holds a
= b
and
A3: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f,g be
Morphism of a, b st F(a,b,f)
= F(a,b,g) holds f
= g
and
A4: for a,b be
Object of B() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds ex c,d be
Object of A(), g be
Morphism of c, d st b
= O(c) & a
= O(d) &
<^c, d^>
<>
{} & f
= F(c,d,g);
consider F be
contravariant
Functor of A(), B() such that
A5: for a be
Object of A() holds (F
. a)
= O(a) and
A6: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= F(a,b,f) by
A1;
A7: for a,b be
Object of A() st O(a)
= O(b) holds a
= b by
A2;
A8: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f,g be
Morphism of a, b st F(a,b,f)
= F(a,b,g) holds f
= g by
A3;
A9: for a,b be
Object of B() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds ex c,d be
Object of A(), g be
Morphism of c, d st b
= O(c) & a
= O(d) &
<^c, d^>
<>
{} & f
= F(c,d,g) by
A4;
take F;
thus F is
bijective from
ContraBijectiveSch(
A5,
A6,
A7,
A8,
A9);
thus thesis;
end;
definition
let A,B be
category;
::
YELLOW18:def2
pred A,B
are_equivalent means ex F be
covariant
Functor of A, B, G be
covariant
Functor of B, A st ((G
* F),(
id A))
are_naturally_equivalent & ((F
* G),(
id B))
are_naturally_equivalent ;
reflexivity
proof
let A be
category;
take (
id A), (
id A);
thus thesis by
FUNCTOR3: 4;
end;
symmetry ;
end
theorem ::
YELLOW18:3
Th3: for A,B,C be non
empty
reflexive
AltGraph holds for F1,F2 be
feasible
FunctorStr over A, B holds for G1,G2 be
FunctorStr over B, C st the FunctorStr of F1
= the FunctorStr of F2 & the FunctorStr of G1
= the FunctorStr of G2 holds (G1
* F1)
= (G2
* F2)
proof
let A,B,C be non
empty
reflexive
AltGraph;
let F1,F2 be
feasible
FunctorStr over A, B;
let G1,G2 be
FunctorStr over B, C such that
A1: the FunctorStr of F1
= the FunctorStr of F2 and
A2: the FunctorStr of G1
= the FunctorStr of G2;
A3: the
ObjectMap of (G1
* F1)
= (the
ObjectMap of G1
* the
ObjectMap of F1) by
FUNCTOR0:def 36;
the
MorphMap of (G1
* F1)
= ((the
MorphMap of G1
* the
ObjectMap of F1)
** the
MorphMap of F1) by
FUNCTOR0:def 36;
hence thesis by
A1,
A2,
A3,
FUNCTOR0:def 36;
end;
theorem ::
YELLOW18:4
Th4: for A,B,C be
category st (A,B)
are_equivalent & (B,C)
are_equivalent holds (A,C)
are_equivalent
proof
let A,B,C be
category;
given F1 be
covariant
Functor of A, B, G1 be
covariant
Functor of B, A such that
A1: ((G1
* F1),(
id A))
are_naturally_equivalent and
A2: ((F1
* G1),(
id B))
are_naturally_equivalent ;
given F2 be
covariant
Functor of B, C, G2 be
covariant
Functor of C, B such that
A3: ((G2
* F2),(
id B))
are_naturally_equivalent and
A4: ((F2
* G2),(
id C))
are_naturally_equivalent ;
take F = (F2
* F1), G = (G1
* G2);
the FunctorStr of F1
= the FunctorStr of F1;
then
A5: ( the FunctorStr of G1
* F1)
= (G1
* F1) by
Th3;
the FunctorStr of G2
= the FunctorStr of G2;
then
A6: ( the FunctorStr of F2
* G2)
= (F2
* G2) by
Th3;
A7: (G1
* (
id B))
= the FunctorStr of G1 by
FUNCTOR3: 5;
A8: (F2
* (
id B))
= the FunctorStr of F2 by
FUNCTOR3: 5;
A9: (G
* F2)
= (G1
* (G2
* F2)) by
FUNCTOR0: 32;
A10: (F
* G1)
= (F2
* (F1
* G1)) by
FUNCTOR0: 32;
A11: ((G
* F2)
* F1)
= (G
* F) by
FUNCTOR0: 32;
A12: ((F
* G1)
* G2)
= (F
* G) by
FUNCTOR0: 32;
A13: ((G
* F2),(G1
* (
id B)))
are_naturally_equivalent by
A3,
A9,
FUNCTOR3: 35;
A14: ((F
* G1),(F2
* (
id B)))
are_naturally_equivalent by
A2,
A10,
FUNCTOR3: 35;
A15: ((G
* F),(G1
* F1))
are_naturally_equivalent by
A5,
A7,
A11,
A13,
FUNCTOR3: 36;
((F
* G),(F2
* G2))
are_naturally_equivalent by
A6,
A8,
A12,
A14,
FUNCTOR3: 36;
hence thesis by
A1,
A4,
A15,
FUNCTOR3: 33;
end;
theorem ::
YELLOW18:5
Th5: for A,B be
category st (A,B)
are_isomorphic holds (A,B)
are_equivalent
proof
let A,B be
category;
assume (A,B)
are_isomorphic ;
then
consider F be
Functor of A, B such that
A1: F is
bijective
covariant;
reconsider F as
covariant
Functor of A, B by
A1;
consider G be
Functor of B, A such that
A2: G
= (F
" ) and
A3: G is
bijective
covariant by
A1,
FUNCTOR0: 48;
reconsider G as
covariant
Functor of B, A by
A3;
take F, G;
thus thesis by
A1,
A2,
FUNCTOR1: 18,
FUNCTOR1: 19;
end;
scheme ::
YELLOW18:sch14
NatTransLambda { A,B() ->
category , F,G() ->
covariant
Functor of A(), B() , T(
object) ->
object } :
ex t be
natural_transformation of F(), G() st F()
is_naturally_transformable_to G() & for a be
Object of A() holds (t
! a)
= T(a)
provided
A1: for a be
Object of A() holds T(a)
in
<^(F()
. a), (G()
. a)^>
and
A2: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds for g1 be
Morphism of (F()
. a), (G()
. a) st g1
= T(a) holds for g2 be
Morphism of (F()
. b), (G()
. b) st g2
= T(b) holds (g2
* (F()
. f))
= ((G()
. f)
* g1);
consider t be
ManySortedSet of the
carrier of A() such that
A3: for a be
Element of A() holds (t
. a)
= T(a) from
PBOOLE:sch 5;
A4: F()
is_transformable_to G() by
A1;
now
let a be
Object of A();
(t
. a)
= T(a) by
A3;
hence (t
. a) is
Morphism of (F()
. a), (G()
. a) by
A1;
end;
then
reconsider t as
transformation of F(), G() by
A4,
FUNCTOR2:def 2;
A5:
now
let a be
Object of A();
(t
. a)
= T(a) by
A3;
hence (t
! a)
= T(a) by
A4,
FUNCTOR2:def 4;
end;
A6: F()
is_naturally_transformable_to G()
proof
thus F()
is_transformable_to G() by
A4;
take t;
let a,b be
Object of A();
A7: (t
! a)
= T(a) by
A5;
(t
! b)
= T(b) by
A5;
hence thesis by
A2,
A7;
end;
now
let a,b be
Object of A();
A8: (t
! a)
= T(a) by
A5;
(t
! b)
= T(b) by
A5;
hence
<^a, b^>
<>
{} implies for f be
Morphism of a, b holds ((t
! b)
* (F()
. f))
= ((G()
. f)
* (t
! a)) by
A2,
A8;
end;
then t is
natural_transformation of F(), G() by
A6,
FUNCTOR2:def 7;
hence thesis by
A5,
A6;
end;
scheme ::
YELLOW18:sch15
NatEquivalenceLambda { A,B() ->
category , F,G() ->
covariant
Functor of A(), B() , T(
object) ->
object } :
ex t be
natural_equivalence of F(), G() st (F(),G())
are_naturally_equivalent & for a be
Object of A() holds (t
! a)
= T(a)
provided
A1: for a be
Object of A() holds T(a)
in
<^(F()
. a), (G()
. a)^> &
<^(G()
. a), (F()
. a)^>
<>
{} & for f be
Morphism of (F()
. a), (G()
. a) st f
= T(a) holds f is
iso
and
A2: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds for g1 be
Morphism of (F()
. a), (G()
. a) st g1
= T(a) holds for g2 be
Morphism of (F()
. b), (G()
. b) st g2
= T(b) holds (g2
* (F()
. f))
= ((G()
. f)
* g1);
A3: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds for g1 be
Morphism of (F()
. a), (G()
. a) st g1
= T(a) holds for g2 be
Morphism of (F()
. b), (G()
. b) st g2
= T(b) holds (g2
* (F()
. f))
= ((G()
. f)
* g1) by
A2;
A4: for a be
Object of A() holds T(a)
in
<^(F()
. a), (G()
. a)^> by
A1;
consider t be
natural_transformation of F(), G() such that
A5: F()
is_naturally_transformable_to G() and
A6: for a be
Object of A() holds (t
! a)
= T(a) from
NatTransLambda(
A4,
A3);
A7: G()
is_transformable_to F() by
A1;
A8: (F(),G())
are_naturally_equivalent
proof
thus F()
is_naturally_transformable_to G() by
A5;
thus G()
is_transformable_to F() by
A7;
take t;
let a be
Object of A();
(t
! a)
= T(a) by
A6;
hence thesis by
A1;
end;
now
let a be
Object of A();
(t
! a)
= T(a) by
A6;
hence (t
! a) is
iso by
A1;
end;
then t is
natural_equivalence of F(), G() by
A8,
FUNCTOR3:def 5;
hence thesis by
A6,
A8;
end;
begin
definition
let C1,C2 be non
empty
AltCatStr;
::
YELLOW18:def3
pred C1,C2
are_opposite means the
carrier of C2
= the
carrier of C1 & the
Arrows of C2
= (
~ the
Arrows of C1) & for a,b,c be
Object of C1 holds for a9,b9,c9 be
Object of C2 st a9
= a & b9
= b & c9
= c holds (the
Comp of C2
. (a9,b9,c9))
= (
~ (the
Comp of C1
. (c,b,a)));
symmetry
proof
let C1,C2 be non
empty
AltCatStr;
assume that
A1: the
carrier of C2
= the
carrier of C1 and
A2: the
Arrows of C2
= (
~ the
Arrows of C1) and
A3: for a,b,c be
Object of C1 holds for a9,b9,c9 be
Object of C2 st a9
= a & b9
= b & c9
= c holds (the
Comp of C2
. (a9,b9,c9))
= (
~ (the
Comp of C1
. (c,b,a)));
thus the
carrier of C1
= the
carrier of C2 by
A1;
(
dom the
Arrows of C1)
=
[:the
carrier of C1, the
carrier of C1:] by
PARTFUN1:def 2;
hence the
Arrows of C1
= (
~ the
Arrows of C2) by
A2,
FUNCT_4: 52;
let a,b,c be
Object of C2;
let a9,b9,c9 be
Object of C1;
assume that
A4: a9
= a and
A5: b9
= b and
A6: c9
= c;
A7: (the
Comp of C2
. (c,b,a))
= (
~ (the
Comp of C1
. (a9,b9,c9))) by
A3,
A4,
A5,
A6;
(
dom (the
Comp of C1
. (a9,b9,c9)))
c=
[:(the
Arrows of C1
. (b9,c9)), (the
Arrows of C1
. (a9,b9)):];
hence thesis by
A7,
FUNCT_4: 52;
end;
end
theorem ::
YELLOW18:6
for A,B be non
empty
AltCatStr st (A,B)
are_opposite holds for a be
Object of A holds a is
Object of B;
theorem ::
YELLOW18:7
Th7: for A,B be non
empty
AltCatStr st (A,B)
are_opposite holds for a,b be
Object of A, a9,b9 be
Object of B st a9
= a & b9
= b holds
<^a, b^>
=
<^b9, a9^> by
ALTCAT_2: 6;
theorem ::
YELLOW18:8
for A,B be non
empty
AltCatStr st (A,B)
are_opposite holds for a,b be
Object of A, a9,b9 be
Object of B st a9
= a & b9
= b holds for f be
Morphism of a, b holds f is
Morphism of b9, a9 by
Th7;
theorem ::
YELLOW18:9
Th9: for C1,C2 be non
empty
transitive
AltCatStr holds (C1,C2)
are_opposite iff the
carrier of C2
= the
carrier of C1 & for a,b,c be
Object of C1 holds for a9,b9,c9 be
Object of C2 st a9
= a & b9
= b & c9
= c holds
<^a, b^>
=
<^b9, a9^> & (
<^a, b^>
<>
{} &
<^b, c^>
<>
{} implies for f be
Morphism of a, b, g be
Morphism of b, c holds for f9 be
Morphism of b9, a9, g9 be
Morphism of c9, b9 st f9
= f & g9
= g holds (f9
* g9)
= (g
* f))
proof
let C1,C2 be non
empty
transitive
AltCatStr;
A1: (
dom the
Arrows of C1)
=
[:the
carrier of C1, the
carrier of C1:] by
PARTFUN1:def 2;
A2: (
dom the
Arrows of C2)
=
[:the
carrier of C2, the
carrier of C2:] by
PARTFUN1:def 2;
hereby
assume
A3: (C1,C2)
are_opposite ;
hence the
carrier of C2
= the
carrier of C1;
let a,b,c be
Object of C1;
let a9,b9,c9 be
Object of C2 such that
A4: a9
= a and
A5: b9
= b and
A6: c9
= c;
A7:
[a, b]
in (
dom the
Arrows of C1) by
A1,
ZFMISC_1:def 2;
A8:
[b, c]
in (
dom the
Arrows of C1) by
A1,
ZFMISC_1:def 2;
thus
A9:
<^a, b^>
= ((
~ the
Arrows of C1)
. (b,a)) by
A7,
FUNCT_4:def 2
.=
<^b9, a9^> by
A3,
A4,
A5;
A10:
<^b, c^>
= ((
~ the
Arrows of C1)
. (c,b)) by
A8,
FUNCT_4:def 2
.=
<^c9, b9^> by
A3,
A5,
A6;
A11: (the
Comp of C2
. (c9,b9,a9))
= (
~ (the
Comp of C1
. (a,b,c))) by
A3,
A4,
A5,
A6;
assume that
A12:
<^a, b^>
<>
{} and
A13:
<^b, c^>
<>
{} ;
let f be
Morphism of a, b, g be
Morphism of b, c;
<^a, c^>
<>
{} by
A12,
A13,
ALTCAT_1:def 2;
then (
dom (the
Comp of C1
. (a,b,c)))
=
[:(the
Arrows of C1
. (b,c)), (the
Arrows of C1
. (a,b)):] by
FUNCT_2:def 1;
then
A14:
[g, f]
in (
dom (the
Comp of C1
. (a,b,c))) by
A12,
A13,
ZFMISC_1:def 2;
let f9 be
Morphism of b9, a9, g9 be
Morphism of c9, b9;
assume that
A15: f9
= f and
A16: g9
= g;
thus (f9
* g9)
= ((
~ (the
Comp of C1
. (a,b,c)))
. (f,g)) by
A9,
A10,
A11,
A12,
A13,
A15,
A16,
ALTCAT_1:def 8
.= ((the
Comp of C1
. (a,b,c))
. (g,f)) by
A14,
FUNCT_4:def 2
.= (g
* f) by
A12,
A13,
ALTCAT_1:def 8;
end;
assume that
A17: the
carrier of C2
= the
carrier of C1 and
A18: for a,b,c be
Object of C1 holds for a9,b9,c9 be
Object of C2 st a9
= a & b9
= b & c9
= c holds
<^a, b^>
=
<^b9, a9^> & (
<^a, b^>
<>
{} &
<^b, c^>
<>
{} implies for f be
Morphism of a, b, g be
Morphism of b, c holds for f9 be
Morphism of b9, a9, g9 be
Morphism of c9, b9 st f9
= f & g9
= g holds (f9
* g9)
= (g
* f));
thus the
carrier of C2
= the
carrier of C1 by
A17;
A19:
now
let x be
object;
hereby
assume x
in (
dom the
Arrows of C2);
then
consider y,z be
object such that
A20: y
in the
carrier of C1 and
A21: z
in the
carrier of C1 and
A22:
[y, z]
= x by
A17,
ZFMISC_1:def 2;
take z, y;
thus x
=
[y, z] &
[z, y]
in (
dom the
Arrows of C1) by
A1,
A20,
A21,
A22,
ZFMISC_1:def 2;
end;
given z,y be
object such that
A23: x
=
[y, z] and
A24:
[z, y]
in (
dom the
Arrows of C1);
A25: z
in the
carrier of C1 by
A24,
ZFMISC_1: 87;
y
in the
carrier of C1 by
A24,
ZFMISC_1: 87;
hence x
in (
dom the
Arrows of C2) by
A2,
A17,
A23,
A25,
ZFMISC_1:def 2;
end;
now
let y,z be
object;
assume
[y, z]
in (
dom the
Arrows of C1);
then
reconsider a = y, b = z as
Object of C1 by
ZFMISC_1: 87;
reconsider a9 = a, b9 = b as
Object of C2 by
A17;
thus (the
Arrows of C2
. (z,y))
=
<^b9, a9^>
.=
<^a, b^> by
A18
.= (the
Arrows of C1
. (y,z));
end;
hence the
Arrows of C2
= (
~ the
Arrows of C1) by
A19,
FUNCT_4:def 2;
let a,b,c be
Object of C1, a9,b9,c9 be
Object of C2 such that
A26: a9
= a and
A27: b9
= b and
A28: c9
= c;
A29:
<^a9, b9^>
=
<^b, a^> by
A18,
A26,
A27;
A30:
<^b9, c9^>
=
<^c, b^> by
A18,
A27,
A28;
A31:
<^a9, c9^>
=
<^c, a^> by
A18,
A26,
A28;
[:
<^b, a^>,
<^c, b^>:]
<>
{} implies
<^b, a^>
<>
{} &
<^c, b^>
<>
{} by
ZFMISC_1: 90;
then
[:
<^b, a^>,
<^c, b^>:]
<>
{} implies
<^c, a^>
<>
{} by
ALTCAT_1:def 2;
then
A32: (
dom (the
Comp of C1
. (c,b,a)))
=
[:(the
Arrows of C1
. (b,a)), (the
Arrows of C1
. (c,b)):] by
FUNCT_2:def 1;
[:
<^c, b^>,
<^b, a^>:]
<>
{} implies
<^b, a^>
<>
{} &
<^c, b^>
<>
{} by
ZFMISC_1: 90;
then
[:
<^c, b^>,
<^b, a^>:]
<>
{} implies
<^c, a^>
<>
{} by
ALTCAT_1:def 2;
then
A33: (
dom (the
Comp of C2
. (a9,b9,c9)))
=
[:(the
Arrows of C2
. (b9,c9)), (the
Arrows of C2
. (a9,b9)):] by
A29,
A30,
A31,
FUNCT_2:def 1;
A34:
now
let x be
object;
hereby
assume x
in (
dom (the
Comp of C2
. (a9,b9,c9)));
then
consider y,z be
object such that
A35: y
in
<^b9, c9^> and
A36: z
in
<^a9, b9^> and
A37:
[y, z]
= x by
ZFMISC_1:def 2;
take z, y;
thus x
=
[y, z] &
[z, y]
in (
dom (the
Comp of C1
. (c,b,a))) by
A29,
A30,
A32,
A35,
A36,
A37,
ZFMISC_1:def 2;
end;
given z,y be
object such that
A38: x
=
[y, z] and
A39:
[z, y]
in (
dom (the
Comp of C1
. (c,b,a)));
A40: z
in
<^b, a^> by
A39,
ZFMISC_1: 87;
y
in
<^c, b^> by
A39,
ZFMISC_1: 87;
hence x
in (
dom (the
Comp of C2
. (a9,b9,c9))) by
A29,
A30,
A33,
A38,
A40,
ZFMISC_1:def 2;
end;
now
let y,z be
object;
assume
A41:
[y, z]
in (
dom (the
Comp of C1
. (c,b,a)));
then
A42: y
in
<^b, a^> by
ZFMISC_1: 87;
A43: z
in
<^c, b^> by
A41,
ZFMISC_1: 87;
reconsider f = y as
Morphism of b, a by
A41,
ZFMISC_1: 87;
reconsider g = z as
Morphism of c, b by
A41,
ZFMISC_1: 87;
reconsider f9 = y as
Morphism of a9, b9 by
A18,
A26,
A27,
A42;
reconsider g9 = z as
Morphism of b9, c9 by
A18,
A27,
A28,
A43;
thus ((the
Comp of C2
. (a9,b9,c9))
. (z,y))
= (g9
* f9) by
A29,
A30,
A42,
A43,
ALTCAT_1:def 8
.= (f
* g) by
A18,
A26,
A27,
A28,
A42,
A43
.= ((the
Comp of C1
. (c,b,a))
. (y,z)) by
A42,
A43,
ALTCAT_1:def 8;
end;
hence thesis by
A34,
FUNCT_4:def 2;
end;
theorem ::
YELLOW18:10
Th10: for A,B be
category st (A,B)
are_opposite holds for a be
Object of A, b be
Object of B st a
= b holds (
idm a)
= (
idm b)
proof
let A,B be
category such that
A1: (A,B)
are_opposite ;
let a be
Object of A, b be
Object of B such that
A2: a
= b;
reconsider i = (
idm b) as
Morphism of a, a by
A1,
A2,
Th9;
now
let c be
Object of A;
assume
A3:
<^a, c^>
<>
{} ;
let f be
Morphism of a, c;
reconsider d = c as
Object of B by
A1;
A4:
<^a, c^>
=
<^d, b^> by
A1,
A2,
Th9;
reconsider g = f as
Morphism of d, b by
A1,
A2,
Th9;
thus (f
* i)
= ((
idm b)
* g) by
A1,
A2,
A3,
Th9
.= f by
A3,
A4,
ALTCAT_1: 20;
end;
hence thesis by
ALTCAT_1:def 17;
end;
theorem ::
YELLOW18:11
Th11: for A,B be
transitive non
empty
AltCatStr st (A,B)
are_opposite holds A is
associative implies B is
associative
proof
let A,B be
transitive non
empty
AltCatStr such that
A1: (A,B)
are_opposite and
A2: A is
associative;
deffunc
C(
set,
set,
set,
set,
set) = ((the
Comp of A
. ($3,$2,$1))
. ($4,$5));
A3:
now
let a,b,c be
Object of B such that
A4:
<^a, b^>
<>
{} and
A5:
<^b, c^>
<>
{} ;
let f be
Morphism of a, b, g be
Morphism of b, c;
reconsider a9 = a, b9 = b, c9 = c as
Object of A by
A1;
A6:
<^a, b^>
=
<^b9, a9^> by
A1,
Th7;
A7:
<^b, c^>
=
<^c9, b9^> by
A1,
Th7;
reconsider f9 = f as
Morphism of b9, a9 by
A1,
Th7;
reconsider g9 = g as
Morphism of c9, b9 by
A1,
Th7;
thus (g
* f)
= (f9
* g9) by
A1,
A4,
A5,
Th9
.=
C(a,b,c,f,g) by
A4,
A5,
A6,
A7,
ALTCAT_1:def 8;
end;
A8:
now
let a,b,c,d be
Object of B, f,g,h be
set;
reconsider a9 = a, b9 = b, c9 = c, d9 = d as
Object of A by
A1;
assume
A9: f
in
<^a, b^>;
then
A10: f
in
<^b9, a9^> by
A1,
Th9;
reconsider f9 = f as
Morphism of b9, a9 by
A1,
A9,
Th9;
assume
A11: g
in
<^b, c^>;
then
A12: g
in
<^c9, b9^> by
A1,
Th9;
reconsider g9 = g as
Morphism of c9, b9 by
A1,
A11,
Th9;
assume
A13: h
in
<^c, d^>;
then
A14: h
in
<^d9, c9^> by
A1,
Th9;
reconsider h9 = h as
Morphism of d9, c9 by
A1,
A13,
Th9;
A15:
<^c9, a9^>
<>
{} by
A10,
A12,
ALTCAT_1:def 2;
A16:
<^d9, b9^>
<>
{} by
A12,
A14,
ALTCAT_1:def 2;
thus
C(a,c,d,C,h)
=
C(a,c,d,*,h) by
A10,
A12,
ALTCAT_1:def 8
.= ((f9
* g9)
* h9) by
A14,
A15,
ALTCAT_1:def 8
.= (f9
* (g9
* h9)) by
A2,
A10,
A12,
A14
.=
C(a,b,d,f,*) by
A10,
A16,
ALTCAT_1:def 8
.=
C(a,b,d,f,C) by
A12,
A14,
ALTCAT_1:def 8;
end;
thus thesis from
CatAssocSch(
A3,
A8);
end;
theorem ::
YELLOW18:12
Th12: for A,B be
transitive non
empty
AltCatStr st (A,B)
are_opposite holds A is
with_units implies B is
with_units
proof
let A,B be
transitive non
empty
AltCatStr such that
A1: (A,B)
are_opposite ;
assume A is
with_units;
then
reconsider A as
with_units
transitive non
empty
AltCatStr;
deffunc
C(
set,
set,
set,
set,
set) = ((the
Comp of A
. ($3,$2,$1))
. ($4,$5));
A2:
now
let a,b,c be
Object of B such that
A3:
<^a, b^>
<>
{} and
A4:
<^b, c^>
<>
{} ;
let f be
Morphism of a, b, g be
Morphism of b, c;
reconsider a9 = a, b9 = b, c9 = c as
Object of A by
A1;
A5:
<^a, b^>
=
<^b9, a9^> by
A1,
Th7;
A6:
<^b, c^>
=
<^c9, b9^> by
A1,
Th7;
reconsider f9 = f as
Morphism of b9, a9 by
A1,
Th7;
reconsider g9 = g as
Morphism of c9, b9 by
A1,
Th7;
thus (g
* f)
= (f9
* g9) by
A1,
A3,
A4,
Th9
.=
C(a,b,c,f,g) by
A3,
A4,
A5,
A6,
ALTCAT_1:def 8;
end;
A7:
now
let a be
Object of B;
reconsider a9 = a as
Object of A by
A1;
reconsider f = (
idm a9) as
set;
take f;
(
idm a9)
in
<^a9, a9^>;
hence f
in
<^a, a^> by
A1,
Th7;
let b be
Object of B, g be
set;
reconsider b9 = b as
Object of A by
A1;
assume
A8: g
in
<^a, b^>;
then
A9: g
in
<^b9, a9^> by
A1,
Th7;
reconsider g9 = g as
Morphism of b9, a9 by
A1,
A8,
Th7;
thus
C(a,a,b,f,g)
= ((
idm a9)
* g9) by
A9,
ALTCAT_1:def 8
.= g by
A9,
ALTCAT_1: 20;
end;
A10:
now
let a be
Object of B;
reconsider a9 = a as
Object of A by
A1;
reconsider f = (
idm a9) as
set;
take f;
(
idm a9)
in
<^a9, a9^>;
hence f
in
<^a, a^> by
A1,
Th7;
let b be
Object of B, g be
set;
reconsider b9 = b as
Object of A by
A1;
assume
A11: g
in
<^b, a^>;
then
A12: g
in
<^a9, b9^> by
A1,
Th7;
reconsider g9 = g as
Morphism of a9, b9 by
A1,
A11,
Th7;
thus
C(b,a,a,g,f)
= (g9
* (
idm a9)) by
A12,
ALTCAT_1:def 8
.= g by
A12,
ALTCAT_1:def 17;
end;
thus thesis from
CatUnitsSch(
A2,
A7,
A10);
end;
theorem ::
YELLOW18:13
Th13: for C,C1,C2 be non
empty
AltCatStr st (C,C1)
are_opposite holds (C,C2)
are_opposite iff the AltCatStr of C1
= the AltCatStr of C2
proof
let C,C1,C2 be non
empty
AltCatStr such that
A1: the
carrier of C1
= the
carrier of C and
A2: the
Arrows of C1
= (
~ the
Arrows of C) and
A3: for a,b,c be
Object of C holds for a9,b9,c9 be
Object of C1 st a9
= a & b9
= b & c9
= c holds (the
Comp of C1
. (a9,b9,c9))
= (
~ (the
Comp of C
. (c,b,a)));
thus (C,C2)
are_opposite implies the AltCatStr of C1
= the AltCatStr of C2
proof
assume that
A4: the
carrier of C2
= the
carrier of C and
A5: the
Arrows of C2
= (
~ the
Arrows of C) and
A6: for a,b,c be
Object of C holds for a9,b9,c9 be
Object of C2 st a9
= a & b9
= b & c9
= c holds (the
Comp of C2
. (a9,b9,c9))
= (
~ (the
Comp of C
. (c,b,a)));
A7: (
dom the
Comp of C1)
=
[:the
carrier of C1, the
carrier of C1, the
carrier of C1:] by
PARTFUN1:def 2;
A8: (
dom the
Comp of C2)
=
[:the
carrier of C2, the
carrier of C2, the
carrier of C2:] by
PARTFUN1:def 2;
now
let x be
object;
assume x
in
[:the
carrier of C, the
carrier of C, the
carrier of C:];
then
consider a,b,c be
object such that
A9: a
in the
carrier of C and
A10: b
in the
carrier of C and
A11: c
in the
carrier of C and
A12: x
=
[a, b, c] by
MCART_1: 68;
reconsider a, b, c as
Object of C by
A9,
A10,
A11;
reconsider a1 = a, b1 = b, c1 = c as
Object of C1 by
A1;
reconsider a2 = a, b2 = b, c2 = c as
Object of C2 by
A4;
A13: (the
Comp of C1
. (a1,b1,c1))
= (
~ (the
Comp of C
. (c,b,a))) by
A3;
(the
Comp of C2
. (a2,b2,c2))
= (
~ (the
Comp of C
. (c,b,a))) by
A6;
hence (the
Comp of C1
. x)
= (the
Comp of C2
. (a2,b2,c2)) by
A12,
A13,
MULTOP_1:def 1
.= (the
Comp of C2
. x) by
A12,
MULTOP_1:def 1;
end;
hence thesis by
A1,
A2,
A4,
A5,
A7,
A8,
FUNCT_1: 2;
end;
assume
A14: the AltCatStr of C1
= the AltCatStr of C2;
hence the
carrier of C2
= the
carrier of C & the
Arrows of C2
= (
~ the
Arrows of C) by
A1,
A2;
let a,b,c be
Object of C, a9,b9,c9 be
Object of C2;
thus thesis by
A3,
A14;
end;
definition
let C be
transitive non
empty
AltCatStr;
::
YELLOW18:def4
func C
opp ->
strict
transitive non
empty
AltCatStr means
:
Def4: (C,it )
are_opposite ;
uniqueness by
Th13;
existence
proof
deffunc
B(
set,
set) = (the
Arrows of C
. ($2,$1));
deffunc
C(
set,
set,
set,
set,
set) = ((the
Comp of C
. ($3,$2,$1))
. ($4,$5));
A1:
now
let a,b,c be
Element of C, f,g be
set;
reconsider a9 = a, b9 = b, c9 = c as
Object of C;
assume
A2: f
in
B(a,b);
then
A3: f
in
<^b9, a9^>;
reconsider f9 = f as
Morphism of b9, a9 by
A2;
assume
A4: g
in
B(b,c);
then
A5: g
in
<^c9, b9^>;
reconsider g9 = g as
Morphism of c9, b9 by
A4;
A6:
<^c9, a9^>
<>
{} by
A3,
A5,
ALTCAT_1:def 2;
C(a,b,c,f,g)
= (f9
* g9) by
A2,
A4,
ALTCAT_1:def 8;
hence
C(a,b,c,f,g)
in
B(a,c) by
A6;
end;
ex C1 be
strict non
empty
transitive
AltCatStr st the
carrier of C1
= the
carrier of C & (for a,b be
Object of C1 holds
<^a, b^>
=
B(a,b)) & for a,b,c be
Object of C1 st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
=
C(a,b,c,f,g) from
AltCatStrLambda(
A1);
then
consider C1 be
strict
transitive non
empty
AltCatStr such that
A7: the
carrier of C1
= the
carrier of C and
A8: for a,b be
Object of C1 holds
<^a, b^>
= (the
Arrows of C
. (b,a)) and
A9: for a,b,c be
Object of C1 st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= ((the
Comp of C
. (c,b,a))
. (f,g));
take C1;
now
let a,b,c be
Object of C;
let a9,b9,c9 be
Object of C1;
assume that
A10: a9
= a and
A11: b9
= b and
A12: c9
= c;
thus
A13:
<^a, b^>
=
<^b9, a9^> by
A8,
A10,
A11;
A14:
<^b, c^>
=
<^c9, b9^> by
A8,
A11,
A12;
assume that
A15:
<^a, b^>
<>
{} and
A16:
<^b, c^>
<>
{} ;
let f be
Morphism of a, b, g be
Morphism of b, c;
let f9 be
Morphism of b9, a9, g9 be
Morphism of c9, b9;
assume that
A17: f9
= f and
A18: g9
= g;
thus (f9
* g9)
= ((the
Comp of C
. (a,b,c))
. (g,f)) by
A9,
A10,
A11,
A12,
A13,
A14,
A15,
A16,
A17,
A18
.= (g
* f) by
A15,
A16,
ALTCAT_1:def 8;
end;
hence thesis by
A7,
Th9;
end;
end
registration
let C be
associative
transitive non
empty
AltCatStr;
cluster (C
opp ) ->
associative;
coherence by
Def4,
Th11;
end
registration
let C be
with_units
transitive non
empty
AltCatStr;
cluster (C
opp ) ->
with_units;
coherence by
Def4,
Th12;
end
definition
let A,B be
category;
deffunc
O(
set) = $1;
deffunc
F(
set,
set,
set) = $3;
A2: for a be
Object of A holds
O(a) is
Object of B by
A1;
A3:
now
let a,b be
Object of A such that
A4:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
reconsider a9 = a, b9 = b as
Object of B by
A2;
<^a, b^>
=
<^b9, a9^> by
A1,
Th9
.= (the
Arrows of B
. (b,a));
hence
F(a,b,f)
in (the
Arrows of B
. (
O(b),
O(a))) by
A4;
end;
A5: for a,b,c be
Object of A st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds for a9,b9,c9 be
Object of B st a9
=
O(a) & b9
=
O(b) & c9
=
O(c) holds for f9 be
Morphism of b9, a9, g9 be
Morphism of c9, b9 st f9
=
F(a,b,f) & g9
=
F(b,c,g) holds
F(a,c,*)
= (f9
* g9) by
A1,
Th9;
A6: for a be
Object of A, a9 be
Object of B st a9
=
O(a) holds
F(a,a,idm)
= (
idm a9) by
A1,
Th10;
::
YELLOW18:def5
func
dualizing-func (A,B) ->
contravariant
strict
Functor of A, B means
:
Def5: (for a be
Object of A holds (it
. a)
= a) & for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (it
. f)
= f;
existence
proof
thus ex F be
contravariant
strict
Functor of A, B st (for a be
Object of A holds (F
. a)
=
O(a)) & for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
=
F(a,b,f) from
ContravariantFunctorLambda(
A2,
A3,
A5,
A6);
end;
uniqueness
proof
let F,G be
contravariant
strict
Functor of A, B such that
A7: for a be
Object of A holds (F
. a)
= a and
A8: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= f and
A9: for a be
Object of A holds (G
. a)
= a and
A10: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (G
. f)
= f;
A11:
now
let a be
Object of A;
thus (F
. a)
= a by
A7
.= (G
. a) by
A9;
end;
now
let a,b be
Object of A such that
A12:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
thus (F
. f)
= f by
A8,
A12
.= (G
. f) by
A10,
A12;
end;
hence thesis by
A11,
Th2;
end;
end
theorem ::
YELLOW18:14
Th14: for A,B be
category st (A,B)
are_opposite holds ((
dualizing-func (A,B))
* (
dualizing-func (B,A)))
= (
id B)
proof
let A,B be
category such that
A1: (A,B)
are_opposite ;
A2:
now
let a be
Object of B;
thus (((
dualizing-func (A,B))
* (
dualizing-func (B,A)))
. a)
= ((
dualizing-func (A,B))
. ((
dualizing-func (B,A))
. a)) by
FUNCTOR0: 33
.= ((
dualizing-func (B,A))
. a) by
A1,
Def5
.= a by
A1,
Def5
.= ((
id B)
. a) by
FUNCTOR0: 29;
end;
now
let a,b be
Object of B;
assume
A3:
<^a, b^>
<>
{} ;
then
A4:
<^((
dualizing-func (B,A))
. b), ((
dualizing-func (B,A))
. a)^>
<>
{} by
FUNCTOR0:def 19;
let f be
Morphism of a, b;
thus (((
dualizing-func (A,B))
* (
dualizing-func (B,A)))
. f)
= ((
dualizing-func (A,B))
. ((
dualizing-func (B,A))
. f)) by
A3,
FUNCTOR3: 7
.= ((
dualizing-func (B,A))
. f) by
A1,
A4,
Def5
.= f by
A1,
A3,
Def5
.= ((
id B)
. f) by
A3,
FUNCTOR0: 31;
end;
hence thesis by
A2,
Th1;
end;
theorem ::
YELLOW18:15
Th15: for A,B be
category st (A,B)
are_opposite holds (
dualizing-func (A,B)) is
bijective
proof
let A,B be
category such that
A1: (A,B)
are_opposite ;
set F = (
dualizing-func (A,B));
deffunc
O(
set) = $1;
deffunc
F(
set,
set,
set) = $3;
A2: for a be
Object of A holds (F
. a)
=
O(a) by
A1,
Def5;
A3: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
=
F(a,b,f) by
A1,
Def5;
A4: for a,b be
Object of A st
O(a)
=
O(b) holds a
= b;
A5: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f,g be
Morphism of a, b st
F(a,b,f)
=
F(a,b,g) holds f
= g;
A6:
now
let a,b be
Object of B;
reconsider a9 = a, b9 = b as
Object of A by
A1;
A7:
<^a, b^>
=
<^b9, a9^> by
A1,
Th9;
assume
A8:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
thus ex c,d be
Object of A, g be
Morphism of c, d st b
=
O(c) & a
=
O(d) &
<^c, d^>
<>
{} & f
=
F(c,d,g) by
A7,
A8;
end;
F is
bijective from
ContraBijectiveSch(
A2,
A3,
A4,
A5,
A6);
hence thesis;
end;
registration
let A be
category;
cluster (
dualizing-func (A,(A
opp ))) ->
bijective;
coherence by
Def4,
Th15;
cluster (
dualizing-func ((A
opp ),A)) ->
bijective;
coherence
proof
(A,(A
opp ))
are_opposite by
Def4;
hence thesis by
Th15;
end;
end
theorem ::
YELLOW18:16
for A,B be
category st (A,B)
are_opposite holds (A,B)
are_anti-isomorphic
proof
let A,B be
category;
assume (A,B)
are_opposite ;
then (
dualizing-func (A,B)) is
bijective by
Th15;
hence thesis;
end;
theorem ::
YELLOW18:17
Th17: for A,B,C be
category st (A,B)
are_opposite holds (A,C)
are_isomorphic iff (B,C)
are_anti-isomorphic
proof
let A,B,C be
category;
assume (A,B)
are_opposite ;
then
A1: (
dualizing-func (A,B)) is
bijective by
Th15;
hereby
assume (A,C)
are_isomorphic ;
then
consider F be
Functor of C, A such that
A2: F is
bijective
covariant by
FUNCTOR0:def 39;
reconsider F as
covariant
Functor of C, A by
A2;
((
dualizing-func (A,B))
* F) is
bijective
contravariant by
A1,
A2,
FUNCTOR1: 12;
hence (B,C)
are_anti-isomorphic by
FUNCTOR0:def 40;
end;
assume (B,C)
are_anti-isomorphic ;
then
consider F be
Functor of B, C such that
A3: F is
bijective
contravariant;
reconsider F as
contravariant
Functor of B, C by
A3;
(F
* (
dualizing-func (A,B))) is
bijective
covariant by
A1,
A3,
FUNCTOR1: 12;
hence thesis;
end;
theorem ::
YELLOW18:18
for A,B,C,D be
category st (A,B)
are_opposite & (C,D)
are_opposite holds (A,C)
are_isomorphic implies (B,D)
are_isomorphic
proof
let A,B,C,D be
category;
assume that
A1: (A,B)
are_opposite and
A2: (C,D)
are_opposite ;
(A,C)
are_isomorphic implies (B,C)
are_anti-isomorphic by
A1,
Th17;
hence thesis by
A2,
Th17;
end;
theorem ::
YELLOW18:19
for A,B,C,D be
category st (A,B)
are_opposite & (C,D)
are_opposite holds (A,C)
are_anti-isomorphic implies (B,D)
are_anti-isomorphic
proof
let A,B,C,D be
category;
assume that
A1: (A,B)
are_opposite and
A2: (C,D)
are_opposite ;
(A,C)
are_anti-isomorphic implies (B,C)
are_isomorphic by
A1,
Th17;
hence thesis by
A2,
Th17;
end;
Lm1:
now
let A,B be
category such that
A1: (A,B)
are_opposite ;
let a,b be
Object of A such that
A2:
<^a, b^>
<>
{} and
A3:
<^b, a^>
<>
{} ;
let a9,b9 be
Object of B such that
A4: a9
= a and
A5: b9
= b;
let f be
Morphism of a, b, f9 be
Morphism of b9, a9 such that
A6: f9
= f;
thus f is
retraction implies f9 is
coretraction
proof
given g be
Morphism of b, a such that
A7: g
is_right_inverse_of f;
reconsider g9 = g as
Morphism of a9, b9 by
A1,
A4,
A5,
Th7;
take g9;
(f
* g)
= (
idm b) by
A7
.= (
idm b9) by
A1,
A5,
Th10;
hence (g9
* f9)
= (
idm b9) by
A1,
A2,
A3,
A4,
A5,
A6,
Th9;
end;
thus f is
coretraction implies f9 is
retraction
proof
given g be
Morphism of b, a such that
A8: g
is_left_inverse_of f;
reconsider g9 = g as
Morphism of a9, b9 by
A1,
A4,
A5,
Th7;
take g9;
(g
* f)
= (
idm a) by
A8
.= (
idm a9) by
A1,
A4,
Th10;
hence (f9
* g9)
= (
idm a9) by
A1,
A2,
A3,
A4,
A5,
A6,
Th9;
end;
end;
theorem ::
YELLOW18:20
for A,B be
category st (A,B)
are_opposite holds for a,b be
Object of A st
<^a, b^>
<>
{} &
<^b, a^>
<>
{} holds for a9,b9 be
Object of B st a9
= a & b9
= b holds for f be
Morphism of a, b, f9 be
Morphism of b9, a9 st f9
= f holds f is
retraction iff f9 is
coretraction
proof
let A,B be
category such that
A1: (A,B)
are_opposite ;
let a,b be
Object of A such that
A2:
<^a, b^>
<>
{} and
A3:
<^b, a^>
<>
{} ;
let a9,b9 be
Object of B such that
A4: a9
= a and
A5: b9
= b;
A6:
<^b9, a9^>
=
<^a, b^> by
A1,
A4,
A5,
Th9;
<^a9, b9^>
=
<^b, a^> by
A1,
A4,
A5,
Th9;
hence thesis by
A1,
A2,
A3,
A4,
A5,
A6,
Lm1;
end;
theorem ::
YELLOW18:21
for A,B be
category st (A,B)
are_opposite holds for a,b be
Object of A st
<^a, b^>
<>
{} &
<^b, a^>
<>
{} holds for a9,b9 be
Object of B st a9
= a & b9
= b holds for f be
Morphism of a, b, f9 be
Morphism of b9, a9 st f9
= f holds f is
coretraction iff f9 is
retraction
proof
let A,B be
category such that
A1: (A,B)
are_opposite ;
let a,b be
Object of A such that
A2:
<^a, b^>
<>
{} and
A3:
<^b, a^>
<>
{} ;
let a9,b9 be
Object of B such that
A4: a9
= a and
A5: b9
= b;
A6:
<^b9, a9^>
=
<^a, b^> by
A1,
A4,
A5,
Th9;
<^a9, b9^>
=
<^b, a^> by
A1,
A4,
A5,
Th9;
hence thesis by
A1,
A2,
A3,
A4,
A5,
A6,
Lm1;
end;
theorem ::
YELLOW18:22
Th22: for A,B be
category st (A,B)
are_opposite holds for a,b be
Object of A st
<^a, b^>
<>
{} &
<^b, a^>
<>
{} holds for a9,b9 be
Object of B st a9
= a & b9
= b holds for f be
Morphism of a, b, f9 be
Morphism of b9, a9 st f9
= f & f is
retraction
coretraction holds (f9
" )
= (f
" )
proof
let A,B be
category such that
A1: (A,B)
are_opposite ;
let a,b be
Object of A such that
A2:
<^a, b^>
<>
{} and
A3:
<^b, a^>
<>
{} ;
let a9,b9 be
Object of B such that
A4: a9
= a and
A5: b9
= b;
A6:
<^b9, a9^>
=
<^a, b^> by
A1,
A4,
A5,
Th9;
A7:
<^a9, b9^>
=
<^b, a^> by
A1,
A4,
A5,
Th9;
let f be
Morphism of a, b, f9 be
Morphism of b9, a9 such that
A8: f9
= f and
A9: f is
retraction
coretraction;
reconsider g = (f
" ) as
Morphism of a9, b9 by
A1,
A4,
A5,
Th7;
A10: ((f
" )
* f)
= (
idm a) by
A2,
A3,
A9,
ALTCAT_3: 2;
A11: (f
* (f
" ))
= (
idm b) by
A2,
A3,
A9,
ALTCAT_3: 2;
A12: (f9
* g)
= (
idm a) by
A1,
A2,
A3,
A4,
A5,
A8,
A10,
Th9;
A13: (g
* f9)
= (
idm b) by
A1,
A2,
A3,
A4,
A5,
A8,
A11,
Th9;
A14: (f9
* g)
= (
idm a9) by
A1,
A4,
A12,
Th10;
A15: (g
* f9)
= (
idm b9) by
A1,
A5,
A13,
Th10;
A16: f9 is
retraction
coretraction by
A1,
A2,
A3,
A4,
A5,
A8,
A9,
Lm1;
A17: g
is_left_inverse_of f9 by
A15;
g
is_right_inverse_of f9 by
A14;
hence thesis by
A2,
A3,
A6,
A7,
A16,
A17,
ALTCAT_3:def 4;
end;
theorem ::
YELLOW18:23
Th23: for A,B be
category st (A,B)
are_opposite holds for a,b be
Object of A st
<^a, b^>
<>
{} &
<^b, a^>
<>
{} holds for a9,b9 be
Object of B st a9
= a & b9
= b holds for f be
Morphism of a, b, f9 be
Morphism of b9, a9 st f9
= f holds f is
iso iff f9 is
iso
proof
let A,B be
category such that
A1: (A,B)
are_opposite ;
let a,b be
Object of A such that
A2:
<^a, b^>
<>
{} and
A3:
<^b, a^>
<>
{} ;
let a9,b9 be
Object of B such that
A4: a9
= a and
A5: b9
= b;
A6:
<^b9, a9^>
=
<^a, b^> by
A1,
A4,
A5,
Th9;
A7:
<^a9, b9^>
=
<^b, a^> by
A1,
A4,
A5,
Th9;
now
let A,B be
category such that
A8: (A,B)
are_opposite ;
let a,b be
Object of A such that
A9:
<^a, b^>
<>
{} and
A10:
<^b, a^>
<>
{} ;
let a9,b9 be
Object of B such that
A11: a9
= a and
A12: b9
= b;
let f be
Morphism of a, b, f9 be
Morphism of b9, a9 such that
A13: f9
= f;
assume
A14: f is
iso;
then
A15: (f
* (f
" ))
= (
idm b);
A16: ((f
" )
* f)
= (
idm a) by
A14;
f is
retraction
coretraction by
A14,
ALTCAT_3: 5;
then
A17: (f9
" )
= (f
" ) by
A8,
A9,
A10,
A11,
A12,
A13,
Th22;
A18: (
idm a)
= (
idm a9) by
A8,
A11,
Th10;
A19: (
idm b)
= (
idm b9) by
A8,
A12,
Th10;
A20: (f9
* (f9
" ))
= (
idm a9) by
A8,
A9,
A10,
A11,
A12,
A13,
A16,
A17,
A18,
Th9;
((f9
" )
* f9)
= (
idm b9) by
A8,
A9,
A10,
A11,
A12,
A13,
A15,
A17,
A19,
Th9;
hence f9 is
iso by
A20;
end;
hence thesis by
A1,
A2,
A3,
A4,
A5,
A6,
A7;
end;
theorem ::
YELLOW18:24
Th24: for A,B,C,D be
category st (A,B)
are_opposite & (C,D)
are_opposite holds for F,G be
covariant
Functor of B, C st (F,G)
are_naturally_equivalent holds ((((
dualizing-func (C,D))
* G)
* (
dualizing-func (A,B))),(((
dualizing-func (C,D))
* F)
* (
dualizing-func (A,B))))
are_naturally_equivalent
proof
let A,B,C,D be
category such that
A1: (A,B)
are_opposite and
A2: (C,D)
are_opposite ;
let F,G be
covariant
Functor of B, C such that
A3: F
is_naturally_transformable_to G and
A4: G
is_transformable_to F;
given t be
natural_transformation of F, G such that
A5: for a be
Object of B holds (t
! a) is
iso;
set dAB = (
dualizing-func (A,B)), dCD = (
dualizing-func (C,D)), dF = ((dCD
* F)
* dAB), dG = ((dCD
* G)
* dAB);
A6: F
is_transformable_to G by
A3;
A7:
now
let a be
Object of A;
A8: (dG
. a)
= ((dCD
* G)
. (dAB
. a)) by
FUNCTOR0: 33;
(dF
. a)
= ((dCD
* F)
. (dAB
. a)) by
FUNCTOR0: 33;
hence (dG
. a)
= (dCD
. (G
. (dAB
. a))) & (dF
. a)
= (dCD
. (F
. (dAB
. a))) by
A8,
FUNCTOR0: 33;
hence (dG
. a)
= (G
. (dAB
. a)) & (dF
. a)
= (F
. (dAB
. a)) by
A2,
Def5;
hence
<^(dG
. a), (dF
. a)^>
=
<^(F
. (dAB
. a)), (G
. (dAB
. a))^> by
A2,
Th9;
end;
A9: dG
is_transformable_to dF
proof
let a be
Object of A;
<^(dG
. a), (dF
. a)^>
=
<^(F
. (dAB
. a)), (G
. (dAB
. a))^> by
A7;
hence thesis by
A6;
end;
(
dom t)
= the
carrier of B by
PARTFUN1:def 2
.= the
carrier of A by
A1;
then
reconsider dt = t as
ManySortedSet of the
carrier of A by
PARTFUN1:def 2,
RELAT_1:def 18;
dt is
transformation of dG, dF
proof
thus dG
is_transformable_to dF by
A9;
let a be
Object of A;
set b = (dAB
. a);
A10: b
= a by
A1,
Def5;
(t
. b)
= (t
! b) by
A6,
FUNCTOR2:def 4;
hence thesis by
A7,
A10;
end;
then
reconsider dt as
transformation of dG, dF;
A11:
now
let a,b be
Object of A such that
A12:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
set b9 = (dAB
. b), a9 = (dAB
. a), f9 = (dAB
. f);
A13: a9
= a by
A1,
Def5;
A14: b9
= b by
A1,
Def5;
then
A15:
<^b9, a9^>
=
<^a, b^> by
A1,
A13,
Th9;
A16: (t
! a9)
= (t
. a) by
A6,
A13,
FUNCTOR2:def 4;
A17: (t
! b9)
= (t
. b) by
A6,
A14,
FUNCTOR2:def 4;
A18: (dt
! a)
= (t
. a) by
A9,
FUNCTOR2:def 4;
A19: (dt
! b)
= (t
. b) by
A9,
FUNCTOR2:def 4;
A20:
<^(F
. b9), (F
. a9)^>
<>
{} by
A12,
A15,
FUNCTOR0:def 18;
A21:
<^(G
. b9), (G
. a9)^>
<>
{} by
A12,
A15,
FUNCTOR0:def 18;
A22: (dF
. f)
= ((dCD
* F)
. f9) by
A12,
FUNCTOR3: 7;
A23: (dG
. f)
= ((dCD
* G)
. f9) by
A12,
FUNCTOR3: 7;
A24: (dF
. f)
= (dCD
. (F
. f9)) by
A12,
A15,
A22,
FUNCTOR3: 8;
A25: (dG
. f)
= (dCD
. (G
. f9)) by
A12,
A15,
A23,
FUNCTOR3: 8;
A26: (dF
. f)
= (F
. f9) by
A2,
A20,
A24,
Def5;
A27: (dG
. f)
= (G
. f9) by
A2,
A21,
A25,
Def5;
A28:
<^(F
. b9), (G
. b9)^>
<>
{} by
A6;
A29:
<^(F
. a9), (G
. a9)^>
<>
{} by
A6;
A30: (dG
. a)
= (G
. a9) by
A7;
A31: (dF
. a)
= (F
. a9) by
A7;
A32: (dG
. b)
= (G
. b9) by
A7;
A33: (dF
. b)
= (F
. b9) by
A7;
hence ((dt
! b)
* (dG
. f))
= ((G
. f9)
* (t
! b9)) by
A2,
A17,
A19,
A21,
A27,
A28,
A30,
A32,
Th9
.= ((t
! a9)
* (F
. f9)) by
A3,
A12,
A15,
FUNCTOR2:def 7
.= ((dF
. f)
* (dt
! a)) by
A2,
A16,
A18,
A20,
A26,
A29,
A30,
A31,
A33,
Th9;
end;
thus dG
is_naturally_transformable_to dF by
A9,
A11;
then
reconsider dt as
natural_transformation of dG, dF by
A11,
FUNCTOR2:def 7;
thus dF
is_transformable_to dG
proof
let a be
Object of A;
A34: (dF
. a)
= (F
. (dAB
. a)) by
A7;
(dG
. a)
= (G
. (dAB
. a)) by
A7;
then
<^(dF
. a), (dG
. a)^>
=
<^(G
. (dAB
. a)), (F
. (dAB
. a))^> by
A2,
A34,
Th9;
hence thesis by
A4;
end;
take dt;
let a be
Object of A;
A35: (dG
. a)
= (G
. (dAB
. a)) by
A7;
A36: (dF
. a)
= (F
. (dAB
. a)) by
A7;
A37: (dAB
. a)
= a by
A1,
Def5;
A38: (dt
! a)
= (t
. a) by
A9,
FUNCTOR2:def 4;
A39: (t
! (dAB
. a))
= (t
. a) by
A6,
A37,
FUNCTOR2:def 4;
A40: (t
! (dAB
. a)) is
iso by
A5;
A41:
<^(F
. (dAB
. a)), (G
. (dAB
. a))^>
<>
{} by
A6;
<^(G
. (dAB
. a)), (F
. (dAB
. a))^>
<>
{} by
A4;
hence thesis by
A2,
A35,
A36,
A38,
A39,
A40,
A41,
Th23;
end;
theorem ::
YELLOW18:25
Th25: for A,B,C,D be
category st (A,B)
are_opposite & (C,D)
are_opposite holds (A,C)
are_equivalent implies (B,D)
are_equivalent
proof
let A,B,C,D be
category;
assume that
A1: (A,B)
are_opposite and
A2: (C,D)
are_opposite ;
given F be
covariant
Functor of A, C, G be
covariant
Functor of C, A such that
A3: ((G
* F),(
id A))
are_naturally_equivalent and
A4: ((F
* G),(
id C))
are_naturally_equivalent ;
take dF = (((
dualizing-func (C,D))
* F)
* (
dualizing-func (B,A))), dG = (((
dualizing-func (A,B))
* G)
* (
dualizing-func (D,C)));
A5: (G
* (
id C))
= the FunctorStr of G by
FUNCTOR3: 5;
A6: ((
dualizing-func (A,B))
* (
id A))
= (
dualizing-func (A,B)) by
FUNCTOR3: 5;
A7: (
id C)
= ((
dualizing-func (D,C))
* (
dualizing-func (C,D))) by
A2,
Th14;
A8: (((
dualizing-func (A,B))
* (G
* F))
* (
dualizing-func (B,A)))
= ((((
dualizing-func (A,B))
* G)
* F)
* (
dualizing-func (B,A))) by
FUNCTOR0: 32
.= (((
dualizing-func (A,B))
* G)
* (F
* (
dualizing-func (B,A)))) by
FUNCTOR0: 32
.= (((
dualizing-func (A,B))
* (G
* (
id C)))
* (F
* (
dualizing-func (B,A)))) by
A5,
Th3
.= ((((
dualizing-func (A,B))
* G)
* (
id C))
* (F
* (
dualizing-func (B,A)))) by
FUNCTOR0: 32
.= ((dG
* (
dualizing-func (C,D)))
* (F
* (
dualizing-func (B,A)))) by
A7,
FUNCTOR0: 32
.= (dG
* ((
dualizing-func (C,D))
* (F
* (
dualizing-func (B,A))))) by
FUNCTOR0: 32
.= (dG
* dF) by
FUNCTOR0: 32;
(((
dualizing-func (A,B))
* (
id A))
* (
dualizing-func (B,A)))
= (
id B) by
A1,
A6,
Th14;
hence ((dG
* dF),(
id B))
are_naturally_equivalent by
A1,
A3,
A8,
Th24;
A9: (F
* (
id A))
= the FunctorStr of F by
FUNCTOR3: 5;
A10: ((
dualizing-func (C,D))
* (
id C))
= (
dualizing-func (C,D)) by
FUNCTOR3: 5;
A11: (
id A)
= ((
dualizing-func (B,A))
* (
dualizing-func (A,B))) by
A1,
Th14;
A12: (((
dualizing-func (C,D))
* (F
* G))
* (
dualizing-func (D,C)))
= ((((
dualizing-func (C,D))
* F)
* G)
* (
dualizing-func (D,C))) by
FUNCTOR0: 32
.= (((
dualizing-func (C,D))
* F)
* (G
* (
dualizing-func (D,C)))) by
FUNCTOR0: 32
.= (((
dualizing-func (C,D))
* (F
* (
id A)))
* (G
* (
dualizing-func (D,C)))) by
A9,
Th3
.= ((((
dualizing-func (C,D))
* F)
* (
id A))
* (G
* (
dualizing-func (D,C)))) by
FUNCTOR0: 32
.= ((dF
* (
dualizing-func (A,B)))
* (G
* (
dualizing-func (D,C)))) by
A11,
FUNCTOR0: 32
.= (dF
* ((
dualizing-func (A,B))
* (G
* (
dualizing-func (D,C))))) by
FUNCTOR0: 32
.= (dF
* dG) by
FUNCTOR0: 32;
(((
dualizing-func (C,D))
* (
id C))
* (
dualizing-func (D,C)))
= (
id D) by
A2,
A10,
Th14;
hence thesis by
A2,
A4,
A12,
Th24;
end;
definition
let A,B be
category;
::
YELLOW18:def6
pred A,B
are_dual means
:
Def6: (A,(B
opp ))
are_equivalent ;
symmetry
proof
let A,B be
category;
A1: (A,(A
opp ))
are_opposite by
Def4;
(B,(B
opp ))
are_opposite by
Def4;
hence thesis by
A1,
Th25;
end;
end
theorem ::
YELLOW18:26
for A,B be
category st (A,B)
are_anti-isomorphic holds (A,B)
are_dual
proof
let A,B be
category;
A1: (B,(B
opp ))
are_opposite by
Def4;
assume (A,B)
are_anti-isomorphic ;
then (A,(B
opp ))
are_isomorphic by
A1,
Th17;
hence (A,(B
opp ))
are_equivalent by
Th5;
end;
theorem ::
YELLOW18:27
for A,B,C be
category st (A,B)
are_opposite holds (A,C)
are_equivalent iff (B,C)
are_dual
proof
let A,B,C be
category such that
A1: (A,B)
are_opposite ;
(C,(C
opp ))
are_opposite by
Def4;
hence thesis by
A1,
Th25;
end;
theorem ::
YELLOW18:28
for A,B,C be
category st (A,B)
are_dual & (B,C)
are_equivalent holds (A,C)
are_dual
proof
let A,B,C be
category such that
A1: (A,(B
opp ))
are_equivalent and
A2: (B,C)
are_equivalent ;
A3: (B,(B
opp ))
are_opposite by
Def4;
(C,(C
opp ))
are_opposite by
Def4;
then ((B
opp ),(C
opp ))
are_equivalent by
A2,
A3,
Th25;
hence (A,(C
opp ))
are_equivalent by
A1,
Th4;
end;
theorem ::
YELLOW18:29
for A,B,C be
category st (A,B)
are_dual & (B,C)
are_dual holds (A,C)
are_equivalent
proof
let A,B,C be
category such that
A1: (A,(B
opp ))
are_equivalent and
A2: (B,C)
are_dual ;
(C,(B
opp ))
are_equivalent by
A2,
Def6;
hence thesis by
A1,
Th4;
end;
begin
theorem ::
YELLOW18:30
Th30: for X,Y,x be
set holds x
in (
Funcs (X,Y)) iff x is
Function & (
proj1 x)
= X & (
proj2 x)
c= Y
proof
let X,Y,x be
set;
hereby
assume x
in (
Funcs (X,Y));
then ex f be
Function st x
= f & (
dom f)
= X & (
rng f)
c= Y by
FUNCT_2:def 2;
hence x is
Function & (
proj1 x)
= X & (
proj2 x)
c= Y;
end;
assume x is
Function;
then
reconsider x as
Function;
(
dom x)
= (
proj1 x);
hence thesis by
FUNCT_2:def 2;
end;
definition
let C be
category;
::
YELLOW18:def7
attr C is
para-functional means ex F be
ManySortedSet of C st for a1,a2 be
Object of C holds
<^a1, a2^>
c= (
Funcs ((F
. a1),(F
. a2)));
end
registration
cluster
quasi-functional ->
para-functional for
category;
coherence
proof
let C be
category such that
A1: for a1,a2 be
Object of C holds
<^a1, a2^>
c= (
Funcs (a1,a2));
reconsider F = (
id the
carrier of C) as
ManySortedSet of C;
take F;
let a1,a2 be
Object of C;
thus thesis by
A1;
end;
end
definition
let C be
category;
let a be
set;
::
YELLOW18:def8
func C
-carrier_of a ->
set means
:
Def8: ex b be
Object of C st b
= a & it
= (
proj1 (
idm b)) if a is
Object of C
otherwise it
=
{} ;
consistency ;
existence
proof
hereby
assume a is
Object of C;
then
reconsider b = a as
Object of C;
take x = (
proj1 (
idm b)), b;
thus b
= a & x
= (
proj1 (
idm b));
end;
thus thesis;
end;
uniqueness ;
end
notation
let C be
category;
let a be
Object of C;
synonym
the_carrier_of a for C
-carrier_of a;
end
definition
let C be
category;
let a be
Object of C;
:: original:
the_carrier_of
redefine
::
YELLOW18:def9
func
the_carrier_of a equals (
proj1 (
idm a));
compatibility by
Def8;
end
theorem ::
YELLOW18:31
Th31: for A be non
empty
set, a be
Object of (
EnsCat A) holds (
idm a)
= (
id a)
proof
let A be non
empty
set, a be
Object of (
EnsCat A);
<^a, a^>
= (
Funcs (a,a)) by
ALTCAT_1:def 14;
then
reconsider e = (
id a) as
Morphism of a, a by
FUNCT_2: 126;
now
let b be
Object of (
EnsCat A) such that
A1:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
A2:
<^a, b^>
= (
Funcs (a,b)) by
ALTCAT_1:def 14;
then
reconsider g = f as
Function;
A3: (
dom g)
= a by
A1,
A2,
Th30;
thus (f
* e)
= (g
* (
id a)) by
A1,
ALTCAT_1:def 12
.= f by
A3,
RELAT_1: 52;
end;
hence thesis by
ALTCAT_1:def 17;
end;
theorem ::
YELLOW18:32
Th32: for A be non
empty
set holds for a be
Object of (
EnsCat A) holds (
the_carrier_of a)
= a
proof
let A be non
empty
set;
let a be
Object of (
EnsCat A);
thus (
the_carrier_of a)
= (
proj1 (
id a)) by
Th31
.= a;
end;
definition
let C be
category;
::
YELLOW18:def10
attr C is
set-id-inheriting means
:
Def10: for a be
Object of C holds (
idm a)
= (
id (
the_carrier_of a));
end
registration
let A be non
empty
set;
cluster (
EnsCat A) ->
set-id-inheriting;
coherence
proof
let a be
Object of (
EnsCat A);
thus (
idm a)
= (
id a) by
Th31
.= (
id (
the_carrier_of a)) by
Th32;
end;
end
definition
let C be
category;
::
YELLOW18:def11
attr C is
concrete means C is
para-functional
semi-functional
set-id-inheriting;
end
registration
cluster
concrete ->
para-functional
semi-functional
set-id-inheriting for
category;
coherence ;
cluster
para-functional
semi-functional
set-id-inheriting ->
concrete for
category;
coherence ;
end
registration
cluster
concrete
quasi-functional
strict for
category;
existence
proof
take (
EnsCat
NAT );
thus thesis;
end;
end
theorem ::
YELLOW18:33
Th33: for C be
category holds C is
para-functional iff for a1,a2 be
Object of C holds
<^a1, a2^>
c= (
Funcs ((
the_carrier_of a1),(
the_carrier_of a2)))
proof
let C be
category;
thus C is
para-functional implies for a1,a2 be
Object of C holds
<^a1, a2^>
c= (
Funcs ((
the_carrier_of a1),(
the_carrier_of a2)))
proof
given F be
ManySortedSet of C such that
A1: for a1,a2 be
Object of C holds
<^a1, a2^>
c= (
Funcs ((F
. a1),(F
. a2)));
let a1,a2 be
Object of C;
A2: (
idm a1)
in
<^a1, a1^>;
A3:
<^a1, a1^>
c= (
Funcs ((F
. a1),(F
. a1))) by
A1;
A4:
<^a2, a2^>
c= (
Funcs ((F
. a2),(F
. a2))) by
A1;
A5: (
idm a2)
in
<^a2, a2^>;
A6: ex f1 be
Function st ((
idm a1)
= f1) & ((
dom f1)
= (F
. a1)) & ((
rng f1)
c= (F
. a1)) by
A2,
A3,
FUNCT_2:def 2;
ex f2 be
Function st ((
idm a2)
= f2) & ((
dom f2)
= (F
. a2)) & ((
rng f2)
c= (F
. a2)) by
A4,
A5,
FUNCT_2:def 2;
hence thesis by
A1,
A6;
end;
assume
A7: for a1,a2 be
Object of C holds
<^a1, a2^>
c= (
Funcs ((
the_carrier_of a1),(
the_carrier_of a2)));
deffunc
O(
set) = (C
-carrier_of $1);
consider F be
ManySortedSet of the
carrier of C such that
A8: for a be
Element of C holds (F
. a)
=
O(a) from
PBOOLE:sch 5;
take F;
let a,b be
Object of C;
A9: (F
. a)
= (
the_carrier_of a) by
A8;
(F
. b)
= (
the_carrier_of b) by
A8;
hence thesis by
A7,
A9;
end;
theorem ::
YELLOW18:34
Th34: for C be
para-functional
category holds for a,b be
Object of C st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds f is
Function of (
the_carrier_of a), (
the_carrier_of b)
proof
let C be
para-functional
category;
let a,b be
Object of C such that
A1:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
A2:
<^a, b^>
c= (
Funcs ((
the_carrier_of a),(
the_carrier_of b))) by
Th33;
f
in
<^a, b^> by
A1;
hence thesis by
A2,
FUNCT_2: 66;
end;
registration
let A be
para-functional
category;
let a,b be
Object of A;
cluster ->
Function-like
Relation-like for
Morphism of a, b;
coherence
proof
let f be
Morphism of a, b;
per cases ;
suppose
<^a, b^>
<>
{} ;
hence thesis by
Th34;
end;
suppose
<^a, b^>
=
{} ;
hence thesis;
end;
end;
end
theorem ::
YELLOW18:35
Th35: for C be
para-functional
category holds for a,b be
Object of C st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (
dom f)
= (
the_carrier_of a) & (
rng f)
c= (
the_carrier_of b)
proof
let C be
para-functional
category;
let a,b be
Object of C such that
A1:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
A2:
<^a, b^>
c= (
Funcs ((
the_carrier_of a),(
the_carrier_of b))) by
Th33;
f
in
<^a, b^> by
A1;
hence thesis by
A2,
FUNCT_2: 92;
end;
theorem ::
YELLOW18:36
Th36: for C be
para-functional
semi-functional
category holds for a,b,c be
Object of C st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= (g qua
Function
* f qua
Function)
proof
let C be
para-functional
semi-functional
category;
let a,b,c be
Object of C such that
A1:
<^a, b^>
<>
{} and
A2:
<^b, c^>
<>
{} ;
let f be
Morphism of a, b, g be
Morphism of b, c;
<^a, c^>
<>
{} by
A1,
A2,
ALTCAT_1:def 2;
hence thesis by
A1,
A2,
ALTCAT_1:def 12;
end;
theorem ::
YELLOW18:37
Th37: for C be
para-functional
semi-functional
category holds for a be
Object of C st (
id (
the_carrier_of a))
in
<^a, a^> holds (
idm a)
= (
id (
the_carrier_of a))
proof
let C be
para-functional
semi-functional
category;
let a be
Object of C;
assume (
id (
the_carrier_of a))
in
<^a, a^>;
then
reconsider f = (
id (
the_carrier_of a)) as
Morphism of a, a;
now
let b be
Object of C such that
A1:
<^a, b^>
<>
{} ;
let g be
Morphism of a, b;
A2: (
dom g)
= (
the_carrier_of a) by
A1,
Th35;
thus (g
* f)
= (g
* (
id (
the_carrier_of a))) by
A1,
Th36
.= g by
A2,
RELAT_1: 52;
end;
hence thesis by
ALTCAT_1:def 17;
end;
scheme ::
YELLOW18:sch16
ConcreteCategoryLambda { A() -> non
empty
set , B(
object,
object) ->
set , D(
object) ->
set } :
ex C be
concrete
strict
category st the
carrier of C
= A() & (for a be
Object of C holds (
the_carrier_of a)
= D(a)) & for a,b be
Object of C holds
<^a, b^>
= B(a,b)
provided
A1: for a,b,c be
Element of A(), f,g be
Function st f
in B(a,b) & g
in B(b,c) holds (g
* f)
in B(a,c)
and
A2: for a,b be
Element of A() holds B(a,b)
c= (
Funcs (D(a),D(b)))
and
A3: for a be
Element of A() holds (
id D(a))
in B(a,a);
deffunc
C(
set,
set,
set,
set,
set) = ($4
(#) $5);
A4:
now
let a,b be
Element of A(), f be
set such that
A5: f
in B(a,b);
B(a,b)
c= (
Funcs (D(a),D(b))) by
A2;
hence f is
Function by
A5;
end;
A6: for a,b,c be
Element of A(), f,g be
set st f
in B(a,b) & g
in B(b,c) holds
C(a,b,c,f,g)
in B(a,c)
proof
let a,b,c be
Element of A(), f,g be
set;
assume that
A7: f
in B(a,b) and
A8: g
in B(b,c);
reconsider f, g as
Function by
A4,
A7,
A8;
(g
* f)
= (f
(#) g);
hence thesis by
A1,
A7,
A8;
end;
A9: for a,b,c,d be
Element of A(), f,g,h be
set st f
in B(a,b) & g
in B(b,c) & h
in B(c,d) holds
C(a,c,d,C,h)
=
C(a,b,d,f,C)
proof
let a,b,c,d be
Element of A();
let f,g,h be
set;
assume that
A10: f
in B(a,b) and
A11: g
in B(b,c) and
A12: h
in B(c,d);
reconsider f, g, h as
Function by
A4,
A10,
A11,
A12;
((f
(#) g)
(#) h)
= (f
(#) (h
* g)) by
RELAT_1: 36;
hence thesis;
end;
A13: for a be
Element of A() holds ex f be
set st f
in B(a,a) & for b be
Element of A(), g be
set st g
in B(a,b) holds
C(a,a,b,f,g)
= g
proof
let a be
Element of A();
take f = (
id D(a));
thus f
in B(a,a) by
A3;
let b be
Element of A(), g be
set such that
A14: g
in B(a,b);
B(a,b)
c= (
Funcs (D(a),D(b))) by
A2;
then
consider h be
Function such that
A15: g
= h and
A16: (
dom h)
= D(a) and (
rng h)
c= D(b) by
A14,
FUNCT_2:def 2;
thus (f
(#) g)
= g by
A15,
A16,
RELAT_1: 52;
end;
A17: for a be
Element of A() holds ex f be
set st f
in B(a,a) & for b be
Element of A(), g be
set st g
in B(b,a) holds
C(b,a,a,g,f)
= g
proof
let a be
Element of A();
take f = (
id D(a));
thus f
in B(a,a) by
A3;
let b be
Element of A(), g be
set such that
A18: g
in B(b,a);
B(b,a)
c= (
Funcs (D(b),D(a))) by
A2;
then
consider h be
Function such that
A19: g
= h and (
dom h)
= D(b) and
A20: (
rng h)
c= D(a) by
A18,
FUNCT_2:def 2;
thus (g
(#) f)
= g by
A19,
A20,
RELAT_1: 53;
end;
consider C be
strict
category such that
A21: the
carrier of C
= A() and
A22: for a,b be
Object of C holds
<^a, b^>
= B(a,b) and
A23: for a,b,c be
Object of C st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
=
C(a,b,c,f,g) from
CategoryLambda(
A6,
A9,
A13,
A17);
consider D be
ManySortedSet of C such that
A24: for x be
Element of C holds (D
. x)
= D(x) from
PBOOLE:sch 5;
A25: C is
para-functional
proof
take D;
let a1,a2 be
Object of C;
A26:
<^a1, a2^>
= B(a1,a2) by
A22;
A27: D(a1)
= (D
. a1) by
A24;
D(a2)
= (D
. a2) by
A24;
hence thesis by
A2,
A21,
A26,
A27;
end;
A28: C is
semi-functional by
A23;
A29:
now
let a be
Object of C;
(
id D(a))
in B(a,a) by
A3,
A21;
then
reconsider e = (
id D(a)) as
Morphism of a, a by
A22;
now
let b be
Object of C such that
A30:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
A31:
<^a, b^>
= B(a,b) by
A22;
A32: B(a,b)
c= (
Funcs (D(a),D(b))) by
A2,
A21;
f
in
<^a, b^> by
A30;
then
consider h be
Function such that
A33: f
= h and
A34: (
dom h)
= D(a) and (
rng h)
c= D(b) by
A31,
A32,
FUNCT_2:def 2;
thus (f
* e)
= (h
* (
id D(a))) by
A28,
A30,
A33
.= f by
A33,
A34,
RELAT_1: 52;
end;
hence (
idm a)
= (
id D(a)) by
ALTCAT_1:def 17;
end;
A35:
now
let i be
set;
assume i
in the
carrier of C;
then
reconsider a = i as
Object of C;
thus (C
-carrier_of i)
= (
proj1 (
idm a)) by
Def8
.= (
proj1 (
id D(a))) by
A29
.= D(a)
.= (D
. i) by
A24;
end;
C is
set-id-inheriting
proof
let a be
Object of C;
thus (
idm a)
= (
id D(a)) by
A29
.= (
id (D
. a)) by
A24
.= (
id (
the_carrier_of a)) by
A35;
end;
then
reconsider C as
para-functional
semi-functional
set-id-inheriting
strict
category by
A25,
A28;
take C;
thus the
carrier of C
= A() by
A21;
hereby
let a be
Object of C;
thus (
the_carrier_of a)
= (D
. a) by
A35
.= D(a) by
A24;
end;
thus thesis by
A22;
end;
scheme ::
YELLOW18:sch17
ConcreteCategoryQuasiLambda { A() -> non
empty
set , P[
object,
object,
object], D(
object) ->
set } :
ex C be
concrete
strict
category st the
carrier of C
= A() & (for a be
Object of C holds (
the_carrier_of a)
= D(a)) & for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C
. (a,b)) iff f
in (
Funcs (D(a),D(b))) & P[a, b, f]
provided
A1: for a,b,c be
Element of A(), f,g be
Function st P[a, b, f] & P[b, c, g] holds P[a, c, (g
* f)]
and
A2: for a be
Element of A() holds P[a, a, (
id D(a))];
set A = A();
defpred
P[
object,
object] means ex a,b be
object, c be
set st $1
=
[a, b] & c
= $2 & for f be
object holds f
in c iff f
in (
Funcs (D(a),D(b))) & P[a, b, f];
A3:
now
let x be
object;
assume x
in
[:A, A:];
then
consider a,b be
object such that a
in A and b
in A and
A4: x
=
[a, b] by
ZFMISC_1:def 2;
defpred
Q[
object] means P[a, b, $1];
consider y be
set such that
A5: for f be
object holds f
in y iff f
in (
Funcs (D(a),D(b))) &
Q[f] from
XBOOLE_0:sch 1;
reconsider y as
object;
take y;
thus
P[x, y] by
A4,
A5;
end;
consider F be
Function such that (
dom F)
=
[:A, A:] and
A6: for x be
object st x
in
[:A, A:] holds
P[x, (F
. x)] from
CLASSES1:sch 1(
A3);
A7:
now
let a,b be
set;
assume that
A8: a
in A and
A9: b
in A;
[a, b]
in
[:A, A:] by
A8,
A9,
ZFMISC_1: 87;
then
P[
[a, b], (F
.
[a, b])] by
A6;
then
consider a9,b9,c be
object such that
A10:
[a, b]
=
[a9, b9] & c
= (
Funcs (D(a9),D(b9))) and
A11: for f be
object holds f
in (F
.
[a, b]) iff f
in (
Funcs (D(a9),D(b9))) & P[a9, b9, f];
A12: a
= a9 by
A10,
XTUPLE_0: 1;
A13: b
= b9 by
A10,
XTUPLE_0: 1;
let f be
set;
thus f
in (F
.
[a, b]) iff P[a, b, f] & f
in (
Funcs (D(a),D(b))) by
A11,
A12,
A13;
end;
deffunc
B(
set,
set) = (F
.
[$1, $2]);
A14:
now
let a,b,c be
Element of A, f,g be
Function;
assume that
A15: f
in
B(a,b) and
A16: g
in
B(b,c);
A17: P[a, b, f] by
A7,
A15;
A18: f
in (
Funcs (D(a),D(b))) by
A7,
A15;
A19: P[b, c, g] by
A7,
A16;
A20: g
in (
Funcs (D(b),D(c))) by
A7,
A16;
A21: (
dom f)
= D(a) by
A18,
Th30;
A22: (
rng f)
c= D(b) by
A18,
Th30;
A23: (
dom g)
= D(b) by
A20,
Th30;
A24: (
rng g)
c= D(c) by
A20,
Th30;
A25: (
rng (g
* f))
c= (
rng g) by
RELAT_1: 26;
A26: (
dom (g
* f))
= D(a) by
A21,
A22,
A23,
RELAT_1: 27;
(
rng (g
* f))
c= D(c) by
A24,
A25;
then
A27: (g
* f)
in (
Funcs (D(a),D(c))) by
A26,
FUNCT_2:def 2;
P[a, c, (g
* f)] by
A1,
A17,
A19;
hence (g
* f)
in
B(a,c) by
A7,
A27;
end;
A28: for a,b be
Element of A holds
B(a,b)
c= (
Funcs (D(a),D(b))) by
A7;
A29: for a be
Element of A() holds (
id D(a))
in
B(a,a)
proof
let a be
Element of A();
A30: (
dom (
id D(a)))
= D(a);
A31: (
rng (
id D(a)))
= D(a);
A32: P[a, a, (
id D(a))] by
A2;
(
id D(a))
in (
Funcs (D(a),D(a))) by
A30,
A31,
FUNCT_2:def 2;
hence thesis by
A7,
A32;
end;
consider C be
para-functional
semi-functional
set-id-inheriting
strict
category such that
A33: the
carrier of C
= A() and
A34: for a be
Object of C holds (
the_carrier_of a)
= D(a) and
A35: for a,b be
Object of C holds
<^a, b^>
=
B(a,b) from
ConcreteCategoryLambda(
A14,
A28,
A29);
take C;
thus the
carrier of C
= A() by
A33;
thus for a be
Object of C holds (
the_carrier_of a)
= D(a) by
A34;
let a,b be
Element of A(), f be
Function;
reconsider a, b as
Object of C by
A33;
(the
Arrows of C
. (a,b))
=
<^a, b^>
.= (F
.
[a, b]) by
A35;
hence thesis by
A7;
end;
scheme ::
YELLOW18:sch18
ConcreteCategoryEx { A() -> non
empty
set , B(
object) ->
set , D[
object,
object], P[
object,
object,
object] } :
ex C be
concrete
strict
category st the
carrier of C
= A() & (for a be
Object of C holds for x be
set holds x
in (
the_carrier_of a) iff x
in B(a) & D[a, x]) & for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C
. (a,b)) iff f
in (
Funcs ((C
-carrier_of a),(C
-carrier_of b))) & P[a, b, f]
provided
A1: for a,b,c be
Element of A(), f,g be
Function st P[a, b, f] & P[b, c, g] holds P[a, c, (g
* f)]
and
A2: for a be
Element of A(), X be
set st for x be
set holds x
in X iff x
in B(a) & D[a, x] holds P[a, a, (
id X)];
A3: for a,b,c be
Element of A(), f,g be
Function st P[a, b, f] & P[b, c, g] holds P[a, c, (g
* f)] by
A1;
consider D be
Function such that (
dom D)
= A() and
A4: for a be
object st a
in A() holds for y be
object holds y
in (D
. a) iff y
in B(a) & D[a, y] from
CARD_3:sch 2;
deffunc
D(
set) = (D
. $1);
A5:
now
let a be
Element of A();
for y be
set holds y
in (D
. a) iff y
in B(a) & D[a, y] by
A4;
hence P[a, a, (
id
D(a))] by
A2;
end;
consider C be
para-functional
semi-functional
set-id-inheriting
strict
category such that
A6: the
carrier of C
= A() and
A7: for a be
Object of C holds (
the_carrier_of a)
=
D(a) and
A8: for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C
. (a,b)) iff f
in (
Funcs (
D(a),
D(b))) & P[a, b, f] from
ConcreteCategoryQuasiLambda(
A3,
A5);
take C;
thus the
carrier of C
= A() by
A6;
hereby
let a be
Object of C;
(
the_carrier_of a)
= (D
. a) by
A7;
hence for x be
set holds x
in (
the_carrier_of a) iff x
in B(a) & D[a, x] by
A4,
A6;
end;
let a,b be
Element of A();
A9: (D
. a)
= (C
-carrier_of a) by
A6,
A7;
(D
. b)
= (C
-carrier_of b) by
A6,
A7;
hence thesis by
A8,
A9;
end;
scheme ::
YELLOW18:sch19
ConcreteCategoryUniq1 { A() -> non
empty
set , B(
object,
object) ->
object } :
for C1,C2 be
para-functional
semi-functional
category st the
carrier of C1
= A() & (for a,b be
Object of C1 holds
<^a, b^>
= B(a,b)) & the
carrier of C2
= A() & (for a,b be
Object of C2 holds
<^a, b^>
= B(a,b)) holds the AltCatStr of C1
= the AltCatStr of C2;
deffunc
C(
set,
set,
set,
set,
set) = ($4
(#) $5);
A1: for C1,C2 be non
empty
transitive
AltCatStr st the
carrier of C1
= A() & (for a,b be
Object of C1 holds
<^a, b^>
= B(a,b)) & (for a,b,c be
Object of C1 st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
=
C(a,b,c,f,g)) & the
carrier of C2
= A() & (for a,b be
Object of C2 holds
<^a, b^>
= B(a,b)) & (for a,b,c be
Object of C2 st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
=
C(a,b,c,f,g)) holds the AltCatStr of C1
= the AltCatStr of C2 from
CategoryLambdaUniq;
let C1,C2 be
para-functional
semi-functional
category;
A2: for C1 be
para-functional
semi-functional
category, a,b,c be
Object of C1 st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= (f
(#) g) by
Th36;
then
A3: for a,b,c be
Object of C1 st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= (f
(#) g);
for a,b,c be
Object of C2 st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds (g
* f)
= (f
(#) g) by
A2;
hence thesis by
A1,
A3;
end;
scheme ::
YELLOW18:sch20
ConcreteCategoryUniq2 { A() -> non
empty
set , P[
object,
object,
object], D(
object) ->
set } :
for C1,C2 be
para-functional
semi-functional
category st the
carrier of C1
= A() & (for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C1
. (a,b)) iff f
in (
Funcs (D(a),D(b))) & P[a, b, f]) & the
carrier of C2
= A() & (for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C2
. (a,b)) iff f
in (
Funcs (D(a),D(b))) & P[a, b, f]) holds the AltCatStr of C1
= the AltCatStr of C2;
let C1,C2 be
para-functional
semi-functional
category such that
A1: the
carrier of C1
= A() and
A2: for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C1
. (a,b)) iff f
in (
Funcs (D(a),D(b))) & P[a, b, f] and
A3: the
carrier of C2
= A() and
A4: for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C2
. (a,b)) iff f
in (
Funcs (D(a),D(b))) & P[a, b, f];
deffunc
B(
set,
set) = (the
Arrows of C1
. ($1,$2));
A5: for C1,C2 be
para-functional
semi-functional
category st the
carrier of C1
= A() & (for a,b be
Object of C1 holds
<^a, b^>
=
B(a,b)) & the
carrier of C2
= A() & (for a,b be
Object of C2 holds
<^a, b^>
=
B(a,b)) holds the AltCatStr of C1
= the AltCatStr of C2 from
ConcreteCategoryUniq1;
A6: for a,b be
Object of C1 holds
<^a, b^>
=
B(a,b);
now
let a,b be
Object of C2;
reconsider x = a, y = b as
Element of A() by
A3;
reconsider a9 = x, b9 = y as
Object of C1 by
A1;
thus
<^a, b^>
=
B(a,b)
proof
hereby
let z be
object;
assume
A7: z
in
<^a, b^>;
then
A8: z
in (
Funcs (D(x),D(y))) by
A4;
P[x, y, z] by
A4,
A7;
hence z
in
B(a,b) by
A2,
A8;
end;
let z be
object;
assume
A9: z
in
B(a,b);
then
A10: z is
Morphism of a9, b9;
then
A11: z
in (
Funcs (D(x),D(y))) by
A2,
A9;
P[x, y, z] by
A2,
A9,
A10;
hence thesis by
A4,
A11;
end;
end;
hence thesis by
A1,
A3,
A5,
A6;
end;
scheme ::
YELLOW18:sch21
ConcreteCategoryUniq3 { A() -> non
empty
set , B(
object) ->
set , D[
object,
object], P[
object,
object,
object] } :
for C1,C2 be
para-functional
semi-functional
category st the
carrier of C1
= A() & (for a be
Object of C1 holds for x be
set holds x
in (
the_carrier_of a) iff x
in B(a) & D[a, x]) & (for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C1
. (a,b)) iff f
in (
Funcs ((C1
-carrier_of a),(C1
-carrier_of b))) & P[a, b, f]) & the
carrier of C2
= A() & (for a be
Object of C2 holds for x be
set holds x
in (
the_carrier_of a) iff x
in B(a) & D[a, x]) & (for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C2
. (a,b)) iff f
in (
Funcs ((C2
-carrier_of a),(C2
-carrier_of b))) & P[a, b, f]) holds the AltCatStr of C1
= the AltCatStr of C2;
let C1,C2 be
para-functional
semi-functional
category such that
A1: the
carrier of C1
= A() and
A2: for a be
Object of C1 holds for x be
set holds x
in (
the_carrier_of a) iff x
in B(a) & D[a, x] and
A3: for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C1
. (a,b)) iff f
in (
Funcs ((C1
-carrier_of a),(C1
-carrier_of b))) & P[a, b, f] and
A4: the
carrier of C2
= A() and
A5: for a be
Object of C2 holds for x be
set holds x
in (
the_carrier_of a) iff x
in B(a) & D[a, x] and
A6: for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C2
. (a,b)) iff f
in (
Funcs ((C2
-carrier_of a),(C2
-carrier_of b))) & P[a, b, f];
deffunc
D(
set) = (C1
-carrier_of $1);
A7: for C1,C2 be
para-functional
semi-functional
category st the
carrier of C1
= A() & (for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C1
. (a,b)) iff f
in (
Funcs (
D(a),
D(b))) & P[a, b, f]) & the
carrier of C2
= A() & (for a,b be
Element of A(), f be
Function holds f
in (the
Arrows of C2
. (a,b)) iff f
in (
Funcs (
D(a),
D(b))) & P[a, b, f]) holds the AltCatStr of C1
= the AltCatStr of C2 from
ConcreteCategoryUniq2;
A8:
now
let a be
Element of A();
reconsider a1 = a as
Object of C1 by
A1;
reconsider a2 = a as
Object of C2 by
A4;
now
let x be
object;
x
in (
the_carrier_of a1) iff x
in B(a) & D[a, x] by
A2;
hence x
in (
the_carrier_of a1) iff x
in (
the_carrier_of a2) by
A5;
end;
hence (C1
-carrier_of a)
= (C2
-carrier_of a) by
TARSKI: 2;
end;
now
let a,b be
Element of A(), f be
Function;
A9:
D(a)
= (C2
-carrier_of a) by
A8;
D(b)
= (C2
-carrier_of b) by
A8;
hence f
in (the
Arrows of C2
. (a,b)) iff f
in (
Funcs (
D(a),
D(b))) & P[a, b, f] by
A6,
A9;
end;
hence thesis by
A1,
A3,
A4,
A7;
end;
begin
theorem ::
YELLOW18:38
Th38: for C be
concrete
category holds for a,b be
Object of C st
<^a, b^>
<>
{} &
<^b, a^>
<>
{} holds for f be
Morphism of a, b st f is
retraction holds (
rng f)
= (
the_carrier_of b)
proof
let C be
concrete
category;
let a,b be
Object of C;
assume that
A1:
<^a, b^>
<>
{} and
A2:
<^b, a^>
<>
{} ;
let f be
Morphism of a, b;
given g be
Morphism of b, a such that
A3: g
is_right_inverse_of f;
A4: (f
* g)
= (
idm b) by
A3;
A5: (f qua
Function
* g)
= (f
* g) by
A1,
A2,
Th36;
A6: f is
Function of (
the_carrier_of a), (
the_carrier_of b) by
A1,
Th34;
A7: g is
Function of (
the_carrier_of b), (
the_carrier_of a) by
A2,
Th34;
(
idm b)
= (
id (
the_carrier_of b)) by
Def10;
hence thesis by
A4,
A5,
A6,
A7,
FUNCT_2: 18;
end;
theorem ::
YELLOW18:39
Th39: for C be
concrete
category holds for a,b be
Object of C st
<^a, b^>
<>
{} &
<^b, a^>
<>
{} holds for f be
Morphism of a, b st f is
coretraction holds f is
one-to-one
proof
let C be
concrete
category;
let a,b be
Object of C;
assume that
A1:
<^a, b^>
<>
{} and
A2:
<^b, a^>
<>
{} ;
let f be
Morphism of a, b;
given g be
Morphism of b, a such that
A3: g
is_left_inverse_of f;
A4: (g
* f)
= (
idm a) by
A3;
A5: (g qua
Function
* f)
= (g
* f) by
A1,
A2,
Th36;
A6: (
dom f)
= (
the_carrier_of a) by
A1,
Th35;
(
idm a)
= (
id (
the_carrier_of a)) by
Def10;
hence thesis by
A4,
A5,
A6,
FUNCT_1: 31;
end;
theorem ::
YELLOW18:40
Th40: for C be
concrete
category holds for a,b be
Object of C st
<^a, b^>
<>
{} &
<^b, a^>
<>
{} holds for f be
Morphism of a, b st f is
iso holds f is
one-to-one & (
rng f)
= (
the_carrier_of b) by
ALTCAT_3: 5,
Th38,
Th39;
theorem ::
YELLOW18:41
Th41: for C be
para-functional
semi-functional
category holds for a,b be
Object of C st
<^a, b^>
<>
{} holds for f be
Morphism of a, b st f is
one-to-one & (f qua
Function
" )
in
<^b, a^> holds f is
iso
proof
let C be
para-functional
semi-functional
category;
let a,b be
Object of C such that
A1:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
assume
A2: f is
one-to-one;
assume
A3: (f qua
Function
" )
in
<^b, a^>;
then
reconsider g = (f qua
Function
" ) as
Morphism of b, a;
(
dom g)
= (
the_carrier_of b) by
A3,
Th35;
then
A4: (
rng f)
= (
the_carrier_of b) by
A2,
FUNCT_1: 33;
A5: ((f qua
Function
" )
* f)
= (
id (
dom f)) by
A2,
FUNCT_1: 39;
A6: (f
* (f qua
Function
" ))
= (
id (
rng f)) by
A2,
FUNCT_1: 39;
A7: (
dom f)
= (
the_carrier_of a) by
A1,
Th35;
A8: (f
* g)
= (
id (
the_carrier_of b)) by
A1,
A3,
A4,
A6,
Th36;
A9: (g
* f)
= (
id (
the_carrier_of a)) by
A1,
A3,
A5,
A7,
Th36;
A10: (
idm b)
= (f
* g) by
A8,
Th37;
(
idm a)
= (g
* f) by
A9,
Th37;
then
A11: g
is_left_inverse_of f;
A12: g
is_right_inverse_of f by
A10;
then f is
retraction
coretraction by
A11;
hence (f
* (f
" ))
= (
idm b) & ((f
" )
* f)
= (
idm a) by
A1,
A3,
A11,
A12,
ALTCAT_3:def 4;
end;
theorem ::
YELLOW18:42
for C be
concrete
category holds for a,b be
Object of C st
<^a, b^>
<>
{} &
<^b, a^>
<>
{} holds for f be
Morphism of a, b st f is
iso holds (f
" )
= (f qua
Function
" )
proof
let C be
concrete
category;
let a,b be
Object of C;
assume that
A1:
<^a, b^>
<>
{} and
A2:
<^b, a^>
<>
{} ;
let f be
Morphism of a, b;
assume
A3: f is
iso;
then
A4: ((f
" )
* f)
= (
idm a);
A5: ((f
" )
* f qua
Function)
= ((f
" )
* f) by
A1,
A2,
Th36;
A6: (
dom (f
" ))
= (
the_carrier_of b) by
A2,
Th35;
A7: (
dom f)
= (
the_carrier_of a) by
A1,
Th35;
A8: f is
one-to-one by
A1,
A2,
A3,
Th40;
A9: (
rng f)
= (
the_carrier_of b) by
A1,
A2,
A3,
Th40;
(
idm a)
= (
id (
the_carrier_of a)) by
Def10;
hence thesis by
A4,
A5,
A6,
A7,
A8,
A9,
FUNCT_1: 41;
end;
scheme ::
YELLOW18:sch22
ConcreteCatEquivalence { A,B() ->
para-functional
semi-functional
category , O1,O2(
object) ->
object , F1,F2(
object,
object,
object) ->
Function , A,B(
object) ->
Function } :
(A(),B())
are_equivalent
provided
A1: ex F be
covariant
Functor of A(), B() st (for a be
Object of A() holds (F
. a)
= O1(a)) & for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= F1(a,b,f)
and
A2: ex G be
covariant
Functor of B(), A() st (for a be
Object of B() holds (G
. a)
= O2(a)) & for a,b be
Object of B() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (G
. f)
= F2(a,b,f)
and
A3: for a,b be
Object of A() st a
= O2(O1) holds A(b)
in
<^a, b^> & (A(b)
" )
in
<^b, a^> & A(b) is
one-to-one
and
A4: for a,b be
Object of B() st b
= O1(O2) holds B(a)
in
<^a, b^> & (B(a)
" )
in
<^b, a^> & B(a) is
one-to-one
and
A5: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (A(b)
* F2(O1,O1,F1))
= (f
* A(a))
and
A6: for a,b be
Object of B() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F1(O2,O2,F2)
* B(a))
= (B(b)
* f);
consider F be
covariant
Functor of A(), B() such that
A7: for a be
Object of A() holds (F
. a)
= O1(a) and
A8: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (F
. f)
= F1(a,b,f) by
A1;
consider G be
covariant
Functor of B(), A() such that
A9: for a be
Object of B() holds (G
. a)
= O2(a) and
A10: for a,b be
Object of B() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (G
. f)
= F2(a,b,f) by
A2;
take F, G;
set GF = (G
* F), I = (
id A());
A11: for a be
Object of A() holds A(a)
in
<^(GF
. a), (I
. a)^> &
<^(I
. a), (GF
. a)^>
<>
{} & for f be
Morphism of (GF
. a), (I
. a) st f
= A(a) holds f is
iso
proof
let a be
Object of A();
A12: (GF
. a)
= (G
. (F
. a)) by
FUNCTOR0: 33
.= O2(.) by
A9
.= O2(O1) by
A7;
A13: (I
. a)
= a by
FUNCTOR0: 29;
then
A14: A(a)
in
<^(GF
. a), (I
. a)^> by
A3,
A12;
A15: (A(a)
" )
in
<^(I
. a), (GF
. a)^> by
A3,
A12,
A13;
A(a) is
one-to-one by
A3,
A12;
hence thesis by
A14,
A15,
Th41;
end;
A16: for a,b be
Object of A() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds for g1 be
Morphism of (GF
. a), (I
. a) st g1
= A(a) holds for g2 be
Morphism of (GF
. b), (I
. b) st g2
= A(b) holds (g2
* (GF
. f))
= ((I
. f)
* g1)
proof
let a,b be
Object of A() such that
A17:
<^a, b^>
<>
{} ;
A18: A(a)
in
<^(GF
. a), (I
. a)^> by
A11;
A19: A(b)
in
<^(GF
. b), (I
. b)^> by
A11;
reconsider g2 = A(b) as
Morphism of (GF
. b), (I
. b) by
A11;
A20:
<^(GF
. a), (GF
. b)^>
<>
{} by
A17,
FUNCTOR0:def 18;
A21:
<^(I
. a), (I
. b)^>
<>
{} by
A17,
FUNCTOR0:def 18;
let f be
Morphism of a, b;
A22: (GF
. f)
= (G
. (F
. f)) by
A17,
FUNCTOR3: 6;
A23: O1(a)
= (F
. a) by
A7;
A24: O1(b)
= (F
. b) by
A7;
A25: F1(a,b,f)
= (F
. f) by
A8,
A17;
<^(F
. a), (F
. b)^>
<>
{} by
A17,
FUNCTOR0:def 18;
then F2(O1,O1,F1)
= (GF
. f) by
A10,
A22,
A23,
A24,
A25;
then (g2
* (GF
. f))
= (A(b)
* F2(O1,O1,F1)) by
A19,
A20,
Th36
.= (f
* A(a)) by
A5,
A17
.= ((I
. f)
* A(a)) by
A17,
FUNCTOR0: 31;
hence thesis by
A18,
A21,
Th36;
end;
ex t be
natural_equivalence of (G
* F), (
id A()) st ((G
* F),(
id A()))
are_naturally_equivalent & for a be
Object of A() holds (t
! a)
= A(a) from
NatEquivalenceLambda(
A11,
A16);
hence ((G
* F),(
id A()))
are_naturally_equivalent ;
set I = (
id B()), FG = (F
* G);
A26: for a be
Object of B() holds B(a)
in
<^(I
. a), (FG
. a)^> &
<^(FG
. a), (I
. a)^>
<>
{} & for f be
Morphism of (I
. a), (FG
. a) st f
= B(a) holds f is
iso
proof
let a be
Object of B();
A27: (FG
. a)
= (F
. (G
. a)) by
FUNCTOR0: 33
.= O1(.) by
A7
.= O1(O2) by
A9;
A28: (I
. a)
= a by
FUNCTOR0: 29;
then
A29: B(a)
in
<^(I
. a), (FG
. a)^> by
A4,
A27;
A30: (B(a)
" )
in
<^(FG
. a), (I
. a)^> by
A4,
A27,
A28;
B(a) is
one-to-one by
A4,
A27;
hence thesis by
A29,
A30,
Th41;
end;
A31: for a,b be
Object of B() st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds for g1 be
Morphism of (I
. a), (FG
. a) st g1
= B(a) holds for g2 be
Morphism of (I
. b), (FG
. b) st g2
= B(b) holds (g2
* (I
. f))
= ((FG
. f)
* g1)
proof
let a,b be
Object of B() such that
A32:
<^a, b^>
<>
{} ;
A33: B(a)
in
<^(I
. a), (FG
. a)^> by
A26;
reconsider g1 = B(a) as
Morphism of (I
. a), (FG
. a) by
A26;
A34: B(b)
in
<^(I
. b), (FG
. b)^> by
A26;
A35:
<^(FG
. a), (FG
. b)^>
<>
{} by
A32,
FUNCTOR0:def 18;
A36:
<^(I
. a), (I
. b)^>
<>
{} by
A32,
FUNCTOR0:def 18;
let f be
Morphism of a, b;
A37: (FG
. f)
= (F
. (G
. f)) by
A32,
FUNCTOR3: 6;
A38: O2(a)
= (G
. a) by
A9;
A39: O2(b)
= (G
. b) by
A9;
A40: F2(a,b,f)
= (G
. f) by
A10,
A32;
<^(G
. a), (G
. b)^>
<>
{} by
A32,
FUNCTOR0:def 18;
then F1(O2,O2,F2)
= (FG
. f) by
A8,
A37,
A38,
A39,
A40;
then ((FG
. f)
* g1)
= (F1(O2,O2,F2)
* B(a)) by
A33,
A35,
Th36
.= (B(b)
* f) by
A6,
A32
.= (B(b)
* (I
. f)) by
A32,
FUNCTOR0: 31;
hence thesis by
A34,
A36,
Th36;
end;
ex t be
natural_equivalence of I, FG st (I,FG)
are_naturally_equivalent & for a be
Object of B() holds (t
! a)
= B(a) from
NatEquivalenceLambda(
A26,
A31);
hence thesis;
end;
begin
definition
let C be
category;
defpred
D[
set,
set] means $1
= ($2
`22 );
defpred
P[
set,
set,
Function] means ex fa,fb be
Object of C, g be
Morphism of fa, fb st fa
= $1 & fb
= $2 &
<^fa, fb^>
<>
{} & for o be
Object of C st
<^o, fa^>
<>
{} holds for h be
Morphism of o, fa holds ($3
.
[h,
[o, fa]])
=
[(g
* h),
[o, fb]];
deffunc
B(
set) = (
Union (
disjoin the
Arrows of C));
A1: for a,b,c be
Element of C, f,g be
Function st
P[a, b, f] &
P[b, c, g] holds
P[a, c, (g
* f)]
proof
let a,b,c be
Element of C, f,g be
Function;
given fa,fb be
Object of C, ff be
Morphism of fa, fb such that
A2: fa
= a and
A3: fb
= b and
A4:
<^fa, fb^>
<>
{} and
A5: for o be
Object of C st
<^o, fa^>
<>
{} holds for h be
Morphism of o, fa holds (f
.
[h,
[o, fa]])
=
[(ff
* h),
[o, fb]];
given ga,gb be
Object of C, gf be
Morphism of ga, gb such that
A6: ga
= b and
A7: gb
= c and
A8:
<^ga, gb^>
<>
{} and
A9: for o be
Object of C st
<^o, ga^>
<>
{} holds for h be
Morphism of o, ga holds (g
.
[h,
[o, ga]])
=
[(gf
* h),
[o, gb]];
reconsider gf as
Morphism of fb, gb by
A3,
A6;
take fa, gb, k = (gf
* ff);
thus fa
= a & gb
= c &
<^fa, gb^>
<>
{} by
A2,
A3,
A4,
A6,
A7,
A8,
ALTCAT_1:def 2;
let o be
Object of C such that
A10:
<^o, fa^>
<>
{} ;
A11:
<^o, fb^>
<>
{} by
A4,
A10,
ALTCAT_1:def 2;
let h be
Morphism of o, fa;
A12: (f
.
[h,
[o, fa]])
=
[(ff
* h),
[o, fb]] by
A5,
A10;
then
[h,
[o, fa]]
in (
dom f) by
FUNCT_1:def 2;
hence ((g
* f)
.
[h,
[o, fa]])
= (g
.
[(ff
* h),
[o, fb]]) by
A12,
FUNCT_1: 13
.=
[(gf
* (ff
* h)),
[o, gb]] by
A3,
A6,
A9,
A11
.=
[(k
* h),
[o, gb]] by
A3,
A4,
A6,
A8,
A10,
ALTCAT_1: 21;
end;
A13: for a be
Element of C, X be
set st for x be
set holds x
in X iff x
in
B(a) &
D[a, x] holds
P[a, a, (
id X)]
proof
let a be
Element of C, X be
set such that
A14: for x be
set holds x
in X iff x
in (
Union (
disjoin the
Arrows of C)) &
D[a, x];
reconsider fa = a as
Object of C;
take fa, fa, g = (
idm fa);
thus fa
= a & fa
= a &
<^fa, fa^>
<>
{} ;
let o be
Object of C such that
A15:
<^o, fa^>
<>
{} ;
let h be
Morphism of o, fa;
A16: (
[h,
[o, fa]]
`1 )
= h;
A17: (
[h,
[o, fa]]
`2 )
=
[o, fa];
A18: (
[h,
[o, fa]]
`22 )
= fa by
MCART_1: 85;
(
dom the
Arrows of C)
=
[:the
carrier of C, the
carrier of C:] by
PARTFUN1:def 2;
then
[o, fa]
in (
dom the
Arrows of C) by
ZFMISC_1:def 2;
then
[h,
[o, fa]]
in (
Union (
disjoin the
Arrows of C)) by
A15,
A16,
A17,
CARD_3: 22;
then
[h,
[o, fa]]
in X by
A14,
A18;
hence ((
id X)
.
[h,
[o, fa]])
=
[h,
[o, fa]] by
FUNCT_1: 18
.=
[(g
* h),
[o, fa]] by
A15,
ALTCAT_1: 20;
end;
::
YELLOW18:def12
func
Concretized C ->
concrete
strict
category means
:
Def12: the
carrier of it
= the
carrier of C & (for a be
Object of it holds for x be
set holds x
in (
the_carrier_of a) iff x
in (
Union (
disjoin the
Arrows of C)) & a
= (x
`22 )) & for a,b be
Element of C, f be
Function holds f
in (the
Arrows of it
. (a,b)) iff f
in (
Funcs ((it
-carrier_of a),(it
-carrier_of b))) & ex fa,fb be
Object of C, g be
Morphism of fa, fb st fa
= a & fb
= b &
<^fa, fb^>
<>
{} & for o be
Object of C st
<^o, fa^>
<>
{} holds for h be
Morphism of o, fa holds (f
.
[h,
[o, fa]])
=
[(g
* h),
[o, fb]];
uniqueness
proof
for C1,C2 be
para-functional
semi-functional
category st the
carrier of C1
= the
carrier of C & (for a be
Object of C1 holds for x be
set holds x
in (
the_carrier_of a) iff x
in
B(a) &
D[a, x]) & (for a,b be
Element of C, f be
Function holds f
in (the
Arrows of C1
. (a,b)) iff f
in (
Funcs ((C1
-carrier_of a),(C1
-carrier_of b))) &
P[a, b, f]) & the
carrier of C2
= the
carrier of C & (for a be
Object of C2 holds for x be
set holds x
in (
the_carrier_of a) iff x
in
B(a) &
D[a, x]) & (for a,b be
Element of C, f be
Function holds f
in (the
Arrows of C2
. (a,b)) iff f
in (
Funcs ((C2
-carrier_of a),(C2
-carrier_of b))) &
P[a, b, f]) holds the AltCatStr of C1
= the AltCatStr of C2 from
ConcreteCategoryUniq3;
hence thesis;
end;
existence
proof
thus ex C9 be
concrete
strict
category st the
carrier of C9
= the
carrier of C & (for a be
Object of C9 holds for x be
set holds x
in (
the_carrier_of a) iff x
in
B(a) &
D[a, x]) & for a,b be
Element of C, f be
Function holds f
in (the
Arrows of C9
. (a,b)) iff f
in (
Funcs ((C9
-carrier_of a),(C9
-carrier_of b))) &
P[a, b, f] from
ConcreteCategoryEx(
A1,
A13);
end;
end
theorem ::
YELLOW18:43
Th43: for A be
category, a be
Object of A, x be
set holds x
in ((
Concretized A)
-carrier_of a) iff ex b be
Object of A, f be
Morphism of b, a st
<^b, a^>
<>
{} & x
=
[f,
[b, a]]
proof
let A be
category, a be
Object of A, x be
set;
set B = (
Concretized A);
reconsider ac = a as
Object of B by
Def12;
A1: x
in (
the_carrier_of ac) iff x
in (
Union (
disjoin the
Arrows of A)) & ac
= (x
`22 ) by
Def12;
A2: (
dom the
Arrows of A)
=
[:the
carrier of A, the
carrier of A:] by
PARTFUN1:def 2;
hereby
assume
A3: x
in (B
-carrier_of a);
then
A4: (x
`2 )
in (
dom the
Arrows of A) by
A1,
CARD_3: 22;
A5: (x
`1 )
in (the
Arrows of A
. (x
`2 )) by
A1,
A3,
CARD_3: 22;
A6: x
=
[(x
`1 ), (x
`2 )] by
A1,
A3,
CARD_3: 22;
consider b,c be
object such that
A7: b
in the
carrier of A and c
in the
carrier of A and
A8: (x
`2 )
=
[b, c] by
A4,
ZFMISC_1:def 2;
reconsider b as
Object of A by
A7;
take b;
reconsider f = (x
`1 ) as
Morphism of b, a by
A1,
A3,
A5,
A6,
A8,
MCART_1: 85;
take f;
thus
<^b, a^>
<>
{} & x
=
[f,
[b, a]] by
A1,
A3,
A5,
A6,
A8,
MCART_1: 85;
end;
given b be
Object of A, f be
Morphism of b, a such that
A9:
<^b, a^>
<>
{} and
A10: x
=
[f,
[b, a]];
A11: (x
`1 )
= f by
A10;
A12: (x
`2 )
=
[b, a] by
A10;
[b, a]
in (
dom the
Arrows of A) by
A2,
ZFMISC_1:def 2;
hence thesis by
A1,
A9,
A10,
A11,
A12,
CARD_3: 22,
MCART_1: 85;
end;
registration
let A be
category;
let a be
Object of A;
cluster ((
Concretized A)
-carrier_of a) -> non
empty;
coherence
proof
[(
idm a),
[a, a]]
in ((
Concretized A)
-carrier_of a) by
Th43;
hence thesis;
end;
end
theorem ::
YELLOW18:44
Th44: for A be
category, a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds ex F be
Function of ((
Concretized A)
-carrier_of a), ((
Concretized A)
-carrier_of b) st F
in (the
Arrows of (
Concretized A)
. (a,b)) & for c be
Object of A, g be
Morphism of c, a st
<^c, a^>
<>
{} holds (F
.
[g,
[c, a]])
=
[(f
* g),
[c, b]]
proof
let A be
category, a,b be
Object of A such that
A1:
<^a, b^>
<>
{} ;
set B = (
Concretized A);
let f be
Morphism of a, b;
defpred
P[
object,
object] means ex o be
Object of A, g be
Morphism of o, a st
<^o, a^>
<>
{} & $1
=
[g,
[o, a]] & $2
=
[(f
* g),
[o, b]];
A2: for x be
object st x
in (B
-carrier_of a) holds ex y be
object st y
in (B
-carrier_of b) &
P[x, y]
proof
let x be
object;
assume x
in (B
-carrier_of a);
then
consider o be
Object of A, g be
Morphism of o, a such that
A3:
<^o, a^>
<>
{} and
A4: x
=
[g,
[o, a]] by
Th43;
take
[(f
* g),
[o, b]];
<^o, b^>
<>
{} by
A1,
A3,
ALTCAT_1:def 2;
hence thesis by
A3,
A4,
Th43;
end;
consider F be
Function such that
A5: (
dom F)
= (B
-carrier_of a) & (
rng F)
c= (B
-carrier_of b) and
A6: for x be
object st x
in (B
-carrier_of a) holds
P[x, (F
. x)] from
FUNCT_1:sch 6(
A2);
A7: F
in (
Funcs ((B
-carrier_of a),(B
-carrier_of b))) by
A5,
FUNCT_2:def 2;
then
reconsider F as
Function of (B
-carrier_of a), (B
-carrier_of b) by
FUNCT_2: 66;
take F;
ex fa,fb be
Object of A, g be
Morphism of fa, fb st fa
= a & fb
= b &
<^fa, fb^>
<>
{} & for o be
Object of A st
<^o, fa^>
<>
{} holds for h be
Morphism of o, fa holds (F
.
[h,
[o, fa]])
=
[(g
* h),
[o, fb]]
proof
take fa = a, fb = b;
reconsider g = f as
Morphism of fa, fb;
take g;
thus fa
= a & fb
= b &
<^fa, fb^>
<>
{} by
A1;
let o be
Object of A such that
A8:
<^o, fa^>
<>
{} ;
let h be
Morphism of o, fa;
[h,
[o, fa]]
in (B
-carrier_of fa) by
A8,
Th43;
then
consider c be
Object of A, k be
Morphism of c, fa such that
<^c, fa^>
<>
{} and
A9:
[h,
[o, fa]]
=
[k,
[c, fa]] and
A10: (F
.
[h,
[o, fa]])
=
[(g
* k),
[c, fb]] by
A6;
[o, fa]
=
[c, fa] by
A9,
XTUPLE_0: 1;
then o
= c by
XTUPLE_0: 1;
hence thesis by
A9,
A10,
XTUPLE_0: 1;
end;
hence F
in (the
Arrows of B
. (a,b)) by
A7,
Def12;
let c be
Object of A, g be
Morphism of c, a;
assume
<^c, a^>
<>
{} ;
then
[g,
[c, a]]
in (B
-carrier_of a) by
Th43;
then
consider o be
Object of A, h be
Morphism of o, a such that
<^o, a^>
<>
{} and
A11:
[g,
[c, a]]
=
[h,
[o, a]] and
A12: (F
.
[g,
[c, a]])
=
[(f
* h),
[o, b]] by
A6;
[c, a]
=
[o, a] by
A11,
XTUPLE_0: 1;
then c
= o by
XTUPLE_0: 1;
hence thesis by
A11,
A12,
XTUPLE_0: 1;
end;
theorem ::
YELLOW18:45
Th45: for A be
category, a,b be
Object of A holds for F1,F2 be
Function st F1
in (the
Arrows of (
Concretized A)
. (a,b)) & F2
in (the
Arrows of (
Concretized A)
. (a,b)) & (F1
.
[(
idm a),
[a, a]])
= (F2
.
[(
idm a),
[a, a]]) holds F1
= F2
proof
let A be
category, a,b be
Object of A;
set B = (
Concretized A);
let F1,F2 be
Function such that
A1: F1
in (the
Arrows of (
Concretized A)
. (a,b)) and
A2: F2
in (the
Arrows of (
Concretized A)
. (a,b)) and
A3: (F1
.
[(
idm a),
[a, a]])
= (F2
.
[(
idm a),
[a, a]]);
A4: F1
in (
Funcs ((B
-carrier_of a),(B
-carrier_of b))) by
A1,
Def12;
A5: F2
in (
Funcs ((B
-carrier_of a),(B
-carrier_of b))) by
A2,
Def12;
A6: (
dom F1)
= (B
-carrier_of a) by
A4,
FUNCT_2: 92;
A7: (
dom F2)
= (B
-carrier_of a) by
A5,
FUNCT_2: 92;
consider fa,fb be
Object of A, f be
Morphism of fa, fb such that
A8: fa
= a and
A9: fb
= b and
A10:
<^fa, fb^>
<>
{} and
A11: for o be
Object of A st
<^o, fa^>
<>
{} holds for h be
Morphism of o, fa holds (F1
.
[h,
[o, fa]])
=
[(f
* h),
[o, fb]] by
A1,
Def12;
consider ga,gb be
Object of A, g be
Morphism of ga, gb such that
A12: ga
= a and
A13: gb
= b and
<^ga, gb^>
<>
{} and
A14: for o be
Object of A st
<^o, ga^>
<>
{} holds for h be
Morphism of o, ga holds (F2
.
[h,
[o, ga]])
=
[(g
* h),
[o, gb]] by
A2,
Def12;
reconsider f, g as
Morphism of a, b by
A8,
A9,
A12,
A13;
A15: (F1
.
[(
idm a),
[a, a]])
=
[(f
* (
idm a)),
[a, b]] by
A8,
A9,
A11;
A16: (f
* (
idm a))
= f by
A8,
A9,
A10,
ALTCAT_1:def 17;
A17: (g
* (
idm a))
= g by
A8,
A9,
A10,
ALTCAT_1:def 17;
(F2
.
[(
idm a),
[a, a]])
=
[(g
* (
idm a)),
[a, b]] by
A12,
A13,
A14;
then
A18: f
= g by
A3,
A15,
A16,
A17,
XTUPLE_0: 1;
now
let x be
object;
assume x
in (B
-carrier_of a);
then
consider bb be
Object of A, ff be
Morphism of bb, a such that
A19:
<^bb, a^>
<>
{} and
A20: x
=
[ff,
[bb, a]] by
Th43;
thus (F1
. x)
=
[(f
* ff),
[bb, b]] by
A8,
A9,
A11,
A19,
A20
.= (F2
. x) by
A12,
A13,
A14,
A18,
A19,
A20;
end;
hence thesis by
A6,
A7;
end;
scheme ::
YELLOW18:sch23
NonUniqMSFunctionEx { I() ->
set , A,B() ->
ManySortedSet of I() , P[
object,
object,
object] } :
ex F be
ManySortedFunction of A(), B() st for i,x be
object st i
in I() & x
in (A()
. i) holds ((F
. i)
. x)
in (B()
. i) & P[i, x, ((F
. i)
. x)]
provided
A1: for i,x be
object st i
in I() & x
in (A()
. i) holds ex y be
object st y
in (B()
. i) & P[i, x, y];
defpred
P[
object,
object] means ex f be
Function of (A()
. $1), (B()
. $1) st $2
= f & for x be
set st x
in (A()
. $1) holds (f
. x)
in (B()
. $1) & P[$1, x, (f
. x)];
A2: for i be
object st i
in I() holds ex y be
object st
P[i, y]
proof
let i be
object such that
A3: i
in I();
defpred
Q[
object,
object] means $2
in (B()
. i) & P[i, $1, $2];
A4:
now
let x be
object;
assume x
in (A()
. i);
then ex y be
object st y
in (B()
. i) & P[i, x, y] by
A1,
A3;
hence ex y be
object st y
in (B()
. i) &
Q[x, y];
end;
consider f be
Function such that
A5: (
dom f)
= (A()
. i) & (
rng f)
c= (B()
. i) and
A6: for x be
object st x
in (A()
. i) holds
Q[x, (f
. x)] from
FUNCT_1:sch 6(
A4);
reconsider f as
Function of (A()
. i), (B()
. i) by
A5,
FUNCT_2: 2;
take f, f;
thus thesis by
A6;
end;
consider F be
Function such that
A7: (
dom F)
= I() and
A8: for i be
object st i
in I() holds
P[i, (F
. i)] from
CLASSES1:sch 1(
A2);
reconsider F as
ManySortedSet of I() by
A7,
PARTFUN1:def 2,
RELAT_1:def 18;
now
let i be
object;
assume i
in I();
then ex f be
Function of (A()
. i), (B()
. i) st (F
. i)
= f & for x be
set st x
in (A()
. i) holds (f
. x)
in (B()
. i) & P[i, x, (f
. x)] by
A8;
hence (F
. i) is
Function of (A()
. i), (B()
. i);
end;
then
reconsider F as
ManySortedFunction of A(), B() by
PBOOLE:def 15;
take F;
let i,x be
object;
assume i
in I();
then ex f be
Function of (A()
. i), (B()
. i) st (F
. i)
= f & for x be
set st x
in (A()
. i) holds (f
. x)
in (B()
. i) & P[i, x, (f
. x)] by
A8;
hence thesis;
end;
definition
let A be
category;
set B = (
Concretized A);
::
YELLOW18:def13
func
Concretization A ->
covariant
strict
Functor of A, (
Concretized A) means
:
Def13: (for a be
Object of A holds (it
. a)
= a) & for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds ((it
. f)
.
[(
idm a),
[a, a]])
=
[f,
[a, b]];
uniqueness
proof
let F,G be
covariant
strict
Functor of A, B such that
A1: for a be
Object of A holds (F
. a)
= a and
A2: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds ((F
. f)
.
[(
idm a),
[a, a]])
=
[f,
[a, b]] and
A3: for a be
Object of A holds (G
. a)
= a and
A4: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds ((G
. f)
.
[(
idm a),
[a, a]])
=
[f,
[a, b]];
A5:
now
let a be
Object of A;
thus (F
. a)
= a by
A1
.= (G
. a) by
A3;
end;
now
let a,b be
Object of A;
assume
A6:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
A7: ((F
. f)
.
[(
idm a),
[a, a]])
=
[f,
[a, b]] by
A2,
A6;
A8: ((G
. f)
.
[(
idm a),
[a, a]])
=
[f,
[a, b]] by
A4,
A6;
A9:
<^(F
. a), (F
. b)^>
<>
{} by
A6,
FUNCTOR0:def 18;
A10: (F
. a)
= a by
A1;
A11: (F
. b)
= b by
A1;
A12: (G
. a)
= a by
A3;
(G
. b)
= b by
A3;
hence (F
. f)
= (G
. f) by
A7,
A8,
A9,
A10,
A11,
A12,
Th45;
end;
hence thesis by
A5,
Th1;
end;
existence
proof
deffunc
O(
set) = $1;
A13: the
carrier of B
= the
carrier of A by
Def12;
A14: for a be
Object of A holds
O(a) is
Object of B by
Def12;
reconsider AA = the
Arrows of B as
ManySortedSet of
[:the
carrier of A, the
carrier of A:] by
A13;
defpred
P[
object,
object,
object] means ex a,b be
Object of A, f be
Morphism of a, b, G be
Function of (B
-carrier_of a), (B
-carrier_of b) st $1
=
[a, b] & $2
= f & $3
= G & for c be
Object of A, g be
Morphism of c, a st
<^c, a^>
<>
{} holds (G
.
[g,
[c, a]])
=
[(f
* g),
[c, b]];
A15: for i,x be
object st i
in
[:the
carrier of A, the
carrier of A:] & x
in (the
Arrows of A
. i) holds ex y be
object st y
in (AA
. i) &
P[i, x, y]
proof
let i,x be
object;
assume i
in
[:the
carrier of A, the
carrier of A:];
then
consider a,b be
object such that
A16: a
in the
carrier of A and
A17: b
in the
carrier of A and
A18: i
=
[a, b] by
ZFMISC_1:def 2;
reconsider a, b as
Object of A by
A16,
A17;
assume
A19: x
in (the
Arrows of A
. i);
then
reconsider f = x as
Morphism of a, b by
A18;
consider G be
Function of (B
-carrier_of a), (B
-carrier_of b) such that
A20: G
in (AA
. (a,b)) and
A21: for c be
Object of A, g be
Morphism of c, a st
<^c, a^>
<>
{} holds (G
.
[g,
[c, a]])
=
[(f
* g),
[c, b]] by
A18,
A19,
Th44;
take G;
thus thesis by
A18,
A20,
A21;
end;
consider F be
ManySortedFunction of the
Arrows of A, AA such that
A22: for i,x be
object st i
in
[:the
carrier of A, the
carrier of A:] & x
in (the
Arrows of A
. i) holds ((F
. i)
. x)
in (AA
. i) &
P[i, x, ((F
. i)
. x)] from
NonUniqMSFunctionEx(
A15);
deffunc
F(
set,
set,
set) = ((F
.
[$1, $2])
. $3);
A23: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds
F(a,b,f)
in (the
Arrows of B
. (
O(a),
O(b)))
proof
let a,b be
Object of A such that
A24:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
[a, b]
in
[:the
carrier of A, the
carrier of A:] by
ZFMISC_1:def 2;
hence thesis by
A22,
A24;
end;
A25: for a,b,c be
Object of A st
<^a, b^>
<>
{} &
<^b, c^>
<>
{} holds for f be
Morphism of a, b, g be
Morphism of b, c holds for a9,b9,c9 be
Object of B st a9
=
O(a) & b9
=
O(b) & c9
=
O(c) holds for f9 be
Morphism of a9, b9, g9 be
Morphism of b9, c9 st f9
=
F(a,b,f) & g9
=
F(b,c,g) holds
F(a,c,*)
= (g9
* f9)
proof
let a,b,c be
Object of A such that
A26:
<^a, b^>
<>
{} and
A27:
<^b, c^>
<>
{} ;
let f be
Morphism of a, b, g be
Morphism of b, c;
let a9,b9,c9 be
Object of B such that
A28: a9
= a and
A29: b9
= b and
A30: c9
= c;
let f9 be
Morphism of a9, b9, g9 be
Morphism of b9, c9 such that
A31: f9
= ((F
.
[a, b])
. f) and
A32: g9
= ((F
.
[b, c])
. g);
A33:
[a, b]
in
[:the
carrier of A, the
carrier of A:] by
ZFMISC_1:def 2;
then
consider a1,b1 be
Object of A, f1 be
Morphism of a1, b1, G1 be
Function of (B
-carrier_of a1), (B
-carrier_of b1) such that
A34:
[a, b]
=
[a1, b1] and
A35: f
= f1 and
A36: ((F
.
[a, b])
. f)
= G1 and
A37: for c be
Object of A, g be
Morphism of c, a1 st
<^c, a1^>
<>
{} holds (G1
.
[g,
[c, a1]])
=
[(f1
* g),
[c, b1]] by
A22,
A26;
A38:
[b, c]
in
[:the
carrier of A, the
carrier of A:] by
ZFMISC_1:def 2;
then
consider b2,c2 be
Object of A, g2 be
Morphism of b2, c2, G2 be
Function of (B
-carrier_of b2), (B
-carrier_of c2) such that
A39:
[b, c]
=
[b2, c2] and
A40: g
= g2 and
A41: ((F
.
[b, c])
. g)
= G2 and
A42: for c be
Object of A, g be
Morphism of c, b2 st
<^c, b2^>
<>
{} holds (G2
.
[g,
[c, b2]])
=
[(g2
* g),
[c, c2]] by
A22,
A27;
A43:
<^a, c^>
<>
{} by
A26,
A27,
ALTCAT_1:def 2;
[a, c]
in
[:the
carrier of A, the
carrier of A:] by
ZFMISC_1:def 2;
then
consider a3,c3 be
Object of A, h3 be
Morphism of a3, c3, G3 be
Function of (B
-carrier_of a3), (B
-carrier_of c3) such that
A44:
[a, c]
=
[a3, c3] and
A45: (g
* f)
= h3 and
A46: ((F
.
[a, c])
. (g
* f))
= G3 and
A47: for c be
Object of A, g be
Morphism of c, a3 st
<^c, a3^>
<>
{} holds (G3
.
[g,
[c, a3]])
=
[(h3
* g),
[c, c3]] by
A22,
A43;
A48: ((F
.
[a, b])
. f)
in
<^a9, b9^> by
A22,
A26,
A28,
A29,
A33;
A49: ((F
.
[b, c])
. g)
in
<^b9, c9^> by
A22,
A27,
A29,
A30,
A38;
A50: a
= a1 by
A34,
XTUPLE_0: 1;
A51: b
= b1 by
A34,
XTUPLE_0: 1;
A52: b
= b2 by
A39,
XTUPLE_0: 1;
A53: c
= c2 by
A39,
XTUPLE_0: 1;
A54: a
= a3 by
A44,
XTUPLE_0: 1;
A55: c
= c3 by
A44,
XTUPLE_0: 1;
reconsider G1 as
Function of (B
-carrier_of a), (B
-carrier_of b) by
A34,
A50,
XTUPLE_0: 1;
reconsider G2 as
Function of (B
-carrier_of b), (B
-carrier_of c) by
A39,
A52,
XTUPLE_0: 1;
reconsider G3 as
Function of (B
-carrier_of a), (B
-carrier_of c) by
A44,
A54,
XTUPLE_0: 1;
now
let x be
Element of (B
-carrier_of a);
consider bb be
Object of A, ff be
Morphism of bb, a such that
A56:
<^bb, a^>
<>
{} and
A57: x
=
[ff,
[bb, a]] by
Th43;
A58:
<^bb, b^>
<>
{} by
A26,
A56,
ALTCAT_1:def 2;
thus (G3
. x)
=
[((g
* f)
* ff),
[bb, c]] by
A45,
A47,
A54,
A55,
A56,
A57
.=
[(g
* (f
* ff)),
[bb, c]] by
A26,
A27,
A56,
ALTCAT_1: 21
.= (G2
.
[(f
* ff),
[bb, b]]) by
A40,
A42,
A52,
A53,
A58
.= (G2
. (G1
. x)) by
A35,
A37,
A50,
A51,
A56,
A57
.= ((G2
* G1)
. x) by
FUNCT_2: 15;
end;
then G3
= (G2
* G1);
hence thesis by
A31,
A32,
A36,
A41,
A46,
A48,
A49,
Th36;
end;
A59: for a be
Object of A, a9 be
Object of B st a9
=
O(a) holds
F(a,a,idm)
= (
idm a9)
proof
let a be
Object of A, a9 be
Object of B such that
A60: a9
= a;
[a, a]
in
[:the
carrier of A, the
carrier of A:] by
ZFMISC_1:def 2;
then
consider c,b be
Object of A, f be
Morphism of c, b, G be
Function of (B
-carrier_of c), (B
-carrier_of b) such that
A61:
[a, a]
=
[c, b] and
A62: (
idm a)
= f and
A63: ((F
.
[a, a])
. (
idm a))
= G and
A64: for d be
Object of A, g be
Morphism of d, c st
<^d, c^>
<>
{} holds (G
.
[g,
[d, c]])
=
[(f
* g),
[d, b]] by
A22;
A65: (
idm a9)
= (
id (
the_carrier_of a9)) by
Def10;
A66: a
= c by
A61,
XTUPLE_0: 1;
A67: a
= b by
A61,
XTUPLE_0: 1;
now
let x be
Element of (
the_carrier_of a9);
consider bb be
Object of A, ff be
Morphism of bb, a such that
A68:
<^bb, a^>
<>
{} and
A69: x
=
[ff,
[bb, a]] by
A60,
Th43;
thus (G
. x)
=
[((
idm a)
* ff),
[bb, a]] by
A62,
A64,
A66,
A67,
A68,
A69
.= x by
A68,
A69,
ALTCAT_1: 20
.= ((
id (
the_carrier_of a9))
. x);
end;
hence thesis by
A60,
A63,
A65,
A66,
A67,
FUNCT_2: 63;
end;
consider FF be
covariant
strict
Functor of A, B such that
A70: for a be
Object of A holds (FF
. a)
=
O(a) and
A71: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (FF
. f)
=
F(a,b,f) from
CovariantFunctorLambda(
A14,
A23,
A25,
A59);
take FF;
thus for a be
Object of A holds (FF
. a)
= a by
A70;
let a,b be
Object of A such that
A72:
<^a, b^>
<>
{} ;
let f be
Morphism of a, b;
[a, b]
in
[:the
carrier of A, the
carrier of A:] by
ZFMISC_1:def 2;
then
consider a9,b9 be
Object of A, f9 be
Morphism of a9, b9, G be
Function of (B
-carrier_of a9), (B
-carrier_of b9) such that
A73:
[a, b]
=
[a9, b9] and
A74: f
= f9 and
A75: ((F
.
[a, b])
. f)
= G and
A76: for c be
Object of A, g be
Morphism of c, a9 st
<^c, a9^>
<>
{} holds (G
.
[g,
[c, a9]])
=
[(f9
* g),
[c, b9]] by
A22,
A72;
A77: G
= (FF
. f) by
A71,
A72,
A75;
A78: a
= a9 by
A73,
XTUPLE_0: 1;
b
= b9 by
A73,
XTUPLE_0: 1;
hence ((FF
. f)
.
[(
idm a),
[a, a]])
=
[(f
* (
idm a)),
[a, b]] by
A74,
A76,
A77,
A78
.=
[f,
[a, b]] by
A72,
ALTCAT_1:def 17;
end;
end
registration
let A be
category;
cluster (
Concretization A) ->
bijective;
coherence
proof
set B = (
Concretized A);
set FF = (
Concretization A);
deffunc
O(
set) = $1;
A1: for a be
Object of A holds (FF
. a)
=
O(a) by
Def13;
deffunc
F(
Object of A,
Object of A,
Morphism of $1, $2) = (FF
. $3);
A2: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds (FF
. f)
=
F(a,b,f);
A3: for a,b be
Object of A st
O(a)
=
O(b) holds a
= b;
A4: for a,b be
Object of A st
<^a, b^>
<>
{} holds for f,g be
Morphism of a, b st
F(a,b,f)
=
F(a,b,g) holds f
= g
proof
let a,b be
Object of A such that
A5:
<^a, b^>
<>
{} ;
let f,g be
Morphism of a, b;
A6: ((FF
. f)
.
[(
idm a),
[a, a]])
=
[f,
[a, b]] by
A5,
Def13;
((FF
. g)
.
[(
idm a),
[a, a]])
=
[g,
[a, b]] by
A5,
Def13;
hence thesis by
A6,
XTUPLE_0: 1;
end;
A7: for a,b be
Object of B st
<^a, b^>
<>
{} holds for f be
Morphism of a, b holds ex c,d be
Object of A, g be
Morphism of c, d st a
=
O(c) & b
=
O(d) &
<^c, d^>
<>
{} & f
=
F(c,d,g)
proof
let a,b be
Object of B such that
A8:
<^a, b^>
<>
{} ;
reconsider c = a, d = b as
Object of A by
Def12;
let f be
Morphism of a, b;
take c, d;
consider fa,fb be
Object of A, g be
Morphism of fa, fb such that
A9: fa
= c and
A10: fb
= d and
A11:
<^fa, fb^>
<>
{} and
A12: for o be
Object of A st
<^o, fa^>
<>
{} holds for h be
Morphism of o, fa holds (f
.
[h,
[o, fa]])
=
[(g
* h),
[o, fb]] by
A8,
Def12;
reconsider g as
Morphism of c, d by
A9,
A10;
take g;
A13: ((FF
. g)
.
[(
idm c),
[c, c]])
=
[g,
[c, d]] by
A9,
A10,
A11,
Def13;
(g
* (
idm c))
= g by
A9,
A10,
A11,
ALTCAT_1:def 17;
then
A14: ((FF
. g)
.
[(
idm c),
[c, c]])
= (f
.
[(
idm c),
[c, c]]) by
A9,
A10,
A12,
A13;
A15: (FF
. c)
= a by
Def13;
(FF
. d)
= b by
Def13;
hence thesis by
A8,
A9,
A10,
A11,
A14,
A15,
Th45;
end;
thus thesis from
CoBijectiveSch(
A1,
A2,
A3,
A4,
A7);
end;
end
::$Notion-Name
theorem ::
YELLOW18:46
for A be
category holds (A,(
Concretized A))
are_isomorphic
proof
let A be
category;
take (
Concretization A);
thus thesis;
end;