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

[Merged by Bors] - feat(category_theory): left-exact functors preserve finite limits #14026

Closed
wants to merge 55 commits into from
Closed

[Merged by Bors] - feat(category_theory): left-exact functors preserve finite limits #14026

wants to merge 55 commits into from

Conversation

javra
Copy link
Collaborator

@javra javra commented May 8, 2022 •
edited
Loading

Also adds the following:

  • Convenient constructors for binary_fan and adjustments to its simp NF
  • Generalize the (co)kernel constructions in inclusions and projections of binary biproducts
  • Fixes the name of kernel_fork.is_limit.of_ι
  • Derives preserves_limits_of_shape (discrete pempty) G from the preservation of just the terminal morphism
  • Preserving zero morphisms implies preserving terminal morphisms
  • Isomorphisms from any fork to an application of fork.of_ι

Open in Gitpod

javra added 19 commits April 25, 2022 13:09
@javra
necessary generalizations to biproducts
d1e1594
@javra
add doc strings
b7e0ce7
@javra
change name of kernel_fork.is_limit.of_iota
3cbd24f
@javra
fixes following renaming
e790b44
@javra
more renaming fixes
39605d2
@javra
add convenient way to show that a binary (co)fans are limits
69cdf7b
@javra
still missed one 'co'
02c98e2
@javra
better simp behaviour for binary product constructor
f591018
@javra
fix biproducts
3994388
@javra
generalize split_mono instances of inl, inr
7fa53dc
@javra
start showing preservation of products
ea01df7
@javra
move left exactness char and complete it
f2536e6
@javra
move construction to category_theory.abelian.exact
04b71c8
@javra
lint
290347b
@javra
add dual
92ace36
@javra
add preservation statements, still with sorries
d47f699
@javra
closer to the desired form of the preserves statement
f5e8c18
@javra
finish desired preservation statement
02de75f
@javra
remove recursors, prove equality of cones instead
a255cb7
@javra javra changed the title Left exact char feat(category_theory): left-exact functors preserve binary products May 8, 2022
@javra javra requested a review from TwoFX May 8, 2022 08:40
@javra javra added awaiting-review The author would like community review of the PR WIP Work in progress and removed awaiting-review The author would like community review of the PR labels May 8, 2022
TwoFX
TwoFX reviewed May 8, 2022
View reviewed changes
src/category_theory/abelian/exact.lean Outdated Show resolved Hide resolved
src/category_theory/abelian/exact.lean Outdated Show resolved Hide resolved
src/category_theory/abelian/exact.lean Outdated Show resolved Hide resolved
src/category_theory/abelian/exact.lean Outdated Show resolved Hide resolved
@javra javra added awaiting-review The author would like community review of the PR and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels May 24, 2022
@javra javra requested a review from semorrison May 24, 2022 07:07
@TwoFX TwoFX added WIP Work in progress and removed awaiting-review The author would like community review of the PR labels May 27, 2022
@javra javra added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Jul 8, 2022
@javra javra requested a review from TwoFX July 8, 2022 19:28
TwoFX
TwoFX reviewed Jul 10, 2022
View reviewed changes
src/category_theory/limits/preserves/shapes/zero.lean Show resolved Hide resolved
src/category_theory/limits/preserves/shapes/zero.lean Outdated Show resolved Hide resolved
src/category_theory/limits/shapes/biproducts.lean Outdated Show resolved Hide resolved
src/category_theory/limits/shapes/equalizers.lean Outdated Show resolved Hide resolved
src/category_theory/limits/shapes/equalizers.lean Outdated Show resolved Hide resolved
src/category_theory/preadditive/left_exact.lean Outdated Show resolved Hide resolved
src/category_theory/preadditive/left_exact.lean Outdated Show resolved Hide resolved
src/category_theory/preadditive/left_exact.lean Outdated Show resolved Hide resolved
src/category_theory/preadditive/left_exact.lean Outdated Show resolved Hide resolved
src/category_theory/preadditive/left_exact.lean Show resolved Hide resolved
@TwoFX TwoFX added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 10, 2022
@TwoFX
Copy link
Member

TwoFX commented Jul 11, 2022

Thanks!
bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 11, 2022
bors bot pushed a commit that referenced this pull request Jul 11, 2022
@javra @TwoFX
feat(category_theory): left-exact functors preserve finite limits (#1…
bbe25d4 
…4026)

Also adds the following:
* Convenient constructors for `binary_fan` and adjustments to its simp NF
* Generalize the (co)kernel constructions in inclusions and projections of binary biproducts
* Fixes the name of `kernel_fork.is_limit.of_ι`
* Derives `preserves_limits_of_shape (discrete pempty) G` from the preservation of just *the* terminal morphism
* Preserving zero morphisms implies preserving terminal morphisms
* Isomorphisms from any fork to an application of `fork.of_ι`



Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
@bors
Copy link

bors bot commented Jul 11, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category_theory): left-exact functors preserve finite limits [Merged by Bors] - feat(category_theory): left-exact functors preserve finite limits Jul 11, 2022
@bors bors bot closed this Jul 11, 2022
@bors bors bot deleted the left-exact-char branch July 11, 2022 19:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX left review comments

@semorrison semorrison Awaiting requested review from semorrison

Assignees
No one assigned
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.

None yet
3 participants
@javra @TwoFX @semorrison