η_comp_tensorDesc_app — Mathlib

English

The morphism ν is the unit for the Day convolution functor, giving the unit of the Day convolution monoidal structure.

Русский

Морфизм ν является единицей Day конволюции, образуя единицу моноидальной структуры Day конволюции.

LaTeX

$$$\\nu : \\mathbf{1}_V \\to (\\mathbf{1}_{C ⊛⥤ V}).functor.obj (\\mathbf{1}_C)$$$

Lean4

@[reassoc (attr := simp)]
theorem η_comp_tensorDesc_app {F G H : C ⊛⥤ V} (α : F.functor ⊠ G.functor ⟶ tensor C ⋙ H.functor) (x y : C) :
    (η F G).app (x, y) ≫ (tensorDesc α).natTrans.app (x ⊗ y) = α.app (x, y) :=
  Functor.descOfIsLeftKanExtension_fac_app _ _ _ _ _

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