η — Mathlib · SciLib

English

The unit η exhibits tensorDesc as a left Kan extension of F functor ⊠ G functor

Русский

Единичный η устанавливает tensorDesc как левый канлевский расст F.functor ⊠ G.functor.

LaTeX

$$$ (\\eta F G) \\; \\circ \\; Functor.whiskerLeft _ (tensorDesc α).natTrans = α $$$

Lean4

/-- The unit transformation exhibiting `(F ⊗ G).functor` as a left Kan extension of
`F.functor ⊠ G.functor` along `tensor C`. -/
def η (F G : C ⊛⥤ V) : F.functor ⊠ G.functor ⟶ tensor C ⋙ (F ⊗ G).functor :=
  LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V F G

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