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 CategoryTheory.Endofunctor.Algebra #3541

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat: port CategoryTheory.Endofunctor.Algebra #3541

wants to merge 9 commits into from

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Apr 20, 2023

Open in Gitpod

@nomeata
feat: port CategoryTheory.Endofunctor.Algebra
2ef4c34
@nomeata
Initial file copy from mathport
645b334
@nomeata
automated fixes
f18ccfa 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@nomeata nomeata added the help-wanted The author needs attention to resolve issues label Apr 20, 2023
@nomeata
Copy link
Collaborator Author

nomeata commented Apr 20, 2023

Stuck at def isoMk: The hom_inv_id field used to be auto-solved, but no longer isn’t (with aesop_cat). Goal is

Hom.mk h.hom ≫ Hom.mk h.inv = 𝟙 A₀

Not sure if this is something that aesop_cat should solve here, or if manual work is now needed.

@int-y1 int-y1 added the mathlib-port This is a port of a theory file from mathlib. label Apr 23, 2023
@int-y1 int-y1 changed the title Port/category theory.endofunctor.algebra feat: port CategoryTheory.Endofunctor.Algebra Apr 23, 2023
@jjaassoonn jjaassoonn added awaiting-review The author would like community review of the PR awaiting-CI and removed help-wanted The author needs attention to resolve issues labels May 15, 2023
@semorrison
Copy link
Contributor

Please use porting note rather than port note for consistency (so we can easily grep for these notes).

Otherwise, looks great.

bors d+

@bors
Copy link

bors bot commented May 16, 2023

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

@github-actions github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels May 16, 2023
@jjaassoonn
Copy link
Collaborator

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

@nomeata Could you merge this PR please, Thanks

@nomeata
Copy link
Collaborator Author

nomeata commented May 16, 2023

bors r+

bors bot pushed a commit that referenced this pull request May 16, 2023
@nomeata @jjaassoonn
feat: port CategoryTheory.Endofunctor.Algebra (#3541)
258e751 


Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
bors bot pushed a commit that referenced this pull request May 16, 2023
@nomeata @jjaassoonn
feat: port CategoryTheory.Endofunctor.Algebra (#3541)
bb4ae7c 


Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
@bors
Copy link

bors bot commented May 16, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: port CategoryTheory.Endofunctor.Algebra [Merged by Bors] - feat: port CategoryTheory.Endofunctor.Algebra May 16, 2023
@bors bors bot closed this May 16, 2023
@bors bors bot deleted the port/CategoryTheory.Endofunctor.Algebra branch May 16, 2023 15:19
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
delegated mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@nomeata @semorrison @jjaassoonn @int-y1