unit_app_shift_commShiftIso_inv_app

English

The unit after shifting commutes with the shift isomorphism in the way prescribed by the commShiftIso_hom_app_counit_app_shift relation.

Русский

Единица после сдвига согласуется с изоморфизмами сдвига так, как предписано relation.

LaTeX

$$$ \text{unit}_X^{\text{shift}} = \text{shift-compatibility-map}$$$

Lean4

@[reassoc (attr := simp)]
theorem unit_app_shift_commShiftIso_inv_app [adj.CommShift A] (a : A) (X : C) :
    (adj.unit.app X)⟦a⟧' ≫ ((F ⋙ G).commShiftIso a).inv.app X = adj.unit.app (X⟦a⟧) := by
  simp [← cancel_mono (((F ⋙ G).commShiftIso _).hom.app _)]

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