category theory PR

Stream: maths

[Scott Morrison]

@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]

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]

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.

[Johan Commelin]

Ok

[Johan Commelin]

I submitted a review with 6 trivial comments.

[Sean Leather]

@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]

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]

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

[Johan Commelin]

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]

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]

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]

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]

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

[Reid Barton]

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]

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

[Patrick Massot]

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

[Ned Summers]

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