English
Abbreviation constructing a monoidal category structure on D using Day convolution data and a fully faithful functor.
Русский
Сокращение построения моноидальной категории на D с использованием Day-конволюции и полностью сохраняющего фуктора.
LaTeX
$$$ \text{mkMonoidalCategoryStruct }(C,V,D) : \text{MonoidalCategoryStruct } D $$$
Lean4
theorem ι_map_leftUnitor_hom_eq_leftUnitor_hom (d : D)
[∀ (v : V) (d : C),
Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit.{0} <| 𝟙_ C) d) (tensorRight v)] :
(ι C V D).map (λ_ d).hom = (DayConvolutionUnit.leftUnitor (ι C V D |>.obj <| 𝟙_ D) (ι C V D |>.obj d)).hom :=
by
apply corepresentableByLeft (ι C V D |>.obj <| 𝟙_ D) (ι C V D |>.obj d) |>.homEquiv.injective
dsimp
ext ⟨_, x⟩
dsimp [corepresentableByLeft]
simp only [whiskerLeft_id, Category.comp_id, DayConvolutionUnit.leftUnitor_hom_unit_app]
exact leftUnitor_hom_unit_app V d x
