## Stream: Is there code for X?

### Topic: prefunctor?

#### Adam Topaz (Sep 12 2020 at 15:41):

I don't know what this is actually called....

structure prefunctor (C : Type*) [has_hom C] (D : Type*) [has_hom D] :=
(obj : C → D)
(map {X Y : C} : (X ⟶ Y) → (obj X ⟶ obj Y))


Does this exist somewhere in mathlib?

#### Kenny Lau (Sep 12 2020 at 15:42):

it's like functor (the _root_ one)

#### Adam Topaz (Sep 12 2020 at 15:42):

Right, I know that. But I would like to use it with has_hom, as above.

#### Adam Topaz (Sep 12 2020 at 15:43):

I'm building the free category associated to a type C with a has_hom instance, and this is what is needed to state its universal property.

#### Kenny Lau (Sep 12 2020 at 15:48):

it probably doesn't exist (otherwise functor would have depended on it)

#### Reid Barton (Sep 12 2020 at 15:49):

I was at one point meaning to give this the perhaps controversial name of "diagram"

#### Adam Topaz (Sep 12 2020 at 15:50):

These things do actually show up in math. One thing I know about specifically is in defining Nori's version of the motivic Galois group, and he does indeed call them "diagrams"

#### Adam Topaz (Sep 12 2020 at 15:52):

"pregraph" also makes sense for a name.

#### Adam Topaz (Sep 12 2020 at 15:53):

Anyway, in case anyone is interested:
https://github.com/leanprover-community/mathlib/blob/free_cat/src/category_theory/category/free.lean

#### Reid Barton (Sep 12 2020 at 15:53):

You can also define what it means to be the (co)limit of one of these things--having a functor and, in particular, a domain category isn't necessary, and not always convenient. (I guess this is to some extent related to wanting to use these things to talk about free categories.)

Right.

#### Reid Barton (Sep 12 2020 at 15:54):

e.g. a pushout is a colimit of a diagram indexed on $\cdot \leftarrow \cdot \to \cdot$, with no category structure implied & therefore no identity morphisms

#### Reid Barton (Sep 12 2020 at 15:55):

so in that context, the name diagram makes some sense.

#### Adam Topaz (Sep 12 2020 at 15:57):

Yeah I agree. A guess a lot of the stuff in the shapes dir can be made into diagrams (or free categories associated with a diagram).

#### Adam Topaz (Sep 12 2020 at 16:46):

This is completely unrelated, but is there a simple way to input the functor symbol in emacs? @Reid Barton

nope

#### Julian Berman (Sep 12 2020 at 16:53):

This is completely unrelated, but is there a simple way to input the functor symbol in emacs? Reid Barton

On the "unrelated" topic -- I recently did something with those given I wanted to keep using vim for lean -- the most straightforward way for all the unicode stuff without getting too far inside the lean LSP was I basically used the translations.json file from the lean vscode extension and autogenerated snippets from it for vim to use, which I put here: https://github.com/Julian/lean-unicode.vim/blob/main/Ultisnips/lean.snippets -- presuming emacs has a way to load ultisnips formatted snippets that may already be usable exactly as is)

#### Adam Topaz (Sep 12 2020 at 16:54):

Yeah I guess I can do something with yasnippet (the canonocal(?) snippet package in emacs)

#### Adam Topaz (Sep 12 2020 at 16:58):

Okay, that works. I just made a snippet file for yasnippet that looks like this:

# key: funct
# name: func_symb
# --
⥤\$0


#### Kyle Miller (Sep 12 2020 at 19:46):

This is completely unrelated, but is there a simple way to input the functor symbol in emacs? Reid Barton

I think we might be allowed to add it to lean-mode. All the input translations are defined by lean-input-translations in https://github.com/leanprover/lean-mode/blob/master/lean-input.el (though if you want to experiment locally, you can customize lean-input-user-translations)

Does VSCode already have a way to input the category theory functor symbol? If not, maybe \Functor (vs \functor)?

#### Alex Peattie (Sep 12 2020 at 20:05):

Kyle Miller said:

Does VSCode already have a way to input the category theory functor symbol? If not, maybe \Functor (vs \functor)?

Yeah it's \functor currently (source)

#### Alex Peattie (Sep 12 2020 at 20:06):

oh sorry, I misunderstood \functor is mapped to ⥤

#### Adam Topaz (Sep 12 2020 at 20:11):

I think \func suffices in vscode.

#### Kyle Miller (Sep 12 2020 at 20:12):

Actually, that's useful to know. It seems like \functor in VSCode is ⥤ and \Rightarrow is ⇒, where in emacs \functor and various other options give only ⇒.

#### Kyle Miller (Sep 12 2020 at 20:12):

I wouldn't mind if \functor in emacs were ⥤

#### Kyle Miller (Sep 12 2020 at 20:21):

Ok, here's a PR: https://github.com/leanprover/lean-mode/pull/29

#### Adam Topaz (Sep 12 2020 at 20:23):

Does the melpa package mirror this?

#### Kyle Miller (Sep 12 2020 at 20:25):

I don't know how it works, other than changes I've made in the past eventually appear in melpa

Ok cool

#### Adam Topaz (Sep 12 2020 at 20:26):

I look forward to this getting merged!

#### Kyle Miller (Sep 12 2020 at 20:26):

If there are other missing symbols, this might be a good time to add them

#### Adam Topaz (Sep 12 2020 at 20:28):

That's the main one I've been frustrated with. Maybe @Reid Barton has others he would like to see?

#### Reid Barton (Sep 12 2020 at 20:28):

Nothing else comes to mind

#### Scott Morrison (Sep 12 2020 at 23:01):

Refactoring functor to use prefunctor (I like diagram!) sounds like a great idea.

#### Adam Topaz (Sep 12 2020 at 23:45):

Scott Morrison said:

Refactoring functor to use prefunctor (I like diagram!) sounds like a great idea.

I agree. The question is how to do it. Note that to define a sufficiently nontrivial notion of a morphism between prefunctors, you need to make some sort of has_comp class (in order to state the naturality condition).

#### Scott Morrison (Sep 13 2020 at 00:06):

Isn't src#category_theory.category_struct all that we need?

#### Adam Topaz (Sep 13 2020 at 00:19):

Oh right. And that also allows us to define an "indentity" morphism.

#### Jesse Michael Han (Sep 13 2020 at 23:54):

you guys can use func for ⥤ in Emacs by adding the following snippet as part of your lean-mode-hook:

  (lean-input-incorporate-changed-setting
'lean-input-user-translations
( ("func" "⥤")
("tf" "⟨╯°□°⟩╯︵┻━┻")
))


tf?

#### Kyle Miller (Sep 14 2020 at 00:28):

It must be the little-used principle of tabula furorem

#### Eric Wieser (Oct 01 2020 at 15:23):

Did you make any progress on prefunctor / diagram, @Adam Topaz? We'll soon have three copies of the lift/ ι relationship ((free|exterior|universal_enveloping) _algebra), and I was looking at adding clifford_algebra too...

#### Adam Topaz (Oct 01 2020 at 15:23):

Sorry, I've been busy with teaching :(

#### Adam Topaz (Oct 01 2020 at 15:24):

But I'm not sure the lift / \iota stuff really relates to this.

#### Adam Topaz (Oct 01 2020 at 15:26):

How would you like to use these diagrams in this context?

#### Eric Wieser (Oct 01 2020 at 15:29):

You said yourself you wanted to use it to state the universal property, and I think somehow I saw a connection - but I can't see it any more.

#### Adam Topaz (Oct 01 2020 at 15:31):

Oh, I was referring to the universal property specifically for the free category associated to a diagram.

#### Adam Topaz (Oct 01 2020 at 15:31):

the analogue of \iota in that case is a prefunctor.

#### Eric Wieser (Oct 01 2020 at 15:34):

I think I was hoping for a bundling of lift and ι, so that we can state the theorems about the bundle in just one place rather than repeating them

#### Adam Topaz (Oct 01 2020 at 18:24):

The bundle of lift and \iota in this case just means that you have an initial object in some category, and initial objects are in mathlib already. But I don't necessarily think that's a more useful description than just keeping lift and \iota around as is.

(deleted)

#### Scott Morrison (Oct 01 2020 at 23:50):

My preference would be for adding in addition to the existing lift and \iota the formulation as an initial object.

#### Scott Morrison (Oct 01 2020 at 23:51):

In practice one is usually happy to use the explicit lift and \iota in most places. But it is a nice verification that we've really stated the right properties to have the initial object formulation.

#### Adam Topaz (Oct 02 2020 at 00:33):

I agree with this. But the examples @Eric Wieser mentioned are all left adjoints. I presume a better route would be to prove the adjunction :smile:

#### Reid Barton (Oct 02 2020 at 00:41):

Some other category libraries have a notion like "something determined by a universal property", generally an initial/terminal object of a comma category, I think. Then this can be used to define limits and maybe adjunctions and so on.

#### Reid Barton (Oct 02 2020 at 00:42):

I think it's the kind of concept that in informal mathematics we can recognize but don't really have a name for.

#### Reid Barton (Oct 02 2020 at 00:42):

Because it is too basic/central somehow.

#### Adam Topaz (Oct 02 2020 at 00:43):

Do you have an example of such a library in mind?

#### Adam Topaz (Oct 02 2020 at 00:43):

Could this be a replacement for, e.g. the localization stuff?

#### Reid Barton (Oct 02 2020 at 00:45):

https://github.com/HoTT/HoTT/blob/master/theories/Categories/UniversalProperties.v#L68-L69

#### Reid Barton (Oct 02 2020 at 00:46):

https://github.com/HoTT/HoTT/blob/master/theories/Categories/Limits/Core.v#L107-L108

#### Adam Topaz (Oct 02 2020 at 00:50):

Is this definition of initial objects correct? is the empty type contractible (in HoTT)?

#### Reid Barton (Oct 02 2020 at 00:51):

It's the homsets out that are contractible

Oh right

#### Adam Topaz (Oct 02 2020 at 00:53):

wait I mean what happens if there are no morphisms from x to x'?

#### Reid Barton (Oct 02 2020 at 00:53):

The empty type is not contractible

#### Reid Barton (Oct 02 2020 at 00:54):

(whoops internet is flaky in that room)

#### Reid Barton (Oct 02 2020 at 00:57):

I think one version of this concept is as follows. Sometimes, you have a functor $U : D \to C$ which doesn't necessarily have a left adjoint but for some particular $X \in C$, you can still find an object $FX \in D$ such that for all $Y$ there's an iso $\mathrm{Hom}(FX, Y) = \mathrm{Hom}(X, UY)$.

#### Reid Barton (Oct 02 2020 at 00:58):

for example, $U : C \to C^I$ could be the diagonal functor and $FX$ the colimit of a specific diagram $X : I \to C$

#### Reid Barton (Oct 02 2020 at 01:00):

We have the notion of a colimit of a specific diagram, and we know (I guess, or could easily add) that the whole colimit functor is adjoint to the diagonal functor when it exists, but AFAIK we don't have a way to say how an individual colimit is related to the diagonal functor.

#### Adam Topaz (Oct 02 2020 at 01:01):

You can probably do something with cones

#### Reid Barton (Oct 02 2020 at 01:03):

The cone category we have is basically a one-off construction of the comma category of the diagonal functor.

#### Reid Barton (Oct 02 2020 at 01:04):

whereas those HoTT library snippets I linked to build it up incrementally

#### Reid Barton (Oct 02 2020 at 01:04):

I have no idea how well that works for usability, of course

#### Reid Barton (Oct 02 2020 at 01:07):

For localization (of a ring, say, $R[S^{-1}]$) you could look for an initial object of the full subcategory of the slice category consisting of the guys where $S$ gets sent to invertible elements. But I don't know if it's the most convenient way to say it.

#### Reid Barton (Oct 02 2020 at 01:19):

I imagine there are a few styles that might possibly work, such as "every concept is an initial/terminal object in some auxiliary category", or "every concept is a Kan extension", or to do everything with profunctors and the coend calculus.

#### Adam Topaz (Oct 02 2020 at 01:33):

None of these approaches (if implemented in lean) would solve the issue of universes when defining the universal properties, would they?

#### Reid Barton (Oct 02 2020 at 02:06):

I don't think so, and moreover I think this is actually a real math issue that we usually ignore (generally it's obvious once you've constructed the object that satisfies the universal property, but a priori the object could depend on the ambient universe).

#### Reid Barton (Oct 27 2020 at 23:39):

I was just looking up a result in Makkai and Paré's book on accessible categories and I notice that they define the notions of (co)limit (co)cone in the generality being discussed here. They call a has_hom a "graph* (actually I don't think they ever define the term "graph", but it's clear this must be what they mean) and a prefunctor a "diagram".

#### Reid Barton (Oct 27 2020 at 23:40):

Also, I think in Higher Topos Theory (co)limits can be indexed on any simplicial set, which are basically the higher equivalent of graphs in this context.

#### Adam Topaz (Oct 28 2020 at 00:43):

Sounds good to me! (I wonder what the people in the secret graph theory stream think about this @Kyle Miller @Jalex Stark ?)

It's public now!

#### Jalex Stark (Oct 28 2020 at 00:45):

I think the graphs in mathlib are not so great at carrying data for other structures yet, but I bet Kyle would have useful opinions.

#### Reid Barton (Oct 28 2020 at 00:47):

I guess this was meant to lend weight more to the term "diagram" than the term "graph", which might mean other things elsewhere (though category_theory.graph seems okay, for a renaming of category_theory.has_hom?)

#### Adam Topaz (Oct 28 2020 at 00:48):

Maybe has_arrow instead of has_hom?

#### Adam Topaz (Oct 28 2020 at 00:49):

Or more precisely has_arrow (in the root namespace) instead of category_theory.has_hom?

#### Kyle Miller (Oct 28 2020 at 06:17):

This notion of a graph sounds like a quiver to me (and quivers evoke category theory, which is a nice perk, compared to "directed graph"). Calling it a quiver might be too restrictive, though, if you want to study different collections of arrows on the same objects type, but I can't immediately think of a case where you'd want to do this.

I like @Adam Topaz's suggestion, but maybe plural as has_arrows:

universes u v

class has_arrows (obj : Type u) : Type (max u (v+1)) :=
(arrows : obj → obj → Type v)


#### Julian Külshammer (Oct 28 2020 at 12:33):

To me (as someone working on representation theory of finite dimensional algebras and quivers), quiver sounds like the correct notion for that kind of object. It means precisely directed graph (with multiple arrows and loops allowed, and typically also has no finiteness restrictions). I definitely know use-cases where one would like to study different collections of arrows on the same object type. As discussed in some other graph theory thread previously, a typical other way to encode a quiver is via a collection of vertices (objects), a collection of arrows (homs) and two functions (in my area called either s and t or t and h, indicating the start and terminal vertex).

#### Adam Topaz (Oct 28 2020 at 14:25):

The nlab agrees: https://ncatlab.org/nlab/show/quiver

#### Adam Topaz (Oct 28 2020 at 14:27):

Although my brain associates the term quiver specifically to a diagram with values in the category of k-vector spaces.

#### Reid Barton (Oct 28 2020 at 14:27):

Presumably this object is still going to underlie every category, though. I don't think it's really normal to say that the category of groups has an underlying "quiver" (https://ncatlab.org/nlab/show/concept+with+an+attitude#quivers)

#### Adam Topaz (Oct 28 2020 at 14:28):

I agree. That's why I think has_arrow(s) is a good compromise between category theory and graph theory.

#### Reid Barton (Oct 28 2020 at 14:29):

It still means we would change the name hom for the homsets of a category. Would we change the field name for the action of a functor too?

#### Adam Topaz (Oct 28 2020 at 14:31):

We could keep the name hom X Y for has_arrow.arrow X Y in the case where X Y : C and C is a category.

#### Reid Barton (Oct 28 2020 at 14:32):

How would we do that?

#### Adam Topaz (Oct 28 2020 at 14:32):

Or just make hom an alias for has_arrow.arrow.

#### Reid Barton (Oct 28 2020 at 14:32):

Like as an abbreviation?

#### Reid Barton (Oct 28 2020 at 14:33):

It's used in so many places in record constructor syntax, and as a component in other names, that it just feels like stirring up trouble to think about changing it...

#### Adam Topaz (Oct 28 2020 at 14:38):

Will this work?

import category_theory.category

class has_arrow (α : Type*) extends category_theory.has_hom α


#### Kyle Miller (Oct 28 2020 at 18:41):

It seems like the easiest thing is to call it a "hom-graph" in the docstring and then do nothing :smile:

/-- A "hom-graph" is a directed graph attached to a vertex type.  The
set of directed edges ("arrows") from vertex a to vertex b is
given by hom a b, for which this module provides the notation a ⟶ b -/
class has_hom (obj : Type u) : Type (max u (v+1)) :=
(hom : obj → obj → Type v)


Then we can say a quiver "is" a hom-graph, in the sense that a quiver's vertex type can be given a has_hom instance. With one possible definition of a quiver:

structure quiver :=
(V : Type u)
(homs : Type v)
(s t : homs → V)

instance quiver.has_hom (Q : quiver) : has_hom Q.V :=
{ hom := λ v w, subtype {f : Q.homs | Q.s f = v ∧ Q.t f = w} }


With this setup, it would be nice if prefunctors (or preprefunctors?) would apply to has_hom to be able to study quiver representations.

#### Kyle Miller (Oct 28 2020 at 19:04):

(I've wondered about the duality between defining directed graphs in terms of directed edge sets (has_hom) or as spans (quiver). Is there a category theoretic name for the kind of object has_hom is?)

#### Reid Barton (Oct 28 2020 at 22:29):

In the case of graphs (without composition/category structure) this is the equivalence of categories between, for a fixed set $B$, the category of sets with a map to $B$ and the category of $B$-indexed families of sets. I think this one is too basic to really have a name, but fancier versions of it go by names like the Grothendieck construction or straightening/unstraightening.

#### Reid Barton (Oct 28 2020 at 22:29):

For graphs $B$ would be $V \times V$.

#### Reid Barton (Oct 28 2020 at 22:31):

For categories, the presentation in terms of s and t` is as the models of an essentially algebraic theory while the one in terms of a family of sets indexed by two objects is as the modules of a generalized algebraic theory.

#### Reid Barton (Oct 28 2020 at 22:33):

I also like to think of the first one as "categories internal to Set" and the second as "categories enriched in Set" although those phrases are likely to be confusing.

#### Johan Commelin (Oct 29 2020 at 06:07):

Another applications of quivers and diagrams that I dream of leanifying is the category of Nori motives, which built as quiver representation on a quiver of schemes.

Last updated: May 17 2021 at 15:13 UTC