unitDesc — Mathlib

English

Definition of ν as a unit object for DayFunctor convolution

Русский

Определение ν как единицы для конволюции DayFunctor.

LaTeX

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

Lean4

/-- Given `F : C ⊛⥤ V`, a morphism `𝟙_ V ⟶ F.functor.obj (𝟙_ C)` induces a
(unique) morphism `𝟙_ (C ⊛⥤ V) ⟶ F`. -/
def unitDesc {F : C ⊛⥤ V} (φ : 𝟙_ V ⟶ F.functor.obj (𝟙_ C)) : 𝟙_ (C ⊛⥤ V) ⟶ F :=
  .mk <| Functor.descOfIsLeftKanExtension (𝟙_ (C ⊛⥤ V)).functor (νNatTrans C V) F.functor { app _ := φ }

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