[Merged by Bors] - feat(CategoryTheory/Enriched): functoriality of the enrichment of functor categories#18414
[Merged by Bors] - feat(CategoryTheory/Enriched): functoriality of the enrichment of functor categories#18414
Conversation
…to enriched-category-functor-category
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…to category-limits-shapes-end
… enriched-category-functor-category
… enriched-category-functor-category
…category-functoriality
…category-functoriality
|
@joelriou do you think the |
As the internals of some terms are |
|
Thanks! maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by dagurtomas. |
| dsimp | ||
| ext j | ||
| rw [end_.lift_π, assoc] | ||
| erw [end_.lift_π, end_.lift_π] |
There was a problem hiding this comment.
Almost all of these new erws involve end_.lift_π, and it looks like those are all applied to precompEnrichedHom composed with end_.π or enrichedHomπ. Would it work to make a lemma for those two cases, so we can use rw instead of erw?
There was a problem hiding this comment.
This didn't work, Joël had a lemma precompEnrichedHom_π for the case enrichedHomπ, and I tried the other case, and erw was still required.
|
Thanks 🎉 bors merge |
…ctor categories (#18414) Let `C` be a `V`-enriched ordinary category. Functor categories `J ⥤ C` have been `V`-enriched in #18009. Given two functors `F₁` and `F₂` in `J ⥤ C`, we use the previous results for functors `Under j ⥤ C` for all `j : J` in order to construct `functorEnrichedHom V F₁ F₂ : J ⥤ V`, and show that the limit of this functor identifies to `enrichedHom V F₁ F₂`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
Let
Cbe aV-enriched ordinary category. Functor categoriesJ ⥤ Chave beenV-enriched in #18009. Given two functorsF₁andF₂inJ ⥤ C, we use the previous results for functorsUnder j ⥤ Cfor allj : Jin order to constructfunctorEnrichedHom V F₁ F₂ : J ⥤ V, and show that the limit of this functor identifies toenrichedHom V F₁ F₂.