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: port AlgebraicTopology.DoldKan.GammaCompN #3568

Closed
wants to merge 25 commits into from
Closed

[Merged by Bors] - feat: port AlgebraicTopology.DoldKan.GammaCompN #3568

wants to merge 25 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented Apr 21, 2023 •
edited by ChrisHughes24
Loading

@joelriou
feat: port AlgebraicTopology.DoldKan.Degeneracies
bd6858c
@joelriou
Initial file copy from mathport
227a8d2
@joelriou
automated fixes
cdcd07a 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@joelriou
started working on this file
6053e8e
@joelriou
it compiles
495f1fb
@joelriou
feat: port AlgebraicTopology.DoldKan.SplitSimplicialObject
545b8f9
@joelriou
Initial file copy from mathport
75dbf1a
@joelriou
automated fixes
6add734 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@joelriou
Merge remote-tracking branch 'origin/port/AlgebraicTopology.DoldKan.D…
617a068 
…egeneracies' into port/AlgebraicTopology.DoldKan.SplitSimplicialObject
@joelriou
it compiles
0f02de2
@joelriou
feat: port AlgebraicTopology.DoldKan.FunctorGamma
661663e
@joelriou
Initial file copy from mathport
b9bfb64
@joelriou
automated fixes
e7b8ddd 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@joelriou
Merge remote-tracking branch 'origin/port/AlgebraicTopology.DoldKan.S…
5825b25 
…plitSimplicialObject' into port/AlgebraicTopology.DoldKan.FunctorGamma
@joelriou
it compiles
fd57286
@joelriou
feat: port AlgebraicTopology.DoldKan.GammaCompN
25fb74d
@joelriou
Initial file copy from mathport
a5d19ed
@joelriou
automated fixes
c944ecd 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@joelriou
Merge remote-tracking branch 'origin/port/AlgebraicTopology.DoldKan.F…
678e9c7 
…unctorGamma' into port/AlgebraicTopology.DoldKan.GammaCompN
@joelriou joelriou added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 21, 2023
@kim-em kim-em added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Apr 21, 2023
@joelriou joelriou mentioned this pull request Apr 21, 2023
Closed
3 tasks
@joelriou joelriou removed the WIP Work in progress label Apr 21, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 21, 2023
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 21, 2023
@joelriou joelriou mentioned this pull request Apr 21, 2023
Closed
3 tasks
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Apr 22, 2023
@kim-em
Copy link
Contributor

kim-em commented Apr 22, 2023

This PR/issue depends on:

@kim-em
Copy link
Contributor

kim-em commented Apr 22, 2023

@joelriou, I've pushed a commit that fixes the timeout with exact h, by adding some irreducible attributes.

I haven't tested this downstream (or by backporting), so please feel free to revert if this won't work out.

I wish carefully adding irreducible everywhere possible was part of our usual routine building an API, but it isn't. :-)

@kim-em kim-em added the awaiting-author A reviewer has asked the author a question or requested changes label Apr 22, 2023
@joelriou
Copy link
Collaborator Author

Thanks very much @semorrison ! I had similar timeout problems downstream in NCompGamma and EquivalenceAdditive. As the proofs relies much more on the simplification lemmas than the actual def, making some definitions irreducible seems to be the best solution. So far, NCompGamma and EquivalenceAdditive still compiles with this change, so that this PR should be good to go.

@joelriou joelriou added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 22, 2023
@ChrisHughes24
Copy link
Member

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 22, 2023
bors bot pushed a commit that referenced this pull request Apr 22, 2023
@joelriou @kim-em
feat: port AlgebraicTopology.DoldKan.GammaCompN (#3568)
0b676a2 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Apr 22, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port AlgebraicTopology.DoldKan.GammaCompN [Merged by Bors] - feat: port AlgebraicTopology.DoldKan.GammaCompN Apr 22, 2023
@bors bors bot closed this Apr 22, 2023
@bors bors bot deleted the port/AlgebraicTopology.DoldKan.GammaCompN branch April 22, 2023 16:56
kim-em added a commit that referenced this pull request May 10, 2023
@joelriou @kim-em
feat: port AlgebraicTopology.DoldKan.GammaCompN (#3568)
d4fbb04 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
hrmacbeth pushed a commit that referenced this pull request May 10, 2023
@joelriou @kim-em @hrmacbeth
feat: port AlgebraicTopology.DoldKan.GammaCompN (#3568)
dc33cf3 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
hrmacbeth pushed a commit that referenced this pull request May 11, 2023
@joelriou @kim-em @hrmacbeth
feat: port AlgebraicTopology.DoldKan.GammaCompN (#3568)
e4fe90e 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@joelriou @kim-em @ChrisHughes24