:: Algebra of Morphisms
:: by Grzegorz Bancerek
::
:: Received January 28, 1997
:: Copyright (c) 1997-2019 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);