## Stream: maths

### Topic: category theory PR

#### 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!

#### 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?

#### 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.

Ok

#### Johan Commelin (Jun 04 2018 at 06:49):

I submitted a review with 6 trivial comments.

#### 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.

#### 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.

#### Sean Leather (Jun 04 2018 at 08:55):

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

#### 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.

#### 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!

#### 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".

#### 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.

#### Reid Barton (Jul 25 2018 at 15:21):

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

#### 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.

#### Kevin Buzzard (Jul 25 2018 at 18:34):

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

#### Patrick Massot (Jul 25 2018 at 18:35):

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

#### 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