Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Artur Kornilowicz
- Received January 21, 1998
- MML identifier: FUNCTOR3
- [
Mizar article,
MML identifier index
]
environ
vocabulary RELAT_2, BINOP_1, ALTCAT_1, FUNCTOR0, MSUALG_6, FUNCOP_1, CAT_1,
RELAT_1, BOOLE, FUNCT_1, MSUALG_3, PBOOLE, PRALG_1, NATTRA_1, QC_LANG1,
FUNCTOR2, SEQ_1, ALTCAT_3, CAT_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
STRUCT_0, BINOP_1, FUNCOP_1, PBOOLE, MSUALG_1, MSUALG_3, ALTCAT_1,
ALTCAT_2, ALTCAT_3, FUNCTOR0, FUNCTOR2;
constructors ALTCAT_3, FUNCTOR2;
clusters STRUCT_0, ALTCAT_1, ALTCAT_4, FUNCTOR0, FUNCTOR2, PRALG_1, FUNCT_1,
RELSET_1, SUBSET_1, MSUALG_1, FUNCT_2, XBOOLE_0;
requirements SUBSET, BOOLE;
begin :: Preliminaries
definition
cluster transitive associative with_units strict (non empty AltCatStr);
end;
definition let A be non empty transitive AltCatStr,
B be with_units (non empty AltCatStr);
cluster strict comp-preserving comp-reversing Covariant Contravariant
feasible FunctorStr over A, B;
end;
definition let A be with_units transitive (non empty AltCatStr),
B be with_units (non empty AltCatStr);
cluster strict comp-preserving comp-reversing Covariant Contravariant
feasible id-preserving FunctorStr over A, B;
end;
definition let A be with_units transitive (non empty AltCatStr),
B be with_units (non empty AltCatStr);
cluster strict feasible covariant contravariant Functor of A, B;
end;
theorem :: FUNCTOR3:1
for C being category, o1, o2, o3, o4 being object of C
for a being Morphism of o1, o2, b being Morphism of o2, o3
for c being Morphism of o1, o4, d being Morphism of o4, o3 st
b*a = d*c & a*(a") = idm o2 & d"*d = idm o4 & <^o1,o2^> <> {} &
<^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {}
holds c*(a") = d"*b;
theorem :: FUNCTOR3:2
for A being non empty transitive AltCatStr
for B, C being with_units (non empty AltCatStr)
for F being feasible Covariant FunctorStr over A, B
for G being FunctorStr over B, C, o, o1 being object of A
holds Morph-Map(G*F,o,o1) = Morph-Map(G,F.o,F.o1)*Morph-Map(F,o,o1);
theorem :: FUNCTOR3:3
for A being non empty transitive AltCatStr
for B, C being with_units (non empty AltCatStr)
for F being feasible Contravariant FunctorStr over A, B
for G being FunctorStr over B, C, o, o1 being object of A
holds Morph-Map(G*F,o,o1) = Morph-Map(G,F.o1,F.o)*Morph-Map(F,o,o1);
theorem :: FUNCTOR3:4
for A being non empty transitive AltCatStr
for B being with_units (non empty AltCatStr)
for F being feasible FunctorStr over A, B holds
(id B) * F = the FunctorStr of F;
theorem :: FUNCTOR3:5
for A being with_units transitive (non empty AltCatStr)
for B being with_units (non empty AltCatStr)
for F being feasible FunctorStr over A, B holds
F * (id A) = the FunctorStr of F;
reserve A for non empty AltCatStr,
B, C for non empty reflexive AltCatStr,
F for feasible Covariant FunctorStr over A, B,
G for feasible Covariant FunctorStr over B, C,
M for feasible Contravariant FunctorStr over A, B,
N for feasible Contravariant FunctorStr over B, C,
o1, o2 for object of A,
m for Morphism of o1, o2;
theorem :: FUNCTOR3:6
<^o1,o2^> <> {} implies (G*F).m = G.(F.m);
theorem :: FUNCTOR3:7
<^o1,o2^> <> {} implies (N*M).m = N.(M.m);
theorem :: FUNCTOR3:8
<^o1,o2^> <> {} implies (N*F).m = N.(F.m);
theorem :: FUNCTOR3:9
<^o1,o2^> <> {} implies (G*M).m = G.(M.m);
definition let A be non empty transitive AltCatStr,
B be transitive with_units (non empty AltCatStr),
C be with_units (non empty AltCatStr),
F be feasible Covariant comp-preserving FunctorStr over A, B,
G be feasible Covariant comp-preserving FunctorStr over B, C;
cluster G*F -> comp-preserving;
end;
definition let A be non empty transitive AltCatStr,
B be transitive with_units (non empty AltCatStr),
C be with_units (non empty AltCatStr),
F be feasible Contravariant comp-reversing FunctorStr over A, B,
G be feasible Contravariant comp-reversing FunctorStr over B, C;
cluster G*F -> comp-preserving;
end;
definition let A be non empty transitive AltCatStr,
B be transitive with_units (non empty AltCatStr),
C be with_units (non empty AltCatStr),
F be feasible Covariant comp-preserving FunctorStr over A, B,
G be feasible Contravariant comp-reversing FunctorStr over B, C;
cluster G*F -> comp-reversing;
end;
definition let A be non empty transitive AltCatStr,
B be transitive with_units (non empty AltCatStr),
C be with_units (non empty AltCatStr),
F be feasible Contravariant comp-reversing FunctorStr over A, B,
G be feasible Covariant comp-preserving FunctorStr over B, C;
cluster G*F -> comp-reversing;
end;
definition let A, B be transitive with_units (non empty AltCatStr),
C be with_units (non empty AltCatStr),
F be covariant Functor of A, B,
G be covariant Functor of B, C;
redefine func G*F -> strict covariant Functor of A, C;
end;
definition let A, B be transitive with_units (non empty AltCatStr),
C be with_units (non empty AltCatStr),
F be contravariant Functor of A, B,
G be contravariant Functor of B, C;
redefine func G*F -> strict covariant Functor of A, C;
end;
definition let A, B be transitive with_units (non empty AltCatStr),
C be with_units (non empty AltCatStr),
F be covariant Functor of A, B,
G be contravariant Functor of B, C;
redefine func G*F -> strict contravariant Functor of A, C;
end;
definition let A, B be transitive with_units (non empty AltCatStr),
C be with_units (non empty AltCatStr),
F be contravariant Functor of A, B,
G be covariant Functor of B, C;
redefine func G*F -> strict contravariant Functor of A, C;
end;
reserve A, B, C, D for transitive with_units (non empty AltCatStr),
F1, F2, F3 for covariant Functor of A, B,
G1, G2, G3 for covariant Functor of B, C,
H1, H2 for covariant Functor of C, D,
p for transformation of F1, F2,
p1 for transformation of F2, F3,
q for transformation of G1, G2,
q1 for transformation of G2, G3,
r for transformation of H1, H2;
theorem :: FUNCTOR3:10
F1 is_transformable_to F2 & G1 is_transformable_to G2 implies
G1*F1 is_transformable_to G2*F2;
begin :: The composition of functors with transformations
definition let A, B, C be transitive with_units (non empty AltCatStr),
F1, F2 be covariant Functor of A, B,
t be transformation of F1, F2,
G be covariant Functor of B, C such that
F1 is_transformable_to F2;
func G*t -> transformation of G*F1,G*F2 means
:: FUNCTOR3:def 1
for o being object of A holds it.o = G.(t!o);
end;
theorem :: FUNCTOR3:11
for o being object of A st F1 is_transformable_to F2 holds
(G1*p)!o = G1.(p!o);
definition let A, B, C be transitive with_units (non empty AltCatStr),
G1, G2 be covariant Functor of B, C,
F be covariant Functor of A, B,
s be transformation of G1, G2 such that
G1 is_transformable_to G2;
func s*F -> transformation of G1*F,G2*F means
:: FUNCTOR3:def 2
for o being object of A holds it.o = s!(F.o);
end;
theorem :: FUNCTOR3:12
for o being object of A st G1 is_transformable_to G2 holds
(q*F1)!o = q!(F1.o);
theorem :: FUNCTOR3:13
F1 is_transformable_to F2 & F2 is_transformable_to F3 implies
G1*(p1`*`p) = (G1*p1)`*`(G1*p);
theorem :: FUNCTOR3:14
G1 is_transformable_to G2 & G2 is_transformable_to G3 implies
(q1`*`q)*F1 = (q1*F1)`*`(q*F1);
theorem :: FUNCTOR3:15
H1 is_transformable_to H2 implies r*G1*F1 = r*(G1*F1);
theorem :: FUNCTOR3:16
G1 is_transformable_to G2 implies H1*q*F1 = H1*(q*F1);
theorem :: FUNCTOR3:17
F1 is_transformable_to F2 implies H1*G1*p = H1*(G1*p);
theorem :: FUNCTOR3:18
(idt G1)*F1 = idt (G1*F1);
theorem :: FUNCTOR3:19
G1 * idt F1 = idt (G1*F1);
theorem :: FUNCTOR3:20
F1 is_transformable_to F2 implies (id B) * p = p;
theorem :: FUNCTOR3:21
G1 is_transformable_to G2 implies q * id B = q;
begin :: The composition of transformations
definition let A, B, C be transitive with_units (non empty AltCatStr),
F1, F2 be covariant Functor of A, B,
G1, G2 be covariant Functor of B, C,
t be transformation of F1, F2,
s be transformation of G1, G2;
func s (#) t -> transformation of G1*F1, G2*F2 equals
:: FUNCTOR3:def 3
(s*F2) `*` (G1*t);
end;
theorem :: FUNCTOR3:22
for q being natural_transformation of G1, G2 st
F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2
holds q (#) p = (G2*p) `*` (q*F1);
theorem :: FUNCTOR3:23
F1 is_transformable_to F2 implies (idt id B)(#)p = p;
theorem :: FUNCTOR3:24
G1 is_transformable_to G2 implies q(#)(idt id B) = q;
theorem :: FUNCTOR3:25
F1 is_transformable_to F2 implies G1*p = (idt G1) (#) p;
theorem :: FUNCTOR3:26
G1 is_transformable_to G2 implies q*F1 = q (#) idt F1;
reserve A, B, C, D for category,
F1, F2, F3 for covariant Functor of A, B,
G1, G2, G3 for covariant Functor of B, C;
theorem :: FUNCTOR3:27
for H1, H2 being covariant Functor of C, D
for t being transformation of F1, F2, s being transformation of G1, G2
for u being transformation of H1, H2 st
F1 is_transformable_to F2 & G1 is_transformable_to G2 &
H1 is_transformable_to H2 holds
u(#)s(#)t = u(#)(s(#)t);
reserve t for natural_transformation of F1, F2,
s for natural_transformation of G1, G2,
s1 for natural_transformation of G2, G3;
theorem :: FUNCTOR3:28
F1 is_naturally_transformable_to F2 implies
G1*t is natural_transformation of G1*F1, G1*F2;
theorem :: FUNCTOR3:29
G1 is_naturally_transformable_to G2 implies
s*F1 is natural_transformation of G1*F1, G2*F1;
theorem :: FUNCTOR3:30
F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2
implies
G1*F1 is_naturally_transformable_to G2*F2 &
s(#)t is natural_transformation of G1*F1, G2*F2;
theorem :: FUNCTOR3:31
for t being transformation of F1, F2, t1 being transformation of F2, F3 st
F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 &
G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3
holds (s1`*`s)(#)(t1`*`t) = (s1(#)t1)`*`(s(#)t);
begin :: Natural equivalences
theorem :: FUNCTOR3:32
F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 &
(for a being object of A holds t!a is iso) implies
F2 is_naturally_transformable_to F1 &
ex f being natural_transformation of F2, F1 st
for a being object of A holds f.a = (t!a)" & f!a is iso;
definition let A, B be category,
F1, F2 be covariant Functor of A, B;
pred F1, F2 are_naturally_equivalent means
:: FUNCTOR3:def 4
F1 is_naturally_transformable_to F2 &
F2 is_transformable_to F1 &
ex t being natural_transformation of F1, F2 st
for a being object of A holds t!a is iso;
reflexivity;
symmetry;
end;
definition let A, B be category,
F1, F2 be covariant Functor of A, B such that
F1, F2 are_naturally_equivalent;
mode natural_equivalence of F1, F2 -> natural_transformation of F1, F2 means
:: FUNCTOR3:def 5
for a being object of A holds it!a is iso;
end;
reserve e for natural_equivalence of F1, F2,
e1 for natural_equivalence of F2, F3,
f for natural_equivalence of G1, G2;
theorem :: FUNCTOR3:33
F1, F2 are_naturally_equivalent & F2, F3 are_naturally_equivalent implies
F1, F3 are_naturally_equivalent;
theorem :: FUNCTOR3:34
F1, F2 are_naturally_equivalent & F2, F3 are_naturally_equivalent implies
e1 `*` e is natural_equivalence of F1, F3;
theorem :: FUNCTOR3:35
F1, F2 are_naturally_equivalent implies
G1*F1, G1*F2 are_naturally_equivalent &
G1*e is natural_equivalence of G1*F1, G1*F2;
theorem :: FUNCTOR3:36
G1, G2 are_naturally_equivalent implies
G1*F1, G2*F1 are_naturally_equivalent &
f*F1 is natural_equivalence of G1*F1, G2*F1;
theorem :: FUNCTOR3:37
F1, F2 are_naturally_equivalent & G1, G2 are_naturally_equivalent
implies
G1*F1, G2*F2 are_naturally_equivalent &
f (#) e is natural_equivalence of G1*F1, G2*F2;
definition let A, B be category,
F1, F2 be covariant Functor of A, B,
e be natural_equivalence of F1, F2 such that
F1, F2 are_naturally_equivalent;
func e" -> natural_equivalence of F2, F1 means
:: FUNCTOR3:def 6
for a being object of A holds it.a = (e!a)";
end;
theorem :: FUNCTOR3:38
for o being object of A st F1, F2 are_naturally_equivalent holds
e"!o = (e!o)";
theorem :: FUNCTOR3:39
F1, F2 are_naturally_equivalent implies e `*` e" = idt F2;
theorem :: FUNCTOR3:40
F1, F2 are_naturally_equivalent implies e" `*` e = idt F1;
definition let A, B be category,
F be covariant Functor of A, B;
redefine func idt F -> natural_equivalence of F, F;
end;
theorem :: FUNCTOR3:41
F1, F2 are_naturally_equivalent implies (e")" = e;
theorem :: FUNCTOR3:42
for k being natural_equivalence of F1, F3 st k = e1 `*` e &
F1, F2 are_naturally_equivalent & F2, F3 are_naturally_equivalent
holds k" = e" `*` e1";
theorem :: FUNCTOR3:43
(idt F1)" = idt F1;
Back to top