English
Compatibility of the map ι with tensor operations in the Day convolution framework.
Русский
Совместимость отображения ι с тензор-операциями в рамках Day-конволюции.
LaTeX
$$$ (ι C V D).map (f \otimes_ m f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f') $$$
Lean4
theorem ι_map_rightUnitor_hom_eq_rightUnitor_hom (d : D)
[∀ (v : V) (d : C),
Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit.{0} <| 𝟙_ C) d) (tensorLeft v)] :
(ι C V D).map (ρ_ d).hom = (DayConvolutionUnit.rightUnitor (ι C V D |>.obj <| 𝟙_ D) (ι C V D |>.obj d)).hom :=
by
apply corepresentableByRight (ι C V D |>.obj <| 𝟙_ D) (ι C V D |>.obj d) |>.homEquiv.injective
dsimp
ext ⟨x, _⟩
dsimp [corepresentableByRight]
simp only [id_whiskerRight, Category.id_comp, DayConvolutionUnit.rightUnitor_hom_unit_app]
exact rightUnitor_hom_unit_app V d x
