ν_comp_unitDesc — Mathlib

English

Let F, G be functors and ν the Day convolution unit; then composing ν with the unit-desc construction yields the original morphism φ: 1_V ⟶ F ⊛ G at the unit object; i.e., the unit desc is a retraction for φ.

Русский

Пусть F, G — функторы, а ν — единичное преобразование Day convolution; тогда композиция ν с constructions of unit-desc возвращает исходное отображение φ: 1_V ⟶ F ⊛ G на единичном объекте; т. е. единично-описательный конструктор образует рекацию для φ.

LaTeX

$$$\\nu_{C,V} \\; \\circ \\; (\\text{unit } \\varphi)_{\\mathbb{1}_C} = \\varphi$$$

Lean4

@[reassoc (attr := simp)]
theorem ν_comp_unitDesc {F : C ⊛⥤ V} (φ : 𝟙_ V ⟶ F.functor.obj (𝟙_ C)) : ν C V ≫ (unitDesc φ).natTrans.app (𝟙_ C) = φ :=
  Functor.descOfIsLeftKanExtension_fac_app (𝟙_ (C ⊛⥤ V)).functor (νNatTrans C V) F.functor { app _ := φ } default

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