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(algebraic_topology/dold_kan): technical lemmas about face maps #14044

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat(algebraic_topology/dold_kan): technical lemmas about face maps #14044

wants to merge 19 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented May 9, 2022 •
edited

This PR introduces technical lemmas about face maps and the null homotopic maps Hσ that will be used in the proof of the Dold-Kan equivalence.

Open in Gitpod

@semorrison semorrison added the awaiting-CI The author would like to see what CI has to say before doing more work. label May 9, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label May 10, 2022
@joelriou joelriou added the awaiting-review The author would like community review of the PR label May 10, 2022
@semorrison semorrison 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 May 22, 2022
@joelriou joelriou added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 22, 2022
@joelriou joelriou added the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 10, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 10, 2022
jcommelin
jcommelin reviewed Jun 18, 2022
View reviewed changes
src/algebraic_topology/dold_kan/faces.lean Outdated Show resolved Hide resolved
src/algebraic_topology/dold_kan/faces.lean Outdated Show resolved Hide resolved
src/algebraic_topology/dold_kan/faces.lean Show resolved Hide resolved
src/algebraic_topology/dold_kan/faces.lean Outdated Show resolved Hide resolved
@jcommelin jcommelin 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 Jun 18, 2022
joelriou and others added 2 commits June 20, 2022 07:19
@joelriou joelriou added the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 20, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 20, 2022
@joelriou joelriou added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 20, 2022
@joelriou joelriou added the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 12, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 12, 2022
kbuzzard
kbuzzard approved these changes Jul 20, 2022
View reviewed changes
Copy link
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

Very nice!

src/algebraic_topology/alternating_face_map_complex.lean Outdated Show resolved Hide resolved
src/algebraic_topology/dold_kan/faces.lean Show resolved Hide resolved
src/algebraic_topology/dold_kan/faces.lean Outdated Show resolved Hide resolved
src/algebraic_topology/dold_kan/faces.lean Outdated Show resolved Hide resolved
joelriou and others added 4 commits July 21, 2022 14:45
@joelriou @kbuzzard
Update src/algebraic_topology/alternating_face_map_complex.lean
e31d95d 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@joelriou @kbuzzard
Update src/algebraic_topology/dold_kan/faces.lean
095c325 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@joelriou @kbuzzard
Update src/algebraic_topology/dold_kan/faces.lean
e44fe26 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@joelriou
Merge remote-tracking branch 'origin' into dold-kan-2
a4e4894
jcommelin
jcommelin reviewed Jul 21, 2022
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.

bors d+

@bors
Copy link

bors bot commented Jul 21, 2022

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 21, 2022
@joelriou @jcommelin
Update src/algebraic_topology/dold_kan/faces.lean
8406791 
Co-authored-by: Johan Commelin <johan@commelin.net>
@joelriou
Copy link
Collaborator Author

Thanks @kbuzzard and @jcommelin for your suggestions.

@joelriou joelriou added the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 21, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 21, 2022
@joelriou
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Jul 21, 2022
@joelriou
feat(algebraic_topology/dold_kan): technical lemmas about face maps (#…
d29aca8 
…14044)

This PR introduces technical lemmas about face maps and the null homotopic maps Hσ that will be used in the proof of the Dold-Kan equivalence.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@bors
Copy link

bors bot commented Jul 21, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebraic_topology/dold_kan): technical lemmas about face maps [Merged by Bors] - feat(algebraic_topology/dold_kan): technical lemmas about face maps Jul 21, 2022
@bors bors bot closed this Jul 21, 2022
@bors bors bot deleted the dold-kan-2 branch July 21, 2022 18:20
joelriou added a commit that referenced this pull request Jul 23, 2022
@joelriou
feat(algebraic_topology/dold_kan): technical lemmas about face maps (#…
08235e7 
…14044)

This PR introduces technical lemmas about face maps and the null homotopic maps Hσ that will be used in the proof of the Dold-Kan equivalence.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

@jcommelin jcommelin jcommelin left review comments

@kbuzzard kbuzzard kbuzzard approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@joelriou @semorrison @jcommelin @kbuzzard @leanprover-community-bot-assistant