:: Algebra of Morphisms
::  by Grzegorz Bancerek
::
:: Received January 28, 1997
:: Copyright (c) 1997-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 FUNCT_1, PBOOLE, RELAT_1, FUNCOP_1, CARD_3, TARSKI, FUNCT_6,
      MEMBER_1, XBOOLE_0, FINSEQ_1, MSUALG_1, STRUCT_0, PROB_2, MSAFREE, NAT_1,
      ZFMISC_1, CARD_1, FINSEQ_2, MCART_1, SUBSET_1, ORDINAL4, MSUALG_6, CAT_5,
      INSTALG1, NUMBERS, MARGREL1, CAT_1, PUA2MSS1, GRAPH_1, PARTFUN1,
      MSUALG_3, CATALG_1, MONOID_0;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1,
      ORDINAL1, NUMBERS, MCART_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, FUNCOP_1, NAT_1, MSAFREE1, FINSEQ_1, FINSEQ_2, CARD_3, FINSEQ_4,
      FUNCT_6, STRUCT_0, PBOOLE, MSUALG_1, MSUALG_3, MSAFREE, PUA2MSS1,
      MSUALG_6, INSTALG1, GRAPH_1, CAT_1;
 constructors ENUMSET1, FINSEQ_4, CAT_1, MSUALG_3, MSAFREE1, PUA2MSS1,
      MSUALG_6, INSTALG1, RELSET_1, XTUPLE_0, XFAMILY;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
      FUNCOP_1, FINSEQ_1, FINSEQ_2, STRUCT_0, MSUALG_1, RELSET_1, MSAFREE,
      INSTALG1, MSAFREE1, MSSUBFAM, PBOOLE, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Preliminaries

definition
  let I be set;
  let A,f be Function;
  func f-MSF(I,A) -> ManySortedFunction of I means
:: CATALG_1:def 1

  for i being object st i in I holds it.i = f|(A.i);
end;

theorem :: CATALG_1:1
  for I being set, A being ManySortedSet of I holds (id Union A)-MSF(I,A
  ) = id A;

theorem :: CATALG_1:2
  for I being set, A,B being ManySortedSet of I for f,g being Function
  st rngs (f-MSF(I,A)) c= B holds (g*f)-MSF(I,A) = (g-MSF(I,B))**(f-MSF(I,A));

theorem :: CATALG_1:3
  for f being Function, I being set for A,B being ManySortedSet of I st
for i being set st i in I holds A.i c= dom f & f.:(A.i) c= B.i holds f-MSF(I,A)
  is ManySortedFunction of A,B;

definition
  let S be non empty ManySortedSign;
  let A be MSAlgebra over S;

  attr A is empty means
:: CATALG_1:def 2

  the Sorts of A is empty-yielding;
end;

registration
  let S be non empty ManySortedSign;
  cluster non-empty -> non empty for MSAlgebra over S;
end;

registration
  let S be non empty non void ManySortedSign;
  cluster strict non-empty disjoint_valued for MSAlgebra over S;
end;

registration
  let S be non empty non void ManySortedSign;
  let A be non empty MSAlgebra over S;
  cluster the Sorts of A -> non empty-yielding;
end;

registration
  cluster non empty-yielding for Function;
end;

begin :: Signature of a category

definition
  let A be set;
  func CatSign A -> strict ManySortedSign means
:: CATALG_1:def 3

  the carrier of it = [:{0},2-tuples_on A:] &
   the carrier' of it = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] &
   (for a being set st a in A
     holds (the Arity of it).[1,<*a*>] ={} &
         (the ResultSort of it).[1,<*a*>] = [0,<*a,a*>]) &
    for a,b,c being set st a in A & b in A & c in A
      holds (the Arity of it).[2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> &
       (the ResultSort of it).[2,<*a,b,c*>] = [0,<*a,c*>];
end;

registration
  let A be set;
  cluster CatSign A -> feasible;
end;

registration
  let A be non empty set;
  cluster CatSign A -> non empty non void;
end;

definition
  mode Signature is feasible ManySortedSign;
end;

definition
  let S be Signature;
  attr S is Categorial means
:: CATALG_1:def 4

  ex A being set st CatSign A is
  Subsignature of S & the carrier of S = [:{0},2-tuples_on A:];
end;

registration
  cluster Categorial -> non void for non empty Signature;
end;

registration
  cluster Categorial non empty strict for Signature;
end;

definition
  mode CatSignature is Categorial Signature;
end;

definition
  let A be set;
  mode CatSignature of A -> Signature means
:: CATALG_1:def 5

    CatSign A is Subsignature
    of it & the carrier of it = [:{0},2-tuples_on A:];
end;

theorem :: CATALG_1:4
  for A1,A2 being set, S being CatSignature of A1 st S is CatSignature
  of A2 holds A1 = A2;

registration
  let A be set;
  cluster -> Categorial for CatSignature of A;
end;

registration
  let A be non empty set;
  cluster -> non empty for CatSignature of A;
end;

registration
  let A be set;
  cluster strict for CatSignature of A;
end;

definition
  let A be set;
  redefine func CatSign A -> strict CatSignature of A;
end;

definition
  let S be ManySortedSign;
  assume
  for x being object
    st x in proj2((the carrier of S) \/ (the carrier' of S))
     holds x is Function;
  func underlay S -> set means
:: CATALG_1:def 6
 for x being object holds x in it iff
   ex a being set, f being Function
     st [a,f] in (the carrier of S) \/ (the carrier' of S) & x in rng f;
end;

definition
  let S be ManySortedSign;
  attr S is delta-concrete means
:: CATALG_1:def 7

  ex f being sequence of NAT st
   ( for s being object st s in the carrier of S
     ex i being (Element of NAT), p being FinSequence st s = [i,p]
      & len p = f.i & [:{i}, (f.i)-tuples_on underlay S:] c= the carrier of S)
     &  (for o being object st o in the carrier' of S
     ex i being (Element of NAT), p being FinSequence st o = [i,p] &
    len p = f.i & [:{i}, (f.i) -tuples_on underlay S:] c= the carrier' of S);
end;

theorem :: CATALG_1:5
  for A being set holds underlay CatSign A = A;

registration
  let A be set;
  cluster CatSign A -> delta-concrete;
end;

registration
  cluster delta-concrete non empty strict for CatSignature;
  let A be set;
  cluster delta-concrete strict for CatSignature of A;
end;

theorem :: CATALG_1:6
  for A being set holds underlay CatSign A = A;

registration
  let A be set;
  cluster CatSign A -> delta-concrete;
end;

registration
  cluster delta-concrete non empty strict for CatSignature;
  let A be set;
  cluster delta-concrete strict for CatSignature of A;
end;

theorem :: CATALG_1:7
  for S being delta-concrete ManySortedSign, x being set st x in
the carrier of S or x in the carrier' of S ex i being (Element of NAT), p being
  FinSequence st x = [i,p] & rng p c= underlay S;

theorem :: CATALG_1:8
  for S being delta-concrete ManySortedSign, i being set, p1,p2 being
FinSequence st [i,p1] in the carrier of S & [i,p2] in the carrier of S or [i,p1
  ] in the carrier' of S & [i,p2] in the carrier' of S holds len p1 = len p2;

theorem :: CATALG_1:9
  for S being delta-concrete ManySortedSign, i being set, p1,p2 being
  FinSequence st len p2 = len p1 & rng p2 c= underlay S holds ([i,p1] in the
carrier of S implies [i,p2] in the carrier of S) & ([i,p1] in the carrier' of S
  implies [i,p2] in the carrier' of S);

theorem :: CATALG_1:10
  for S being delta-concrete Categorial non empty Signature holds S is
  CatSignature of underlay S;

begin :: Symbols of categorial sygnature

registration
  let S be non empty CatSignature;
  let s be SortSymbol of S;
  cluster s`2 -> Relation-like Function-like for set;
end;

registration
  let S be non empty delta-concrete ManySortedSign;
  let s be SortSymbol of S;
  cluster s`2 -> Relation-like Function-like for set;
end;

registration
  let S be non void delta-concrete ManySortedSign;
  let o be Element of the carrier' of S;
  cluster o`2 -> Relation-like Function-like for set;
end;

registration
  let S be non empty CatSignature;
  let s be SortSymbol of S;
  cluster s`2 -> FinSequence-like for Function;
end;

registration
  let S be non empty delta-concrete ManySortedSign;
  let s be SortSymbol of S;
  cluster s`2 -> FinSequence-like for Function;
end;

registration
  let S be non void delta-concrete ManySortedSign;
  let o be Element of the carrier' of S;
  cluster o`2 -> FinSequence-like for Function;
end;

definition
  let a be set;
  func idsym a -> set equals
:: CATALG_1:def 8
  [1,<*a*>];
  let b be set;
  func homsym(a,b) -> set equals
:: CATALG_1:def 9
  [0,<*a,b*>];
  let c be set;
  func compsym(a,b,c) -> set equals
:: CATALG_1:def 10
  [2,<*a,b,c*>];
end;

theorem :: CATALG_1:11
  for A being non empty set, S being CatSignature of A for a being
  Element of A holds idsym a in the carrier' of S & for b being Element of A
holds homsym(a,b) in the carrier of S & for c being Element of A holds compsym(
  a,b,c) in the carrier' of S;

definition
  let A be non empty set;
  let a be Element of A;
  redefine func idsym a -> OperSymbol of CatSign A;
  let b be Element of A;
  redefine func homsym(a,b) -> SortSymbol of CatSign A;
  let c be Element of A;
  redefine func compsym(a,b,c) -> OperSymbol of CatSign A;
end;

theorem :: CATALG_1:12
  for a,b being set st idsym(a) = idsym(b) holds a = b;

theorem :: CATALG_1:13
  for a1,b1,a2,b2 being set st homsym(a1,a2) = homsym(b1,b2) holds
  a1 = b1 & a2 = b2;

theorem :: CATALG_1:14
  for a1,b1,a2,b2,a3,b3 being set st compsym(a1,a2,a3) = compsym(
  b1,b2,b3) holds a1 = b1 & a2 = b2 & a3 = b3;

theorem :: CATALG_1:15
  for A being non empty set, S being CatSignature of A for s being
  SortSymbol of S ex a,b being Element of A st s = homsym(a,b);

theorem :: CATALG_1:16
  for A being non empty set, o being OperSymbol of CatSign A holds
  o`1 = 1 & len o`2 = 1 or o`1 = 2 & len o`2 = 3;

theorem :: CATALG_1:17
  for A being non empty set, o being OperSymbol of CatSign A st o
  `1 = 1 or len o`2 = 1 ex a being Element of A st o = idsym(a);

theorem :: CATALG_1:18
  for A being non empty set, o being OperSymbol of CatSign A st o
  `1 = 2 or len o`2 = 3 ex a,b,c being Element of A st o = compsym(a,b,c);

theorem :: CATALG_1:19
  for A being non empty set, a being Element of A holds the_arity_of
  idsym(a) = {} & the_result_sort_of idsym(a) = homsym(a,a);

theorem :: CATALG_1:20
  for A being non empty set, a,b,c being Element of A holds the_arity_of
compsym(a,b,c) = <*homsym(b,c),homsym(a,b)*> & the_result_sort_of compsym(a,b,c
  ) = homsym(a,c);

begin :: Signature homomorphism generated by a functor

definition
  let C1,C2 be Category;
  let F be Functor of C1,C2;
  func Upsilon F -> Function of the carrier of CatSign the carrier of C1, the
  carrier of CatSign the carrier of C2 means
:: CATALG_1:def 11

  for s being SortSymbol of
  CatSign the carrier of C1 holds it.s = [0,(Obj F)*s`2];
  func Psi F -> Function of the carrier' of CatSign the carrier of C1, the
  carrier' of CatSign the carrier of C2 means
:: CATALG_1:def 12

  for o being OperSymbol of
  CatSign the carrier of C1 holds it.o = [o`1,(Obj F)*o`2];
end;

theorem :: CATALG_1:21
  for C1,C2 being Category, F being Functor of C1,C2 for a,b being
  Object of C1 holds (Upsilon F).homsym(a,b) = homsym(F.a,F.b);

theorem :: CATALG_1:22
  for C1,C2 being Category, F being Functor of C1,C2 for a being
  Object of C1 holds (Psi F).idsym(a) = idsym(F.a);

theorem :: CATALG_1:23
  for C1,C2 being Category, F being Functor of C1,C2 for a,b,c
  being Object of C1 holds (Psi F).compsym(a,b,c) = compsym(F.a,F.b,F.c);

theorem :: CATALG_1:24
  for C1,C2 being Category, F being Functor of C1,C2 holds Upsilon
  F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier
  of C2;

begin :: Algebra of morphisms

theorem :: CATALG_1:25
  for C being non empty set, A being MSAlgebra over CatSign C for
  a being Element of C holds Args(idsym(a), A) = {{}};

scheme :: CATALG_1:sch 1
  CatAlgEx { X, Y() -> non empty set, H(set,set) -> set,
  R(set,set,set,object,object) -> set, I(set) -> set}:
  ex A being strict MSAlgebra over CatSign X() st (for
a,b being Element of X() holds (the Sorts of A).homsym(a,b) = H(a,b)) & (for a
being Element of X() holds Den(idsym(a),A).{} = I(a)) & for a,b,c being Element
  of X() for f,g being Element of Y() st f in H(a,b) & g in H(b,c) holds Den(
  compsym(a,b,c),A).<*g,f*> = R(a,b,c,g,f)
provided
 for a,b being Element of X() holds H(a,b) c= Y() and
 for a being Element of X() holds I(a) in H(a,a) and
 for a,b,c being Element of X() for f,g being Element of Y() st f in
H(a,b) & g in H(b,c) holds R(a,b,c,g,f) in H(a,c);

definition
  let C be Category;
  func MSAlg C -> strict MSAlgebra over CatSign the carrier of C means
:: CATALG_1:def 13


  ( for a,b being Object of C holds (the Sorts of it).homsym(a,b) = Hom(a,b)) &
  (for a being Object of C holds Den(idsym(a),it).{} = id a) & for a,b,c being
Object of C for f,g being Morphism of C st dom f = a & cod f = b & dom g = b &
  cod g = c holds Den(compsym(a,b,c),it).<*g,f*> = g(*)f;
end;

theorem :: CATALG_1:26
  for A being Category, a being Object of A holds Result(idsym a,
  MSAlg A) = Hom(a,a);

theorem :: CATALG_1:27
  for A being Category, a,b,c being Object of A holds Args(compsym
  (a,b,c), MSAlg A) = product <*Hom(b,c), Hom(a,b)*> & Result(compsym(a,b,c),
  MSAlg A) = Hom(a,c);

registration
  let C be Category;
  cluster MSAlg C -> disjoint_valued feasible;
end;

theorem :: CATALG_1:28
  for C1,C2 being Category, F being Functor of C1,C2 holds F-MSF(
  the carrier of CatSign the carrier of C1, the Sorts of MSAlg C1) is
ManySortedFunction of MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1, Upsilon
  F, Psi F);

theorem :: CATALG_1:29
  for C being Category, a,b,c being Object of C for x being set
holds x in Args(compsym(a,b,c), MSAlg C) iff ex g,f being Morphism of C st x =
  <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c;

theorem :: CATALG_1:30
  for C1,C2 being Category, F being Functor of C1,C2 for a,b,c
being Object of C1 for f,g being Morphism of C1 st f in Hom(a,b) & g in Hom(b,c
  ) for x being Element of Args(compsym(a,b,c),MSAlg C1) st x = <*g,f*> for H
  being ManySortedFunction of MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1,
  Upsilon F, Psi F) st H = F-MSF(the carrier of CatSign the carrier of C1, the
  Sorts of MSAlg C1) holds H#x = <*F.g,F.f*>;

theorem :: CATALG_1:31
  for C being Category, a,b,c being Object of C, f,g being
Morphism of C st f in Hom(a,b) & g in Hom(b,c) holds Den(compsym(a,b,c), MSAlg
  C).<*g,f*> = g(*)f;

theorem :: CATALG_1:32
  for C being Category, a,b,c,d being Object of C, f,g,h being Morphism
of C st f in Hom(a,b) & g in Hom(b,c) & h in Hom(c,d) holds Den(compsym(a,c,d),
  MSAlg C).<*h, Den(compsym(a,b,c), MSAlg C).<*g,f*>*> = Den(compsym(a,b,d),
  MSAlg C).<*Den(compsym(b,c,d), MSAlg C).<*h,g*>, f*>;

theorem :: CATALG_1:33
  for C being Category, a,b being Object of C, f being Morphism of C st
f in Hom(a,b) holds Den(compsym(a,b,b), MSAlg C).<*id b, f*> = f & Den(compsym(
  a,a,b), MSAlg C).<*f, id a*> = f;

theorem :: CATALG_1:34
  for C1,C2 being Category, F being Functor of C1,C2 ex H being
ManySortedFunction of MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1, Upsilon
  F, Psi F) st H = F-MSF(the carrier of CatSign the carrier of C1, the Sorts of
MSAlg C1) & H is_homomorphism MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1,
  Upsilon F, Psi F);