η_comp_tensorDec — Mathlib

English

Alternate expression for the η-component with isoPointwiseLeftKanExtension

Русский

Альтернативное выражение компоненты η через isoPointwiseLeftKanExtension.

LaTeX

$$$ (\\eta F G)_{(x,y)} \\;\\circ \\; (\\mathrm{isoPointwiseLeftKanExtension} F G).hom.app (x ⊗ y) = \\text{colimit injection}$$$

Lean4

theorem η_comp_tensorDec {F G H : C ⊛⥤ V} (α : F.functor ⊠ G.functor ⟶ tensor C ⋙ H.functor) :
    η F G ≫ Functor.whiskerLeft _ (tensorDesc α).natTrans = α :=
  Functor.descOfIsLeftKanExtension_fac _ _ _ _

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