[Merged by Bors] - feat(CategoryTheory/Monoidal/Closed): Prove the isomorphism of internal hom objects C(x \otimes y, z) and C(y, C(x, z)) by daniel-carranza · Pull Request #35436 · leanprover-community/mathlib4

daniel-carranza · 2026-02-17T09:20:53Z

Prove the currying-uncurrying isomorphism C(x \otimes y, z) \iso C(y, C(x, z)) between internal hom objects of a closed monoidal category C.

This result is connected to the infinity-cosmos project, and is used to prove that a closed monoidal category enriched in itself admits all cotensors.

~~Line 81 currently contains a one-line proof in tactics mode exact rfl. When trying to use rfl outside of tactics mode, an error is thrown~~ (Fixed, thank you @robin-carlier!). Any help with this (or any other aspect of the formalization) is greatly appreciated!

github-actions · 2026-02-17T09:21:06Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-02-17T09:22:07Z

PR summary 7bdf4031a0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying` (new file)	462

Declarations diff

+ ihomCurry
+ ihomCurryIso
+ ihomCurry_ihomUncurry
+ ihomUncurry
+ ihomUncurry_ihomCurry
+ uncurry_ihomCurry
+ uncurry_ihomUncurry
+ uncurry_uncurry_ihomCurry

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

github-actions · 2026-02-17T09:22:20Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

robin-carlier · 2026-02-20T09:48:20Z

Can you please add a TODO to show the naturality properties in each variable of the morphisms you define here?

I tried looking into it, and it opens a bit of a can of worms that we have missing instances for closed objects in the opposite category. So we can’t readily talk about things like pre (f.op) which would be necessary to state naturality properties. This might be outside of the scope of this PR, but eventually Mathlib will want these kind of things.

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

daniel-carranza · 2026-02-20T11:41:32Z

Can you please add a TODO to show the naturality properties in each variable of the morphisms you define here?

I tried looking into it, and it opens a bit of a can of worms that we have missing instances for closed objects in the opposite category. So we can’t readily talk about things like pre (f.op) which would be necessary to state naturality properties. This might be outside of the scope of this PR, but eventually Mathlib will want these kind of things.

ihomCurry and ihomUncurry now have comments above them describing the TODO mentioned here. Does this seem correct?

dagurtomas

Thanks!

maintainer merge

github-actions · 2026-02-26T20:31:21Z

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

riccardobrasca · 2026-02-26T22:13:03Z

Thanks!

bors d+

mathlib-bors · 2026-02-26T22:13:05Z

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

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

daniel-carranza · 2026-03-06T18:53:33Z

bors r+

…al hom objects C(x \otimes y, z) and C(y, C(x, z)) (#35436) Prove the currying-uncurrying isomorphism `C(x \otimes y, z) \iso C(y, C(x, z))` between internal hom objects of a closed monoidal category `C`. Co-authored-by: daniel-carranza <carranzajdaniel@gmail.com>

mathlib-bors · 2026-03-06T18:55:27Z

Build failed:

ci (staging) / Post-Build Step

dagurtomas · 2026-05-07T04:26:51Z

bors retry

adomani · 2026-05-07T04:32:39Z

Thanks!

bors merge

bryangingechen · 2026-05-07T04:53:21Z

bors r+

bryangingechen · 2026-05-07T04:55:05Z

bors r+

bryangingechen · 2026-05-07T05:01:35Z

bors r+

mathlib-bors · 2026-05-07T06:13:19Z

Already running a review

mathlib-bors · 2026-05-07T06:19:51Z

Already running a review

…al hom objects C(x \otimes y, z) and C(y, C(x, z)) (#35436) Prove the currying-uncurrying isomorphism `C(x \otimes y, z) \iso C(y, C(x, z))` between internal hom objects of a closed monoidal category `C`. Co-authored-by: daniel-carranza <carranzajdaniel@gmail.com> Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

mathlib-bors · 2026-05-07T06:46:07Z

Pull request successfully merged into master.

Build succeeded:

mathlib-bors · 2026-05-07T06:53:25Z

Already running a review

mathlib-bors · 2026-05-07T06:59:14Z

Already running a review

…al hom objects C(x \otimes y, z) and C(y, C(x, z)) (leanprover-community#35436) Prove the currying-uncurrying isomorphism `C(x \otimes y, z) \iso C(y, C(x, z))` between internal hom objects of a closed monoidal category `C`. Co-authored-by: daniel-carranza <carranzajdaniel@gmail.com> Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

daniel-carranza added 3 commits February 16, 2026 18:29

added file header, changed V to C

67b60aa

corrected typo in docstrings

060c260

added InternalCurrying file to Mathlib.lean

8b8c608

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Feb 17, 2026

github-actions Bot added the t-category-theory Category theory label Feb 17, 2026

daniel-carranza changed the title ~~feat<CategoryTheory/Monoidal/Closed>: Prove the isomorphism of internal hom objects C(x \otimes y, z) and C(y, C(x, z)).~~ feat(CategoryTheory/Monoidal/Closed): Prove the isomorphism of internal hom objects C(x \otimes y, z) and C(y, C(x, z)). Feb 17, 2026

daniel-carranza changed the title ~~feat(CategoryTheory/Monoidal/Closed): Prove the isomorphism of internal hom objects C(x \otimes y, z) and C(y, C(x, z)).~~ feat(CategoryTheory/Monoidal/Closed): Prove the isomorphism of internal hom objects C(x \otimes y, z) and C(y, C(x, z)) Feb 17, 2026

daniel-carranza requested a review from emilyriehl February 17, 2026 09:29

daniel-carranza added the infinity-cosmos This PR is associated with Infinity Cosmos project label Feb 17, 2026

daniel-carranza mentioned this pull request Feb 17, 2026

feat(CategoryTheory/Enriched/Limits): define cotensors in an enriched category #35411

Open

2 tasks

robin-carlier reviewed Feb 17, 2026

View reviewed changes

Comment thread Mathlib/CategoryTheory/Monoidal/Closed/InternalCurrying.lean Outdated

daniel-carranza added 2 commits February 19, 2026 11:41

added @[expose] at start of section; added @[simps] to the isomorphism

b0d59a0

added additional "end"

5f0b942

joelriou reviewed Feb 20, 2026

View reviewed changes

Comment thread Mathlib/CategoryTheory/Monoidal/Closed/InternalCurrying.lean Outdated

joelriou reviewed Feb 20, 2026

View reviewed changes

Comment thread Mathlib/CategoryTheory/Monoidal/Closed/InternalCurrying.lean Outdated

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 20, 2026

added reassoc and simp to uncurry_curry and curry_uncurry lemmas

fb7225b

daniel-carranza and others added 4 commits February 20, 2026 12:25

Update Mathlib/CategoryTheory/Monoidal/Closed/InternalCurrying.lean

c732b49

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Update Mathlib/CategoryTheory/Monoidal/Closed/InternalCurrying.lean

f74aab5

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

renaming + added TODO comment to show naturality

24f55f8

trying to resolve merge conflicts

041cf6a

daniel-carranza removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 20, 2026

joelriou reviewed Feb 20, 2026

View reviewed changes

Comment thread Mathlib/CategoryTheory/Monoidal/Closed/InternalCurrying.lean Outdated

mathlib-triage Bot assigned adamtopaz Feb 24, 2026

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 24, 2026

daniel-carranza removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 25, 2026

dagurtomas reviewed Feb 26, 2026

View reviewed changes

Comment thread Mathlib/CategoryTheory/Monoidal/Closed/InternalCurrying.lean Outdated

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 26, 2026

mathlib-triage Bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 26, 2026

Update Mathlib/CategoryTheory/Monoidal/Closed/InternalCurrying.lean

ee7b613

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

dagurtomas added 2 commits May 6, 2026 21:59

Merge branch 'master' into internal-currying-isomorphism

7420d6c

fix the build

e556b82

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 7, 2026

mathlib-bors Bot closed this May 7, 2026

Conversation

daniel-carranza commented Feb 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Feb 17, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Feb 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 7bdf4031a0

Import changes for modified files

Declarations diff

Uh oh!

github-actions Bot commented Feb 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

Uh oh!

Uh oh!

Uh oh!

robin-carlier commented Feb 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

daniel-carranza commented Feb 20, 2026

Uh oh!

Uh oh!

dagurtomas left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions Bot commented Feb 26, 2026

Uh oh!

riccardobrasca commented Feb 26, 2026

Uh oh!

mathlib-bors Bot commented Feb 26, 2026

Uh oh!

daniel-carranza commented Mar 6, 2026

Uh oh!

mathlib-bors Bot commented Mar 6, 2026

Uh oh!

dagurtomas commented May 7, 2026

Uh oh!

adomani commented May 7, 2026

Uh oh!

bryangingechen commented May 7, 2026

Uh oh!

bryangingechen commented May 7, 2026

Uh oh!

bryangingechen commented May 7, 2026

Uh oh!

mathlib-bors Bot commented May 7, 2026

Uh oh!

mathlib-bors Bot commented May 7, 2026

Uh oh!

mathlib-bors Bot commented May 7, 2026

Uh oh!

mathlib-bors Bot commented May 7, 2026

Uh oh!

mathlib-bors Bot commented May 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

daniel-carranza commented Feb 17, 2026 •

edited

Loading

github-actions Bot commented Feb 17, 2026 •

edited

Loading

github-actions Bot commented Feb 17, 2026 •

edited

Loading

robin-carlier commented Feb 20, 2026 •

edited

Loading