ι_map_associator_hom_eq_associator_hom

English

A Lawful structure on the Day convolution gives a monoidal category on D via an induced construction.

Русский

Законная структура Day-конволюции задаёт моноидальную категорию на D через индуцированную конструкцию.

LaTeX

$$$ \text{lawful}_{C,V,D} \Rightarrow \text{MonoidalCategory } D $$$

Lean4

theorem ι_map_associator_hom_eq_associator_hom (d d' d'')
    [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)]
    [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] :
    (ι C V D).map (α_ d d' d'').hom =
      (DayConvolution.associator (ι C V D |>.obj d) (ι C V D |>.obj d') (ι C V D |>.obj d'')).hom :=
  by
  apply corepresentableBy₂' (ι C V D |>.obj d) (ι C V D |>.obj d') (ι C V D |>.obj d'') |>.homEquiv.injective
  dsimp
  ext ⟨⟨x, y⟩, z⟩
  simp only [externalProductBifunctor_obj_obj, Functor.comp_obj, Functor.prod_obj, tensor_obj, Functor.id_obj,
    Functor.homEquivOfIsLeftKanExtension_apply_app, externalProductBifunctor_map_app, Functor.leftUnitor_inv_app,
    whiskerLeft_id, Category.comp_id, corepresentableBy_homEquiv_apply_app, DayConvolution.associator_hom_unit_unit]
  exact associator_hom_unit_unit V _ _ _ _ _ _

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