Zulip Chat Archive

Stream: maths

Topic: Basic category theory observations


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

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 18:53):

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

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

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

view this post on Zulip Reid Barton (Mar 07 2020 at 19:07):

But yes, this seems not ideal

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 19:08):

You're avoiding the question.

view this post on Zulip Reid Barton (Mar 07 2020 at 19:08):

What was the question?

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 19:08):

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

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 19:09):

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

view this post on Zulip Reid Barton (Mar 07 2020 at 19:09):

oh, no

view this post on Zulip Reid Barton (Mar 07 2020 at 19:09):

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 19:10):

This is doing my head in

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 19:10):

OK fair enough

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 19:10):

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

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 19:11):

Are we getting that in Lean 4?

view this post on Zulip Reid Barton (Mar 07 2020 at 19:11):

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 19:11):

I see.

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 19:11):

Very nice!

view this post on Zulip Reid Barton (Mar 07 2020 at 19:11):

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

view this post on Zulip Reid Barton (Mar 07 2020 at 19:12):

Similarly composition of functors is definitionally associative

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

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

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

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

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

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

view this post on Zulip Scott Morrison (Mar 07 2020 at 19:58):

Okay, I did it anyway. :-)

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

view this post on Zulip Scott Morrison (Mar 07 2020 at 20:01):

How about , , , , , , , ?

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

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

view this post on Zulip Scott Morrison (Mar 07 2020 at 20:23):

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

view this post on Zulip Scott Morrison (Mar 07 2020 at 20:23):

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

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

view this post on Zulip Scott Morrison (Mar 07 2020 at 21:06):

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

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

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

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

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

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

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

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

view this post on Zulip Patrick Massot (Mar 08 2020 at 09:06):

I can't unvariable a variable

Maybe you need sections then.

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

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

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

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

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

view this post on Zulip Scott Morrison (Mar 08 2020 at 16:39):

Here are some other possibilities:

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

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

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

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

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

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

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

view this post on Zulip Scott Morrison (Mar 08 2020 at 18:04):

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

view this post on Zulip Scott Morrison (Mar 08 2020 at 18:04):

Okay, I'll tweak this now.

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 18:04):

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

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

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 18:05):

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

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 18:05):

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

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

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 18:08):

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

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 18:09):

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

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

view this post on Zulip Reid Barton (Mar 08 2020 at 19:30):

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

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

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 20:37):

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

view this post on Zulip Patrick Massot (Mar 08 2020 at 20:40):

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

view this post on Zulip Patrick Massot (Mar 08 2020 at 20:41):

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

view this post on Zulip Scott Morrison (Mar 08 2020 at 20:41):

No, no tactic state at all.

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

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

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

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

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

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

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

view this post on Zulip Scott Morrison (Mar 15 2020 at 05:19):

Lovely.

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