Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### 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);

Back to top