Commit 2025-07-05 12:52 f956f067

feat(CategoryTheory/Monoidal/DayConvolution): Associators and pentagon for Day Convolution (#25756) Under some assumptions on the tensor product of a monoidal category V, we show that if three functors F, G, H are such that the relevant Day convolutions exist, then there is an associator isomorphism for day convolution. We characterize this isomorphism, and show it is natural. When all relevant Day convolutions exist, we show that the pentagon identity holds for these associators.