[Merged by Bors] - feat(category_theory/enriched): abstract enriched categories

[semorrison]

Enriched categories

We set up the basic theory of V-enriched categories,
for V an arbitrary monoidal category.

We do not assume here that V is a concrete category,
so there does not need to be a "honest" underlying category!

Use X ⟶[V] Y to obtain the V object of morphisms from X to Y.

This file contains the definitions of V-enriched categories and
V-functors.

We don't yet define the V-object of natural transformations
between a pair of V-functors (this requires limits in V),
but we do provide a presheaf isomorphic to the Yoneda embedding of this object.

We verify that when V = Type v, all these notion reduce to the usual ones.

---

Note that this is not an attempt to make enriched categories that "stack" with existing categories, and interact well with existing algebraic structures, etc. It's just the abstract theory. Hopefully we'll be able to work out a different enriched_over typeclass that is a mixin for category, and from which an "abstract" enriched category can be extracted.

• depends on: [Merged by Bors] - feat(category_theory/monoidal): Drinfeld center #7186

[b-mehta]

I'm a little confused about why we can't do enriched natural transformations: It seems to me that the definition here works in Lean...

structure enriched_nat_trans (F G : enriched_functor V C D) :=
(app : Π (X : C), 𝟙_ V ⟶ (F.obj X ⟶[V] G.obj X))
(naturality' : ∀ (X Y : C), (λ_ _).inv ≫ (app _ ⊗ G.map X Y) ≫ e_comp V _ _ _ = (ρ_ _).inv ≫ (F.map X Y ⊗ app _) ≫ e_comp V _ _ _)

[b-mehta]

Ah, unless you're saying that we can't make the morphisms in the V-enriched functor category without ends

[semorrison]

Yes, the definition on ncatlab is what I've called a graded_nat_trans (𝟙_ V). I guess I was distracted by the fact that in places IRL I've used enriched categories, I needed to either care about other gradings, or the V-object of natural transformations.

The (𝟙_ V) graded natural transformations probably deserve their own definition -- this can be done without assuming a grading, but then it can't be done as a specialisation of the general case. Not sure what to do there. I guess the general case could be done for any A : V with a lift to the center...

[b-mehta]

Yes, the definition on ncatlab is what I've called a graded_nat_trans (𝟙_ V). I guess I was distracted by the fact that in places IRL I've used enriched categories, I needed to either care about other gradings, or the V-object of natural transformations.

The (𝟙_ V) graded natural transformations probably deserve their own definition -- this can be done without assuming a grading, but then it can't be done as a specialisation of the general case. Not sure what to do there. I guess the general case could be done for any A : V with a lift to the center...

From my understanding what you called the "graded_nat_trans" is referred to as the enriched natural transformations - which may not be the most helpful in general but still allows us to form the non-enriched category of enriched functors. And as you say the V-object is usually more helpful but we can't do it yet - does there need to be an explicit specialisation?

[semorrison]

I think the discrepancy is that my graded_nat_trans is slightly more general than "enriched natural transformation" on n-lab. graded_nat_trans is parametrised by an object A, and an "enriched natural transformation" is the case A := 𝟙_ V.

Unfortunately the general case away from 𝟙_ V can't be stated without the category being braided (or A lifting to the center), and this where I was sad about not being able to easily say the specialisation.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(category_theory/monoidal): Drinfeld center #7186

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[adamtopaz]

A couple of minor comments/questions, but otherwise LGTM!

[b-mehta]

Thanks!

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests