## Stream: maths

### Topic: Basic category theory observations

#### Kevin Buzzard (Mar 07 2020 at 18:47):

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 (Mar 07 2020 at 18:52):

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 (Mar 07 2020 at 18:53):

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


#### Kevin Buzzard (Mar 07 2020 at 18:58):

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 (Mar 07 2020 at 19:07):

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 (Mar 07 2020 at 19:07):

But yes, this seems not ideal

#### Kevin Buzzard (Mar 07 2020 at 19:08):

You're avoiding the question.

#### Reid Barton (Mar 07 2020 at 19:08):

What was the question?

#### Kevin Buzzard (Mar 07 2020 at 19:08):

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

#### Reid Barton (Mar 07 2020 at 19:08):

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 (Mar 07 2020 at 19:09):

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

oh, no

#### Reid Barton (Mar 07 2020 at 19:09):

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

#### Kevin Buzzard (Mar 07 2020 at 19:10):

This is doing my head in

OK fair enough

#### Kevin Buzzard (Mar 07 2020 at 19:10):

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

#### Reid Barton (Mar 07 2020 at 19:10):

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 (Mar 07 2020 at 19:11):

Are we getting that in Lean 4?

#### Reid Barton (Mar 07 2020 at 19:11):

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

I see.

Very nice!

#### Reid Barton (Mar 07 2020 at 19:11):

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

#### Reid Barton (Mar 07 2020 at 19:12):

Similarly composition of functors is definitionally associative

#### Kevin Buzzard (Mar 07 2020 at 19:16):

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 (Mar 07 2020 at 19:30):

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 (Mar 07 2020 at 19:31):

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 (Mar 07 2020 at 19:50):

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 (Mar 07 2020 at 19:52):

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 (Mar 07 2020 at 19:57):

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

#### Scott Morrison (Mar 07 2020 at 19:58):

Okay, I did it anyway. :-)

#### Scott Morrison (Mar 07 2020 at 20:01):

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 (Mar 07 2020 at 20:01):

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

#### Kevin Buzzard (Mar 07 2020 at 20:15):

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 (Mar 07 2020 at 20:22):

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 (Mar 07 2020 at 20:23):

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

#### Scott Morrison (Mar 07 2020 at 20:23):

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

#### Kevin Buzzard (Mar 07 2020 at 21:01):

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 (Mar 07 2020 at 21:06):

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

#### Patrick Massot (Mar 07 2020 at 21:17):

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 (Mar 07 2020 at 21:37):

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 (Mar 08 2020 at 04:43):

@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 (Mar 08 2020 at 04:45):

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 (Mar 08 2020 at 04:45):

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 (Mar 08 2020 at 04:46):

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 (Mar 08 2020 at 08:59):

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 (Mar 08 2020 at 09:06):

I can't unvariable a variable

Maybe you need sections then.

#### Kevin Buzzard (Mar 08 2020 at 09:31):

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 (Mar 08 2020 at 09:34):

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 (Mar 08 2020 at 09:48):

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 (Mar 08 2020 at 16:38):

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

#### Kevin Buzzard (Mar 08 2020 at 16:39):

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

#### Scott Morrison (Mar 08 2020 at 16:39):

Here are some other possibilities:

#### Scott Morrison (Mar 08 2020 at 16:40):

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

#### Scott Morrison (Mar 08 2020 at 16:42):

1. 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 (Mar 08 2020 at 16:43):

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 (Mar 08 2020 at 18:01):

@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 (Mar 08 2020 at 18:02):

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

#### Kevin Buzzard (Mar 08 2020 at 18:03):

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 (Mar 08 2020 at 18:03):

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

#### Scott Morrison (Mar 08 2020 at 18:04):

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

#### Scott Morrison (Mar 08 2020 at 18:04):

Okay, I'll tweak this now.

#### Kevin Buzzard (Mar 08 2020 at 18:04):

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

#### Kevin Buzzard (Mar 08 2020 at 18:05):

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 (Mar 08 2020 at 18:05):

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

#### Kevin Buzzard (Mar 08 2020 at 18:07):

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 (Mar 08 2020 at 18:08):

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

#### Kevin Buzzard (Mar 08 2020 at 18:09):

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

#### Scott Morrison (Mar 08 2020 at 18:10):

@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 (Mar 08 2020 at 19:30):

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

#### Reid Barton (Mar 08 2020 at 19:32):

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 (Mar 08 2020 at 19:41):

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 (Mar 08 2020 at 20:14):

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 (Mar 08 2020 at 20:15):

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 (Mar 08 2020 at 20:18):

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 (Mar 08 2020 at 20:20):

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 (Mar 08 2020 at 20:33):

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 (Mar 08 2020 at 20:37):

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

#### Patrick Massot (Mar 08 2020 at 20:40):

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

#### Patrick Massot (Mar 08 2020 at 20:41):

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

#### Scott Morrison (Mar 08 2020 at 20:41):

No, no tactic state at all.

#### Kevin Buzzard (Mar 08 2020 at 20:41):

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 (Mar 08 2020 at 20:42):

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 (Mar 08 2020 at 20:43):

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 (Mar 08 2020 at 20:47):

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 (Mar 08 2020 at 20:49):

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 (Mar 08 2020 at 22:34):

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

#### Bryan Gin-ge Chen (Mar 15 2020 at 05:13):

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

Lovely.

#### Kevin Buzzard (Mar 15 2020 at 08:08):

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.

Last updated: May 18 2021 at 08:14 UTC