Co-tabulations, Bicolimits and Van-Kampen Squares in Collagories Electronic Communications of the EASST Volume 29 (2010) Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010) Co-tabulations, Bicolimits and Van-Kampen Squares in Collagories Wolfram Kahl 15 pages Guest Editors: Jochen Küster, Emilio Tuosto Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST Co-tabulations, Bicolimits and Van-Kampen Squares in Collagories Wolfram Kahl∗ kahl@cas.mcmaster.ca, http://sqrl.mcmaster.ca/∼kahl/ Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada Abstract: We previously defined collagories essentially as “distributive allegories without zero morphisms”. Collagories are sufficient for accommodating the relation-algebraic ap- proach to graph transformation, and closely correspond to the adhesive categories important for the categorical DPO approach to graph transformation. Heindel and Sobociński have recently characterised the Van-Kampen colimits used in adhe- sive categories as bicolimits in span categories. In this paper, we study both bicolimits and lax colimits in collagories. We show that the relation-algebraic co-tabulation concept is equivalent to lax colimits of difunctional mor- phisms and to bipushouts, but much more concise and accessible. From this, we also obtain an interesting characterisation of Van-Kampen squares in collagories. Keywords: Relation-algebraic graph transformation, Collagories, Allegories, Pushout, Adhesive categories 1 Introduction One of the hallmarks of the relation-algebraic approach to graph transformation [Kaw90, Kah01, Kah04] is that it allows an abstract characterisation of the gluing condition for the double pushout approach. Nevertheless, the categorical approach to graph transformation has continued to use the node-and-edge-based formulation of the gluing condition even in the handbook chap- ter [CMR+97]. Recently, the literature of the categorical approach, starting essentially with [EPPH06] has adopted the “adhesive categories” of Lack and Sobociński [LS04], where how- ever the details of the gluing condition are completely sidestepped. In [Kah09a], we introduced collagories essentially as “distributive allegories without zero morphisms”. We redeveloped in collagories the fundamentals of the relation-algebraic approach to graph transformation, and showed that adhesive categories arise, and also that bitabular col- lagories share the most important construction principles, such as slice and co-slice category constructions, with adhesive categories. Inspired by Heindel and Sobociński’s characterisation of van Kampen squares as bicolimits in the bicategory of spans [HS09], we establish in this paper (Sect. 6) the connections between our co-tabulations and bicolimits in collagories, succeding to show that the co-tabulation characteri- sation of pushouts, which essentially goes back to Kawahara [Kaw90], has a precise categorical counterpart in bipushouts, and, even more closely, in lax colimits of difunctional morphisms in a collagory context. We also succeed in providing, in Sect. 7, an original collagory-theoretic characterisation of van Kampen squares, significantly advancing over the results of [Kah09a, Kah09b]. ∗ This research is supported by the National Science and Engineering Research Council of Canada (NSERC). 1 / 15 Volume 29 (2010) mailto:kahl@cas.mcmaster.ca http://sqrl.mcmaster.ca/~kahl/ Co-tabulations, Bicolimits and Van-Kampen Squares in Collagories 2 Categories, Allegories This section only serves to fix notation and terminology for standard concepts, see [FS90, SS93, Kah04]. Like Freyd and Scedrov and a slowly increasing number of categorists, we denote com- position in “diagram order” not only in relation-algebraic contexts, where this is customary, but also in the context of categories. We will always use the infix operator “.,” to make composition explicit: R ., S = A R-B S-C . Definition 2.1. A category C is a tuple (ObjC, MorC, src, trg, I, .,) where • ObjC is a collection of objects. • MorC is a collection of arrows or morphisms. • src (resp. trg) maps each morphism to its source (resp. target) object. Instead of src(f ) = A ∧ trg(f ) = B we write f : A → B. The collection of all morphisms f with f : A → B is denoted as MorC[A , B] and also called a homset. • “.,” is the binary composition operator, and composition of two morphisms f : A → B and g : B′ → C is defined iff B = B′, and then (f ., g) : A → C ; composition is associative. • I associates with every object A a morphism IA which is both a right and left unit for com- position. Definition 2.2. An ordered category is a category C such that • for each two objects A and B, the relation vA ,B is a partial order on MorC[A , B] (the indices will usually be omitted), and • composition is monotonic with respect to v in both arguments. For homsets that have least or greatest elements, we introduce corresponding notation: Definition 2.3. In an ordered category, for each two objects A and B we introduce the following notions: • If the homset MorC[A , B] contains a greatest element, this is denoted >>A ,B . • If the homset MorC[A , B] contains a least element, this is denoted ⊥⊥A ,B . For these extremal morphisms and for identities we frequently omit indices where these can be induced from the context. Definition 2.4. An ordered category with converse, or OCC, is an ordered category such that • each morphism R : A → B has a converse R` : B → A , • the involution equations hold for all R : A → B and S : B → C : (R`)` = R I`A = IA (R ., S)` = S`., R` • conversion is monotonic with respect to v. Many standard properties of relations can be characterised in the context of OCCs [Kah04]: Definition 2.5. A morphism R : A → B in an OCC is called: • univalent iff R`., R v IB , • total iff IA v R ., R `, • injective iff R ., R`v IA , • surjective iff IB v R `., R, • a mapping iff it is univalent and total, Proc. GT-VMT 2010 2 / 15 ECEASST • bijective iff it is injective and surjective, • difunctional iff R ., R`., R v R. For an OCC C, we write Map C for the sub-category of C that contains only the mappings as arrows. Difunctionality will play an important rôle in this paper; a concrete relation, understood as a Boolean matrix, is difunctional iff it can be rearranged into “loose block-diagonal form”, with full rectangular blocks such that there is no overlap between different blocks in either direction. (See [SS93, 4.4] for more about difunctionality). For endomorphisms, there are a few additional properties of interest: Definition 2.6. A morphism R : A → A in an OCC is called: • reflexive iff I v R, • transitive iff R ., R v R, and idempotent iff R ., R = R, • co-reflexive or a sub-identity iff R v IA , • symmetric iff R`v R, • an equivalence iff it is symmetric, reflexive and transitive. Lemma 2.7. If B P� A Q-C is a span and P` ., Q is difunctional, then P ., P` ., Q ., Q` is idem- potent. If P and Q are moreover total, then P ., P`., Q ., Q` is an equivalence. PROOF: The first claim is immediate: P ., P`., Q ., Q`., P ., P`., Q ., Q` = P ., P`., Q ., Q`. For the second claim, reflexivity is obvious from totality, and the first claim implies transitivity, and, together with totality, also symmetry: Q ., Q `., P ., P ` = IA ., Q ., Q `., P ., P `., IA v P ., P `., Q ., Q `., P ., P `., Q ., Q ` = P ., P`., Q ., Q` While Freyd and Scedrov [FS90] derive the homset ordering in their allegories from the meet operation, we define allegories on top of ordered categories — the composition operator has higher precedence than all other binary operators. Definition 2.8. An allegory is an OCC such that • each homset is a lower semilattice with binary meet u. • for all Q : A → B, R : B → C , and S : A → C , the modal rule holds: Q ., RuS v (QuS ., R`) ., R . The most well-known allegory is the category Rel of sets with relations and standard relational operations. Logical theories give rise to allegories of derived predicates [FS90, App. B]. A sim- pler case of that are the allegories arising from Σ-algebras (over some signature Σ) as objects, and with “relational Σ-homomorphisms”, i.e. bisimulations in the sense of [Kah04], as morphisms. In allegories, one can define domain and range operators: Definition 2.9. For every morphism R : A ↔ B in an allegory, we define dom R : A ↔ A and ran R : B ↔ B as: dom R := IA uR ., R ` ran R := IB uR `., R 3 / 15 Volume 29 (2010) Co-tabulations, Bicolimits and Van-Kampen Squares in Collagories 3 Collagories κ óλ λ α : glue In Freyd and Scedrov’s treatment, although allegories are not required to have zero-ary meets, distributive allegories are required to have zero-ary joins (least elements) together with distribu- tivity of composition over them, that is, the zero law ⊥⊥ ., R = ⊥⊥. In [Kah09a], we introduced an intermediate concept that does not assume anything about zero-ary joins: Definition 3.1. A collagory is an allegory where each homset is a distributive lattice with binary join t, and composition distributes over binary joins from both sides. We directly axiomatise difunctional closure, without introducing Kleene star: Definition 3.2. A difunctionally closed collagory is a collagory where, there is an additional unary operation ∗� which satisfies the following axioms for all R : A → B, Q : C → A , and S : B → C : Q′ : C → B, and S′ : A → C : R∗� = RtR∗� ., (R∗�)`., R∗� recursive definition Q ., R v Q′ ∧ Q′ ., R`., R v Q′ ⇒ Q ., R∗� v Q′ right induction R ., S v S′ ∧ R ., R`., S′ v S′ ⇒ R∗� ., S v S′ left induction We further define R∗B : A → A and R ∗C : B → B as: R∗B := ItR∗� ., (R∗�)` and R ∗C := It(R∗�)`., R∗� . In a difunctionally closed collagory, the operation ∗� produces difunctional closures [Kah09a]. Requiring least morphisms satisfying zero laws turns collagories into distributive allegories, which still heave a much weaker theory than relations in a topos, so graph structures (unary algebras) with relational graph homomorphism in particular also form collagories. In [Kah09a], we showed that the absence of the zero laws enables the presence of constant symbols (allowing for example pointed sets), and also that restrictions to sub-collagories in sig- nature reducts (for example fixing label sets) and nested algebra constructions (interpreting sig- natures in the mapping categories of arbitrary collagories instead of just in Map Rel) both con- struct new collagories. These constructions are directly useful for concrete modelling tasks, and for implementation of the resulting models as data structures; they also subsume the construc- tion methods presented by Lack and Sobociński [LS04] for adhesive categories, in particular comprising clice and co-slice category construction. 4 Tabulations and Co-tabulations Central to the connection between pullbacks and pushouts in categories of mappings on the one hand and constructions in relational theories on the other hand is the fact that a square of mappings commutes iff the “relation” induced by the source span is contained in that induced by the target co-span. The proof of this does not need the modal rule. A � � P @ @R Q B C @ @RR � � S D Proc. GT-VMT 2010 4 / 15 ECEASST Lemma 4.1. [FS90, 2.146] Given a square of mappings in an allegory as drawn above, we have P ., R = Q ., S iff P`., Q v R ., S`. This provides a first hint that in the relational setting, the identity of the two mappings P and Q does not matter when looking for a pushout of the span B P� A Q-C — we only need to con- sider the diagonal P` ., Q. Dually, when looking for a pullback of the co-span B R-D S� C , only R ., S` needs to be considered. The gap between the two ways of calculating the horizon- tal diagonal can be significant since R ., S` is always difunctional. In fact, Lemma 4.1 can be strenghtened: Lemma 4.2. Given a square of mappings in an allegory as drawn above, and existence of the difunctional closure of P`., Q, we have P ., R = Q ., S iff (P`., Q)∗� v R ., S`. PROOF: The “if” direction follows immediately from P`., Q v (P`., Q)∗� and the “if” direction of Lemma 4.1. For “only if”, assume P ., R = Q ., S. Then P`., Q v R ., S` by Lemma 4.1, and R ., S`., Q`., P ., P`., Q = R ., R`., P`., P ., P`., Q commutativity = R ., R`., P`., Q P unival. = R ., S`., Q`., Q commutativity v R ., S` Q unival. By left-induction for difunctional closure we therefore have (P`., Q)∗� v R ., S` . Producing the result span of a pullback (respectively the result co-span of a pushout) from the horizontal diagonal alone is, in some sense, a generalisation of Freyd and Scedrov’s splitting of idempotents; [Kah04] contains more discussion of this aspect. Definition 4.3. [FS90, 2.14] In an allegory, let a morphism V : B → C be given. The span B P� A Q-C of mappings P and Q is called a tabulation of V iff the following equations hold: P `., Q = V P ., P`uQ ., Q` = IA . A � �� P @ @@R Q B V - C B W - C @ @@RR � �� S D Definition 4.4. [Kah04] In a collagory, let a morphism W : B → C be given. The co-span B R-D S� C of mappings R and S is called a co-tabulation of W iff the following equations hold: R ., S ` = W R`., RtS`., S = ID . The first equation implies W ., W`., W = R ., S`., S ., R`., R ., S`v R ., S` = W (using univalence of R and S), so if W has a co-tabulation, it has to be difunctional. Furthermore, from univalence of R and S we also obtain the lax cocone conditions R` ., W = R`., R ., S`v S` and W ., S = R ., S`., S v R. The following equivalent characterisations provided by [Kah04] have the advantage that they are fully equational, without the implicit inclusions in the mapping conditions. This frequently 5 / 15 Volume 29 (2010) Co-tabulations, Bicolimits and Van-Kampen Squares in Collagories facilitates calculations. Note that IuV ., V` = dom V ; we use the expanded form to emphasise the duality. Proposition 4.5. In an allegory, the span B P� A Q-C is a tabulation of V : B → C if and only if the following equations hold: P `., Q = V P`., P = IuV ., V` Q`., Q = IuV`., V P ., P `uQ ., Q` = IA . Proposition 4.6. In a collagory, the co-span B R-D S� C is a co-tabulation of W : B → C iff the following equations hold: R ., S ` = W R ., R` = ItW ., W` S ., S` = ItW`., W R `., RtS`., S = ID . Definition 4.7. If an allegory has a tabulation for each morphism, we call it tabular. If a collagory has a co-tabulation for each morphism, we call it co-tabular, and if it is further- more tabular, we call it bi-tabular. Tabulations in an allegory are unique up to isomorphism (this uses the modal rule), and include the following special cases: • In a tabulation of a sub-identity, both tabulation morphisms are the induced sub-object injec- tion [FS90, 2.145]. • We can define a direct product of A and B to be a tabulation of a >>A ,B , provided that greatest morphism exists. The resulting direct product definition differs from that of [SS93] in extending naturally to “empty” objects (e.g., empty sets) by not demanding surjectivity of the projections, but only π`., π = dom>>A ,B and ρ `., ρ = ran>>A ,B . • If a co-span B R-D S� C of mappings is given, then each tabulation of R ., S` (there might be none) is a pullback in Map A [FS90, 2.147]. For a tabular allegory A, this implies that each pullback in Map A is isomorphic to a tab- ulation, and therefore is itself a tabulation. However, if A is not tabular, then a co-span B R-D S� C of mappings for which no tabulation of R ., S` exists may still have a pull- back in Map A, which then cannot be a tabulation. If an allegory is known to have all direct products and subobjects, then these can be used to construct a tabulation for each morphism. In a collagory, we have the following special cases of co-tabulations, dual to the special tabu- lations above: • In a co-tabulation of an equivalence relation, both R and S are the induced quotient projections. • We can define a direct sum of A and B to be a co-tabulation of ⊥⊥A ,B , if that least morphism exists. • If a span B P� A Q-C of mappings is given, and the difunctional closure W := (P` ., Q)∗� exists then each co-tabulation of W (there might be none) is a pushout in Map A [Kah09a]. The situation is, except for the addition of the difunctional closure, perfectly dual to the sit- uation for pullbacks described above: For a co-tabular collagory C, each pushout in Map C is isomorphic to a co-tabulation, and therefore is itself a co-tabulation. However, if C is not Proc. GT-VMT 2010 6 / 15 ECEASST co-tabular, then a span B P� A Q-C of mappings for which no co-tabulation of (P` ., Q)∗� exists may still have a pushout in Map C, which then cannot be a co-tabulation. If direct sums and quotients are available, then a co-tabulation can be constructed for each di- functional morphism. A co-tabulation for a difunctional closure Z∗� satisfies the following equations: R ., S ` = Z∗� R ., R` = Z∗B S ., S` = Z ∗C R`., RtS`., S = ID . This was introduced as a gluing for the morphism Z in [Kah01]. Kawahara is the first to have characterised pushouts relation-algebraically in essentially this way [Kaw90]; he used relation- algebraic operations on relations arising in toposes. Convention 4.8. For a square of morphisms as drawn at the beginning of this section, we say that • it is a tabulation iff B P� A Q-C is a tabulation for R ., S`, • it is a (direct) co-tabulation iff B R-D S� C is a co-tabulation for P`., Q, • it is a gluing iff B R-D S� C is a gluing for P` ., Q, that is, if it is a co-tabulation for (P`., Q)∗�. 5 The Gluing Condition in Collagories We can now state a relational variant of the gluing condition, first introduced by Kawahara [Kaw90]: Definition 5.1. Let two morphisms1 Φ : G → L and X : L → A in a collagory with pseudo- complements on subidentities be given.2 • We say that the identification condition holds iff X ., X`v It(ran Φ) ., X ., X`., ran Φ . • We say that the dangling condition holds iff ran Xt(ran X → ran (Φ ., X)) = I . The proofs that the gluing condition is sufficient for the existence of a pushout complement [Kaw90], and that injectivity of Φ is suf- ficient for unambiguity of the pushout complement [Kah01] carry over to the collagory setting, but are outside the scope of this paper. Another related condition is important in the context of the single-pushout approach [Löw90, LE91]: L Φ� G X ? Ξ pppppppppp? A Ψ pppppppppp� H Definition 5.2. In an allegory, we call X conflict-free for Φ iff ran (Φ ., X ., X`) v ran Φ. 1 Note that “X” is a capital “χ ”. 2 Pseudo-complements are residuation of meet in lower semilattice categories; where pseudo-complements exist, we denote the pseudo-complement or R with respect to S as R → S, and we have: XuR v S ⇔ X v (R → S) For example, the pseudo-complement of a subgraph R of a graph G with respect to another subgraph S consists of all nodes of G that are in S or not in R, and all edges in S or not in R that are also nor incident with nodes in R. Intuitively, R → S therefore is G with the parts of R outside S removed, and then also all dangling edges removed. 7 / 15 Volume 29 (2010) Co-tabulations, Bicolimits and Van-Kampen Squares in Collagories For a node-and-edges-level formulation of conflict-freeness it is well-known that the induced single-pushout squares have a total embedding of the right-hand side into the application graph [Löw90, Cor. 3.18.5]. The component-free formulation above was first given in [Kah01], where it is also shown (Thm. 5.4.11) that a restricting derivation step for a conflict-free redex produces a pushout of partial functions. 6 Co-tabulations as Bicolimits and Lax Colimits Ordered categories are a simple example of 2-categories and bicategories: For two morphisms R, S : A → B of an ordered category, there is at most one two-cell from R to S, and there is a two-cell from R to S iff R v S. Therefore, there is an invertible two-cell between R and S if and only if R = S. 6.1 OC-Colimits: Bicolimits in Ordered Categories The general notion of bicolimits takes as its point of departure a diagram defined via a functor from a category. We introduce a specialised variant of the definition used in [HS09] by restricting our attention to ordered categories. Definition 6.1. Given a category C, an (index) category J, a functor D : J → C defining a dia- gram, and an object D , a cocone η from D to D consists of a morphism ηA : D A → D in C for each object A of J, satisfying the following cocone commutativity condition: D F ., ηB = ηA for each morphism F : A → B in J. Definition 6.2. Given an ordered category C, an (index) category J, and a functor D : J → C, an OC-colimit of D is given by an object D of C, and a cocone η from D to D , satisfying the following conditions: 1. factorisation: for any other object D′ of C with cocone κ from D to D′, there is a morphism h : D → D′ in C with ηA ., h = κA for each object A in J. 2. isotony: for any other object D′ of C and any two morphisms h, h′ : D →D′, if ηA ., h v ηA ., h′ for all objects A in J, then h v h′. OC-colimits are unique up to isomorphism. 6.2 Lax Colimits in OCCs For lax cocones, we only need the concept of lax functor, which differs from the functor concept in that a lax functor D only needs to satisfy ID A v D IA and (D f ) ., (D g) v D(f ., g), see, e.g., [Stu05, Sect. 8, p. 37ff]. Again, we provide specialised definition of lax cocones and lax colimits for the ordered category case: Definition 6.3. Given an ordered category C, an (index) category J, a lax functor D : J → C defining a diagram, and an object D , a lax cocone η from D to D consists of a morphism Proc. GT-VMT 2010 8 / 15 ECEASST ηA : D A → D in C for each object A of J, satisfying the following cocone subcommutativity condition: D F ., ηB v ηA for each morphism F : A → B in J. Definition 6.4. Given an ordered category C, an (index) category J, and a lax functor D : J → C, a lax colimit of D is given by an object D of C, and a lax cocone η from D to D satisfying the following conditions 1. factorisation: for any object D′ of C with lax cocone κ from D to D′, there is a morphism U : D → D′ in C with ηA ., U = κA for each object A in J, 2. isotony: for any object D′ of C and any two morphisms U, U′ : D → D′, if ηA ., U v ηA ., U′ for each object A in J, then U v U′. Lax colimits are unique up to isomorphism, too. We now add the converse operator to our consideration of lax colimits, and when we use “•→•” to denote an OCC, that OCC has the homset from the first object A to the second, different object B contain exactly one morphism, say F, from A to B. As an OCC, it needs to also have F`, which will be the only morphism from B to A . Since in this OCC, also F ., F` ., F needs to exist as a morphism from A to B, it has to be equal to F, which therefore is difunctional. If a lax functor D maps F : A → B to W : A ′ → B′, then W ., W `., W = D F ., (D F)`., D F v D (F ., F`., F) = D F = W , so it can map F only to difunctional morphisms. Furthermore, if, for a lax cocone, its source J is considered as an OCC, this implies that for each morphism F : A →B in J, also the converse morphism F`: B →A needs to be considered. Such a lax cocone therefore automatically has to satisfy both the following conditions: D F ., ηB v ηA (D F)`., ηA v ηB } for each morphism F : A → B in J. Convention 6.5. Given a morphism W : B → C in the OCC C, we will frequently identify W with the functor D mapping the single morphism explicitly mentioned in the OCC •→• to W. (Since we are dealing with an OCC, that morphism also has a converse, which then must be mapped to W`.) A lax cocone from W to D therefore is a cospan B R-D S� C satisfying W ., S v R and W`., R v S. C @ @ @R S W 6 D � � �� R B C @ @ @R S H H H H H HHj S′ W 6 D Up p p p p p p p-D′ � � �� R � � � � � ��* R′ B We explicitly state the definition of resulting special case of lax colimits: 9 / 15 Volume 29 (2010) Co-tabulations, Bicolimits and Van-Kampen Squares in Collagories Definition 6.6. An OCC-colimit of W : B → C in the OCC C is a lax cocone B R-D S� C from W to D (with W ., S v R and W`., R v S) satisfying the following conditions: 1. factorisation: for any object D′ of C with lax cocone B R ′ -D′ S ′ � C from W to D′, there is a morphism U : D → D′ in C with R ., U = R′ and S ., U = S′ ; 2. isotony: for any object D′ of C and any two morphisms U, U′ : D → D′, if R ., U v R ., U′ and S ., U v S ., U′, then U v U′. The crucial aspect of the following theorem (proof in [Kah10]) is that it connects the respecive O*-limits for spans B P� A Q-C of mappings with those for the single difunctional mor- phisms (P`., Q)∗� (which do not need to be mappings). Theorem 6.7. If a span B P� A Q-C of mappings in a collagory is given, then a cospan B R-D S� C is an OCC-colimit for (P`., Q)∗� iff it is an OC-pushout (i.e., OC-colimit for a span) for B P� A Q-C . 6.3 OCC-Colimits are Co-tabulations In a collagory C that is not co-tabular, categorical pushouts in Map C are not necessarily gluings — the pushout conditions establish no connection between mappings and other morphisms, and pathological cases cannot be excluded. However, OC-colimits and OCC-colimits do establish the necessary connections; one direc- tion is easy to see (details in [Kah10]): Theorem 6.8. If a cospan B R-D S� C in a collagory is a co-tabulation of W : B →C , then it is also an OCC-colimit for W. We now show that all OCC-colimits (of necessarily difunctional morphisms) are in fact co- tabulations. The proof needs to rely on the lax colimit properties, and therefore needs to use appropriate lax cocones constructed from the morphisms known to exist for a given OCC-colimit. The following lemma already follows this pattern: Lemma 6.9. If, in an allegory, B R-D S� C is an OCC-colimit for W, then W`., R = S ., ran R W`., R ., R` = S ., R` W ., S = R ., ran S W ., S ., S` = R ., S` PROOF: Let R0 = W ., S and S0 = S. This defines a lax cocone B R0-D S0� C from W to D , since: W`., R0 = W `., W ., S v W`., R v S = S0 ; W ., S0 = W ., S = R0 . Then factorisation gives us a U0 : D →D such that R0 = W ., S = R ., U0 and S0 = S = S ., U0. Since R ., U0 = W ., S v R = R ., ID and S ., U0 = S v S ., ID , isotony gives us U0 v ID . So U0 is a sub-identity, and S = S ., U0 implies ran S v U0. Since composition of sub-identities is meet, we obtain the following (which implies U0 = ran S): W ., S = W ., S ., ran S = R ., U0 ., ran S = R ., ran S Proc. GT-VMT 2010 10 / 15 ECEASST Analogously, W`., R = S ., ran R also holds, and these further imply W `., R ., R ` = S ., R` and W ., S ., S` = R ., S` . Lemma 6.9 does not use difunctionality of W, and implies: W`., W ., W`., R = W`., W ., S ., ran R = W`., R ., ran S ., ran R = W`., R ., ran S = S ., ran R ., ran S = S ., ran R = W`., R and, analogously, W ., W`., W ., S = W ., S. Therefore, even with a weaker concept of OCC-colimit, we would still have, in some sense, “almost-difunctionality” of W. Lemma 6.9 did use allegory properties (for sub-identities); to show the opposite inclusion to Theorem 6.8 we need full collagories (detailed proof in [Kah10]): Theorem 6.10. If, in a collagory, W : B → C is a difunctional morphism and B R-D S� C is an OCC-colimit for W, then it is also a co-tabulation for W. In summary, we have shown in Theorem 6.7 that OC-pushouts (i.e., OC-colimits) of a span are the same as OCC-colimits of the difunctional closure of the composition across that span. Furthermore, OCC-colimits of difunctional morphisms are the same as co-tabulations, as shown in Theorems 6.8 and 6.10. 7 Van Kampen Squares in Collagories Adhesive categories as a more specific setting for double-pushout graph rewriting have been introduced by Lack and Sobociński [LS04, LS05]; the following two definitions are taken from there: Definition 7.1. A van Kampen square (i) is a pushout which satisfies the following condition: given a commutative cube (ii) of which (i) forms the bottom face and the back faces are pullbacks (where C is considered to be in the back), the front faces are pullbacks if and only if the top face is a pushout. C � � � M @ @ @R F A B @ @ @R G � � � N D (i) C ′ f -B′ � � m � � n A ′ g- c ? D′ ? b a ? C -F ? d B � �� M � �� N A -G D (ii) Definition 7.2. A category C is said to be adhesive if 1. C has pushouts along monomorphisms; 2. C has pullbacks; 3. pushouts along monomorphisms are van Kampen squares. 11 / 15 Volume 29 (2010) Co-tabulations, Bicolimits and Van-Kampen Squares in Collagories For more concise formulations, we define: Definition 7.3. A van Kampen setup in a collagory C for a square as in Def. 7.1(i) is a commuting cube in Map C as in Def. 7.1(ii) where the bottom square is a gluing and the two back squares are tabulations. In [Kah09b], the following two lemmas were only shown for co-tabulations (i.e., assuming that M` ., F is difunctional, and also of m` ., f where it is assumed to be a gluing), not for general gluings. In [Kah10], we show the following significantly strengthened versions. Lemma 7.4. In a collagory, if the front squares of a van Kampen setup are tabulations, then the top square is a gluing. If furthermore M`., F is difunctional, then m`., f is difunctional, too. Lemma 7.5. In a van Kampen setup where the top square is a gluing, the front squares are tabulations iff the following holds: m ., (m`., f )∗� ., f`uc ., c`v IC ′ The condition here is equivalent to the following inclusion in the lattice of equivalences on C ′: (m ., m`∨ f ., f`) ∧ c ., c` = IC ′ Since equivalence lattices are not necessarily distributive, we cannot derive this from the tabula- tion equations m ., m`∧ c ., c` = IC ′ and f ., f `∧ c ., c` = IC ′. From Lemmas 7.4 and 7.5, we also directly obtain a characterisation of van Kampen squares in bitabular collagories: Theorem 7.6. A gluing square (as in Def. 7.1(i)) in a bitabular collagory is van Kampen iff all its van Kampen setups (as in Def. 7.3) where the top square is a gluing satisfy the following: m ., (m`., f )∗� ., f`uc ., c`v IC ′ The bitabularity condition could be weakened, but even then, this characterisation theorem is still very different from the appropriate diagram instance of Heindel and Sobociński’s charac- terisation theorem [HS09, Theorem 22], due to the fact that, by assuming a gluing, we already restricted ourselves to “well-behaved” pushouts. Our theorem also stays more in the typical relation-algebraic spirit: instead of Heindel and Sobociński’s condition “a colimit exists”, we have a local inclusion to check. The universal quantification this is embedded in is essentially the same as in [HS09, Theorem 22]. An interesting question is whether there is a useful characterisation that employs a local con- dition only on the candidate square, beyond injectivity of one M and F, as used in the definition of adhesive categories. First we observe (proof in [Kah10]): Lemma 7.7. In a van Kampen setup where M ., M`uF ., F`v IC , the following hold: 1. f ., f`um ., m`., c ., c`v IC ′ 2. c ., c`um ., m`., f ., f`v IC ′ Injectivity of M makes M` ., F difunctional and also enforces injectivity of m and therewith di- functionality of m`., f . In the general case, however, we have seen above that difunctionality of m`., f requires not only difunctionality of M`., F, but also the front tabulation conditions. Proc. GT-VMT 2010 12 / 15 ECEASST This failure of difunctionality propagation can be understood as coming from the fact that in the difunctionality inclusion M` ., F ., F` ., M ., M` ., F v M` ., F, the right-hand side passes through a “C element” that may be distinct from the three “C elements” of the left-hand side. This distinct “C element” gives rise to a “C ′ element” that is, in the absence of the front tabulation conditions, determined only up to c ., c`. One way to avoid this unwanted factor is to specify that in any chain diagram documenting M ., M` ., F ., F` ., M ., M`, the fourth (i.e., last) C element needs to be one of the previous three C elements. Referring to so many elements simultaneously in a relation-algebraic way requires direct products — we use π and ρ as the projections. The following is one formulation of this condition: M ., M `., (π`uF ., F`., M ., M`., ρ`) v M ., M`., (π`u(F ., F`tM ., M`) ., ρ`) However, it is not hard to see that this is equivalent to the following, much simpler condition: F ., F `., M ., M `v F ., F`tM ., M` This is obviously satisfied if one of M and F is injective. It can also be strengthened to an equality, since M and F are both total. This implies symmetry: F ., F `., M ., M ` = F ., F`tM ., M` = M ., M`., F ., F` and, furthermore, difunctionality of M`., F: M `., F ., F `., M ., M `., F = M`., M ., M`., F ., F`., F = M`., F . Assuming also M ., M`uF ., F`v IC , we obtain f ., f `., m ., m` = f ., f`tm ., m`: f ., f`., m ., m` = f ., f`., m ., m`uc ., F ., F`., M ., M`., c` v f ., f`., m ., m`uc ., (F ., F`tM ., M`) ., c` assumption = f ., f`., m ., m`u(c ., c`., f ., f`tc ., c`., m ., m`) = (f ., f`., m ., m`uc ., c`., f ., f`)t(f ., f`., m ., m`uc ., c`., m ., m`) v f ., f`tm ., m` Lemma 7.7 Therefore, m`., f is difunctional, too, and together with Lemma 7.7 we obtain m ., (m`., f )∗� ., f`uc ., c` = m ., m`., f ., f`uc ., c`v IC ′ . Altogether we have shown the following: Theorem 7.8. In the category Map C of maps over a bi-tabular collagory C, pushouts for spans A M� C F-B that satisfy also F ., F `uM ., M`v IC and F ., F `., M ., M `v F ., F`tM ., M` are van Kampen squares. Both inclusions can be strengthened to equalities, and since the second condition implies difunctionality, both together imply that such pushouts are also pullbacks. 13 / 15 Volume 29 (2010) Co-tabulations, Bicolimits and Van-Kampen Squares in Collagories 8 Conclusion We have shown that, in collagories, lax colimits of single morphisms are the same as co-tabu- lations, and bicolimits of spans (bipushouts) are the same as gluings. Furthermore, the move from a span B P� A Q-C to the difunctional closure of P` ., Q preserves both kinds of colimits. (The opposite move could be achieved via a tabulation, and may still deserve to be spelt out.) We also strengthened our previous results about the two implications involved in van Kampen squares from difunctional spans to arbitrary spans, extracted a precise relation-algebraic condi- tion for van Kampen squares in collagories, and gave a new, purely local sufficient condition for van Kampen squares that is more general than the “pushouts along monomorphisms” used in adhesive categories. These two results together with the fact that the equational characterisation of co-tabulations enables a nice, calculational proof style make a strong case to employ collagories as a conve- nient basis for theoretical investigations of graph structure transformations. In addition, relation- algebraic formulations and reasoning are accessible to a wide audience due to the fact that in the intuitive special case of Rel, they can be understood as Boolean matrix operations. Future investigations will explore how these new conditions for van Kampen squares can be combined with the different variations of adhesive categories in a collagory setting, including the quasiadhesive categories of [LS05], and their applications. Bibliography [CMR+97] A. Corradini, U. Montanari, F. Rossi, H. Ehrig, R. Heckel, M. Löwe. Algebraic Approaches to Graph Transformation, Part I: Basic Concepts and Double Pushout Approach. In Rozenberg (ed.), Handbook of Graph Grammars and Computing by Graph Transformation, Vol. 1: Foundations. Chapter 3, pp. 163–245. World Scien- tific, Singapore, 1997. [EPPH06] H. Ehrig, J. Padberg, U. Prange, A. Habel. Adhesive High-Level Replacement Sys- tems: A New Categorical Framework for Graph Transformation. Fund. Inform. 74(1):1–29, 2006. http://iospress.metapress.com/content/f89c8ba4nbeq1xc4/ [FS90] P. J. Freyd, A. Scedrov. Categories, Allegories. North-Holland Mathematical Li- brary 39. North-Holland, Amsterdam, 1990. [HS09] T. Heindel, P. Sobociński. Van Kampen Colimits as Bicolimits in Span. In Kurz et al. (eds.), Algebra and Coalgebra in Computer Science, CALCO 2009. LNCS 5728, pp. 335–349. Springer, 2009. (To appear). doi:10.1007/978-3-642-03741-2 23 [Kah01] W. Kahl. A Relation-Algebraic Approach to Graph Structure Transformation. 2001. Habil. Thesis, Fakultät für Informatik, Univ. der Bundeswehr München, Techn. Re- port 2002-03, http://sqrl.mcmaster.ca/∼kahl/Publications/RelRew/. [Kah04] W. Kahl. Refactoring Heterogeneous Relation Algebras around Ordered Categories and Converse. J. Relational Methods in Comp. Sci. 1:277–313, 2004. http://www.jormics.org/ Proc. GT-VMT 2010 14 / 15 http://iospress.metapress.com/content/f89c8ba4nbeq1xc4/ http://dx.doi.org/10.1007/978-3-642-03741-2_23 http://sqrl.mcmaster.ca/~kahl/Publications/RelRew/ http://www.jormics.org/ ECEASST [Kah09a] W. Kahl. Collagories for Relational Adhesive Rewriting. In Berghammer et al. (eds.), Relations and Kleene Algebra in Computer Science, RelMiCS/AKA 2009. LNCS 5827, pp. 211–226. Springer, 2009. doi:10.1007/978-3-642-04639-1 [Kah09b] W. Kahl. Collagories for Relational Adhesive Rewriting. SQRL Report 56, Software Quality Research Laboratory, Department of Computing and Software, McMaster University, July 2009. 24 pages. In: http://sqrl.mcmaster.ca/sqrl reports.html. (Su- perseded by [Kah10]). [Kah10] W. Kahl. Collagory Notes, Version 1. SQRL Report 57, Software Quality Research Laboratory, Department of Computing and Software, McMaster University, Mar. 2010. 53 pages. In: http://sqrl.mcmaster.ca/sqrl reports.html. [Kaw90] Y. Kawahara. Pushout-Complements and Basic Concepts of Grammars in Toposes. Theoretical Computer Science 77:267–289, 1990. doi:10.1016/0304-3975(90)90171-D [LE91] M. Löwe, H. Ehrig. Algebraic Approach to Graph Transformation Based on Single Pushout Derivations. In Möhring (ed.), Graph-Theoretic Concepts in Computer Sci- ence, WG ’90. LNCS 484, pp. 338–353. Springer, 1991. doi:10.1007/3-540-53832-1 52 [Löw90] M. Löwe. Algebraic Approach to Graph Transformation Based on Single Pushout Derivations. Technical report 90/05, TU Berlin, 1990. [LS04] S. Lack, P. Sobociński. Adhesive Categories. In Walukiewicz (ed.), FOSSACS 2004. LNCS 2987, pp. 273–288. 2004. doi:10.1007/b95995 [LS05] S. Lack, P. Sobociński. Adhesive and quasiadhesive categories. RAIRO Inform. Théor. Appl. 39(3):511–545, 2005. doi:10.1051/ita:2005028 [SS93] G. Schmidt, T. Ströhlein. Relations and Graphs, Discrete Mathematics for Computer Scientists. EATCS-Monographs on Theoretical Computer Science. Springer, 1993. [Stu05] I. Stubbe. Categorical Structures Enriched in a Quantaloid: Categories, Distributors and Fuctors. Theory and Appl. of Categories 14(1):1–45, 2005. http://tac.mta.ca/tac/volumes/14/1/14-01abs.html 15 / 15 Volume 29 (2010) http://dx.doi.org/10.1007/978-3-642-04639-1 http://sqrl.mcmaster.ca/sqrl_reports.html http://sqrl.mcmaster.ca/sqrl_reports.html http://dx.doi.org/10.1016/0304-3975(90)90171-D http://dx.doi.org/10.1007/3-540-53832-1_52 http://dx.doi.org/10.1007/b95995 http://dx.doi.org/10.1051/ita:2005028 http://tac.mta.ca/tac/volumes/14/1/14-01abs.html Introduction Categories, Allegories Collagories Tabulations and Co-tabulations The Gluing Condition in Collagories Co-tabulations as Bicolimits and Lax Colimits OC-Colimits: Bicolimits in Ordered Categories Lax Colimits in OCCs OCC-Colimits are Co-tabulations Van Kampen Squares in Collagories Conclusion