leftUnitor_naturality — Mathlib

English

Characterization of the forward direction of left unitor via universal maps in Day convolution.

Русский

Характеризация направления, соответствующего левому унитору, через единообразные отображения Day-конволюции.

LaTeX

$$$ (\text{leftUnitor_hom_unit_app}) :\; \text{can} \; \text{▷} \; F(_y) \; \to \text{ DayConvolution.unit }.\text{(id, y)} \to (\text{leftUnitor}(F(y))).\text{hom} $$$

Lean4

@[reassoc (attr := simp)]
theorem leftUnitor_naturality {G : C ⥤ V} [DayConvolution U G] (f : F ⟶ G) :
    DayConvolution.map (𝟙 _) f ≫ (leftUnitor U G).hom = (leftUnitor U F).hom ≫ f :=
  by
  apply Functor.hom_ext_of_isLeftKanExtension _ (DayConvolution.unit _ _) _
  apply Functor.hom_ext_of_isLeftKanExtension _ (extensionUnitLeft U (φ U) F) _
  ext
  simp [← whisker_exchange_assoc]

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