Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebra/homology): chain complexes are an additive category #7478

Closed
wants to merge 64 commits into from
Closed

[Merged by Bors] - feat(algebra/homology): chain complexes are an additive category #7478

wants to merge 64 commits into from

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented May 4, 2021 •
edited by github-actions bot
Loading

kim-em and others added 21 commits May 4, 2021 19:55
@kim-em
feat(category_theory/.../images): image.pre_comp_epi_of_epi
ce8b14e
@kim-em
feat(category_theory/.../zero): if a zero morphism is a mono, the sou…
2ab67aa 
…rce is zero
@kim-em
add simp lemmas
dc8ac57
@kim-em
feat(category_theory/.../additive_functor): additive functors preserv…
410a946 
…e zero objects
@kim-em
feat(category_theory/preadditive): reformulation of mono_of_kernel_zero
25a6827
@kim-em
feat(category_theory/subobject): minor tweaks
6fa9bfe
@kim-em
Merge branch 'subobject2' into subobject_limits
62850b8
@kim-em
feat(category_theory/subobjects): more about kernel and image subobjects
d6169aa
@kim-em
minor
3caf09d
@kim-em
Merge branch 'subobject_limits' into homology_redesign
292109b
@kim-em
Merge branch 'subobject2' into subobject_limits
79e72a0
@kim-em
Merge branch 'subobject_limits' into homology_redesign
01f2cc4
@kim-em
Merge branch 'mono_of_kernel_iso_zero' into homology_redesign
723796d
@kim-em
Merge branch 'zero' into homology_redesign
a4635dc
@kim-em
feat(algebra/homology): redesign of homological complexes
b9c853b
@kim-em
feat(algebra/homology/single): chain complexes supported in a single …
5feee94 
…degree
@kim-em
oops
bc59d44
@kim-em
Merge branch 'homology_redesign' into homology_single
7e30250
@kim-em
feat(algebra/homology): chain complexes are an additive category
5f441a0
@kim-em
Merge branch 'functor.map_zero_object' into homology_additive
f2c531f
@kim-em @jcommelin
Apply suggestions from code review
683ac43 
Co-authored-by: Johan Commelin <johan@commelin.net>
@github-actions github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 4, 2021
@kim-em kim-em mentioned this pull request May 4, 2021
Closed
1 task
adamtopaz
adamtopaz approved these changes May 14, 2021
View reviewed changes
Copy link
Collaborator

@adamtopaz adamtopaz left a comment

Choose a reason for hiding this comment

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

Aside from a few minor comments, this looks good to me!

src/algebra/homology/additive.lean Outdated Show resolved Hide resolved
src/algebra/homology/additive.lean Outdated Show resolved Hide resolved
src/algebra/homology/additive.lean Outdated Show resolved Hide resolved
src/algebra/homology/additive.lean Show resolved Hide resolved
kim-em and others added 3 commits May 14, 2021 20:01
jcommelin
jcommelin approved these changes May 14, 2021
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.

Thanks 🎉

bors merge

@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-review The author would like community review of the PR labels May 14, 2021
bors bot pushed a commit that referenced this pull request May 14, 2021
@kim-em
feat(algebra/homology): chain complexes are an additive category (#7478)
e5b678f 


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented May 14, 2021

Build failed:

@bryangingechen bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes delegated The PR author may merge after reviewing final suggestions. and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels May 14, 2021
@jcommelin
Copy link
Member

bors merge

@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 May 14, 2021
bors bot pushed a commit that referenced this pull request May 14, 2021
@kim-em
feat(algebra/homology): chain complexes are an additive category (#7478)
a52f471 


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented May 14, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/homology): chain complexes are an additive category [Merged by Bors] - feat(algebra/homology): chain complexes are an additive category May 14, 2021
@bors bors bot closed this May 14, 2021
@bors bors bot deleted the homology_additive branch May 14, 2021 19:01
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jcommelin jcommelin jcommelin approved these changes

@adamtopaz adamtopaz adamtopaz approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. 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.
4 participants
@kim-em @jcommelin @adamtopaz @bryangingechen