ι_map_tensorHom_hom_eq_tensorHom

English

Compatibility of the Day convolution corepresentable image under the ι-map with tensoring on D.

Русский

Совместимость изображения Day конволюции после ι-подстановки с тензорной структурой на D.

LaTeX

$$$ (ι C V D).map (f \otimes_ m f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f') $$$

Lean4

theorem ι_map_tensorHom_hom_eq_tensorHom {d₁ d₂ : D} {d₁' d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂') :
    (ι C V D).map (f ⊗ₘ f') = DayConvolution.map (ι C V D |>.map f) (ι C V D |>.map f') :=
  by
  apply DayConvolution.corepresentableBy (ι C V D |>.obj d₁) (ι C V D |>.obj d₁') |>.homEquiv.injective
  dsimp
  ext ⟨x, y⟩
  simp only [externalProductBifunctor_obj_obj, Functor.comp_obj, tensor_obj,
    DayConvolution.corepresentableBy_homEquiv_apply_app, DayConvolution.unit_app_map_app]
  exact convolutionExtensionUnit_comp_ι_map_tensorHom_app C V _ _ _ _

Похожие утверждения