## Stream: maths

### Topic: limits 3.0

#### Johan Commelin (Jan 05 2019 at 14:51):

@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 (Jan 06 2019 at 04:02):

@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 (Jan 06 2019 at 04:03):

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 (Jan 06 2019 at 04:03):

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

#### Scott Morrison (Jan 06 2019 at 04:04):

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 (Jan 06 2019 at 05:27):

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

#### Johan Commelin (Jan 14 2019 at 09:43):

@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 (Jan 17 2019 at 15:52):

@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 (Jan 19 2019 at 00:23):

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 (Jan 19 2019 at 00:24):

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

#### Scott Morrison (Jan 19 2019 at 00:25):

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 (Jan 19 2019 at 06:15):

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

#### Johan Commelin (Jan 19 2019 at 09:21):

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 (Jan 19 2019 at 09:48):

@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 (Jan 19 2019 at 09:48):

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

#### Johan Commelin (Jan 19 2019 at 09:49):

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

that

#### Johan Commelin (Jan 19 2019 at 09:49):

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

#### Johan Commelin (Jan 19 2019 at 09:50):

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

#### Johan Commelin (Jan 19 2019 at 09:50):

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

#### Mario Carneiro (Jan 19 2019 at 09:51):

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

#### Scott Morrison (Jan 19 2019 at 10:45):

Ok, #611 contains limits-shapes.

#### Johan Commelin (Feb 05 2019 at 20:43):

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

#### Kevin Buzzard (Feb 05 2019 at 21:36):

"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 (Feb 05 2019 at 21:37):

All these category theory libraries and nobody doing schemes??

#### Scott Morrison (Feb 06 2019 at 04:58):

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

#### Scott Morrison (Feb 06 2019 at 04:59):

Computer scientists know category theory; very few know schemes.

#### Reid Barton (Feb 06 2019 at 05:13):

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

#### Johan Commelin (Feb 06 2019 at 06:12):

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

#### Kevin Buzzard (Feb 06 2019 at 07:50):

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.

Last updated: May 18 2021 at 07:19 UTC