## Stream: graph theory

### Topic: category of graphs

#### Jalex Stark (Aug 29 2020 at 21:50):

@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 (Aug 29 2020 at 21:50):

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

#### Jalex Stark (Aug 29 2020 at 21:53):

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 (Aug 29 2020 at 21:53):

There are a few different definitions?

#### Aaron Anderson (Aug 29 2020 at 21:53):

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

#### Kyle Miller (Aug 29 2020 at 21:53):

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

#### Kyle Miller (Aug 29 2020 at 21:54):

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

#### Jalex Stark (Aug 29 2020 at 21:54):

the category of homormorphisms is more interesting

#### Kyle Miller (Aug 29 2020 at 21:56):

@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 (Aug 29 2020 at 22:00):

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 (Aug 29 2020 at 22:03):

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 (Aug 29 2020 at 22:07):

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 (Aug 29 2020 at 22:08):

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

#### Aaron Anderson (Aug 29 2020 at 22:08):

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

#### Aaron Anderson (Aug 29 2020 at 22:08):

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

#### Kyle Miller (Aug 29 2020 at 22:15):

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 (Aug 29 2020 at 22:16):

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

#### Kyle Miller (Aug 29 2020 at 22:22):

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 (Aug 29 2020 at 22:23):

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

#### Bhavik Mehta (Aug 29 2020 at 22:24):

Pretty sure this matches what you want?

#### Aaron Anderson (Aug 29 2020 at 22:25):

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 (Aug 29 2020 at 22:25):

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 (Aug 29 2020 at 22:26):

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 (Aug 29 2020 at 22:26):

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

#### Aaron Anderson (Aug 29 2020 at 22:26):

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

#### Aaron Anderson (Aug 29 2020 at 22:27):

I do add those abbreviations in #3946

#### Aaron Anderson (Aug 29 2020 at 22:28):

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 (Aug 29 2020 at 22:29):

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 (Aug 29 2020 at 22:30):

so eventually we will have a theorem like

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


?

#### Jalex Stark (Aug 29 2020 at 22:30):

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

#### Bhavik Mehta (Aug 29 2020 at 22:31):

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

got it

#### Bhavik Mehta (Aug 29 2020 at 22:31):

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

#### Bhavik Mehta (Aug 29 2020 at 22:32):

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

#### Jalex Stark (Aug 29 2020 at 22:33):

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 (Aug 29 2020 at 22:34):

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 (Aug 29 2020 at 22:35):

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 (Aug 29 2020 at 23:32):

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 (Aug 29 2020 at 23:33):

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 (Aug 29 2020 at 23:41):

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

#### Alena Gusakov (Aug 30 2020 at 01:53):

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 (Aug 30 2020 at 01:54):

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

#### Aaron Anderson (Aug 30 2020 at 01:55):

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 (Aug 30 2020 at 01:55):

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

#### Alena Gusakov (Aug 30 2020 at 01:55):

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

#### Aaron Anderson (Aug 30 2020 at 01:57):

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

#### Bhavik Mehta (Aug 30 2020 at 02:11):

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 (Aug 30 2020 at 02:53):

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 (Aug 30 2020 at 04:28):

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

-- 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,

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 (Aug 30 2020 at 04:30):

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 (Aug 30 2020 at 04:31):

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

#### Kyle Miller (Aug 30 2020 at 04:35):

(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 (Aug 30 2020 at 04:39):

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 (Aug 30 2020 at 04:59):

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

-- 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,

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,

/--
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 (Aug 30 2020 at 13:32):

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 (Aug 30 2020 at 13:33):

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 (Aug 31 2020 at 16:02):

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 (Aug 31 2020 at 19:37):

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 (Aug 31 2020 at 19:41):

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 (Aug 31 2020 at 19:48):

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 (Aug 31 2020 at 19:52):

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

#### Aaron Anderson (Aug 31 2020 at 19:54):

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 (Aug 31 2020 at 19:56):

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 (Aug 31 2020 at 19:57):

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 (Aug 31 2020 at 19:58):

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 (Aug 31 2020 at 20:00):

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 (Aug 31 2020 at 20:03):

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

#### Kyle Miller (Aug 31 2020 at 20:05):

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

#### Aaron Anderson (Aug 31 2020 at 20:08):

Mostly for studying colorability

#### Aaron Anderson (Aug 31 2020 at 20:08):

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

#### Aaron Anderson (Aug 31 2020 at 20:09):

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 (Aug 31 2020 at 20:10):

locally injective homomorphisms cover that case, at least

#### Kyle Miller (Aug 31 2020 at 20:10):

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

#### Aaron Anderson (Aug 31 2020 at 20:10):

What do you mean by locally injective?

#### Kyle Miller (Aug 31 2020 at 20:11):

I mean

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


#### Kyle Miller (Aug 31 2020 at 20:12):

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 (Aug 31 2020 at 20:13):

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 (Aug 31 2020 at 20:17):

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 (Aug 31 2020 at 20:20):

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 (Aug 31 2020 at 20:21):

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

#### Aaron Anderson (Aug 31 2020 at 20:27):

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 (Aug 31 2020 at 20:28):

@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 (Aug 31 2020 at 20:29):

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

#### Jalex Stark (Aug 31 2020 at 20:31):

And asked a lot of dumb questions to william ballinger

#### Aaron Anderson (Aug 31 2020 at 20:46):

Jalex Stark said:

And asked a lot of dumb questions to william ballinger

Really the best way to learn any subject

#### Aaron Anderson (Aug 31 2020 at 20:47):

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 (Aug 31 2020 at 20:47):

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 (Aug 31 2020 at 20:48):

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 (Aug 31 2020 at 20:49):

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 (Aug 31 2020 at 20:49):

It matters for which gets the simpler notation

#### Kyle Miller (Aug 31 2020 at 20:50):

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

#### Aaron Anderson (Aug 31 2020 at 20:54):

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 (Aug 31 2020 at 20:55):

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 (Aug 31 2020 at 20:56):

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

#### Aaron Anderson (Aug 31 2020 at 20:57):

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 (Aug 31 2020 at 21:00):

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 (Aug 31 2020 at 21:01):

(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 (Aug 31 2020 at 21:02):

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 (Aug 31 2020 at 21:04):

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

Last updated: May 08 2021 at 21:09 UTC