Skip to content

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

Closed
joelriou wants to merge 25 commits intomasterfrom
port/AlgebraicTopology.DoldKan.GammaCompN
Closed

[Merged by Bors] - feat: port AlgebraicTopology.DoldKan.GammaCompN#3568
joelriou wants to merge 25 commits intomasterfrom
port/AlgebraicTopology.DoldKan.GammaCompN

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

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

joelriou added 19 commits April 21, 2023 07:23
@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 (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 (this label is automatically managed by a bot) label Apr 22, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 22, 2023

This PR/issue depends on:

@kim-em
Copy link
Copy Markdown
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
Copy Markdown
Contributor Author

joelriou commented Apr 22, 2023

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
Copy Markdown
Member

ChrisHughes24 commented Apr 22, 2023

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
Copy Markdown

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