[Merged by Bors] - feat(category_theory/monad/kleisli): add Kleisli category of a monad #4542

b-mehta · 2020-10-08T19:15:02Z

Adds the Kleisli category of a monad, and shows the Kleisli category for a lawful control monad is equivalent to the Kleisli category of its category-theoretic version.

Following discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/kleisli.20vs.20kleisli.

I'd appreciate suggestions for names more sensible than the ones already there.

Coauthored by @Vtec234

jcommelin

LGTM

@semorrison Would you please also take a look?

src/category_theory/monad/types.lean

jcommelin

Sorry, I've been quite busy. I should have given these name suggestions earlier.
If you fix them, feel free to merge afterwards.

bors d+

jcommelin · 2020-10-15T14:53:40Z

src/category_theory/monad/kleisli.lean

+namespace adjunction
+
+/-- The left adjoint of the adjunction which induces the monad `T`. -/
+@[simps] def F_T : C ⥤ kleisli T :=


Suggested change

@[simps] def F_T : C ⥤ kleisli T :=

@[simps] def to_kleisli : C ⥤ kleisli T :=

alternatively maybe free?

alternatively, maybe free?

jcommelin · 2020-10-15T14:53:57Z

src/category_theory/monad/kleisli.lean

+  end }
+
+/-- The right adjoint of the adjunction which induces the monad `T`. -/
+@[simps] def U_T : kleisli T ⥤ C :=


Suggested change

@[simps] def U_T : kleisli T ⥤ C :=

@[simps] def from_kleisli : kleisli T ⥤ C :=

and here underlying or forget?

bors · 2020-10-15T14:54:37Z

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

adamtopaz · 2020-10-15T15:20:20Z

src/category_theory/monad/types.lean

+    begin
+      unfold_projs,
+      ext,
+      dsimp,


I think this dsimp can be removed.

adamtopaz · 2020-10-15T15:23:14Z

I also think using the names free / forget would be a better choice. E.g. this would provide consistency with the names for the Eilenberg-Moore category of a monad.

b-mehta · 2020-10-15T16:01:22Z

I don't like the free/forget choice here, since the Kleisli category isn't really adding structure like the EM category, and the forgetful functor is actually applying a function on objects - in particular I think the consistency is misleading rather than helpful. I'll use to_kleisli and from_kleisli instead.

adamtopaz · 2020-10-15T16:12:22Z

I don't like the free/forget choice here, since the Kleisli category isn't really adding structure like the EM category, and the forgetful functor is actually applying a function on objects - in particular I think the consistency is misleading rather than helpful. I'll use to_kleisli and from_kleisli instead.

I should say that I don't really have any strong opinions regarding the names. I just tend to think of the Kleisli category as related to the free objects in the Eilenberg-Moore category (via the comparison functor).

semorrison · 2020-10-15T23:03:54Z

Yes, modulo the renaming, LGTM.

b-mehta · 2020-10-16T16:23:58Z

Thanks for the suggestions all!

b-mehta · 2020-10-16T16:24:04Z

bors r+

bors · 2020-10-16T16:24:05Z

Already running a review

bryangingechen · 2020-10-16T16:28:11Z

Hmm, weird error message from bors. This wasn't on the queue yet, so:
bors r+

…4542) Adds the Kleisli category of a monad, and shows the Kleisli category for a lawful control monad is equivalent to the Kleisli category of its category-theoretic version. Following discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/kleisli.20vs.20kleisli. I'd appreciate suggestions for names more sensible than the ones already there.

b-mehta · 2020-10-16T16:44:45Z

Might be because I accidentally closed and reopened? Thanks for sorting it!

bryangingechen · 2020-10-16T16:49:46Z

No problem! Yeah, I would have expected bors to say something like "Cannot merge a closed PR" instead of "Already running a review"...

bors · 2020-10-16T17:16:37Z

Pull request successfully merged into master.

Build succeeded:

kleisli

9318dbe

b-mehta requested review from cipher1024 and semorrison October 8, 2020 19:15

b-mehta added awaiting-review The author would like community review of the PR needs-documentation This PR is missing required documentation labels Oct 8, 2020

docs

57f09ac

b-mehta force-pushed the kleisli branch from cfcf2e2 to 57f09ac Compare October 11, 2020 18:23

b-mehta removed the needs-documentation This PR is missing required documentation label Oct 11, 2020

jcommelin reviewed Oct 13, 2020

View reviewed changes

src/category_theory/monad/types.lean Show resolved Hide resolved

src/category_theory/monad/types.lean Outdated Show resolved Hide resolved

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 13, 2020

review suggestions

8d3ea96

b-mehta removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 13, 2020

jcommelin reviewed Oct 15, 2020

View reviewed changes

jcommelin requested a review from adamtopaz October 15, 2020 14:56

adamtopaz reviewed Oct 15, 2020

View reviewed changes

src/category_theory/monad/types.lean Outdated

begin

unfold_projs,

ext,

dsimp,

Copy link

Collaborator

adamtopaz Oct 15, 2020

Choose a reason for hiding this comment

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

I think this dsimp can be removed.

semorrison 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 Oct 15, 2020

review suggestions

7454dc7

b-mehta closed this Oct 16, 2020

b-mehta reopened this Oct 16, 2020

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Oct 16, 2020

bryangingechen mentioned this pull request Oct 16, 2020

confusing error message when approving a closed PR bors-ng/bors-ng#1058

Open

bors bot changed the title ~~feat(category_theory/monad/kleisli): add Kleisli category of a monad~~ [Merged by Bors] - feat(category_theory/monad/kleisli): add Kleisli category of a monad Oct 16, 2020

bors bot closed this Oct 16, 2020

bors bot deleted the kleisli branch October 16, 2020 17:16

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(category_theory/monad/kleisli): add Kleisli category of a monad #4542

[Merged by Bors] - feat(category_theory/monad/kleisli): add Kleisli category of a monad #4542

b-mehta commented Oct 8, 2020 •

edited

jcommelin left a comment

jcommelin left a comment

jcommelin Oct 15, 2020

jcommelin Oct 15, 2020

jcommelin Oct 15, 2020

jcommelin Oct 15, 2020

jcommelin Oct 15, 2020

bors bot commented Oct 15, 2020

adamtopaz Oct 15, 2020

adamtopaz commented Oct 15, 2020

b-mehta commented Oct 15, 2020

adamtopaz commented Oct 15, 2020

semorrison commented Oct 15, 2020

b-mehta commented Oct 16, 2020

b-mehta commented Oct 16, 2020

bors bot commented Oct 16, 2020

bryangingechen commented Oct 16, 2020

b-mehta commented Oct 16, 2020

bryangingechen commented Oct 16, 2020

bors bot commented Oct 16, 2020

	@[simps] def F_T : C ⥤ kleisli T :=
	@[simps] def to_kleisli : C ⥤ kleisli T :=

	@[simps] def U_T : kleisli T ⥤ C :=
	@[simps] def from_kleisli : kleisli T ⥤ C :=

[Merged by Bors] - feat(category_theory/monad/kleisli): add Kleisli category of a monad #4542

[Merged by Bors] - feat(category_theory/monad/kleisli): add Kleisli category of a monad #4542

Conversation

b-mehta commented Oct 8, 2020 • edited

jcommelin left a comment

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

jcommelin Oct 15, 2020

Choose a reason for hiding this comment

jcommelin Oct 15, 2020

Choose a reason for hiding this comment

jcommelin Oct 15, 2020

Choose a reason for hiding this comment

jcommelin Oct 15, 2020

Choose a reason for hiding this comment

jcommelin Oct 15, 2020

Choose a reason for hiding this comment

bors bot commented Oct 15, 2020

adamtopaz Oct 15, 2020

Choose a reason for hiding this comment

adamtopaz commented Oct 15, 2020

b-mehta commented Oct 15, 2020

adamtopaz commented Oct 15, 2020

semorrison commented Oct 15, 2020

b-mehta commented Oct 16, 2020

b-mehta commented Oct 16, 2020

bors bot commented Oct 16, 2020

bryangingechen commented Oct 16, 2020

b-mehta commented Oct 16, 2020

bryangingechen commented Oct 16, 2020

bors bot commented Oct 16, 2020

b-mehta commented Oct 8, 2020 •

edited