:: Miscellaneous Facts about Functors
::  by Grzegorz Bancerek
::
:: Received July 31, 2001
:: Copyright (c) 2001-2021 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 RELAT_2, ALTCAT_1, XBOOLE_0, MSUALG_6, FUNCTOR0, FUNCT_2,
      FUNCT_1, RELAT_1, CAT_1, ENS_1, PARTFUN1, ZFMISC_1, STRUCT_0, YELLOW18,
      SETFAM_1, PBOOLE, ALTCAT_2, TARSKI, SUBSET_1, REALSET1, FUNCOP_1,
      FUNCT_3, MCART_1, MSUALG_3, WELLORD1, ARYTM_0, YELLOW20, SETLIM_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, RELAT_1, RELSET_1, FUNCT_1,
      FUNCT_2, MCART_1, BINOP_1, REALSET1, MULTOP_1, PBOOLE, STRUCT_0, FUNCT_4,
      PARTFUN1, FUNCOP_1, MSUALG_3, FUNCT_3, ALTCAT_1, ALTCAT_2, FUNCTOR0,
      FUNCTOR3, YELLOW18;
 constructors REALSET1, MSUALG_3, FUNCTOR3, YELLOW18, RELSET_1, XTUPLE_0;
 registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, PBOOLE, STRUCT_0,
      ALTCAT_2, FUNCTOR0, FUNCTOR2, ALTCAT_4, YELLOW18, RELSET_1, XTUPLE_0;
 requirements SUBSET, BOOLE;


begin :: Reverse functors

reserve x,y for set;

theorem :: YELLOW20:1
  for A,B being transitive with_units non empty AltCatStr for F
being feasible reflexive FunctorStr over A,B st F is coreflexive bijective for
  a being Object of A, b being Object of B holds F.a = b iff F".b = a;

theorem :: YELLOW20:2
  for A,B being transitive with_units non empty AltCatStr for F
  being Covariant feasible FunctorStr over A,B for G being Covariant feasible
  FunctorStr over B,A st F is bijective & G = F" for a1,a2 being Object of A st
  <^a1,a2^> <> {} for f being Morphism of a1,a2, g being Morphism of F.a1, F.a2
  holds F.f = g iff G.g = f;

theorem :: YELLOW20:3
  for A,B being transitive with_units non empty AltCatStr for F
  being Contravariant feasible FunctorStr over A,B for G being Contravariant
feasible FunctorStr over B,A st F is bijective & G = F" for a1,a2 being Object
of A st <^a1,a2^> <> {} for f being Morphism of a1,a2, g being Morphism of F.a2
  , F.a1 holds F.f = g iff G.g = f;

theorem :: YELLOW20:4
  for A,B being category, F being Functor of A,B st F is bijective
  for G being Functor of B,A st F*G = id B holds the FunctorStr of G = F";

theorem :: YELLOW20:5
  for A,B being category, F being Functor of A,B st F is bijective
  for G being Functor of B,A st G*F = id A holds the FunctorStr of G = F";

theorem :: YELLOW20:6
  for A,B being category, F being covariant Functor of A,B st F is
  bijective for G being covariant Functor of B,A st (for b being Object of B
  holds F.(G.b) = b) & (for a,b being Object of B st <^a,b^> <> {} for f being
  Morphism of a,b holds F.(G.f) = f) holds the FunctorStr of G = F";

theorem :: YELLOW20:7
  for A,B being category, F being contravariant Functor of A,B st F is
bijective for G being contravariant Functor of B,A st (for b being Object of B
  holds F.(G.b) = b) & (for a,b being Object of B st <^a,b^> <> {} for f being
  Morphism of a,b holds F.(G.f) = f) holds the FunctorStr of G = F";

theorem :: YELLOW20:8
  for A,B being category, F being covariant Functor of A,B st F is
  bijective for G being covariant Functor of B,A st (for a being Object of A
  holds G.(F.a) = a) & (for a,b being Object of A st <^a,b^> <> {} for f being
  Morphism of a,b holds G.(F.f) = f) holds the FunctorStr of G = F";

theorem :: YELLOW20:9
  for A,B being category, F being contravariant Functor of A,B st F is
bijective for G being contravariant Functor of B,A st (for a being Object of A
  holds G.(F.a) = a) & (for a,b being Object of A st <^a,b^> <> {} for f being
  Morphism of a,b holds G.(F.f) = f) holds the FunctorStr of G = F";

begin :: Intersection of categories

definition
  let A, B be AltCatStr;
  pred A, B have_the_same_composition means
:: YELLOW20:def 1

  for a1, a2, a3 being object
  holds (the Comp of A).[a1,a2,a3] tolerates (the Comp of B).[a1,a2,a3];
  symmetry;
end;

theorem :: YELLOW20:10
  for A, B being AltCatStr holds A,B have_the_same_composition iff
for a1,a2,a3,x being object
st x in dom ((the Comp of A).[a1,a2,a3]) & x in dom ((
the Comp of B).[a1,a2,a3]) holds ((the Comp of A).[a1,a2,a3]).x = ((the Comp of
  B).[a1,a2,a3]).x;

theorem :: YELLOW20:11
  for A, B being transitive non empty AltCatStr holds A,B
have_the_same_composition iff for a1,a2,a3 being Object of A st <^a1,a2^> <> {}
& <^a2,a3^> <> {} for b1,b2,b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^>
  <> {} & b1 = a1 & b2 = a2 & b3 = a3 for f1 being Morphism of a1,a2, g1 being
Morphism of b1,b2 st g1 = f1 for f2 being Morphism of a2,a3, g2 being Morphism
  of b2,b3 st g2 = f2 holds f2 * f1 = g2 * g1;

theorem :: YELLOW20:12
  for A, B being para-functional semi-functional category holds A, B
  have_the_same_composition;

definition
  let f, g be Function;
  func Intersect(f, g) -> Function means
:: YELLOW20:def 2

  dom it = (dom f) /\ (dom g) &
  for x being object st x in (dom f) /\ (dom g) holds it.x = (f.x) /\ (g.x);
  commutativity;
end;

theorem :: YELLOW20:13
  for I being set, A,B being ManySortedSet of I
    holds Intersect(A, B) = A (/\) B;

theorem :: YELLOW20:14
  for I,J being set for A being ManySortedSet of I, B being
  ManySortedSet of J holds Intersect(A, B) is ManySortedSet of I /\ J;

theorem :: YELLOW20:15
  for I,J being set for A being ManySortedSet of I, B being
  Function for C being ManySortedSet of J st C = Intersect(A, B) holds C cc= A;

theorem :: YELLOW20:16
  for I1,I2 being set for A1,B1 being ManySortedSet of I1 for A2,
  B2 being ManySortedSet of I2 for A,B being ManySortedSet of I1 /\ I2 st A =
Intersect(A1, A2) & B = Intersect(B1, B2) for F being ManySortedFunction of A1,
B1 for G being ManySortedFunction of A2,B2 st for x being set st x in dom F & x
in dom G holds F.x tolerates G.x holds Intersect(F, G) is ManySortedFunction of
  A, B;

theorem :: YELLOW20:17
  for I,J being set for F being ManySortedSet of [:I,I:] for G
being ManySortedSet of [:J,J:] ex H being ManySortedSet of [:I/\J,I/\J:] st H =
  Intersect(F, G) & Intersect({|F|}, {|G|}) = {|H|};

theorem :: YELLOW20:18
  for I,J being set for F1,F2 being ManySortedSet of [:I,I:] for
G1,G2 being ManySortedSet of [:J,J:] ex H1,H2 being ManySortedSet of [:I/\J,I/\
  J:] st H1 = Intersect(F1, G1) & H2 = Intersect(F2, G2) & Intersect({|F1,F2|},
  {|G1,G2|}) = {|H1, H2|};

definition
  let A, B be AltCatStr such that
 A, B have_the_same_composition;
  func Intersect(A, B) -> strict AltCatStr means
:: YELLOW20:def 3

  the carrier of it = (
  the carrier of A) /\ (the carrier of B) & the Arrows of it = Intersect(the
  Arrows of A, the Arrows of B) & the Comp of it = Intersect(the Comp of A, the
  Comp of B);
end;

theorem :: YELLOW20:19
  for A, B being AltCatStr st A, B have_the_same_composition holds
  Intersect(A, B) = Intersect(B, A);

theorem :: YELLOW20:20
  for A, B being AltCatStr st A, B have_the_same_composition holds
  Intersect(A, B) is SubCatStr of A;

theorem :: YELLOW20:21
  for A, B being AltCatStr st A, B have_the_same_composition for
  a1,a2 being Object of A, b1,b2 being Object of B for o1, o2 being Object of
Intersect(A, B) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds <^o1,o2^> = <^a1
  ,a2^> /\ <^b1,b2^>;

theorem :: YELLOW20:22
  for A, B being transitive AltCatStr st A, B
  have_the_same_composition holds Intersect(A, B) is transitive;

theorem :: YELLOW20:23
  for A, B being AltCatStr st A, B have_the_same_composition for
  a1,a2 being Object of A, b1,b2 being Object of B for o1,o2 being Object of
Intersect(A, B) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^
b1,b2^> <> {} for f being Morphism of a1,a2, g being Morphism of b1,b2 st f = g
  holds f in <^o1,o2^>;

theorem :: YELLOW20:24
  for A, B being with_units non empty AltCatStr st A, B
  have_the_same_composition for a being Object of A, b being Object of B for o
being Object of Intersect(A, B) st o = a & o = b & idm a = idm b holds idm a in
  <^o,o^>;

theorem :: YELLOW20:25
  for A, B being category st A, B have_the_same_composition & Intersect(
A,B) is non empty & for a being Object of A, b being Object of B st a = b holds
  idm a = idm b holds Intersect(A, B) is subcategory of A;

begin :: Subcategories

scheme :: YELLOW20:sch 1
  SubcategoryUniq { A() -> category, B1, B2() -> non empty subcategory of A(),
  P[set], Q[set,set,set]}: the AltCatStr of B1() = the AltCatStr of B2()
provided
 for a being Object of A() holds a is Object of B1() iff P[a] and
 for a,b being Object of A(), a9,b9 being Object of B1() st a9 = a &
b9 = b & <^a,b^> <> {} for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a
,b,f] and
 for a being Object of A() holds a is Object of B2() iff P[a] and
 for a,b being Object of A(), a9,b9 being Object of B2() st a9 = a &
b9 = b & <^a,b^> <> {} for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a
,b,f];

theorem :: YELLOW20:26
  for A being non empty AltCatStr, B being non empty SubCatStr of
  A holds B is full iff for a1,a2 being Object of A, b1,b2 being Object of B st
  b1 = a1 & b2 = a2 holds <^b1,b2^> = <^a1,a2^>;

scheme :: YELLOW20:sch 2
  FullSubcategoryEx { A() -> category, P[set]}: ex B being strict full non
  empty subcategory of A() st for a being Object of A() holds a is Object of B
  iff P[a]
provided
 ex a being Object of A() st P[a];

scheme :: YELLOW20:sch 3
  FullSubcategoryUniq { A() -> category, B1, B2() -> full non empty
  subcategory of A(), P[set]}: the AltCatStr of B1() = the AltCatStr of B2()
provided
 for a being Object of A() holds a is Object of B1() iff P[a] and
 for a being Object of A() holds a is Object of B2() iff P[a];

begin :: Inclusion functors and functor restrictions

registration
  let f be Function-yielding Function;
  let x,y be set;
  cluster f.(x,y) -> Relation-like Function-like;
end;

theorem :: YELLOW20:27
  for A being category, C being non empty subcategory of A for a,b
being Object of C st <^a,b^> <> {} for f being Morphism of a,b holds (incl C).f
  = f;

registration
  let A be category;
  let C be non empty subcategory of A;
  cluster incl C -> id-preserving comp-preserving;
end;

registration
  let A be category;
  let C be non empty subcategory of A;
  cluster incl C -> Covariant;
end;

definition
  let A be category;
  let C be non empty subcategory of A;
  redefine func incl C -> strict covariant Functor of C,A;
end;

definition
  let A,B be category;
  let C be non empty subcategory of A;
  let F be covariant Functor of A,B;
  redefine func F|C -> strict covariant Functor of C,B;
end;

definition
  let A,B be category;
  let C be non empty subcategory of A;
  let F be contravariant Functor of A,B;
  redefine func F|C -> strict contravariant Functor of C,B;
end;

theorem :: YELLOW20:28
  for A,B being category, C being non empty subcategory of A for F
being FunctorStr over A,B for a being Object of A, c being Object of C st c = a
  holds (F|C).c = F.a;

theorem :: YELLOW20:29
  for A,B being category, C being non empty subcategory of A for F
being covariant Functor of A,B for a,b being Object of A, c,d being Object of C
  st c = a & d = b & <^c,d^> <> {} for f being Morphism of a,b for g being
  Morphism of c,d st g = f holds (F|C).g = F.f;

theorem :: YELLOW20:30
  for A,B being category, C being non empty subcategory of A for F
being contravariant Functor of A,B for a,b being Object of A, c,d being Object
  of C st c = a & d = b & <^c,d^> <> {} for f being Morphism of a,b for g being
  Morphism of c,d st g = f holds (F|C).g = F.f;

theorem :: YELLOW20:31
  for A,B being non empty AltGraph for F being BimapStr over A,B
st F is Covariant one-to-one for a,b being Object of A st F.a = F.b holds a = b
;

theorem :: YELLOW20:32
  for A,B being non empty reflexive AltGraph for F being feasible
Covariant FunctorStr over A,B st F is faithful for a,b being Object of A st <^a
  ,b^> <> {} for f,g being Morphism of a,b st F.f = F.g holds f = g;

theorem :: YELLOW20:33
  for A,B being non empty AltGraph for F being Covariant
FunctorStr over A,B st F is surjective for a,b being Object of B st <^a,b^> <>
{} for f being Morphism of a,b ex c,d being Object of A, g being Morphism of c,
  d st a = F.c & b = F.d & <^c,d^> <> {} & f = F.g;

theorem :: YELLOW20:34
  for A,B being non empty AltGraph for F being BimapStr over A,B
st F is Contravariant one-to-one for a,b being Object of A st F.a = F.b holds a
  = b;

theorem :: YELLOW20:35
  for A,B being non empty reflexive AltGraph for F being feasible
Contravariant FunctorStr over A,B st F is faithful for a,b being Object of A st
  <^a,b^> <> {} for f,g being Morphism of a,b st F.f = F.g holds f = g;

theorem :: YELLOW20:36
  for A,B being non empty AltGraph for F being Contravariant
FunctorStr over A,B st F is surjective for a,b being Object of B st <^a,b^> <>
{} for f being Morphism of a,b ex c,d being Object of A, g being Morphism of c,
  d st b = F.c & a = F.d & <^c,d^> <> {} & f = F.g;

begin :: Isomorphisms under arbitrary functor

definition
  let A,B be category;
  let F be FunctorStr over A,B;
  let A9, B9 be category;
  pred A9,B9 are_isomorphic_under F means
:: YELLOW20:def 4
  A9 is subcategory of A & B9 is
subcategory of B & ex G being covariant Functor of A9,B9 st G is bijective & (
  for a9 being Object of A9, a being Object of A st a9 = a holds G.a9 = F.a) &
for b9,c9 being Object of A9, b,c being Object of A st <^b9,c9^> <> {} & b9 = b
  & c9 = c for f9 being Morphism of b9,c9, f being Morphism of b,c st f9 = f
  holds G.f9 = Morph-Map(F,b,c).f;
  pred A9,B9 are_anti-isomorphic_under F means
:: YELLOW20:def 5
  A9 is subcategory of A & B9 is
subcategory of B & ex G being contravariant Functor of A9,B9 st G is bijective
& (for a9 being Object of A9, a being Object of A st a9 = a holds G.a9 = F.a) &
for b9,c9 being Object of A9, b,c being Object of A st <^b9,c9^> <> {} & b9 = b
  & c9 = c for f9 being Morphism of b9,c9, f being Morphism of b,c st f9 = f
  holds G.f9 = Morph-Map(F,b,c).f;
end;

theorem :: YELLOW20:37
  for A,B, A1, B1 being category, F being FunctorStr over A,B st A1, B1
  are_isomorphic_under F holds A1, B1 are_isomorphic;

theorem :: YELLOW20:38
  for A,B, A1, B1 being category, F being FunctorStr over A,B st A1, B1
  are_anti-isomorphic_under F holds A1, B1 are_anti-isomorphic;

theorem :: YELLOW20:39
  for A,B being category, F being covariant Functor of A,B st A, B
  are_isomorphic_under F holds F is bijective;

theorem :: YELLOW20:40
  for A,B being category, F being contravariant Functor of A,B st A, B
  are_anti-isomorphic_under F holds F is bijective;

theorem :: YELLOW20:41
  for A,B being category, F being covariant Functor of A,B st F is
  bijective holds A, B are_isomorphic_under F;

theorem :: YELLOW20:42
  for A,B being category, F being contravariant Functor of A,B st F is
  bijective holds A, B are_anti-isomorphic_under F;

theorem :: YELLOW20:43
  for A being category, B being non empty subcategory of A holds B,B
  are_isomorphic_under id A;

theorem :: YELLOW20:44
  for f, g being Function st f c= g holds ~f c= ~g;

theorem :: YELLOW20:45
  for f, g being Function st dom f is Relation & ~f c= ~g holds f c= g;

theorem :: YELLOW20:46
  for I, J being set for A being ManySortedSet of [:I,I:], B being
  ManySortedSet of [:J,J:] st A cc= B holds ~A cc= ~B;

theorem :: YELLOW20:47
  for A being transitive non empty AltCatStr for B being
  transitive non empty SubCatStr of A holds B opp is SubCatStr of A opp;

theorem :: YELLOW20:48
  for A being category, B being non empty subcategory of A holds B
  opp is subcategory of A opp;

theorem :: YELLOW20:49
  for A being category, B being non empty subcategory of A holds B,B opp
  are_anti-isomorphic_under dualizing-func(A, A opp);

theorem :: YELLOW20:50
  for A1,A2 being category, F being covariant Functor of A1,A2 st F is
  bijective for B1 being non empty subcategory of A1 for B2 being non empty
  subcategory of A2 st B1,B2 are_isomorphic_under F holds B2,B1
  are_isomorphic_under F";

theorem :: YELLOW20:51
  for A1,A2 being category, F being contravariant Functor of A1,A2 st F
  is bijective for B1 being non empty subcategory of A1 for B2 being non empty
  subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds B2,B1
  are_anti-isomorphic_under F";

theorem :: YELLOW20:52
  for A1,A2,A3 being category for F being covariant Functor of A1,A2 for
G being covariant Functor of A2,A3 for B1 being non empty subcategory of A1 for
  B2 being non empty subcategory of A2 for B3 being non empty subcategory of A3
  st B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G holds B1,B3
  are_isomorphic_under G*F;

theorem :: YELLOW20:53
  for A1,A2,A3 being category for F being contravariant Functor of A1,A2
for G being covariant Functor of A2,A3 for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 for B3 being non empty subcategory of
A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G holds B1
  ,B3 are_anti-isomorphic_under G*F;

theorem :: YELLOW20:54
  for A1,A2,A3 being category for F being covariant Functor of A1,A2 for
G being contravariant Functor of A2,A3 for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 for B3 being non empty subcategory of
A3 st B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds B1
  ,B3 are_anti-isomorphic_under G*F;

theorem :: YELLOW20:55
  for A1,A2,A3 being category for F being contravariant Functor of A1,A2
  for G being contravariant Functor of A2,A3 for B1 being non empty subcategory
  of A1 for B2 being non empty subcategory of A2 for B3 being non empty
  subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3
  are_anti-isomorphic_under G holds B1,B3 are_isomorphic_under G*F;

theorem :: YELLOW20:56
  for A1, A2 be non empty category, F be covariant Functor of A1, A2,
  B1 be non empty subcategory of A1, B2 be non empty subcategory of A2 st
   F is bijective &
   (for a being Object of A1 holds a is Object of B1 iff F.a is Object of B2) &
   (for a,b being Object of A1 st <^a,b^> <> {} for a1,b1 being Object
   of B1 st a1 = a & b1 = b for a2,b2 being Object of B2 st a2 = F.a & b2 =
   F.b for f being Morphism of a,b holds f in <^a1,b1^> iff F.f in <^a2,b2^>)
   holds B1, B2 are_isomorphic_under F;

theorem :: YELLOW20:57
  for A1, A2 be non empty category, F be contravariant Functor of A1,A2,
   B1 be non empty subcategory of A1, B2 be non empty subcategory of A2 st
   F is bijective &
   (for a being Object of A1 holds a is Object of B1 iff
   F.a is Object of B2) &
   (for a,b being Object of A1 st <^a,b^> <> {} for a1,b1 being Object
   of B1 st a1 = a & b1 = b for a2,b2 being Object of B2 st a2 = F.a &
   b2 = F.b
   for f being Morphism of a,b holds f in <^a1,b1^> iff F.f in <^b2,a2^>)
   holds B1, B2 are_anti-isomorphic_under F;