category of graphs

Stream: graph theory

[Jalex Stark]

@Alena Gusakov and I started trying to define this together, but we detoured into doing Scott's lftcm exercises and don't have a definition

[Jalex Stark]

I think there is a category file in branch#hedetniemi ?

[Jalex Stark]

oh, maybe I'm wrong, they do have this, though

def as_graph (C) [category_theory.category C] : directed_multigraph C :=
{ edge := λ x y, x ⟶ y }

[Aaron Anderson]

There are a few different definitions?

[Aaron Anderson]

In your attempts so far, are the morphisms homomorphisms or embeddings?

[Kyle Miller]

I think that's the definition that takes a category and reinterprets it as a directed multigraph

[Kyle Miller]

it's like the inverse of has_hom (but not quite)

[Jalex Stark]

the category of homormorphisms is more interesting

[Kyle Miller]

@Aaron Anderson in your definition of embedding, why did you make it so that image must be an induced graph? I haven't checked, but I don't think that's what a monomorphism would be given your definition of a homomorphism.

[Aaron Anderson]

The real reason is that that's the definition of an embedding from model theory, but I can think of a few justifications

[Kyle Miller]

It's not what I would expect from the word 'embedding'. I'd like to be able to define a path as an embedding of a path graph, for example. What's a use of your definition of an embedding with respect to graph theory?

[Aaron Anderson]

When showing the random graph is unique, you use an increasing chain of partial embeddings between two random graphs, and you want this definition

[Aaron Anderson]

Sometimes you do want an embedding to have to be an isomorphism onto its image

[Aaron Anderson]

According to nLab, my definition corresponds to a "regular mono"

[Aaron Anderson]

And they philosophically say "A monomorphism is regular if it behaves like an embedding."

[Kyle Miller]

I guess the analogue in topology is that this is the difference between a smooth embedding and an injective smooth map. I tend to think of graphs as being topologically realized, which means arbitrary subdivisions of edges are equivalent, at least as far as maps are concerned. However, if you cannot subdivide edges, then as a simplicial map the embedding really would need to have an image that's an induced subgraph. (Topologically, you want the simplicial image to have a regular neighborhood. Injective graph homomorphisms don't have these in general.)

[Bhavik Mehta]

It's probably worth noting the nlab's definition of the category of graphs as well: https://ncatlab.org/nlab/show/category+of+simple+graphs

[Bhavik Mehta]

Although there's also: https://ncatlab.org/nlab/show/the+category+of+simple+graphs+from+a+graph-theoretic+perspective

[Kyle Miller]

Something I'd like to be true is that if $G'$ is a subgraph of $G$, then there is some notion of an embedding $G' \hookrightarrow G$.

[Bhavik Mehta]

"monos in SimpGph are simple graph maps that are injective on vertices and edges,"

[Bhavik Mehta]

Pretty sure this matches what you want?

[Aaron Anderson]

Yeah, I’d be in favor of having bundled monos and regular monos, but I prefer the regular monos get the name and symbol of embeddings.

[Kyle Miller]

Yeah, exactly. I believe that regular monomorphisms are useful, too, but I'd like to make sure that there is notation for monomorphisms.

[Bhavik Mehta]

In the category theory library, neither of these are bundled (which I think is a good thing) and they're all typeclasses (which I think might be a bad thing)

[Bhavik Mehta]

I can certainly see the value of bundling them for graphs though

[Aaron Anderson]

It’s also nice that the regular mono version is available as an abbreviation

[Aaron Anderson]

I do add those abbreviations in #3946

[Aaron Anderson]

Cycling this thread back around, I’d be happy to help define the category, as I think I understand how bundled categories work

[Bhavik Mehta]

I wonder how horrible it'd be to define the category of graphs like this instead: https://ncatlab.org/nlab/show/category+of+simple+graphs#properties_of_

[Jalex Stark]

so eventually we will have a theorem like

\forall \iota, (Graph.hom_of_embedding \iota).is_mono

?

[Jalex Stark]

uh, i hope you don't mean defining it via theorem 3.1

[Bhavik Mehta]

I do mean that, but I'm not seriously suggesting it as the definition

[Jalex Stark]

got it

[Bhavik Mehta]

I think I do basically have all the language and theory built up to prove most of that though

[Bhavik Mehta]

I expect it won't give results which aren't easier to prove directly but still!

[Jalex Stark]

I'm in favor of the goal "prove all of the theorems on the nlab page for which mathlib already has the categorical definitions"

[Jalex Stark]

and I think the same goal with "mathlib" replaced by "bhavik's topos repo" is interesting but I don't know enough math to contribute at all :sweat_smile:

[Bhavik Mehta]

Haha, entirely reasonable! Unless someone else is interested in helping me do it or there's a result which people who don't care about categories want out of it, I don't think I'll get to it any time soon either :)

[Jalex Stark]

Oh, i just noticed what you said on the other topic about requiring reflexivity. The most natural category of graphs in my mind allows self-loops but doesn't force them. The graph with a single vertex and a single edge is a terminal object.

[Jalex Stark]

But I want to express the property "G is not 3-colorable" as "G does not have a homomorphism to K_3", so I don't want K_3 to be pointed (where by "pointed" i mean "have a map from the terminal object", idk if that is a standard terminology)

[Bhavik Mehta]

Yeah there's sometimes friction between the 'natural' category and the one with lots of good categorical properties

[Alena Gusakov]

Hope I didn't miss anything earlier about this - is there a reason why we're not defining things in a way similar to monoids, e.g. having simple_graph be a class and having bundled structure graph_hom? I'm running into some issues with trying to define the category of simple graphs cause I can't seem to bundle things in a way where we can derive stuff.

[Aaron Anderson]

So the basic idea is that we sometimes want to study multiple graphs on the same type

[Aaron Anderson]

And so we can’t just have a type with an instance on it, because multiple non-equal instances are hard to juggle between

[Aaron Anderson]

But somehow they pulled that off with topological_space, where sometimes it’s an instance, and sometimes it’s not

[Alena Gusakov]

Ohhhh okay gotcha. Sorry, I think I did actually have that conversation with someone and forgot about it

[Aaron Anderson]

We should probably study the topology library and see if we maybe could get away with graph instances sometimes after all

[Bhavik Mehta]

I think it might be worth looking at options which don't use bundled then because it's designed for when the structure is a typeclass

[Kyle Miller]

There's nothing that says the class has to be associated to a type, by the way -- it's just that most algebraic objects tend to be referred to by their carrier type. You can associate it to the $V \to V \to \mathrm{Prop}$ relation if you wanted. (See the graph defs thread from today.) There is a very strong case to be made the adjacency relation is the graph.

I think with topological spaces, most of the time the underlying set has a natural topology, so it still makes sense for a typeclass even if you need the occasional escape hatch. I don't think anyone ever refers to the vertex set of a graph and assumes it has an associated graph structure.

But, if you insist on typeclasses on the vertex type, the trick you can do is something like this:

@[irreducible] def complete_graph (V : Type*) := V

instance {V : Type*} : simple_graph (complete_graph V) := sorry

but then you'd have to deal with the fact that the adjacency relation is defined on complete_graph V rather than V itself.

[Kyle Miller]

Given what @Bhavik Mehta pointed out on ncatlab, maybe this is a reasonable definition of the category? Regarding what @Jalex Stark was saying about colorability, it seems like you can define the notion of local injectivity (a function is locally injective if whenever f(v) = f(w), then v is not adjacent to w), and then a proper coloring is a locally injective graph homomorphism to a complete graph.

import category_theory.category
import tactic

open category_theory

universes u v w

structure simple_graph :=
(V : Type u)
(adj' : V → V → Prop)
(symm' : symmetric adj' . obviously)
(refl' : reflexive adj' . obviously)

namespace simple_graph

abbreviation adj {G : simple_graph.{u}} (u v : G.V) : Prop := G.adj' u v

infix ~ := adj
-- or infix ` ~g ` : 40 := adj

end simple_graph

@[ext]
structure hom (G : simple_graph.{u}) (G' : simple_graph.{v}) :=
(to_fun : G.V → G'.V)
(map_adj : ∀ ⦃v w : G.V⦄, v ~ w → to_fun v ~ to_fun w)

instance (G : simple_graph.{u}) (G' : simple_graph.{v}) : has_coe_to_fun (hom G G') :=
⟨_, hom.to_fun⟩

def hom.id (G : simple_graph.{u}) : hom G G :=
{ to_fun := id,
  map_adj := by tidy }

section hom

variables {G : simple_graph.{u}} {G' : simple_graph.{v}} {G'' : simple_graph.{w}}

def hom.trans (f : hom G G') (f' : hom G' G'') : hom G G'' :=
{ to_fun := ⇑f' ∘ ⇑f,
  map_adj := by { intros v w h, repeat { rw function.comp_app }, exact f'.map_adj (f.map_adj h) } }

def hom.locally_injective (f : hom G G') : Prop := ∀ ⦃v w : G.V⦄, f v = f w → ¬(v ~ w)

end hom

instance : has_hom (simple_graph.{u}) :=
{ hom := hom }

instance : category_struct (simple_graph.{u}) :=
{ id := hom.id,
  comp := @hom.trans }

instance : category (simple_graph.{u}) :=
{ }

def complete_graph (V : Type u) : simple_graph.{u} :=
{ V := V,
  adj' := λ v w, true }

/--
A coloring of the graph G by colors from α.
-/
structure coloring (G : simple_graph.{u}) (α : Type v) :=
(f : hom G (complete_graph α))
(proper : f.locally_injective)

[Kyle Miller]

I tried being a little careful about universes, allowing a homomorphism to go between graphs in different universes. The category itself only has graphs all in the same universe.

[Kyle Miller]

Anyway, this category supports homomorphisms to edge contractions, which is kind of nice.

[Kyle Miller]

(For subgraphs, you could define a category of subgraphs for each graph (morphisms are the poset of inclusions), then for each morphism in the category get an induced functor between subgraph categories. There'd also be the inclusion functor from a subgraph category back to the graph category, each morphism in the image being monic.)

[Kyle Miller]

Oh, I made a mistake with the definition of locally injective, and probably other things. I'm not used to the adjacency relation being reflexive!

One thing to remember is that you'd need the definition for neighbor_set to account for reflexivity:

variables {G : simple_graph.{u}}

def neighbor_set (v : G.V) : set G.V := {w : G.V | v ~ w ∧ v ≠ w}

def closed_neighbor_set (v : G.V) : set G.V := {w : G.V | v ~ w}

[Kyle Miller]

Another option is to define graphs as irreflexive symmetric relations then define homomorphisms in terms of the reflexive closure of the relation:

import category_theory.category
import tactic

open category_theory

universes u v w

structure simple_graph :=
(V : Type u)
(adj' : V → V → Prop)
(symm' : symmetric adj' . obviously)
(irrefl' : irreflexive adj' . obviously)

namespace simple_graph

abbreviation adj {G : simple_graph.{u}} (u v : G.V) : Prop := G.adj' u v

infix ~ := adj
-- or infix ` ~g ` : 40 := adj

abbreviation rel (G : simple_graph.{u}) (u v : G.V) : Prop := u ~ v ∨ u = v

variables {G : simple_graph.{u}}

def neighbor_set (v : G.V) : set G.V := {w : G.V | v ~ w}

def closed_neighbor_set (v : G.V) : set G.V := {w : G.V | G.rel v w}

end simple_graph

@[ext]
structure hom (G : simple_graph.{u}) (G' : simple_graph.{v}) :=
(to_fun : G.V → G'.V)
(map_adj : ∀ ⦃v w : G.V⦄, G.rel v w → G'.rel (to_fun v) (to_fun w))

instance (G : simple_graph.{u}) (G' : simple_graph.{v}) : has_coe_to_fun (hom G G') :=
⟨_, hom.to_fun⟩

def hom.id (G : simple_graph.{u}) : hom G G :=
{ to_fun := id,
  map_adj := by tidy }

section hom

variables {G : simple_graph.{u}} {G' : simple_graph.{v}} {G'' : simple_graph.{w}}

def hom.trans (f : hom G G') (f' : hom G' G'') : hom G G'' :=
{ to_fun := ⇑f' ∘ ⇑f,
  map_adj := by { intros v w h, repeat { rw function.comp_app }, exact f'.map_adj (f.map_adj h) } }

def hom.locally_injective (f : hom G G') : Prop := ∀ ⦃v w : G.V⦄, f v = f w → ¬(v ~ w)

end hom

instance : has_hom (simple_graph.{u}) :=
{ hom := hom }

instance : category_struct (simple_graph.{u}) :=
{ id := hom.id,
  comp := @hom.trans }

instance : category (simple_graph.{u}) :=
{ }

def complete_graph (V : Type u) : simple_graph.{u} :=
{ V := V,
  adj' := ne }

/--
A coloring of the graph G by colors from α.
-/
structure coloring (G : simple_graph.{u}) (α : Type v) :=
(f : hom G (complete_graph α))
(proper : f.locally_injective)

[Bhavik Mehta]

Kyle Miller said:

(For subgraphs, you could define a category of subgraphs for each graph (morphisms are the poset of inclusions), then for each morphism in the category get an induced functor between subgraph categories. There'd also be the inclusion functor from a subgraph category back to the graph category, each morphism in the image being monic.)

I'd hope also that the standard subobject lattice (as a poset) in the category would be the same as the poset of subgraphs as well, and the subobject lattice of an object in a category should be coming to mathlib in the next few days

[Bhavik Mehta]

Kyle Miller said:

There's nothing that says the class has to be associated to a type, by the way -- it's just that most algebraic objects tend to be referred to by their carrier type. You can associate it to the $V \to V \to \mathrm{Prop}$ relation if you wanted. (See the graph defs thread from today.) There is a very strong case to be made the adjacency relation is the graph.

I think with topological spaces, most of the time the underlying set has a natural topology, so it still makes sense for a typeclass even if you need the occasional escape hatch. I don't think anyone ever refers to the vertex set of a graph and assumes it has an associated graph structure.

But, if you insist on typeclasses on the vertex type, the trick you can do is something like this:

@[irreducible] def complete_graph (V : Type*) := V

instance {V : Type*} : simple_graph (complete_graph V) := sorry

but then you'd have to deal with the fact that the adjacency relation is defined on complete_graph V rather than V itself.

Yeah, I don't think in this context it's a great idea to have typeclasses on the vertex type, which I think is an argument against using the bundled API rather than an argument for a different def of graphs or anything like that - the bundled category design is intended for algebraic structures like you mention, which are set up in a different way to this

[Jalex Stark]

Jalex Stark said:

But I want to express the property "G is not 3-colorable" as "G does not have a homomorphism to K_3", so I don't want K_3 to be pointed (where by "pointed" i mean "have a map from the terminal object", idk if that is a standard terminology)

if G and H have no points, then there's a natural bijection between between points of the exponential object $G^H$ and actual morphisms $H \to G$

[Kyle Miller]

Regarding that ncatlab post @Bhavik Mehta pointed out, it's worth knowing that this is the 1-dimensional version of the category of simplicial complexes. A map of simplicial complexes is a function on vertex sets that sends simplices to simplices, but these simplices might be collapsed in different ways. For edges (1-simplices), they can either be sent to other edges or collapsed to a vertex (a 0-simplex).

Thinking forward to graphs as being 1-skeleta of arbitrary simplicial complexes, it is probably worth defining homomorphisms this way. (Plus you get that nice characterization of graph minors as being subquotients.)

[Kyle Miller]

Aaron Anderson said:

Yeah, I’d be in favor of having bundled monos and regular monos, but I prefer the regular monos get the name and symbol of embeddings.

Regarding this, I've created a topic about (regular) monomorphisms: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/embeddings.20and.20hook.20arrow.20notation.3A.20%28regular%29.20monomorphisms

It would be nice to match the way notation works in other parts of mathlib for this, if there's any precedent.

[Kyle Miller]

It might make sense using unadorned hook arrows for embeddings, but, for example, Lee's smooth manifolds book uses the hook arrow for smooth inclusion maps, and uses the word "embedding" as a modifier.

[Aaron Anderson]

I've pulled the graph maps out of my PR so we can keep discussing here.

[Aaron Anderson]

It seems that for topological purposes, it may just be better if we take the definition of a graph to be reflexive, instead of irreflexive, but for combinatorial purposes, we probably still want the usual edge-number formulas and stuff to be true.

[Aaron Anderson]

However, for those topological purposes, we'd probably rather be thinking about simplicial complexes anyway, and sometimes requiring they be only have 0 and 1 dimensional simplices.

[Aaron Anderson]

Is perhaps the solution to have the current irreflexive definition of graph, with its current definition of hom, as one category, and when we want to talk about that graph topologically, we use a function/functor from graphs to simplicial complexes, where there are a few more maps?

[Kyle Miller]

I tried out the reflexive version, and I kept getting confused because I kept forgetting the relation no longer corresponded to edges... This only really helps make the definitions of homomorphisms easier -- for this category it might be better to define it in terms of the reflexive closure of the relation.

[Kyle Miller]

Though, it might be better still to define it like

structure hom G G' :=
(to_fun : V G -> V G')
(map_prop : forall (v w : V G), v ~ w -> (f v = f w \/ f v ~ f w))

since having the reflexive closure on the L.H.S. of the implication is unnecessary. This matches the simplicial complex map definition.

[Kyle Miller]

The fact that minors are subquotients using this hom definition is compelling, I think

[Kyle Miller]

Do you know if there are any reasons to use the rel_hom-with-irreflexive-adjacency definition?

[Aaron Anderson]

Mostly for studying colorability

[Aaron Anderson]

that's really the only context where I've thought much about graph homomorphisms

[Aaron Anderson]

and tbh I think pretty much every definition we mention is going to be implemented eventually, it's just an issue of coming up for a name for each of the 18 categories we're gonna have

[Kyle Miller]

locally injective homomorphisms cover that case, at least

[Kyle Miller]

I haven't been able to determine whether that counts as an immersion or not

[Aaron Anderson]

What do you mean by locally injective?

[Kyle Miller]

I mean

def locally_injective (f : hom G G') := forall (v w : V G), v ~ w -> f v != f w

[Kyle Miller]

it seems somewhat useful in other contexts, too, like for walks of length n. It's a locally injective homomorphism of a path graph with n edges

[Aaron Anderson]

But anyway, I think I'd rather have irrefl_hom and refl_hom, with better names, and then have a theorem that says that a refl_hom is an irrefl_hom iff it's locally injective that have the definition of irrefl_hom be a function with the property v ~ w -> (f v = f w \/ f v ~ f w) /\ f v != f w

[Aaron Anderson]

As I view irrefl_hom as more basic, I'm inclined to call that just hom with the nomenclature ->g, and call the refl_hom something like top_hom or continuous or something, with a different nomenclature, but I really don't care what the nomenclature is at the end of the day.

[Kyle Miller]

Do you view it to be more basic because it's slightly easier to define? Maybe it's because you're thinking of it as being a homomorphism of models of graphs?

I'm having a hard time seeing it being that useful for anything other than graph coloring, and even for graph coloring I'd be more inclined to define graph colorings as their own thing since it's just a function that sends adjacent vertices to non-equal elements.

[Kyle Miller]

It seems like a lemma that graph colorings correspond to (locally injective) homomorphisms to complete graphs

[Aaron Anderson]

I view it as more basic because

• I'm used to model theory
• For multigraphs, it coincides with a pair, consisting of a vertex map and an edge map, which agree
• The only applications that I personally have thought about in any depth are coloring and walks, and those use it
• I've looked up a few internet sources (although none seem authoritative), and all of them use the irreflexive definition, except for nLab, mentions the irreflexive definition as standard before deciding they'd rather study the reflexive version

[Aaron Anderson]

@Jalex Stark, I have it in my head that you've spent some time getting comfortable with graph homomorphisms. Do you have a good source that could help us?

[Jalex Stark]

I think I spent a long time with uh chapter 8? Of godsil's algebraic graph theory

[Jalex Stark]

And asked a lot of dumb questions to william ballinger

[Aaron Anderson]

Jalex Stark said:

And asked a lot of dumb questions to william ballinger

Really the best way to learn any subject

[Aaron Anderson]

Godsil also uses the irreflexive definition. I think it's standard for combinatorial settings, where the reflexive definition is standard for topological settings, so I really think those are not so much the "homomorphisms" of graph theory as the "continuous maps" of graph theory

[Kyle Miller]

Ok, thanks for expanding on your inclinations.

Re model theory: it might be that the definition of a simple graph we have matches intuition but is the wrong structure, so the notion of a homomorphism might need to be non-standard.

Re multigraphs: there's a case to be made that they should be set up to allow edge contractions, but I don't have any idea how to do that cleanly. (I know how to do it, but no one, including me, would like using it.)

If I'm not mistaken, while graph minors are subquotients in the ncatlab category, they are also quotients of subobjects in the irrefl category. Edge contractions could correspond to a span of maps, rather than being a map itself.

Re walks: I see value in making a length-n walk be exactly a homomorphism from an n-edge path, which unfortunately fails with this ncatlab definition of homomorphism. (But for colorings, I'm not convinced homomorphisms to complete graphs are the basic definition. That's not to say I don't see the utility; just that defining homomorphisms only for the sake of colorings doesn't seem right)

I'm mostly undecided one way or the other at this point. I think if we can verify that graph minors are quotients of subobjects in the irrefl category (pretty sure it's true), then I'm satisfied.

[Aaron Anderson]

Also, if we ever want to define graphs that have loops as actual information, and talk about homomorphisms in their context, I think the irreflexive one makes a lot more sense

[Aaron Anderson]

I don't think we have to really pick one, we just call one the category of graphs with homomorphisms, and one the category of graphs with continuous maps.

[Kyle Miller]

It matters for which gets the simpler notation

[Kyle Miller]

And also, if it turned out we might only use one of them, that'd keep maintenance down

[Aaron Anderson]

We could define them both with rel_hom, that might keep maintenance down... but the only way to find out if we only want to use one of them is to start using them

[Kyle Miller]

Is the irrefl category an actual separate category, or is it merely the ncatlab category with the additional constraint that maps are locally injective?

[Kyle Miller]

It's true, we'd need to use both to really know.

[Aaron Anderson]

It is indeed a subcategory of the refl category. I've also yet to see a source that defines graph homomorphisms as the refl definition without first pointing out that there's a choice.

[Kyle Miller]

Yeah, I meant that as a design question. If one is a subcategory of the other, is it worth having both as separate definitions? I imagine many homomorphisms will be injective, where the distinction doesn't matter.

[Kyle Miller]

(I'm pretty sure I was wrong about graph minors being the same as quotients of subobjects. They are quotients of subobjects, but not conversely.)

[Kyle Miller]

Anyway, if there is a precedent to studying the category from the irreflexive relation, then it seems reasonable just defining homomorphisms that way. If anyone proves an excluded minors theorem at some point, this could be revisited.

[Aaron Anderson]

Kyle Miller said:

Yeah, I meant that as a design question. If one is a subcategory of the other, is it worth having both as separate definitions? I imagine many homomorphisms will be injective, where the distinction doesn't matter.

Well, the continuous definition will be in mathlib sooner or later, as a full subcategory of simplicial sets