Basic category theory observations

Stream: maths

[Kevin Buzzard]

import category_theory.functor

universes v₁ v₂ u₁ u₂

open category_theory

variables (C : Type u₁) [𝒞 : category.{v₁} C]
variables (D : Type u₂) [𝒟 : category.{v₂} D]

variables (F : C ⥤ D)

example : F ⋙ 𝟭 D = F := F.comp_id
example : 𝟭 C ⋙ F = F := F.comp_id -- compiled before I'd finished editing to F.id_comp

The last line works; the line above tells you the actual type. I was surprised.

[Kevin Buzzard]

Another surprising functor thing:

example : (F ⋙ G).map f = G.map (F.map f) := F.comp_map G _ _ f -- or rfl

comp_map wants X and Y explicitly (here f: X \h Y)

[Kevin Buzzard]

example : (F ⋙ G).map f = G.map (F.map f) := F.comp_map _ _ _ _ -- or rfl

[Kevin Buzzard]

Surprising natural transformation fact:

@[ext] structure nat_trans (F G : C ⥤ D) : Type (max u₁ v₂) :=

The definition of the structure is tagged ext!

[Reid Barton]

Kevin Buzzard said:

Another surprising functor thing:

example : (F ⋙ G).map f = G.map (F.map f) := F.comp_map G _ _ f -- or rfl

comp_map wants X and Y explicitly (here f: X \h Y)

what are you of all people doing term mode proofs for!

[Reid Barton]

But yes, this seems not ideal

[Kevin Buzzard]

You're avoiding the question.

[Reid Barton]

What was the question?

[Kevin Buzzard]

example : 𝟭 C ⋙ F = F := F.comp_id

[Reid Barton]

Yes because I was still thinking about that one. I mean both proofs look like cases F; refl so I guess that is the reason?

[Kevin Buzzard]

example : F.comp_id = F.id_comp := rfl despite them having different types

[Reid Barton]

oh, no

[Reid Barton]

It's because 1 C >>> F and F >>> 1 D are definitionally equal

[Kevin Buzzard]

This is doing my head in

[Kevin Buzzard]

OK fair enough

[Kevin Buzzard]

So they're not definitionally equal to F, but they're definitionally equal to each other?

[Reid Barton]

I mean, it's "almost" the case that 1 C >>> F = F definitionally in the first place. It would be true with definitional eta expansion for records.

[Kevin Buzzard]

Are we getting that in Lean 4?

[Reid Barton]

They're both definitionally equal to { obj := F.obj, map := F.map, ... } or so

[Kevin Buzzard]

I see.

[Kevin Buzzard]

Very nice!

[Reid Barton]

I doubt it, but wouldn't rule it out entirely

[Reid Barton]

Similarly composition of functors is definitionally associative

[Kevin Buzzard]

Reid Barton said:

what are you of all people doing term mode proofs for!

I'm re-learning all the notation for category theory because I learnt it once, didn't use it for 3 months and then realised I'd forgotten it all. I'm writing some basic docs, I'm nearly done.

[Scott Morrison]

Kevin Buzzard said:

Another surprising functor thing:

example : (F ⋙ G).map f = G.map (F.map f) := F.comp_map G _ _ f -- or rfl

comp_map wants X and Y explicitly (here f: X \h Y)

Fixed in #2103, hopefully.

[Scott Morrison]

These "accidents" that composition of functors is definitionally associative (and almost definitionally unital), have been a cause of trouble: implicitly relying on these facts have resulted in some bad rfl incidents where proofs became extremely slow.

[Kevin Buzzard]

Aah I remember this: at the time someone explained the analogy of proving 11111+22222=33333 by rfl instead of by norm_num. I've mentioned definitional equality a few times in #2104 -- perhaps this is a double-edged sword. I now realise that I did not mention automation once.

[Kevin Buzzard]

Scott Morrison said:

Fixed in #2103, hopefully.

I don't really have any feeling as to whether G and f should also be implicit. Not having F implicit means that you can use projection notation shrug

[Scott Morrison]

@Kevin Buzzard, do you object if I push a commit that linewraps all the paragraphs? It will be easier to review.

[Scott Morrison]

Okay, I did it anyway. :-)

[Scott Morrison]

While we're at this, I'm very happy to replace the choice of \hom arrow. I choose it way back when, before I understood that it was easy to update translations.json.

[Scott Morrison]

How about ⤏, ⤑, ⇢, ⭢, ⤳, ➞, ⇾, ⇥?

[Kevin Buzzard]

Feel free to do what you like with the PR. I think that rather than adding confusion by changing the arrow I should just find how to change the default font in my VS Code set-up. I've seen people with huge arrows in their VS Code.

[Scott Morrison]

A question about tutorials --- my instinct is that it's better to write tutorials as Lean files, using /-! -/ module doc comments for the text, rather than writing as markdown files with code blocks.

[Scott Morrison]

Having the tutorials runnable (and be checked by CI) is pretty useful.

[Scott Morrison]

I appreciate that it's harder to explain how to do imports, etc.

[Kevin Buzzard]

That's an interesting comment. I wrote the simp tutorial as an md file when I was learning about simp but I noticed you preferred lean files

[Scott Morrison]

I do worry about tutorials bit rotting, and CI checked lean files help there.

[Patrick Massot]

We need more tutorials Lean files. Also remember everybody is very welcome to contribute to https://github.com/leanprover-community/tutorials. I'm not saying everything you want to call a tutorial should go there, but it would be nice to have more there.

[Kevin Buzzard]

I think that I want an md file precisely because I found that my workflow yesterday involved having a bunch of lean files from the category theory library open in VS Code and having to switch between them; with an md file I can get the information I needed on a nice web link in GitHub

[Scott Morrison]

@Kevin Buzzard, after playing with fonts for a bit, I think you want Deja Vu Sans Mono, which has a nice big arrow (and seems generally nice). I mentioned that in the new category theory docs. It seems others were already using it. (I read back through zulip, and found various old discussions of fonts.)

[Scott Morrison]

Also, I noticed that I renamed docs/tutorials/category_theory/category_theory_intro.md to docs/tutorials/category_theory/intro.md, and then when you converted it to a Lean file (thanks!) it became again docs/tutorials/category_theory/category_theory_intro.lean.

[Scott Morrison]

I don't think we're having a revert war, just not noticing, but if it's okay with you I'll rename it back to intro.lean, and the principle that the directory it's in already tells you it's about category theory?

[Scott Morrison]

Also -- I'll delete the markdown file now? (I just made a bunch of further changes, all to the Lean file, so they've already parted ways.)

[Kevin Buzzard]

The name "change" was because I made the lean file without noticing you had made a commit -- I don't care what the files are called.

But for me, the markdown file is better. I would go so far to say that the markdown file is what I actually want. It's easier to read in a web browser, it appropriately changes notation (we have f : W -> X when talking about categories because I wanted to talk about transitivity W -> X -> Y -> Z and f : X -> Y when talking about functors because I didn't), and the imports are more explanatory. The variable names in the Lean file are really messed up because I can't unvariable a variable. The natural way to fix this would to be to make three Lean files with different variable names -- one for categories, one for functors and one for natural transformations -- and the very fact that you need three Lean files to explain what is going on is exactly the reason I wrote the md file in the first place: I already have three Lean files which explain what's going on and instead I wanted one file which had markup. If you don't want the markdown file in the tutorials directory that's fine -- why don't we move it to docs/extras? I definitely want to keep the markdown file somewhere. I made the Lean file because you wanted it -- but when I was working on G-modules yesterday I had the markdown file open in a browser whilst I coded in VS Code.

[Patrick Massot]

I can't unvariable a variable

Maybe you need sections then.

[Kevin Buzzard]

An attempt to install it left me with Source Code Variable, where the arrows are hugely different :-) Unfortunately they are still the same in the "Lean Messages" view, which now has a different font to the tabs where I'm editing Lean files...

I now see that there is a different setting which changes the font in the messages view!

[Kevin Buzzard]

Patrick Massot said:

I can't unvariable a variable

Maybe you need sections then.

That should solve the variable problem, and I don't really care about the import issue -- so all that's left is the fact that at the end of the day I want to view the file with markdown in a browser instead of clogging up my VS Code tabs -- the point of this is to get the aid I need out of VS Code.

[Kevin Buzzard]

Here's another potential problem with getting three Lean files into one Lean file -- these universe order issues. In the md file I have universes v u when doing categories, then universes v₁ v₂ v₃ u₁ u₂ u₃ when doing functors. If I do that then u will be introduced before v₁. Will that matter? I still feel that I am fighting things in the Lean file which aren't issues in the markdown file. Why is the markdown file not a good idea?

I'm adding sections to the Lean file.

[Scott Morrison]

Okay! I hadn't appreciated how much you wanted a markdown file. So we better have it!

[Kevin Buzzard]

Oh it's OK, I put the sections in -- I'm much happier with the situation now.

[Scott Morrison]

Here are some other possibilities:

[Scott Morrison]

1. we use the existing tooling to make a nice browser friendly file from the Lean tutorial

[Scott Morrison]

2. rewriting the actual library files for category/functor/natural_transformation, moving as much as possible into other files, possibly combining those three into a single file, and including in that file as much documentation as is reasonable

[Kevin Buzzard]

I'm over it now. My problem was with the variables. I pushed a fix to the Lean file a few hours ago and removed the WIP tag. I'm happy to go ahead with the PR. I can use tooling to see what I want to see.

[Scott Morrison]

@Kevin Buzzard, what do you think of moving the universes into sections too? (I'm happy to do this if you think it's a good idea.)

[Scott Morrison]

That way we won't have to mysteriously introduce 8 universes at once at the top of the file.

[Kevin Buzzard]

universes are I agree a bit ugly still. What I was worried about was that if we moved them to within sections then we would end up with universes v u v1 u1 and would have committed the cardinal sin of declaring u before v1. Is this an issue? That was the only reason I declared them all at the start.

[Scott Morrison]

It's only the pairs which are used together that need to be in the right order.

[Scott Morrison]

There's nothing wrong with v u v1 u1 v2 u2

[Scott Morrison]

Okay, I'll tweak this now.

[Kevin Buzzard]

Oh in which case let's definitely move the universes.

[Kevin Buzzard]

There is definitely some really cool link which I can never find and which I associate with @Bryan Gin-ge Chen , where you can type in a mathlib PR or something, and it displays a Lean file in markdown. This is the last thing I need!

[Kevin Buzzard]

I think it's a link to observable -- maybe an observable notebook?

[Kevin Buzzard]

got it: https://observablehq.com/@bryangingechen/github-lean-doc-preview

[Kevin Buzzard]

Oh darn it, it doesn't display the Lean code when I feed it https://github.com/leanprover-community/mathlib/blob/category_theory_docs/docs/tutorial/category_theory/intro.lean !

[Kevin Buzzard]

I really want to get this out of VS Code somehow.

[Kevin Buzzard]

gaargh I'm going back to my local copy of the md file ;-)

[Scott Morrison]

@Bryan Gin-ge Chen can we arrange for https://observablehq.com/@bryangingechen/github-lean-doc-preview to also display the Lean code? (Maybe via a checkbox option?)

[Reid Barton]

In a tutorial it probably makes no difference in what order you define universe variables anyways

[Reid Barton]

I didn't follow the discussion too closely but I would definitely prefer for these tutorials to be subject to CI somehow, most likely by being lean files. Otherwise I think they will become out of date quickly.

[Bryan Gin-ge Chen]

I can try to add syntax-highlighted Lean code to that notebook later this week. In principle we could also integrate "live" Lean on that page as well but the interface would be pretty ugly so I won't try.

[Kevin Buzzard]

The issue is that md files rot and lean tutorial files which haven't been processed with Patrick's formatter can be read in VS code but if you're just using them as documentation to be read then they'd be better off out of VS code in my opinion -- it's more convenient for me to switch from Vs code to browser than it is to switch tabs in Vs code. At least this is my experience -- I am not sure I can pin tabs in Vs code

[Reid Barton]

So I think the best end goal is a lean file you can reasonably read in a browser. I'm not up to speed on the various tools we currently have to do things like this

[Kevin Buzzard]

Bryan's link above is cool. Is there a way we can make an md file from a lean file? I think Patrick might argue though that his formatter is the correct thing to be using. I guess one would need more tooling to keep an html file up to date though

[Patrick Massot]

I haven't been following this thread. What do you want to do with my formatter? In any case I'm unlikely to argue it is the correct thing to be using, it is still very much an experiment. But I may suggest contributing to it.

[Kevin Buzzard]

In brief: I wanted somewhere where I could just remind myself of the difference between << and <<< etc, because I realised that whenever I wanted to do anything with categories I would have to have category.lean and functor.lean and natural_transformation.lean open in VS Code, and these three tabs were pushing my other tabs off the screen. So I wrote an md file like those simp.md or conv.md files to summarise how things work, and then all of a sudden Scott wanted to turn it back into a Lean file because he was concerned about bitrot, whereas I just wanted to view an md file in the browser.

[Kevin Buzzard]

here is the state of the Lean file. here is what I initially had in mind.

[Patrick Massot]

You don't have much tactic state to inspect in those files, right?

[Patrick Massot]

So you don't really need the non-trivial part of the formatter.

[Scott Morrison]

No, no tactic state at all.

[Kevin Buzzard]

Exactly. I wrote it precisely so I didn't have to keep opening functor.lean and then natural_transformation.lean whenever I saw <<<. I am a slow learner and I wrote precisely what I needed to help me.

[Patrick Massot]

So we could have a simple tool extracting all code-blocks from a md file, concatenate into a Lean file and check whether it compiles.

[Kevin Buzzard]

I was still using the md file even at the end of when I was writing the G-module file, as I still couldn't remember the name of alpha.naturality; I know the maths but I don't remember the Lean notation for the concepts.

[Scott Morrison]

I'm really dubious that the source should be an md file. Extracting documentation from code seems better than extracting code from documentation.

[Kevin Buzzard]

If Bryan's tool could be made to output something that displays like the md file from the Lean file, I will certainly not be complaining.

[Reid Barton]

The extract code from documentation approach is quite common in other languages, I think it is also viable

[Bryan Gin-ge Chen]

@Kevin Buzzard Here's a rough version of a Lean file viewer (applied to the category theory tutorial file). It makes use of @Patrick Massot's highlightjs code, which I copied to an Observable notebook here.

[Scott Morrison]

Lovely.

[Kevin Buzzard]

Perfect! This is precisely the document I needed last week :D Thanks Bryan! So the problem is now completely solved as far as I am concerned -- we can write docs which are Lean files and look at them like this.