limits 3.0

Stream: maths

[Johan Commelin]

@Scott Morrison @Reid Barton Any updates on special shapes? I would love to have (co)equalizers and pullbacks/pushouts. I could try to come up with something myself, but I think I won't get a better interface than what we had before.

[Scott Morrison]

@Johan Commelin I split up what I'd done before into https://github.com/leanprover-community/mathlib/tree/limits-shapes and https://github.com/leanprover-community/mathlib/tree/limits-other.

[Scott Morrison]

The first just has a minimal API for (de)constructing cones corresponding to each of the usual special shapes. It seems like this part, or at least some version of it, is necessary no matter what we do later, and I think @Reid Barton agrees.

[Scott Morrison]

The second is just my original work on the O(M*N) api, rebased onto the limits-shapes branch.

[Scott Morrison]

I would still be perfectly happy to work on getting that merged, but Reid wasn't too happy with it. I've been in holiday mode for a while (...maybe too long... :-) and now really better turn to grant-writing-mode, but if you want to discuss this I'm happy to make changes.

[Johan Commelin]

I see. You didn't PR the limits-shapes branch yet, did you?

[Johan Commelin]

@Reid Barton What's your opinion on https://github.com/leanprover-community/mathlib/commit/a55e2334379c4769220e9446068bac89ddb6f29a? I think this is O(N) stuff that we will want anyway. Should it be PR'd?

[Johan Commelin]

@Scott Morrison @Reid Barton I'm just wondering, wouldn't it be "better" if is_limit.lift was a cone morphism, instead of just a hom between the tips?

[Scott Morrison]

I went back and forth on this a few times. Mario's suggestion had been that for the most basic definitions, it was good to write things out explicitly.

[Scott Morrison]

I would not complain about switching this again. Can you point to places where it would essentially simplify use?

[Scott Morrison]

I should PR the limits-shapes branch, I guess. I haven't had much Lean time recently -- but if, @Johan Commelin , you think it looks plausible, I will hit the PR button soon.

[Johan Commelin]

@Scott Morrison I personally think it looks fine. So let's just go for it...

[Johan Commelin]

Unrelated question: should is_colimit.mk_cocone_morphism be renamed to is_colimit.mk_of_cocone_morphism?
https://github.com/leanprover/mathlib/blob/78f1949719676db358ea5e68e211a73e2ce95e7b/src/category_theory/limits/limits.lean#L149

[Johan Commelin]

@Scott Morrison @Mario Carneiro This is an example where I am using unique: https://github.com/leanprover-community/mathlib/blob/adjunctions-2/src/category_theory/adjunction.lean#L321

[Johan Commelin]

The proof is somewhat annoying with a letI that shouldn't be there.

[Johan Commelin]

That is probably because I didn't listen well enough to Mario, and made equiv.unique_of_equiv use instances, instead of explicit variables.

[Mario Carneiro]

that

[Johan Commelin]

However, this proof captures very well the spirit of the maths proof.

[Johan Commelin]

Right, so I'll improve it by fixing equiv.unique_of_equiv

[Johan Commelin]

And the proof would become even slicker if I don't have to call is_colimit_iso_unique_cocone_morphism two times.

[Mario Carneiro]

feel free to smuggle the change in your next category theory PR

[Scott Morrison]

Ok, #611 contains limits-shapes.

[Johan Commelin]

From the discussion in #611: https://arxiv.org/pdf/1401.7694.pdf
Seems like a very interesting read to me.

[Kevin Buzzard]

"Although pre-existing formalizations of category theory in proof assistants
abound [1, 4, 5, 6, 7, 8, 9, 12, 17, 18, 19, 20, 21, 22, 26, 29, 30, 31, 33, 34,
38, 39, 40, 41, 42, 43, 44, 46, 47, 48, 50, 51, 54, 55, 59, 60, 61], we chose to
implement our library [28] from scratch."

!

[Kevin Buzzard]

All these category theory libraries and nobody doing schemes??

[Scott Morrison]

I'd read that one before even meeting Lean; a lot of their discussion is HoTT specific.

[Scott Morrison]

Computer scientists know category theory; very few know schemes.

[Reid Barton]

I'm really curious which of these libraries have been applied to something other than category theory

[Johan Commelin]

The current library in Lean 3 hasn't been stress-tested too much in that regard either...

[Kevin Buzzard]

I know I've said this before but in my opinion one of the reasons that mathematicians have been slow adopters of these tools is because computer scientists have overwhelmingly been formalising the kind of mathematics they meet/like rather than the kind that is actually in used in maths departments. I don't think it will be long before Lean starts breaking this mould. I think Sebastien's work on the Morse lemma and Johannes' forthcoming work on Ellenberg-Gijswijt are rare examples of "normal" recent theorems formalised in provers but these are rare. Of course, to make progress one has to do category theory :-) but as the others have said, to mathematicians these things are often regarded by mathematicians as just tools, or even just a language, to make doing actual maths easier.