[Merged by Bors] - feat(CategoryTheory/Closed/Enrichment): a closed monoidal category is enriched in itself #17326
Conversation
github-actions
bot
added
the
new-contributor
PR summary ee837dfadeImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
There was a problem hiding this comment.
This is in pretty good shape already for a first contribution! I've left a couple of style comments.
Note that the title of your PR shouldn't be capitalised, see https://leanprover-community.github.io/contribute/commit.html
| rw [uncurry_curry, uncurry_curry]; dsimp | ||
| rw [associator_inv_naturality_middle_assoc] | ||
| rw [← comp_whiskerRight_assoc] | ||
| rw [← uncurry_eq, uncurry_curry] |
There was a problem hiding this comment.
Hmm, I notice you use this particular pair of rewrites pretty often, and I'm guessing it does something like
(A ◁ curry g) ≫ (ihom.ev A).app X = g
Is there a reason the left-hand-side of this is appearing so often? I somewhat expect there's a cleaner way of going about this proof, although I can't be sure
There was a problem hiding this comment.
Indeed, this pair of rewrites is exactly that equality. The current proof is the best I could come up with in terms of cleaning on my end, but my hope is also that there should be a cleaner proof!
There was a problem hiding this comment.
I experimented (locally on my machine) with making this a separate lemma inside the CategoryTheory/Closed/Monoidal.lean file with the simp attribute. The proof now goes through using a single simp wherever these two rewrites originally occurred. Is this a good candidate simp lemma to be added to the CategoryTheory/Closed/Monoidal file? (Posted on Zulip as well)
daniel-carranza
changed the title
|
I think the dual instance could cause issues, but I don't know enough about the context of this to know what the correct solution is. I'd guess we'd like to only have one of them actually active on SSet, prove that they're the same or make the constructions so they're definitionally the same. But I don't know the maths here well enough to be sure (are they even the same, informally?). Asking on the zulip is definitely the correct thing to do. |
|
About the dual instance issue, I would suggest making the new instance in this PR a local or a scoped instance. |
This is to try and prevent errors when V has an alternative instance of being enriched over itself (e.g. when V = SSet)
|
I've implemented Joel's suggestion in the current version, but I created a Zulip chat to discuss this PR in the Infinity-Cosmos channel |
joelriou
added
the
awaiting-author
|
Most of the definitions and compatibilities in this PR could be phrased under the slightly weaker condition that only a few |
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
|
After the kind of style suggestions are taken care of, I think this PR shall be ready. |
joelriou
added
the
awaiting-author
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Thank you! |
daniel-carranza
removed
the
awaiting-author
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Thanks! bors merge |
… enriched in itself (#17326) From a monoidal closed category V, construct an instance of `EnrichedCategory V` on V where the hom-objects are given by the internal homs of the closed structure. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> Co-authored-by: daniel-carranza <carranzajdaniel@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Let `C` be a category that is enriched over a monoidal category `V` in such a way that the category structure and the enriched category structure are compatible. Then, if `J` is a category and that `V` has certain limits, then the functor category `J ⥤ C` is also enriched over `V`. (Plan: using #17326, we may use this for `C := C` closed monoidal in order to show that a category of functors `J ⥤ C` to a monoidal category is enriched over `C`, and, by applying this to all `Under X` categories for `X : C`, it should follow that `J ⥤ C` is also closed monoidal. This should give a more explicit approach as compared to #16067.) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Let `C` be a category that is enriched over a monoidal category `V` in such a way that the category structure and the enriched category structure are compatible. Then, if `J` is a category and that `V` has certain limits, then the functor category `J ⥤ C` is also enriched over `V`. (Plan: using #17326, we may use this for `C := C` closed monoidal in order to show that a category of functors `J ⥤ C` to a monoidal category is enriched over `C`, and, by applying this to all `Under X` categories for `X : C`, it should follow that `J ⥤ C` is also closed monoidal. This should give a more explicit approach as compared to #16067.) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
From a monoidal closed category V, construct an instance of
EnrichedCategory Von V where the hom-objects are given by the internal homs of the closed structure.First time contributor. I am still new to formalization, so I am open any and all suggestions! In particular, the proofs here are a bit long compared to most proofs I see in the library, and I'm not sure if it's couth to use the
@[simp]attribute for some equalities here.Remark: As I understand, the type of simplicial sets
SSet.{v}also has an instance ofEnrichedCategory SSet.{v}constructed inAlgebraicTopology/SimplicialCategory/SimplicialObject. This enrichment comes from viewingSSet.{v}as a category of simplicial objects, rather than as a closed monoidal category. I'm still a beginner, but could this cause any issues if a file imports both instances?