tensorDesc — Mathlib

English

The universal map ι composed with the inverse isomorphism recovers the unit η

Русский

Обобщённая стрелка ι, композиция с обратным изоморфизмом восстанавливает η.

LaTeX

$$$\\iota_{(x,y)} \\;\\circ \\; (\\mathrm{isoPointwiseLeftKanExtension})_{(x ⊗ y)}^{-1} = (\\eta F G)_{(x,y)}$$$

Lean4

/-- A natural transformation `F.functor ⊠ G.functor ⟶ tensor C ⋙ H.functor`
defines a morphism `F ⨂ G ⟶ H`. -/
def tensorDesc {F G H : C ⊛⥤ V} (α : F.functor ⊠ G.functor ⟶ tensor C ⋙ H.functor) : F ⊗ G ⟶ H :=
  .mk <| (F ⊗ G).functor.descOfIsLeftKanExtension (η F G) H.functor α

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