shift_unit_app — Mathlib

English

Compatibility is preserved under addition of two compatible pairs of shifts and isomorphisms.

Русский

Совместимость сохраняется при суммировании двух совместимых пар сдвигов и изоморфизмов.

LaTeX

$$$ CompatUnit(adj, e_1, e_2) \rightarrow CompatUnit(adj, f_1, f_2) \rightarrow CompatUnit(adj, Functor.CommShift.isoAdd(e_1,f_1), Functor.CommShift.isoAdd(e_2,f_2))$$$

Lean4

@[reassoc]
theorem shift_unit_app [adj.CommShift A] (a : A) (X : C) :
    (adj.unit.app X)⟦a⟧' =
      adj.unit.app (X⟦a⟧) ≫ G.map ((F.commShiftIso a).hom.app X) ≫ (G.commShiftIso a).hom.app (F.obj X) :=
  by simpa [Functor.commShiftIso_comp_hom_app] using NatTrans.shift_app_comm adj.unit a X

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