:: Isomorphisms of Categories
:: by Andrzej Trybulec
::
:: Received November 22, 1991
:: Copyright (c) 1991-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies CAT_1, FUNCT_1, ZFMISC_1, RELAT_1, MCART_1, STRUCT_0, ALGSTR_0,
GRAPH_1, PZFMISC1, NATTRA_1, XBOOLE_0, WELLORD1, TARSKI, PARTFUN1,
VALUED_1, REWRITE1, ISOCAT_1, MONOID_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, BINOP_1, FUNCT_3, STRUCT_0, GRAPH_1, CAT_1, CAT_2, CAT_3,
NATTRA_1;
constructors NATTRA_1, FUNCOP_1, RELSET_1, CAT_3, FUNCT_4;
registrations RELSET_1, FUNCT_2, STRUCT_0, CAT_1, FUNCT_3;
requirements SUBSET, BOOLE;
begin
:: Auxiliary theorems
reserve A,B,C,D for Category,
F for Functor of A,B,
G for Functor of B,C;
::$CT 2
theorem :: ISOCAT_1:3
for a,b being Object of A
for f being Morphism of a,b st f is invertible holds F/.f is invertible;
theorem :: ISOCAT_1:4
for F1,F2 being Functor of A,B st F1 is_transformable_to F2 for t
being transformation of F1,F2, a being Object of A holds t.a in Hom(F1.a,F2.a);
theorem :: ISOCAT_1:5
for F1,F2 being Functor of A,B, G1,G2 being Functor of B,C st F1
is_transformable_to F2 & G1 is_transformable_to G2 holds G1*F1
is_transformable_to G2*F2;
theorem :: ISOCAT_1:6
for F1,F2 being Functor of A,B st F1 is_transformable_to F2 for t
being transformation of F1,F2 st t is invertible for a being Object of A holds
F1.a, F2.a are_isomorphic;
definition
let C,D;
redefine mode Functor of C,D means
:: ISOCAT_1:def 1
(for c being Object of C ex d being
Object of D st it.id c = id d) & (for f being Morphism of C holds it.id dom f =
id dom(it.f) & it.id cod f = id cod(it.f)) & for f,g being Morphism of C st dom
g = cod f holds it.(g(*)f) = (it.g)(*)(it.f);
end;
reserve o,m for set;
theorem :: ISOCAT_1:7
F is isomorphic implies for g being Morphism of B ex f being
Morphism of A st F.f = g;
theorem :: ISOCAT_1:8
F is isomorphic implies for b being Object of B ex a being
Object of A st F.a = b;
theorem :: ISOCAT_1:9
F is one-to-one implies Obj F is one-to-one;
definition
let A,B,F;
assume
F is isomorphic;
func F" -> Functor of B,A equals
:: ISOCAT_1:def 2
F";
end;
definition
let A,B,F;
redefine attr F is isomorphic means
:: ISOCAT_1:def 3
F is one-to-one & rng F = the carrier' of B;
end;
theorem :: ISOCAT_1:10
F is isomorphic implies F" is isomorphic;
theorem :: ISOCAT_1:11
F is isomorphic implies (Obj F)" = Obj F";
theorem :: ISOCAT_1:12
F is isomorphic implies F"" = F;
theorem :: ISOCAT_1:13
F is isomorphic implies F*F" = id B & F"*F = id A;
theorem :: ISOCAT_1:14
F is isomorphic & G is isomorphic implies G*F is isomorphic;
:: Isomorphism of categories
definition
let A,B;
pred A,B are_isomorphic means
:: ISOCAT_1:def 4
ex F being Functor of A,B st F is isomorphic;
reflexivity;
symmetry;
end;
notation
let A,B;
synonym A ~= B for A,B are_isomorphic;
end;
theorem :: ISOCAT_1:15
A ~= B & B ~= C implies A ~= C;
theorem :: ISOCAT_1:16
[:1Cat(o,m),A:] ~= A;
theorem :: ISOCAT_1:17
[:A,B:] ~= [:B,A:];
theorem :: ISOCAT_1:18
[:[:A,B:],C:] ~= [:A,[:B,C:]:];
theorem :: ISOCAT_1:19
A ~= B & C ~= D implies [:A,C:] ~= [:B,D:];
definition
let A,B,C;
let F1,F2 be Functor of A,B such that
F1 is_transformable_to F2;
let t be transformation of F1,F2;
let G be Functor of B,C;
func G*t -> transformation of G*F1,G*F2 equals
:: ISOCAT_1:def 5
G*t;
end;
definition
let A,B,C;
let G1,G2 be Functor of B,C such that
G1 is_transformable_to G2;
let F be Functor of A,B;
let t be transformation of G1,G2;
func t*F -> transformation of G1*F,G2*F equals
:: ISOCAT_1:def 6
t*Obj F;
end;
theorem :: ISOCAT_1:20
for G1,G2 be Functor of B,C st G1 is_transformable_to G2 for F
be Functor of A,B, t be transformation of G1,G2, a be Object of A holds (t*F).a
= t.(F.a);
theorem :: ISOCAT_1:21
for F1,F2 be Functor of A,B st F1 is_transformable_to F2 for t
be transformation of F1,F2, G be Functor of B,C, a being Object of A
holds (G*t).a = G/.(t.a);
theorem :: ISOCAT_1:22
for F1,F2 being Functor of A,B, G1,G2 being Functor of B,C st F1
is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds G1
*F1 is_naturally_transformable_to G2*F2;
definition
let A,B,C;
let F1,F2 be Functor of A,B such that
F1 is_naturally_transformable_to F2;
let t be natural_transformation of F1,F2;
let G be Functor of B,C;
func G*t -> natural_transformation of G*F1,G*F2 equals
:: ISOCAT_1:def 7
G*t;
end;
theorem :: ISOCAT_1:23
for F1,F2 be Functor of A,B st F1 is_naturally_transformable_to
F2 for t be natural_transformation of F1,F2, G be Functor of B,C, a being
Object of A holds (G*t).a = G/.(t.a);
definition
let A,B,C;
let G1,G2 be Functor of B,C such that
G1 is_naturally_transformable_to G2;
let F be Functor of A,B;
let t be natural_transformation of G1,G2;
func t*F -> natural_transformation of G1*F,G2*F equals
:: ISOCAT_1:def 8
t*F;
end;
theorem :: ISOCAT_1:24
for G1,G2 be Functor of B,C st G1 is_naturally_transformable_to
G2 for F be Functor of A,B, t be natural_transformation of G1,G2, a be Object
of A holds (t*F).a = t.(F.a);
reserve F,F1,F2,F3 for Functor of A,B,
G,G1,G2,G3 for Functor of B,C,
H,H1,H2 for Functor of C,D,
s for natural_transformation of F1,F2,
s9 for natural_transformation of F2,F3,
t for natural_transformation of G1,G2,
t9 for natural_transformation of G2,G3,
u for natural_transformation of H1,H2;
theorem :: ISOCAT_1:25
F1 is_naturally_transformable_to F2 implies for a being Object
of A holds Hom(F1.a,F2.a) <> {};
theorem :: ISOCAT_1:26
F1 is_naturally_transformable_to F2 implies for t1,t2 being
natural_transformation of F1,F2 st for a being Object of A holds t1.a = t2.a
holds t1 = t2;
theorem :: ISOCAT_1:27
F1 is_naturally_transformable_to F2 & F2
is_naturally_transformable_to F3 implies G*(s9`*`s) = (G*s9)`*`(G*s);
theorem :: ISOCAT_1:28
G1 is_naturally_transformable_to G2 & G2
is_naturally_transformable_to G3 implies (t9`*`t)*F = (t9*F)`*`(t*F);
theorem :: ISOCAT_1:29
H1 is_naturally_transformable_to H2 implies u*G*F = u*(G*F);
theorem :: ISOCAT_1:30
G1 is_naturally_transformable_to G2 implies H*t*F = H*(t*F);
theorem :: ISOCAT_1:31
F1 is_naturally_transformable_to F2 implies H*G*s = H*(G*s);
theorem :: ISOCAT_1:32
(id G)*F = id(G*F);
theorem :: ISOCAT_1:33
G*id F = id(G*F);
theorem :: ISOCAT_1:34
G1 is_naturally_transformable_to G2 implies t*id B = t;
theorem :: ISOCAT_1:35
F1 is_naturally_transformable_to F2 implies (id B)*s = s;
definition
let A,B,C,F1,F2,G1,G2;
let s,t;
func t(#)s -> natural_transformation of G1*F1,G2*F2 equals
:: ISOCAT_1:def 9
(t*F2)`*`(G1*s);
end;
theorem :: ISOCAT_1:36
F1 is_naturally_transformable_to F2 & G1
is_naturally_transformable_to G2 implies t(#)s = (G2*s)`*`(t*F1);
theorem :: ISOCAT_1:37
F1 is_naturally_transformable_to F2 implies (id id B)(#)s = s;
theorem :: ISOCAT_1:38
G1 is_naturally_transformable_to G2 implies t(#)(id id B) = t;
theorem :: ISOCAT_1:39
F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to
G2 & H1 is_naturally_transformable_to H2 implies u(#)(t(#)s) = (u(#)t)(#)s;
theorem :: ISOCAT_1:40
G1 is_naturally_transformable_to G2 implies t*F = t(#)id F;
theorem :: ISOCAT_1:41
F1 is_naturally_transformable_to F2 implies G*s = (id G)(#)s;
theorem :: ISOCAT_1:42
F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to
F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3
implies (t9`*`t)(#)(s9`*`s) = (t9(#)s9)`*`(t(#)s);
theorem :: ISOCAT_1:43
for F being Functor of A,B, G being Functor of C,D for I,J being
Functor of B,C st I ~= J holds G*I ~= G*J & I*F ~= J*F;
theorem :: ISOCAT_1:44
for F being Functor of A,B, G being Functor of B,A for I being
Functor of A,A st I ~= id A holds F*I ~= F & I*G ~= G;
definition
let A,B be Category;
pred A is_equivalent_with B means
:: ISOCAT_1:def 10
ex F being Functor of A,B, G being
Functor of B,A st G*F ~= id A & F*G ~= id B;
reflexivity;
symmetry;
end;
notation
let A,B be Category;
synonym A,B are_equivalent for A is_equivalent_with B;
end;
theorem :: ISOCAT_1:45
A ~= B implies A is_equivalent_with B;
theorem :: ISOCAT_1:46
A,B are_equivalent & B,C are_equivalent implies A,C are_equivalent;
definition
let A,B;
assume
A,B are_equivalent;
mode Equivalence of A,B -> Functor of A,B means
:: ISOCAT_1:def 11
ex G being Functor of B,A st G*it ~= id A & it*G ~= id B;
end;
theorem :: ISOCAT_1:47
id A is Equivalence of A,A;
theorem :: ISOCAT_1:48
A,B are_equivalent & B,C are_equivalent implies for F being
Equivalence of A,B, G being Equivalence of B,C holds G*F is Equivalence of A,C;
theorem :: ISOCAT_1:49
A,B are_equivalent implies for F being Equivalence of A,B ex G
being Equivalence of B,A st G*F ~= id A & F*G ~= id B;
theorem :: ISOCAT_1:50
for F being Functor of A,B, G being Functor of B,A st G*F ~= id
A holds F is faithful;
theorem :: ISOCAT_1:51
A,B are_equivalent implies for F being Equivalence of A,B holds F is
full & F is faithful & for b being Object of B ex a being Object of A st b, F.a
are_isomorphic;
:: The elimination of the Id selector caused the necessity to
:: introduce corresponding functor because 'the Id of C' is sometimes
:: separately used, not applied to an object (2012.01.25, A.T.)
definition let C be Category;
func IdMap C -> Function of the carrier of C, the carrier' of C means
:: ISOCAT_1:def 12
for o being Object of C holds it.o = id o;
end;