Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix(category_theory/finite_limits): fix definition, and construct from finite products and equalizers #1427

Merged
merged 27 commits into from
Sep 21, 2019
Merged

fix(category_theory/finite_limits): fix definition, and construct from finite products and equalizers #1427

merged 27 commits into from
Sep 21, 2019

Conversation

semorrison
Copy link
Collaborator

@semorrison semorrison commented Sep 10, 2019 •
edited by rwbarton

This fixes the error in the definition of finite limits noted in #1410, and tests out the new definition by constructing finite limits from finite products and equalizers.

Happily, we can reuse the construction of (arbitrary) limits from (arbitrary) products and equalizers almost verbatim --- all the fintype instances slot into place without any help.

It's a bit sad that constructions/finite_limits.lean duplicates so much of the text from constructions/limits_of_products_and_equalizers.lean, but I don't see how to factor anything out without being extremely awkward.

Fixes #1410.

@semorrison semorrison requested a review from a team as a code owner September 10, 2019 06:53
@semorrison
Copy link
Collaborator Author

I've kept everything constructive, so in particular a fin_category instance contains the fact that objects and morphisms have decidable_eq.

@rwbarton
Copy link
Collaborator

I just learned from reading this PR that fintype is not the same as the usual constructive notion of finiteness, so I will take some time to meditate on this.

However I will say that my instinct is that it would be better to make fin_category J a "mix-in", that is, indexed on category J rather than extending it. I'm also not sure why you chose to extend fintype J but include decidable_eq J as a field.

@jcommelin
Copy link
Member

I'm also not sure why you chose to extend fintype J but include decidable_eq J as a field.

Probably because you can't extend decidable_eq J. It's not a structure.

@semorrison
Copy link
Collaborator Author

Ok, I can make it a mix-in. I was just hoping to minimise the number of separate arguments that need to be passed around.

@rwbarton
Copy link
Collaborator

Ahh, sorry. I really just meant to have fin_category J indexed on category J, but not fintype J or decidable_eq J. I'm not sure how the latter would be useful and it does seem excessively wordy. Unless I'm missing some technical reason for having it?

@semorrison
Copy link
Collaborator Author

Oops, sorry, that should have been obvious. :-) Fixed now.

@semorrison
Copy link
Collaborator Author

(Updated to reflect #1412 being merged.)

@robertylewis
Copy link
Member

Doc strings for defs, please!

@semorrison semorrison added the needs-documentation This PR is missing required documentation label Sep 18, 2019
@semorrison semorrison removed the needs-documentation This PR is missing required documentation label Sep 20, 2019
@semorrison
Copy link
Collaborator Author

I've added documentation, and this should be ready for further review/merging.

@semorrison semorrison added the awaiting-review The author would like community review of the PR label Sep 20, 2019
@rwbarton
Copy link
Collaborator

I really think has_limit_of_has_products_of_has_equalizers and has_limit_of_has_finite_products_of_has_equalizers should not be instances, for the same reason that limits_from_equalizers_and_products and finite_limits_from_equalizers_and_finite_products are not. Arguably you could just inline these definitions into their use sites.

Otherwise, looks great!

@rwbarton rwbarton removed the awaiting-review The author would like community review of the PR label Sep 20, 2019
@semorrison
Copy link
Collaborator Author

I agree the has_limit instances were bad, so I've inlined them as you suggested.

@semorrison
Copy link
Collaborator Author

semorrison commented Sep 20, 2019 •
edited

Hopefully we're ready to go now!

jcommelin
jcommelin approved these changes Sep 21, 2019
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me

@jcommelin jcommelin added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Sep 21, 2019
@mergify mergify bot merged commit 65bf45c into master Sep 21, 2019
@mergify mergify bot deleted the fix_finite_limits branch September 21, 2019 06:13
JaredCorduan pushed a commit to JaredCorduan/mathlib that referenced this pull request Oct 12, 2019
@semorrison @JaredCorduan
fix(category_theory/finite_limits): fix definition, and construct fro…
e3ee989 
…m finite products and equalizers (leanprover-community#1427)

* chore(category_theory): require morphisms live in Type

* move back to Type

* fix(category_theory/finite_limits): fix definition, and construct from finite products and equalizers

* fixes

* fix duplicate name

* make fin_category a mixin

* fix

* fix

* oops

* fixes

* oops missing universe change

* finish documentation

* fix namespace

* move variables to the right place

* don't repeat yourself

* update module doc-string now that the files have been merged

* inlining has_limit instances
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
@semorrison @anrddh
fix(category_theory/finite_limits): fix definition, and construct fro…
f1e0544 
…m finite products and equalizers (leanprover-community#1427)

* chore(category_theory): require morphisms live in Type

* move back to Type

* fix(category_theory/finite_limits): fix definition, and construct from finite products and equalizers

* fixes

* fix duplicate name

* make fin_category a mixin

* fix

* fix

* oops

* fixes

* oops missing universe change

* finish documentation

* fix namespace

* move variables to the right place

* don't repeat yourself

* update module doc-string now that the files have been merged

* inlining has_limit instances
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

@rwbarton rwbarton

Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

definition of has_finite_limits is wrong
4 participants
@semorrison @rwbarton @jcommelin @robertylewis