Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

The abstract of the Mizar article:

The Composition of Functors and Transformations in Alternative Categories

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