learning what a left Kan extension is

Stream: mathlib4

[Kevin Buzzard]

I find myself (for porting reasons) wanting to learn (for the n'th time) what a left Kan extension is, so I figured that rather than facing nLab I'd try and learn from mathlib4 + pen-and-paper.

First thing I've learnt: they're called lan, their URL is docs4#CategoryTheory.lan and the theorems about them are in namespace CategoryTheory.Lan. Is this capital a mistake or is this what the naming convention gods decreed?

Next thing I discovered: the docstring currently isn't helpful (this can easily be fixed, and probably will be by the end of this), and if I click "Equations" then it says One or more equations did not get rendered due to their size. and that's it. Is this expected? Finally, when I click the ink option I jump to the beginning of the file in a web browser rather than the definition of lan, even though the URL ends in #CategoryTheory.lan. I have more ink questions but I'll ask them elsewhere.

I guess I'm interested in the general question as to whether it is possible to imagine using mathlib4 as a resource for learning precise definitions in mathematics at undergraduate and MSc level, and what work needs to be done to make this happen.

[Mario Carneiro]

I don't think that is correct to the naming convention, but the name is very mysterious to me

[Mario Carneiro]

If I go to the source I see even more fun capitalization:

set_option linter.uppercaseLean3 false in
  #align category_theory.Lan CategoryTheory.lan

[Mario Carneiro]

(also this indentation pattern is not standard, set_option ... in should not have an indent after it)

[Mario Carneiro]

Overall, I think you just ran into a lot of bugs. I don't think you can derive much about the effectiveness of mathlib4 as a teaching tool until the bugs are fixed

[Adam Topaz]

Re the name. There’s a left Kan extension (lan) and a right one (ran) which have dual (in some sense) universal properties. In the best situations, they give adjoints to the “whiskering” functor, which is a functor on the category of functor as given on objects by composition with a functor. (Sorry for the functor overload…). I think the adjunction is called docs4#CategoryTheory.Ran.adjunction ?

[Adam Topaz]

(And the analogous thing for lan)

[Adam Topaz]

It is unfortunate that the naming convention has the functor called lan and the namespace Lan :-/

[Adam Topaz]

Mario, what would the naming convention have us do in this case? I still don’t understand the convention

[Mario Carneiro]

The namespace of a function is spelled the same as the function itself

[Mario Carneiro]

otherwise dot notation breaks

[Mario Carneiro]

yes, that means it is lowercase sometimes

[Adam Topaz]

Well dot notation isn’t useful in this case anyway

[Mario Carneiro]

you could also not put them in a namespace and have lan_foo lemmas instead

[Adam Topaz]

So should the adjunction be called lanAdjunction

[Adam Topaz]

Yeah an adjunction has data

[Mario Carneiro]

lanAdjunction sounds fine to me

[Mario Carneiro]

although I really want to put a K in there somewhere

[Adam Topaz]

Yeah I understand but lan and ran are common in the nonformal literature

[Adam Topaz]

nlab#Kan+extension

[Mario Carneiro]

really? I had it pegged as a mathlibism

[Adam Topaz]

See def 2.1 in the above link

[Mario Carneiro]

BTW, I would not be opposed to tweaking the rules around what is a "type" vs "function" in the context of category theory for the purposes of the naming convention

[Mario Carneiro]

I think there is a reasonable argument that functors can be seen as type operators and objects in a category as types

[Adam Topaz]

BTW concerning the question of whether Mathlib is useful for learning… I certainly learned a lot about Kan extensions by formalizing them!

[Reid Barton]

I think Lan/Ran are a lot more common than lan/ran

[Reid Barton]

though even more common is sticking some punctuation somewhere

[Reid Barton]

(which punctuation depends on whether you are an algebraic geometer)

[Reid Barton]

Indeed the mathlib 3 name was Lan

[Moritz Firsching]

Mario Carneiro said:

(also this indentation pattern is not standard, set_option ... in should not have an indent after it)

fixing those in !4#3735

[Thomas Murrills]

Btw, re: the topic of the thread, definition 2.4 on the nLab page is my favorite—Kan extensions are “universal ways to complete a 2-cell” given two 1-arrows that share a source. (Typically the 1-arrows are functors and the 2-arrows are natural transformations, but the definition works in general.)

To complete such a 2-cell, you need to supply both:

• a 1-arrow from the target of one of the given 1-arrow ($p$) to the target of the other given one ($F$) to get a triangle—this new arrow is called $\text{(L/R)an}_p F$—and
• a 2-arrow to fill in the triangle, going between $(\text{(L/R)an}_p F) \circ p$ and $F$. Which way this 2-arrow (called $\eta_F$ on the nLab page) is directed determines the left- or rightness of the Kan extension.

This 2-arrow is (at least in this view) the important data, and we have a Kan extension when this 2-arrow is universal in the same way a universal arrow is: any other 2-cell with the same shape factors uniquely through this one. (See the diagram in def 2.4 on nLab.)

This is a “local” Kan extension because both $p$ and $F$ are fixed. If it so happens that you can generalize the $F$ argument of e.g. $\text{Lan}_p F$ by finding local extensions for all $F$, then the operation $\text{Lan}_p$ becomes one of the adjoint functors described by Adam above. This is analogous to how a family of universal arrows assembles to form an adjunction.

So a pretty good arrows-only characterization of a local Kan extension is a particular kind of “universal 2-arrow”, and global ones are what you get when you organize a family of those into the appropriate adjunction. As you can see, though, it’s the 1-arrow which forms half the (co)domain of this 2-arrow which gets the special name, since it’s the process of making these 1-arrows that actually yields the map on (objects of) the relevant functor category when you have a global Kan extension.

A nice thing about this perspective is that (co)limits are easily visible as the special case where the “middle” vertex of the triangle (codomain of $p$, domain of $\text{(L/R)an}_p F$) is the terminal category. Seeing this fall out is straightforward but pretty gratifying! It lets you see Kan extensions as a sort of generalization of (co)limits.

At least…that’s one perspective. 😁 There’s a bunch captured by other perspectives which isn’t captured by this one. I’m not sure how this fits into mathlib’s characterization, though, or how useful this perspective actually is in the practice of formalizing things.

[Adam Topaz]

One crucial thing that’s still missing from mathlib is a characteristic predicate for (local/global) Kan extensions, and I’m quite sure the “universal 2-cell” would be the right approach for that!

[Scott Morrison]

I would propose we rename the functions themselves to Lan and Ran again.

[Joël Riou]

Adam Topaz said:

One crucial thing that’s still missing from mathlib is a characteristic predicate for (local/global) Kan extensions, and I’m quite sure the “universal 2-cell” would be the right approach for that!

I have draft code for total derived functors, and I have defined it like this:

variables {C D H : Type*} [category C] [category D] [category H]
  {F : C ⥤ D} (RF : H ⥤ D) {L : C ⥤ H} (α : F ⟶ L ⋙ RF)
  (W : morphism_property C) [L.is_localization W]

class is_right_derived_functor : Prop :=
(is_initial [] : nonempty (limits.is_initial (structured_arrow.mk α :
  structured_arrow F ((whiskering_left C H D).obj L))))

This can certainly be adapted for general Kan extensions.