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: category of coalgebras #11972

Closed
wants to merge 22 commits into from
Closed

[Merged by Bors] - feat: category of coalgebras #11972

wants to merge 22 commits into from

Conversation

101damnations
Copy link
Collaborator

@101damnations 101damnations commented Apr 7, 2024 •
edited
Loading

The category of coalgebras over a commutative ring. Mimics Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.

Open in Gitpod

github-actions[bot]
github-actions bot reviewed Apr 7, 2024
View reviewed changes
Mathlib.lean Outdated Show resolved Hide resolved
Mathlib.lean Show resolved Hide resolved
@101damnations 101damnations mentioned this pull request Apr 7, 2024
Closed
6 tasks
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib label Apr 7, 2024
This was referenced Apr 7, 2024
Open
Open
Open
Open
Open
This was referenced Apr 8, 2024
Open
Open
Open
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 16, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 1, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib label May 2, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 2, 2024
@101damnations 101damnations added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels May 2, 2024
eric-wieser
eric-wieser reviewed May 2, 2024
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

As this is new code, I wonder if we should copy the strategy of the QuadraticModuleCat instead, which has slightly more opaque types and is probably more performant as a result.

cc @mattrobball, @joelriou

kbuzzard
kbuzzard reviewed May 6, 2024
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.

I don't understand Eric's comment yet but this all looks good to me.

Mathlib/Algebra/Category/CoalgebraCat/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/Category/CoalgebraCat/Basic.lean Outdated Show resolved Hide resolved
@kbuzzard kbuzzard 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 6, 2024
@101damnations
Copy link
Collaborator Author

Thanks for the suggestion @eric-wieser - I have tried to apply it

@101damnations 101damnations added awaiting-review The author would like community review of the PR awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 11, 2024
kbuzzard
kbuzzard reviewed May 19, 2024
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.

@eric-wieser are you happier with this approach?

Mathlib/Algebra/Category/CoalgebraCat/Basic.lean Outdated Show resolved Hide resolved
eric-wieser
eric-wieser approved these changes May 27, 2024
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

This looks good to me, thanks! I'll ping @joelriou one more time in case they have any post-merge opinions, but I think any objections are probably worth a larger discussion + refactor anyway.

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels May 27, 2024
@eric-wieser
Copy link
Member

I don't understand Eric's comment yet but this all looks good to me.

The key thing is that we change the category-theoretic Hom to be a one-field wrapper for CoAlgebraHom, which means that you get the explicitly-typed coercion functions for free and can state lemmas more clearly with them.

mathlib-bors bot pushed a commit that referenced this pull request May 27, 2024
@eric-wieser
feat: category of coalgebras (#11972)
39dd4f3 
The category of coalgebras over a commutative ring. Mimics `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 27, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: category of coalgebras [Merged by Bors] - feat: category of coalgebras May 27, 2024
@mathlib-bors mathlib-bors bot closed this May 27, 2024
@mathlib-bors mathlib-bors bot deleted the coalgcat branch May 27, 2024 15:31
callesonne pushed a commit that referenced this pull request Jun 4, 2024
@eric-wieser @callesonne
feat: category of coalgebras (#11972)
db4dfba 
The category of coalgebras over a commutative ring. Mimics `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
js2357 pushed a commit that referenced this pull request Jun 18, 2024
@eric-wieser @js2357
feat: category of coalgebras (#11972)
0d59e5e 
The category of coalgebras over a commutative ring. Mimics `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kbuzzard kbuzzard kbuzzard left review comments

@github-actions github-actions[bot] github-actions left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@101damnations @leanprover-community-mathlib4-bot @eric-wieser @kbuzzard