feat(category_theory/limits): kernels #1988
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jcommelin
reviewed
Feb 14, 2020
| /-- Every equalizer of (f, f) is an isomorphism -/ | ||
| def limit_cone_parallel_pair_self_is_iso (c : cone (parallel_pair f f)) (h : is_limit c) : | ||
| is_iso (c.π.app zero) := | ||
| begin |
There was a problem hiding this comment.
In this proof you are defining data using rw and similar tactics. This usually creates problems once you try to use the data.
There was a problem hiding this comment.
Luckily, in this case, z.hom.hom is actually defeq to c.π.app zero, so not only would rfl have shown t, we can simply get rid of the rewrite altogether.
On the other hand, for epi_limit_cone_parallel_pair_is_iso, I cannot see an easy way to get rid of the rewrite and especially the convert (on the other hand, I am not yet convinced that in this situation it really matters how the inverse is defined, as long as there are proofs that it is an inverse).
There was a problem hiding this comment.
In theory it doesn't matter. But it might complicate proving this about it. (Not in a conceptually hard way, but in a tedious, annoying, kind of way.)
jcommelin
reviewed
Feb 17, 2020
jcommelin
reviewed
Feb 19, 2020
jcommelin
reviewed
Feb 21, 2020
There was a problem hiding this comment.
I'm inclined to say that this looks ready for merging, but I would love to also here from other reviewers. @semorrison @rwbarton any comments?
semorrison
approved these changes
Feb 21, 2020
semorrison
reviewed
Feb 21, 2020
jcommelin
approved these changes
Feb 22, 2020
jcommelin
added
the
ready-to-merge
Merged
4 tasks
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this pull request
May 15, 2020
* chore(category_theory): require morphisms live in Type * move back to Type * fixes * feat(category_theory/limits): kernels * finishing basic API for kernels * update post leanprover-community#1412 * fix * documentation * documentation * more docs * replacing dumb code * forall -> Pi * removing all instances * working on Reid's suggested lemmas * experiments * lots to do * Show that equalizers are monomorphisms * Show that equalizer of (f, f) is always an iso * Show that an equalizer that is an epimorphism is an isomorphism * Clean up * Show that the kernel of a monomorphism is zero * Fix * Show that the kernel of a linear map is a kernel in the categorical sense * Modify proof * Compactify proof * Various cleanup * Some more cleanup * Fix bibtex * Address some issues raised during discussion of the PR * Fix some more incorrect indentation * Some more minor fixes * Unify capitalization in Bibtex entries * Replace equalizer.lift.uniq with equalizer.hom_ext * Some more slight refactors * Typo Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this pull request
May 16, 2020
* chore(category_theory): require morphisms live in Type * move back to Type * fixes * feat(category_theory/limits): kernels * finishing basic API for kernels * update post leanprover-community#1412 * fix * documentation * documentation * more docs * replacing dumb code * forall -> Pi * removing all instances * working on Reid's suggested lemmas * experiments * lots to do * Show that equalizers are monomorphisms * Show that equalizer of (f, f) is always an iso * Show that an equalizer that is an epimorphism is an isomorphism * Clean up * Show that the kernel of a monomorphism is zero * Fix * Show that the kernel of a linear map is a kernel in the categorical sense * Modify proof * Compactify proof * Various cleanup * Some more cleanup * Fix bibtex * Address some issues raised during discussion of the PR * Fix some more incorrect indentation * Some more minor fixes * Unify capitalization in Bibtex entries * Replace equalizer.lift.uniq with equalizer.hom_ext * Some more slight refactors * Typo Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list
This PR replaces #1445. Since then, the following has been added:
punit) and all kernels (f.ker.subtype)