commShiftIso_hom_app_counit_app_shift

English

The explicit expression for the inverse of the commShift iso is a long composition of unit, counit, and shifted functor maps, describing how the inverse acts on Y.

Русский

Явное выражение обратной стороны изоморфизма коммShift, задающее как действует обратный на Y через композицию единицы, активации и отображения сдвигов.

LaTeX

$$$ (\mathrm{iso}(\mathrm{adj}, a))^{-1}_{Y} = \text{(long composite of unit, counit and shifted maps)} $$$

Lean4

@[reassoc (attr := simp)]
theorem commShiftIso_hom_app_counit_app_shift [adj.CommShift A] (a : A) (Y : D) :
    ((G ⋙ F).commShiftIso a).hom.app Y ≫ (adj.counit.app Y)⟦a⟧' = adj.counit.app (Y⟦a⟧) := by
  simpa using (NatTrans.shift_app_comm adj.counit a Y)

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