The abstract of the Mizar article:

Algebra of Morphisms

by

Grzegorz Bancerek

Received January 28, 1997

MML identifier: CATALG_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, PRALG_1, RELAT_1, PBOOLE, PROB_1, TARSKI, FUNCT_6,
      MSUALG_3, BOOLE, FINSEQ_1, FINSEQ_2, MSUALG_1, MATRIX_1, ZF_REFLE, AMI_1,
      MSAFREE, PROB_2, MSATERM, MCART_1, MSUALG_6, CAT_5, INSTALG1, FUNCT_5,
      QC_LANG1, CAT_1, PUA2MSS1, CARD_3, TDGROUP, ALG_1, CATALG_1, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0,
      NAT_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2, MSAFREE1, FINSEQ_1, FINSEQ_2,
      PROB_1, CARD_3, FINSEQ_4, FUNCT_5, FUNCT_6, STRUCT_0, PBOOLE, PRALG_1,
      MSUALG_1, MSUALG_3, MSAFREE, MSATERM, EXTENS_1, PUA2MSS1, MSUALG_6,
      INSTALG1, CAT_1;
 constructors ENUMSET1, CAT_1, FINSEQ_4, MSATERM, EXTENS_1, PUA2MSS1, MSUALG_6,
      INSTALG1, TWOSCOMP, MSAFREE1, MEMBERED, XCMPLX_0, ARYTM_0, ORDINAL2,
      FACIRC_1, ORDINAL1, NAT_1;
 clusters SUBSET_1, STRUCT_0, RELSET_1, FUNCT_1, FINSEQ_1, FINSEQ_2, PRALG_1,
      PBOOLE, MSUALG_1, MSAFREE, INSTALG1, ARYTM_3, XBOOLE_0, MEMBERED,
      ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


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 set 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;

theorem :: CATALG_1:4
 for A being set, i being Nat, p being FinSequence holds
   p in i-tuples_on A iff len p = i & rng p c= A;

theorem :: CATALG_1:5
 for A being set, i being Nat, p being FinSequence of A holds
   p in i-tuples_on A iff len p = i;

theorem :: CATALG_1:6
   for A being set, i being Nat holds i-tuples_on A c= A*;

theorem :: CATALG_1:7
 for A being set, i being Nat holds i <> 0 & A = {} iff i-tuples_on A = {};

theorem :: CATALG_1:8
 for A,x being set holds x in 1-tuples_on A iff
  ex a being set st a in A & x = <*a*>;

theorem :: CATALG_1:9
   for A,a being set st <*a*> in 1-tuples_on A holds a in A;

theorem :: CATALG_1:10
 for A,x being set holds x in 2-tuples_on A iff
  ex a,b being set st a in A & b in A & x = <*a,b*>;

theorem :: CATALG_1:11
 for A,a,b being set st <*a,b*> in 2-tuples_on A holds a in A & b in A;

theorem :: CATALG_1:12
 for A,x being set holds x in 3-tuples_on A iff
  ex a,b,c being set st a in A & b in A & c in A & x = <*a,b,c*>;

theorem :: CATALG_1:13
   for A,a,b,c being set st <*a,b,c*> in 3-tuples_on A holds a in A & b in A &
c
in A;

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

 attr A is empty means
:: CATALG_1:def 3

  the Sorts of A is empty-yielding;
end;

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

definition
 let S be non empty non void ManySortedSign;
 let X be non-empty ManySortedSet of the carrier of S;
 cluster FreeMSA X -> disjoint_valued;
end;

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

definition
 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;

definition
 cluster non empty-yielding Function;
end;

begin :: Signature of a category

definition
 let A be set;
 canceled;

 func CatSign A -> strict ManySortedSign means
:: CATALG_1:def 5

  the carrier of it = [:{0},2-tuples_on A:] &
  the OperSymbols 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;

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

definition
 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 6

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

definition
 cluster Categorial -> non void (non empty Signature);
end;

definition
 cluster Categorial non empty strict Signature;
end;

definition
 mode CatSignature is Categorial Signature;
end;

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

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

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

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

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

definition
 let A be set;
 cluster strict CatSignature of A;
end;

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

definition
 let S be ManySortedSign;
 func underlay S means
:: CATALG_1:def 8

   for x being set holds x in it iff
    ex a being set, f being Function st
     [a,f] in (the carrier of S) \/ (the OperSymbols of S) & x in rng f;
end;

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

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

  ex f being Function of NAT,NAT st
   (for s being set st s in the carrier of S
     ex i being 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 set st o in the OperSymbols of S
     ex i being Nat, p being FinSequence st o = [i,p] & len p = f.i &
       [:{i}, (f.i)-tuples_on underlay S:] c= the OperSymbols of S);
end;

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

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

theorem :: CATALG_1:16
 for S being delta-concrete ManySortedSign, x being set
  st x in the carrier of S or x in the OperSymbols of S
 ex i being Nat, p being FinSequence st x = [i,p] & rng p c= underlay S;

theorem :: CATALG_1:17
   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 OperSymbols of S & [i,p2] in the OperSymbols of S
  holds len p1 = len p2;

theorem :: CATALG_1:18
   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 OperSymbols of S implies [i,p2] in the OperSymbols of S);

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

begin :: Symbols of categorial sygnature


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

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

definition
 let S be non void delta-concrete ManySortedSign;
 let o be Element of the OperSymbols of S;
 cluster o`2 -> Relation-like Function-like;
end;

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

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

definition
 let S be non void delta-concrete ManySortedSign;
 let o be Element of the OperSymbols of S;
 cluster o`2 -> FinSequence-like;
end;

definition let a be set;
 func idsym a equals
:: CATALG_1:def 10

   [1,<*a*>];
 let b be set;
 func homsym(a,b) equals
:: CATALG_1:def 11

   [0,<*a,b*>];
 let c be set;
 func compsym(a,b,c) equals
:: CATALG_1:def 12

   [2,<*a,b,c*>];
end;

theorem :: CATALG_1:20
 for A being non empty set, S being CatSignature of A
 for a being Element of A holds idsym a in the OperSymbols 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 OperSymbols of S;

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

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

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

theorem :: CATALG_1:23
 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:24
 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:25
 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:26
 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:27
 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:28
 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:29
 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 Objects of C1,
                               the carrier of CatSign the Objects of C2 means
:: CATALG_1:def 13

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

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

theorem :: CATALG_1:30
 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:31
 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:32
 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:33
 for C1,C2 being Category, F being Functor of C1,C2 holds
   Upsilon F, Psi F form_morphism_between
    CatSign the Objects of C1, CatSign the Objects of C2;

begin :: Algebra of morphisms

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

scheme CatAlgEx { X, Y() -> non empty set,
    H(set,set) -> set, R(set,set,set,set,set) -> 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 Objects of C means
:: CATALG_1:def 15

  (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;

canceled;

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

theorem :: CATALG_1:37
 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);

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

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

theorem :: CATALG_1:39
 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:40
 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 Objects of C1, Upsilon F, Psi F)
 st H = F-MSF(the carrier of CatSign the Objects of C1, the Sorts of MSAlg C1)
 holds H#x = <*F.g,F.f*>;

canceled;

theorem :: CATALG_1:42
 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:43
   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:44
   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:45
   for C1,C2 being Category, F being Functor of C1,C2
 ex H being ManySortedFunction of MSAlg C1,
   (MSAlg C2)|(CatSign the Objects of C1, Upsilon F, Psi F) st
  H = F-MSF(the carrier of CatSign the Objects of C1, the Sorts of MSAlg C1) &
  H is_homomorphism MSAlg C1,
    (MSAlg C2)|(CatSign the Objects of C1, Upsilon F, Psi F);