spans

Stream: graph theory

[Kyle Miller]

Something I've been wanting to understand better is the relationship between two different ways of thinking about directed graphs.

[Kyle Miller]

The first is as an endomorphism in the category of spans, i.e.:

structure dgraph :=
(V : Type u)
(E : Type v)
(s t : E → V)

(This point of view gives the funny definition of a category, which is a monad in the 2-category of spans :upside_down:)

[Kyle Miller]

The second is using edge sets

structure dgraph' :=
(V : Type u)
(edges : V → V → Type v)

[Kyle Miller]

It's not hard going back and forth between these representations, and they seem to have their own strengths and weaknesses. (The first is good for when it's useful having E, and the second is good for paths and subgraphs, it seems.)

[Kyle Miller]

I was wondering (1) whether dgraph' is some sort of categorical construction like a span and (2) whether there is some generalized formal relationship between dgraph and dgraph'. (All I know is that dgraph' isn't a cospan. Well, as far as I can tell.)

[Julian Berman]

If it's not too basic of a question, can I ask what you mean by "good for when it's useful having E"?

[Julian Berman]

(Basically the first way is you have a collection of vertices and a collection of edges and some maps from edges that tell you which vertex is the "start" and which is the "end", yeah? And the second way is just edges are pairs of edges with some labels? And somehow the first way is more convenient when? When you have explicitly some E already?)

[Adam Topaz]

It's easy to go back and forth, and the two approaches are equivalent (except for the universes involved).

import data.equiv.basic

universes u v

structure dgraph :=
(V : Type u)
(E : Type v)
(s t : E → V)

structure dgraph' :=
(V : Type u)
(edges : V → V → Type v)

def foo : dgraph ≃ dgraph' :=
{ to_fun := λ X,
  { V := X.V,
    edges := λ A B, {f : X.E // X.s f = A ∧ X.t f = B } },
  inv_fun := λ X,
  { V := X.V,
    E := Σ (A B : X.V), X.edges A B,
    s := λ f, f.1,
    t := λ f, f.2.1 },
  left_inv := sorry,
  right_inv := sorry }

[Adam Topaz]

Actually, those sorry's aren't that easy... (maybe even false?! The correct thing to do is define an equivalence of categories.)

[Kyle Miller]

Julian Berman said:

If it's not too basic of a question, can I ask what you mean by "good for when it's useful having E"?

One example is you can say [fintype G.E] to deal with directed graphs with finitely many edges -- it's awkward saying you only have finitely many edges in the dgraph' version. Another is you can easily define edge labelings as functions G.E -> L. If you want a subset of edges that satisfy a given property, then set G.E avoids a bunch of dependent types.

The dgraph' one can be convenient when you know what the edge sets are between pairs of vertices, though you can always use a sigma type like in @Adam Topaz's code to construct an edge set this way. (The dgraph' one is also useful because it's compatible with how we think about morphism sets in categories. It's the structure version of has_hom.)

[Julian Berman]

Thanks that's very helpful.

[Kyle Miller]

Adam Topaz said:

Actually, those sorry's aren't that easy... (maybe even false?! The correct thing to do is define an equivalence of categories.)

Yeah, I think it needs some kind of equivalence that looks deeper into the types, and defining the categories and showing they're equivalent seems the right way to go.

I got to trying to show this in left_inv:

(Σ (A B : V), {f : E // s f = A ∧ t f = B}) = E

and that doesn't seem to be provable (type theory's made me uncomfortable saying something like this is false!)

[Bhavik Mehta]

Some time ago I played around with re-defining categories like this; that is with a type for the objects and another for the morphisms, and having source and target maps (and identity and all the other stuff you need) - the main thing I learnt from it was that working with sigma types for this sort of thing leads to a huge amount of pain very quickly. I did manage to get the 2-categorical equivalence between the two definitions, but it was unpleasant to do

[Kyle Miller]

Do you have any thoughts on why this is? I'm wondering if it's because the "a category is a monad in the 2-category of spans" approach needs all these pullbacks, and somehow the transformation to something like dgraph' bakes those in

[Adam Topaz]

You can try to fill in the holes here:

import category_theory.category
import category_theory.equivalence
import data.equiv.basic

open category_theory

universes u v

structure dgraph :=
(V : Type u)
(E : Type v)
(s t : E → V)

namespace dgraph

@[ext]
structure hom (A B : dgraph) :=
(mapV : A.V → B.V)
(mapE : A.E → B.E)
(maps {e} : mapV (A.s e) = B.s (mapE e))
(mapt {e} : mapV (A.t e) = B.t (mapE e))

instance : category dgraph :=
{ hom := hom,
  id := λ X,
  { mapV := id,
    mapE := id,
    maps := by tauto,
    mapt := by tauto },
  comp := λ X Y Z f g,
  { mapV := g.mapV ∘ f.mapV,
    mapE := g.mapE ∘ f.mapE,
    maps := λ e, by simp [f.maps, g.maps],
    mapt := λ e, by simp [f.mapt, g.mapt] } }

end dgraph

structure dgraph' :=
(V : Type u)
(edges : V → V → Type v)

namespace dgraph'

@[ext]
structure hom (A B : dgraph') :=
(mapV : A.V → B.V)
(mapE {X Y : A.V} : A.edges X Y → B.edges (mapV X) (mapV Y))

instance : category dgraph' :=
{ hom := hom,
  id := λ X,
  { mapV := id,
    mapE := λ _ _, id },
  comp := λ X Y Z f g,
  { mapV := g.mapV ∘ f.mapV,
    mapE := λ A B e, g.mapE (f.mapE e) } }

end dgraph'

@[simps]
def forward : dgraph ⥤ dgraph' :=
{ obj := λ X,
    { V := X.V,
      edges := λ A B, { e : X.E // X.s e = A ∧ X.t e = B } },
    map := λ X Y f,
    { mapV := f.mapV,
      mapE := λ A B e,
      { val := f.mapE e,
        property := begin
          split,
          conv_rhs {rw ←e.2.1},
          rw f.maps,
          refl,
          conv_rhs {rw ←e.2.2},
          rw f.mapt,
          refl,
        end } } }

@[simps]
def backward : dgraph' ⥤ dgraph :=
{ obj := λ X,
    { V := X.V,
      E := Σ (A B : X.V), X.edges A B,
      s := λ e, e.1,
      t := λ e, e.2.1 },
    map := λ X Y f,
    { mapV := f.mapV,
      mapE := λ e, ⟨f.mapV e.1, f.mapV e.2.1, f.mapE e.2.2⟩,
      maps := by tauto,
      mapt := by tauto } }

def AA : dgraph ≌ dgraph' :=
{ functor := forward,
  inverse := backward,
  unit_iso :=
  { hom :=
    { app := λ X,
      { mapV := id,
        mapE := λ e, ⟨X.s e,X.t e, ⟨e, by tauto⟩ ⟩,
        maps := by tauto,
        mapt := by tauto },
      naturality' := sorry },
    inv := _,
    hom_inv_id' := _,
    inv_hom_id' := _ },
  counit_iso := _,
  functor_unit_iso_comp' := _ }

[Bhavik Mehta]

Kyle Miller said:

Do you have any thoughts on why this is? I'm wondering if it's because the "a category is a monad in the 2-category of spans" approach needs all these pullbacks, and somehow the transformation to something like dgraph' bakes those in

This sounds reasonable, I think it's also that equality of sigma types means you get heq things floating about which creates a bunch of issues

[Adam Topaz]

I think you mean that a category is an algebra for this monad, right?

[Bhavik Mehta]

Kyle Miller said:

Julian Berman said:

If it's not too basic of a question, can I ask what you mean by "good for when it's useful having E"?

One example is you can say [fintype G.E] to deal with directed graphs with finitely many edges -- it's awkward saying you only have finitely many edges in the dgraph' version. Another is you can easily define edge labelings as functions G.E -> L. If you want a subset of edges that satisfy a given property, then set G.E avoids a bunch of dependent types.

Is there something wrong with defining finitely many edges to be "for every X,Y, edges X Y is a fintype"? I can believe edge labellings aren't as pleasant as in dgraph; but I think the awkwardness of dependent types here is a lot less than the awkwardness of sigma equality you get with dgraph (plus we're in mathlib, dependent types are everywhere anyway :) )

[Kyle Miller]

There's no issue with that notion of finiteness, I don't think. It's when you want to talk about the cardinality of the edge set that it's more annoying. (And when you want to do undirected graphs, I found it got even worse not having some kind of type of all edges.)

I think dgraph vs dgraph' is a matter of application. For categories, composition is important, so dgraph' seems (and seems to have proven) to be better there.

Something I want to experiment sometime is dgraph along with this definition:

def dgraph.edges (G : dgraph.{u v}) (v w : G.V) : Type v :=
{e : G.E // G.s e = v ∧ G.t e = w}

which gives dgraph the dgraph' interface, and then using that definition as much as possible in the API. It potentially seems like the best of both worlds, though taking spanning subgraphs won't be as nice as dgraph'.

[Kyle Miller]

Adam Topaz said:

I think you mean that a category is an algebra for this monad, right?

I'm not too familiar with algebras for monads, but if you're thinking of a monad functorially, then I think that's equivalent (I'm imagining the functor of fiber-product-with? not completely sure though). A Baez tweet led me to this article, which describes monads in monoidal 2-categories, which is a monoid in an endomorphism category with some additional coherence laws.

[Adam Topaz]

@Kyle Miller see the following:
https://ncatlab.org/nlab/show/internal+category

[Adam Topaz]

Especially around the "Alternative Definition" section

[Adam Topaz]

So yes they say it's a monad in spans

[Kyle Miller]

I also realize I have no idea what I was talking about with that last message -- somehow I thought you were saying a module rather than algebra, but that doesn't seem to work. What does it mean for a category to be an algebra for the monad?

[Adam Topaz]

But I like to think of it like this: there is an obvious forgetful functor from the category of categories to dgraph. This has a left adjoint (the free category on a dgraph), and forgetting again yields a monad on dgraph. The algebras for this monad are categories, i.e. this forgetful functor is monadic (in the terminology around the Barr-Beck theorem)

[Adam Topaz]

Essentially the data of an algebra for this monad is the data of a composition rule and identity morphisms, and the associativity condition tells you that the axioms of a category hold true

[Bhavik Mehta]

def AA : dgraph ≌ dgraph' :=
equivalence.mk forward backward
  (begin
    apply (nat_iso.of_components _ _).symm,
    { intro X,
      refine ⟨_, _, _, _⟩,
      { refine ⟨id, λ e, e.2.2.1, _, _⟩;
        tidy },
      { refine ⟨id, λ e, ⟨X.s e, X.t e, e, by tauto⟩, _, _⟩;
        tauto },
      { apply_auto_param },
      { apply_auto_param } },
    { tidy }
  end)
  (begin
    apply (nat_iso.of_components _ _).symm,
    { intro E,
      refine ⟨_, _, _, _⟩,
      { exact ⟨id, λ X Y f, ⟨⟨_, _, f⟩, rfl, rfl⟩⟩ },
      { refine ⟨id, _⟩,
        rintro _ _ ⟨⟨x, y, e⟩, rfl, rfl⟩,
        apply e },
      { apply_auto_param },
      { apply_auto_param } },
    { tidy }
  end)

[Bhavik Mehta]

Tangentially related to this, I'm trying to define the (arbitrary) coproduct of categories as a sigma-type, and it's turning out painful (much like virtually everything with sigma and categories in Lean), what was it like defining the disjoint union of dgraph's?