categories

Stream: new members

[Edward Ayers]

I made a silly .lean file for mathematical category theory.
https://gist.github.com/EdAyers/87fa2de6ddfc13ab273af52c21d48681
Two questions;
- what is the best way to solve the lemmas with sorry in them?
- doesn't the definition of Cat break the type universe hierarchy? And if so why doesn't lean care?

[Edward Ayers]

Also any comments on style / readability would be appreciated

[Kevin Buzzard]

Just to comment that fresh this week we've had a huge category theory PR accepted into mathlib: https://github.com/leanprover/mathlib/commit/9b1be732e122d371100b0df479ca000c2a3f73b0

[Edward Ayers]

ok thanks I can compare it to my code

[Scott Morrison]

Hi @Kevin Buzzard, sorry to disappoint, but that PR that was merged was only the first epsilon of the actual category theory library (just 3 files!) It's still a long way to go anything useful to you is there. :-)

[Scott Morrison]

There's a second PR waiting, if anyone feels like giving some comments.<https://github.com/leanprover/mathlib/pull/239>.

[Patrick Massot]

I made a silly .lean file for mathematical category theory.
https://gist.github.com/EdAyers/87fa2de6ddfc13ab273af52c21d48681

Who keeps the record of all beginners who had category theory as their first idea of something to formalize?

[Kevin Buzzard]

If you want to add to the list of "stuff which it looks like a good idea to be the first thing to formalise" then you seem to be able to add basic number theory to that list. My students ended up in coercion hell going from nat to int to zmod n

[Reid Barton]

Heh, the first two things I tried to formalize were fibrations of categories (that went poorly) and FLT for n=4

[Kevin Buzzard]

At least FLT for n=4 is a statement about nat.

[Kevin Buzzard]

The proof might not stray too far from nat either

[Kevin Buzzard]

oh actually maybe it strays into int a fair bit...

[Reid Barton]

I managed to nearly avoid using int, I think, but it might have been better to use it more. Lots of annoying inequality side conditions to check when doing algebraic manipulations over nat

[Edward Ayers]

I chose cats because that's the area of maths I'm strongest at and because it forces me to use lots of dependent-type features

[Mario Carneiro]

I don't disagree that it's a logical choice when starting to play with a DTT prover, but it really is so common it's almost a joke

[Mario Carneiro]

I'm sure I've seen this happen at least 8 times

[Edward Ayers]

Another fun one is making vec n and matrices and so on.

[Mario Carneiro]

Those might be in TPIL though

[David Michael Roberts]

So I would like to say that I have some category, and say that it has some object. It's not obvious how to even declare a variable of type category. What I would like to do is to define the type of terminal objects of a given category. In type theory I guess I would do something like the dependent type

C:category |- terminalObj(C): C.obj

where C.obj is the type of objects of C.

[David Michael Roberts]

(I should say I'm using category_theory in mathlib)

Then terminalObj(C) := Σ t: C.Obj Π_{x:C.Obj} Π_{f,g:Hom(x,t)} f = g

[Mario Carneiro]

In lean, we have category A as the type of categories where A is the type of objects. (That is, they are "partially unbundled" with the type of objects exposed.) Then you can define a structure is_terminal (X : A) : Type with fields for the unique map in, and the statement of uniqueness

[David Michael Roberts]

Ah, that makes sense. Particularly as Cat is fibred over Class by sending a category to its class of objects, so that it makes sense to talk of the dependent type A:Type |- category(A): Type.

[Mario Carneiro]

Yes, what you call fibration is what we call unbundling

[Scott Morrison]

Terminal objects (along with every other shape of (co)limit) are on the horizon. If you want to peek, and don't mind peeking at often-broken code, see the working branch of https://github.com/semorrison/lean-category-theory/tree/working/src/category_theory/limits.

[Scott Morrison]

("working" here is as-in "I'm working on it", not "it is working"...)

[Mario Carneiro]

I think wip is less susceptible to misinterpretation

[Scott Morrison]

ok, I'll use that in future! thanks.

[David Michael Roberts]

@Scott Morrison thanks, I'll check it out