Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Andrzej Trybulec
- Received June 5, 1992
- MML identifier: ISOCAT_2
- [
Mizar article,
MML identifier index
]
environ
vocabulary FUNCT_1, FUNCT_2, FUNCT_5, RELAT_1, BOOLE, FUNCT_3, CAT_1,
NATTRA_1, CAT_2, FINSEQ_2, FUNCOP_1, PARTFUN1, BORSUK_1, ISOCAT_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1,
FUNCT_2, FUNCT_3, FUNCT_5, FRAENKEL, CAT_1, CAT_2, NATTRA_1, ISOCAT_1;
constructors DOMAIN_1, ISOCAT_1, MEMBERED, XBOOLE_0;
clusters RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;
begin :: Preliminaries
definition let A,B,C be non empty set;
let f be Function of A, Funcs(B,C);
redefine func uncurry f -> Function of [:A,B:],C;
end;
theorem :: ISOCAT_2:1
for A,B,C being non empty set, f being Function of A,Funcs(B,C)
holds curry uncurry f = f;
theorem :: ISOCAT_2:2
for A,B,C being non empty set, f being Function of A, Funcs(B,C)
for a being Element of A, b being Element of B
holds (uncurry f).[a,b] = f.a.b;
theorem :: ISOCAT_2:3
for x being set, A being non empty set
for f,g being Function of {x}, A st f.x = g.x holds f = g;
theorem :: ISOCAT_2:4
for A,B being non empty set, x being Element of A,
f being Function of A,B holds f.x in rng f;
theorem :: ISOCAT_2:5
for A,B,C being non empty set, f,g being Function of A,[:B,C:]
st pr1(B,C)*f = pr1(B,C)*g & pr2(B,C)*f = pr2(B,C)*g
holds f = g;
:: Auxiliary category theory facts
reserve A,B,C for Category,
F,F1 for Functor of A,B;
theorem :: ISOCAT_2:6
for f being Morphism of A holds (id cod f)*f = f;
theorem :: ISOCAT_2:7
for f being Morphism of A holds f*(id dom f) = f;
reserve o,m for set;
reserve t for natural_transformation of F,F1;
theorem :: ISOCAT_2:8
o is Object of Functors(A,B) iff o is Functor of A,B;
theorem :: ISOCAT_2:9
for f being Morphism of Functors(A,B)
ex F1,F2 being Functor of A,B,
t being natural_transformation of F1,F2 st
F1 is_naturally_transformable_to F2 &
dom f = F1 & cod f = F2 & f = [[F1,F2],t];
begin :: The isomorphism between A^1 and A
definition let A,B;
let a be Object of A;
func a |-> B -> Functor of Functors(A,B), B means
:: ISOCAT_2:def 1
for F1,F2 being Functor of A,B, t being natural_transformation of F1,F2
st F1 is_naturally_transformable_to F2
holds it.[[F1,F2],t] = t.a;
end;
canceled;
theorem :: ISOCAT_2:11
Functors(1Cat(o,m),A) ~= A;
begin :: The isomorphism between C^(A x B) and C^(A^B)
theorem :: ISOCAT_2:12
for F being Functor of [:A,B:],C, a being Object of A, b being Object of B
holds (F?-a).b = F.[a,b];
theorem :: ISOCAT_2:13
for a1,a2 being Object of A, b1,b2 being Object of B
holds Hom(a1,a2) <> {} & Hom(b1,b2) <> {} iff Hom([a1,b1],[a2,b2]) <> {};
theorem :: ISOCAT_2:14
for a1,a2 being Object of A, b1,b2 being Object of B
st Hom([a1,b1],[a2,b2]) <> {}
for f being (Morphism of A), g being Morphism of B
holds [f,g] is Morphism of [a1,b1],[a2,b2] iff
f is Morphism of a1,a2 & g is Morphism of b1,b2;
theorem :: ISOCAT_2:15
for F1,F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2
for t being natural_transformation of F1,F2, a being Object of A holds
F1?-a is_naturally_transformable_to F2?-a &
(curry t).a is natural_transformation of F1?-a,F2?-a;
definition let A,B,C; let F be Functor of [:A,B:],C;
let f be Morphism of A;
func curry(F,f) -> Function of the Morphisms of B,the Morphisms of C equals
:: ISOCAT_2:def 2
(curry F).f;
end;
theorem :: ISOCAT_2:16
for a1,a2 being Object of A, b1,b2 being Object of B,
f being (Morphism of A), g being Morphism of B
st f in Hom(a1,a2) & g in Hom(b1,b2)
holds [f,g] in Hom([a1,b1],[a2,b2]);
theorem :: ISOCAT_2:17
for F being Functor of [:A,B:], C
for a,b being Object of A st Hom(a,b) <> {}
for f being Morphism of a,b holds
F?-a is_naturally_transformable_to F?-b &
curry(F,f)*the Id of B is natural_transformation of F?-a,F?-b;
definition let A,B,C; let F be Functor of [:A,B:],C;
let f be Morphism of A;
func F?-f -> natural_transformation of F?-dom f, F?-cod f equals
:: ISOCAT_2:def 3
curry(F,f)*the Id of B;
end;
theorem :: ISOCAT_2:18
for F being Functor of [:A,B:],C, g being Morphism of A
holds F?-dom(g) is_naturally_transformable_to F?-cod(g);
theorem :: ISOCAT_2:19
for F being Functor of [:A,B:],C, f being (Morphism of A), b being Object of B
holds (F?-f).b = F.[f, id b];
theorem :: ISOCAT_2:20
for F being Functor of [:A,B:],C, a being Object of A
holds id(F?-a) = F?-id a;
theorem :: ISOCAT_2:21
for F being Functor of [:A,B:],C, g,f being Morphism of A st dom g = cod f
for t being natural_transformation of F?-dom f, F?-dom g st t = F?-f
holds F?-(g*f) = (F?-g)`*`t;
definition let A,B,C;
let F be Functor of [:A,B:],C;
func export F -> Functor of A, Functors(B,C) means
:: ISOCAT_2:def 4
for f being Morphism of A holds it.f =[[F?-dom f,F?-cod f],F?-f];
end;
canceled 2;
theorem :: ISOCAT_2:24
for F being Functor of [:A,B:],C, a being Object of A
holds (export F).a = F?-a;
theorem :: ISOCAT_2:25
for F being Functor of [:A,B:],C, a being Object of A
holds (export F).a is Functor of B,C;
theorem :: ISOCAT_2:26
for F1,F2 being Functor of [:A,B:],C holds
export F1 = export F2 implies F1 = F2;
theorem :: ISOCAT_2:27
for F1,F2 being Functor of [:A,B:], C st
F1 is_naturally_transformable_to F2
for t being natural_transformation of F1,F2
holds export F1 is_naturally_transformable_to export F2 &
ex G being natural_transformation of export F1, export F2 st
for s being Function of
[:the Objects of A, the Objects of B:], the Morphisms of C st t = s
for a being Object of A
holds G.a = [[(export F1).a,(export F2).a],(curry s).a];
definition let A,B,C; let F1,F2 be Functor of [:A,B:],C such that
F1 is_naturally_transformable_to F2;
let t be natural_transformation of F1,F2;
func export t -> natural_transformation of export F1, export F2 means
:: ISOCAT_2:def 5
for s being Function of
[:the Objects of A, the Objects of B:], the Morphisms of C st t = s
for a being Object of A
holds it.a = [[(export F1).a,(export F2).a],(curry s).a];
end;
theorem :: ISOCAT_2:28
for F being Functor of [:A,B:],C holds id export F = export id F;
theorem :: ISOCAT_2:29
for F1,F2,F3 being Functor of [:A,B:],C st
F1 is_naturally_transformable_to F2 &
F2 is_naturally_transformable_to F3
for t1 being natural_transformation of F1,F2,
t2 being natural_transformation of F2,F3
holds export(t2`*`t1) = (export t2)`*`(export t1);
theorem :: ISOCAT_2:30
for F1,F2 being Functor of [:A,B:],C
st F1 is_naturally_transformable_to F2
for t1,t2 being natural_transformation of F1,F2 holds
export t1 = export t2 implies t1 = t2;
theorem :: ISOCAT_2:31
for G being Functor of A, Functors(B,C)
ex F being Functor of [:A,B:],C st G = export F;
theorem :: ISOCAT_2:32
for F1,F2 being Functor of [:A,B:],C st
export F1 is_naturally_transformable_to export F2
for t being natural_transformation of export F1, export F2
holds F1 is_naturally_transformable_to F2 &
ex u being natural_transformation of F1,F2 st t = export u;
definition let A,B,C;
func export(A,B,C)-> Functor of Functors([:A,B:],C),Functors(A,Functors(B,C))
means
:: ISOCAT_2:def 6
for F1,F2 being Functor of [:A,B:], C
st F1 is_naturally_transformable_to F2
for t being natural_transformation of F1,F2
holds it.[[F1,F2],t] = [[export F1, export F2],export t];
end;
theorem :: ISOCAT_2:33
export(A,B,C) is_an_isomorphism;
theorem :: ISOCAT_2:34
Functors([:A,B:],C) ~= Functors(A,Functors(B,C));
begin :: The isomorphism between (B x C)^A and B^A x C^A
theorem :: ISOCAT_2:35
for F1,F2 being Functor of A,B, G being Functor of B,C
st F1 is_naturally_transformable_to F2
for t being natural_transformation of F1,F2 holds
G*t = G*(t qua Function);
definition let A,B;
redefine func pr1(A,B) -> Functor of [:A,B:], A;
func pr2(A,B) -> Functor of [:A,B:], B;
end;
definition let A,B,C;
let F be Functor of A,B, G be Functor of A,C;
redefine func <:F,G:> -> Functor of A, [:B,C:];
end;
definition let A,B,C; let F be Functor of A, [:B,C:];
func Pr1 F -> Functor of A,B equals
:: ISOCAT_2:def 7
pr1(B,C)*F;
func Pr2 F -> Functor of A,C equals
:: ISOCAT_2:def 8
pr2(B,C)*F;
end;
theorem :: ISOCAT_2:36
for F being Functor of A,B, G being Functor of A,C holds
Pr1<:F,G:> = F & Pr2<:F,G:> = G;
theorem :: ISOCAT_2:37
for F,G being Functor of A, [:B,C:] st Pr1 F = Pr1 G & Pr2 F = Pr2 G
holds F = G;
definition let A,B,C; let F1,F2 be Functor of A, [:B,C:];
let t be natural_transformation of F1,F2;
func Pr1 t -> natural_transformation of Pr1 F1, Pr1 F2 equals
:: ISOCAT_2:def 9
pr1(B,C)*t;
func Pr2 t -> natural_transformation of Pr2 F1, Pr2 F2 equals
:: ISOCAT_2:def 10
pr2(B,C)*t;
end;
theorem :: ISOCAT_2:38
for F,G being Functor of A, [:B,C:] st
F is_naturally_transformable_to G
holds Pr1 F is_naturally_transformable_to Pr1 G
& Pr2 F is_naturally_transformable_to Pr2 G;
theorem :: ISOCAT_2:39
for F1,F2,G1,G2 being Functor of A, [:B,C:] st
F1 is_naturally_transformable_to F2 &
G1 is_naturally_transformable_to G2
for s being natural_transformation of F1,F2,
t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t
holds s = t;
theorem :: ISOCAT_2:40
for F being Functor of A, [:B,C:]
holds id Pr1 F = Pr1 id F & id Pr2 F = Pr2 id F;
theorem :: ISOCAT_2:41
for F,G,H being Functor of A, [:B,C:] st
F is_naturally_transformable_to G &
G is_naturally_transformable_to H
for s being natural_transformation of F,G,
t being natural_transformation of G,H
holds Pr1 t`*`s = (Pr1 t)`*`Pr1 s & Pr2 t`*`s = (Pr2 t)`*`Pr2 s;
theorem :: ISOCAT_2:42
for F being Functor of A,B, G being Functor of A,C
for a,b being Object of A st Hom(a,b) <> {}
for f being Morphism of a,b holds <:F,G:>.f = [F.f,G.f];
theorem :: ISOCAT_2:43
for F being Functor of A,B, G being Functor of A,C
for a being Object of A
holds <:F,G:>.a = [F.a,G.a];
theorem :: ISOCAT_2:44
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st
F1 is_transformable_to G1 & F2 is_transformable_to G2
holds <:F1,F2:> is_transformable_to <:G1,G2:>;
definition let A,B,C;
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
F1 is_transformable_to G1 & F2 is_transformable_to G2;
let t1 be transformation of F1,G1, t2 be transformation of F2,G2;
func <:t1,t2:> -> transformation of <:F1,F2:>,<:G1,G2:> equals
:: ISOCAT_2:def 11
<:t1,t2:>;
end;
theorem :: ISOCAT_2:45
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C
st F1 is_transformable_to G1 & F2 is_transformable_to G2
for t1 being transformation of F1,G1, t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:>.a = [t1.a,t2.a];
theorem :: ISOCAT_2:46
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st
F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2
holds <:F1,F2:> is_naturally_transformable_to <:G1,G2:>;
definition let A,B,C;
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
F1 is_naturally_transformable_to G1 and
F2 is_naturally_transformable_to G2;
let t1 be natural_transformation of F1,G1,
t2 be natural_transformation of F2,G2;
func <:t1,t2:> -> natural_transformation of <:F1,F2:>,<:G1,G2:> equals
:: ISOCAT_2:def 12
<:t1,t2:>;
end;
theorem :: ISOCAT_2:47
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st
F1 is_naturally_transformable_to G1 &
F2 is_naturally_transformable_to G2
for t1 being natural_transformation of F1,G1,
t2 being natural_transformation of F2,G2 holds
Pr1<:t1,t2:> = t1 & Pr2<:t1,t2:> = t2;
definition let A,B,C;
func distribute(A,B,C) ->
Functor of Functors(A,[:B,C:]), [:Functors(A,B),Functors(A,C):] means
:: ISOCAT_2:def 13
for F1,F2 being Functor of A,[:B,C:]
st F1 is_naturally_transformable_to F2
for t being natural_transformation of F1,F2
holds it.[[F1,F2],t] =
[[[Pr1 F1, Pr1 F2],Pr1 t],[[Pr2 F1, Pr2 F2],Pr2 t]];
end;
theorem :: ISOCAT_2:48
distribute(A,B,C) is_an_isomorphism;
theorem :: ISOCAT_2:49
Functors(A,[:B,C:]) ~= [:Functors(A,B),Functors(A,C):];
Back to top