instIsLeftKanExtensionProdFunctorTensorObjη

English

Extensionality of Day convolution morphisms along tensor hom yields equality

Русский

Расширение Day конволютивных морфизмов по tensor hom даёт равенство.

LaTeX

$$$\\forall x,y, (\\eta F G)_{(x,y)} \\;\\cdot\\; α.natTrans.(x ⊗ y) = (\\eta F G)_{(x,y)} \\cdot β.natTrans.(x ⊗ y) \\Rightarrow α = β$$$

Lean4

instance (F G : C ⊛⥤ V) : (F ⊗ G).functor.IsLeftKanExtension (η F G) :=
  (isPointwiseLeftKanExtensionConvolutionExtensionUnit F G).isLeftKanExtension

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