prefunctor?

Stream: Is there code for X?

[Adam Topaz]

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]

it's like functor (the _root_ one)

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Reid Barton]

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

[Adam Topaz]

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]

"pregraph" also makes sense for a name.

[Adam Topaz]

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

[Reid Barton]

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

[Adam Topaz]

Right.

[Reid Barton]

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]

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

[Adam Topaz]

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]

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

[Reid Barton]

nope

[Julian Berman]

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)

[Adam Topaz]

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

[Adam Topaz]

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

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

[Kyle Miller]

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

[Alex Peattie]

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]

oh sorry, I misunderstood \functor is mapped to ⥤

[Adam Topaz]

I think \func suffices in vscode.

[Kyle Miller]

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]

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

[Kyle Miller]

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

[Adam Topaz]

Does the melpa package mirror this?

[Kyle Miller]

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

[Adam Topaz]

Ok cool

[Adam Topaz]

I look forward to this getting merged!

[Kyle Miller]

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

[Adam Topaz]

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

[Reid Barton]

Nothing else comes to mind

[Scott Morrison]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Jesse Michael Han]

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" "⟨╯°□°⟩╯︵┻━┻")
))

[Adam Topaz]

tf?

[Kyle Miller]

It must be the little-used principle of tabula furorem

[Eric Wieser]

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]

Sorry, I've been busy with teaching :(

[Adam Topaz]

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

[Adam Topaz]

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

[Eric Wieser]

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]

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

[Adam Topaz]

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

[Eric Wieser]

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]

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.

[Eric Wieser]

(deleted)

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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]

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]

Because it is too basic/central somehow.

[Adam Topaz]

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

[Adam Topaz]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Adam Topaz]

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

[Reid Barton]

It's the homsets out that are contractible

[Adam Topaz]

Oh right

[Adam Topaz]

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

[Reid Barton]

The empty type is not contractible

[Reid Barton]

(whoops internet is flaky in that room)

[Reid Barton]

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]

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]

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]

You can probably do something with cones

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

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]

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]

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

[Jalex Stark]

It's public now!

[Jalex Stark]

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]

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]

Maybe has_arrow instead of has_hom?

[Adam Topaz]

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

[Kyle Miller]

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]

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]

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

[Adam Topaz]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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]

How would we do that?

[Adam Topaz]

Or just make hom an alias for has_arrow.arrow.

[Reid Barton]

Like as an abbreviation?

[Reid Barton]

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]

Will this work?

import category_theory.category

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

[Kyle Miller]

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]

(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]

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]

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

[Reid Barton]

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]

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]

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.

[Eric Wieser]

Scott Morrison said:

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

I finally got around to learning how to use category_theory and proved this for clifford_algebra as

/--
The category of pairs of algebras and `clifford_hom`s to those algebras.

https://empg.maths.ed.ac.uk/Activities/Spin/Lecture1.pdf
-/
structure Cliff :=
(alg : Algebra.{v} R)
(hom : clifford_hom Q alg)

/-- The clifford algebra is the initial object in `Cliff`. -/
def clifford_algebra.is_initial : limits.is_initial (Cliff.of Q ⟨ι Q, ι_sq_scalar Q⟩) :=
limits.is_initial.of_unique _

It looks like phrasing this as an adjunction is quite tricky, and you can't just use the functor QuadraticModule.{u} R ⥤ Algebra.{u} R

[Eric Wieser]

(I'm afraid it's Lean3, but I'll port it at some point)