Zulip Chat Archive

Stream: Is there code for X?

Topic: prefunctor?


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Sep 12 2020 at 15:42):

it's like functor (the _root_ one)

view this post on Zulip Adam Topaz (Sep 12 2020 at 15:42):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Sep 12 2020 at 15:48):

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

view this post on Zulip Reid Barton (Sep 12 2020 at 15:49):

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

view this post on Zulip 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"

view this post on Zulip Adam Topaz (Sep 12 2020 at 15:52):

"pregraph" also makes sense for a name.

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip Adam Topaz (Sep 12 2020 at 15:54):

Right.

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 12 2020 at 15:55):

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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 12 2020 at 16:47):

nope

view this post on Zulip Julian Berman (Sep 12 2020 at 16:53):

Adam Topaz said:

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)

view this post on Zulip Adam Topaz (Sep 12 2020 at 16:54):

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

view this post on Zulip 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

view this post on Zulip Kyle Miller (Sep 12 2020 at 19:46):

Adam Topaz said:

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)?

view this post on Zulip 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)

view this post on Zulip Alex Peattie (Sep 12 2020 at 20:06):

oh sorry, I misunderstood \functor is mapped to ⥤

view this post on Zulip Adam Topaz (Sep 12 2020 at 20:11):

I think \func suffices in vscode.

view this post on Zulip 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 .

view this post on Zulip Kyle Miller (Sep 12 2020 at 20:12):

I wouldn't mind if \functor in emacs were

view this post on Zulip Kyle Miller (Sep 12 2020 at 20:21):

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

view this post on Zulip Adam Topaz (Sep 12 2020 at 20:23):

Does the melpa package mirror this?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Sep 12 2020 at 20:25):

Ok cool

view this post on Zulip Adam Topaz (Sep 12 2020 at 20:26):

I look forward to this getting merged!

view this post on Zulip Kyle Miller (Sep 12 2020 at 20:26):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Sep 12 2020 at 20:28):

Nothing else comes to mind

view this post on Zulip Scott Morrison (Sep 12 2020 at 23:01):

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

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Sep 13 2020 at 00:06):

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

view this post on Zulip Adam Topaz (Sep 13 2020 at 00:19):

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

view this post on Zulip 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" "⟨╯°□°⟩╯︵┻━┻")
))

view this post on Zulip Adam Topaz (Sep 14 2020 at 00:18):

tf?

view this post on Zulip Kyle Miller (Sep 14 2020 at 00:28):

It must be the little-used principle of tabula furorem

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Oct 01 2020 at 15:23):

Sorry, I've been busy with teaching :(

view this post on Zulip Adam Topaz (Oct 01 2020 at 15:24):

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

view this post on Zulip Adam Topaz (Oct 01 2020 at 15:26):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 01 2020 at 15:31):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Oct 01 2020 at 18:40):

(deleted)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 02 2020 at 00:42):

Because it is too basic/central somehow.

view this post on Zulip Adam Topaz (Oct 02 2020 at 00:43):

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

view this post on Zulip Adam Topaz (Oct 02 2020 at 00:43):

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

view this post on Zulip Reid Barton (Oct 02 2020 at 00:44):

e.g. https://github.com/HoTT/HoTT/blob/master/theories/Categories/KanExtensions/Core.v#L167-L168

view this post on Zulip Reid Barton (Oct 02 2020 at 00:45):

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

view this post on Zulip Reid Barton (Oct 02 2020 at 00:46):

https://github.com/HoTT/HoTT/blob/092ebba509710c6e3eadbe03bc68049dd0b4ea0c/theories/Categories/Category/Objects.v#L36-L37

view this post on Zulip Reid Barton (Oct 02 2020 at 00:46):

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

view this post on Zulip Adam Topaz (Oct 02 2020 at 00:50):

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

view this post on Zulip Reid Barton (Oct 02 2020 at 00:51):

It's the homsets out that are contractible

view this post on Zulip Adam Topaz (Oct 02 2020 at 00:51):

Oh right

view this post on Zulip Adam Topaz (Oct 02 2020 at 00:53):

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

view this post on Zulip Reid Barton (Oct 02 2020 at 00:53):

The empty type is not contractible

view this post on Zulip Reid Barton (Oct 02 2020 at 00:54):

(whoops internet is flaky in that room)

view this post on Zulip Reid Barton (Oct 02 2020 at 00:57):

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

view this post on Zulip Reid Barton (Oct 02 2020 at 00:58):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 02 2020 at 01:01):

You can probably do something with cones

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 02 2020 at 01:04):

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

view this post on Zulip Reid Barton (Oct 02 2020 at 01:04):

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

view this post on Zulip Reid Barton (Oct 02 2020 at 01:07):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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 ?)

view this post on Zulip Jalex Stark (Oct 28 2020 at 00:44):

It's public now!

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip Adam Topaz (Oct 28 2020 at 00:48):

Maybe has_arrow instead of has_hom?

view this post on Zulip Adam Topaz (Oct 28 2020 at 00:49):

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

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip Adam Topaz (Oct 28 2020 at 14:25):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 28 2020 at 14:32):

How would we do that?

view this post on Zulip Adam Topaz (Oct 28 2020 at 14:32):

Or just make hom an alias for has_arrow.arrow.

view this post on Zulip Reid Barton (Oct 28 2020 at 14:32):

Like as an abbreviation?

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Oct 28 2020 at 14:38):

Will this work?

import category_theory.category

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

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip 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 BB, the category of sets with a map to BB and the category of BB-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.

view this post on Zulip Reid Barton (Oct 28 2020 at 22:29):

For graphs BB would be V×VV \times V.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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