unit_app_commShiftIso_hom_app — Mathlib

English

The isoZero isomorphisms are compatible with the unit in adjunctions.

Русский

Изоморфизмы isoZero совместимы с единицей в сопряжении.

LaTeX

$$$ CompatUnit(adj, \mathrm{isoZero}F A, \mathrm{isoZero}G A)$$$

Lean4

@[reassoc (attr := simp)]
theorem unit_app_commShiftIso_hom_app [adj.CommShift A] (a : A) (X : C) :
    adj.unit.app (X⟦a⟧) ≫ ((F ⋙ G).commShiftIso a).hom.app X = (adj.unit.app X)⟦a⟧' := by
  simpa using (NatTrans.shift_app_comm adj.unit a X).symm

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