Closed Monoidal cats are self-enriched

Stream: Infinity-Cosmos

[Daniel Carranza]

Hello everyone! I'm writing a message to let folks know of a PR to mathlib4 with a proof that a closed monoidal category is enriched in itself: https://github.com/leanprover-community/mathlib4/pull/17326

A question for this channel ( specifically @Jack McKoen ): as I understand, there is already an instance of SSet as a simplicial category coming from the fact that it's a category of simplicial objects. Is there a chance for errors if a file imports both instances? (tagging @Emily Riehl as the one who originally noticed this)

[Jack McKoen]

I think technically both instances are the same: the monoidal closed instance on SSet comes from docs#CategoryTheory.Functor.functorHom (this is the ihom), and my enriched instance in this case also comes from functorHom. You use the ihom directly in your enriched instance, so in the case of simplicial sets it will be functorHom anyway.

I still think Lean would get confused though (?), so it's probably best to do as Joel suggests here-- https://github.com/leanprover-community/mathlib4/pull/17326#issuecomment-2386533838

[Bhavik Mehta]

Hmm, does this mean that Daniel's new construction generalises the existing one? If so, a better solution - to me - seems to be to refactor the old one to use the new one. But I haven't checked the old one, so I'm not certain

[Jack McKoen]

It's not a generalisation, see: https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Functor/FunctorHom.html#CategoryTheory.Enriched.Functor.instEnrichedCategoryFunctorType

[Jack McKoen]

This says general functor categories are enriched over certain functors to type

[Daniel Carranza]

There's a pair of rewrites rw [← uncurry_eq, uncurry_curry] that appears in all 3 proofs in the file. @Bhavik Mehta correctly pointed out that the rewrite I really want is
(A ◁ curry g) ≫ (ihom.ev A).app X = g
I experimented (locally on my machine) with making this a separate lemma 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? (tagging @Emily Riehl , the one who suggested this simplification)

[Emily Riehl]

This lemma is effectively a second proof that
uncurry_curry : uncurry (curry g) = g
but with uncurry unfolded to its definition. Note
uncurry_eq : uncurry (h) = (A ◁ h) ≫ (ihom.ev A).app X

[Emily Riehl]

Here uncurry_curry is tagged with simp but uncurry_eq is not in the Closed/Monoidal file.