Zulip Chat Archive

Stream: maths

Topic: category theory PR


view this post on Zulip Scott Morrison (Jun 04 2018 at 03:54):

@Kevin Buzzard, @Reid Barton, @Johan Commelin, the first cut of my category theory PR has just landed as https://github.com/leanprover/mathlib/pull/152. Criticisms welcome!

view this post on Zulip Johan Commelin (Jun 04 2018 at 06:31):

Newbie comment: In line 39 of your category.lean, you write

attribute [ematch] category.associativity_lemma

But isn't this also on the previous line?

view this post on Zulip Scott Morrison (Jun 04 2018 at 06:45):

Ooh, good catch. I didn't mean to have associativity marked as a simp, and will have to fix this. It shouldn't be a problem, but won't happen right now.

view this post on Zulip Johan Commelin (Jun 04 2018 at 06:49):

Ok

view this post on Zulip Johan Commelin (Jun 04 2018 at 06:49):

I submitted a review with 6 trivial comments.

view this post on Zulip Sean Leather (Jun 04 2018 at 07:38):

@Scott Morrison You might want to just review your usage of variables. I saw a number of duplicates mentioned in both a variables declaration and used in a def or theorem. I mentioned one on the PR, but there are more.

view this post on Zulip Scott Morrison (Jun 04 2018 at 08:48):

Thanks, @Sean Leather. I'm not sure that there were any actual errors, but I have definitely been writing code that sometimes has an explicit argument in a definition, when there is an implicit variable of the same name in scope. I'll be careful to avoid this.

view this post on Zulip Sean Leather (Jun 04 2018 at 08:55):

No, there were no errors. It's just a comment on readability. Looks better now.

view this post on Zulip Johan Commelin (Jun 04 2018 at 11:19):

Another point is that I think so far in mathlib there is no camel casing. I don't have a strong opinion on this, butI noticed that you use NaturalTransformation.

view this post on Zulip Johan Commelin (Jun 06 2018 at 18:36):

Once this PR has been merged we can formalise pijul.org. Once code extraction is in place we will have a fully verified abstract nonsense version control system!

view this post on Zulip Ned Summers (Jul 25 2018 at 15:04):

I'm working with this and I was wondering why is_Isomorphism is defined as it is. In particular, under the label I'd expect it to be a Prop? I'm new to lean in general so I'm sure it's justified, just having difficulty with any statements that involved "f is an isomorphism".

view this post on Zulip Reid Barton (Jul 25 2018 at 15:14):

If f is an isomorphism, one wants to be able to talk about the inverse of f (compose it with other morphisms, and so on). Even though the inverse of f is uniquely determined by f, from Lean's point of view it is still additional data. If is_Isomorphism was a Prop, it would throw away this data and you would need to use the axiom of choice to get a hold of f's inverse, which is generally less convenient.

view this post on Zulip Reid Barton (Jul 25 2018 at 15:21):

If you want the Prop version, you can use nonempty (is_Isomorphism f).

view this post on Zulip Reid Barton (Jul 25 2018 at 15:26):

This way you have a choice.

def blah1 ... : is_Isomorphism f := ...  -- show f is an isomorphism by exhibiting an inverse;
-- Lean now knows that the inverse is given by definition by whatever formula you gave

lemma blah2 ... : nonempty (is_Isomorphism f) := ...  -- show f is an isomorphism but don't specify the inverse;
-- Lean knows nothing about the inverse other than the equations contained in is_Isomorphism

Sometimes you don't care about the exact construction of the inverse, and then the second option is appropriate.

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 18:34):

If is_Isomorphism is not a prop, isn't the name contrary to mathlib conventions?

view this post on Zulip Patrick Massot (Jul 25 2018 at 18:35):

I agree, but this is in a not yet revised PR.

view this post on Zulip Ned Summers (Jul 26 2018 at 13:49):

Thanks, Reid. Makes a lot of sense; just getting used to this hesitance about choice. Thanks for the suggestion too of the Prop version.


Last updated: May 18 2021 at 08:14 UTC