English
Let F ⊣ G be an adjunction between categories C and D, with A a abelian group indexing shifts, and assume G defines a commutation shift structure. For elements a, b ∈ A with a + b = 0, the hom-component of the canonical commutation isomorphism at an object X ∈ C is given by a specific composite of unit, shift-isomorphisms, and counit from the adjunction.
Русский
Пусть F ⊣ G является сопряжением между категориями C и D, причём A — абелева группа, индексирующая сдвиги, и предположено, что G задаёт структуру коммутирования сдвигов. Для элементов a, b ∈ A с a + b = 0 гом-компонента канонического изоморохизма совместимости по сдвигам в точке X ∈ C задаётся конкретной композицией единицы, изоморфизмов сдвига и контр-однозначения сопряжения.
LaTeX
$$$$(\mathrm{iso}\ adj\ a).\mathrm{hom}.X = F\big((\mathrm{adj}.\mathrm{unit}.X)\langle a \rangle'\big) \\circ \\ F\big(G\big( ((\mathrm{shiftFunctorCompIsoId}\ D\ a\ b\ h)^{-1}.\mathrm{app}(F\mathrm{obj}X)) \big)\big) \\circ \\ F\big(((\mathrm{G}.\mathrm{commShiftIso}\ b).\mathrm{hom}.app((F\mathrmobj X)\langle a \rangle'))\langle a \rangle'\big) \\circ \\ F\big(((\mathrm{shiftFunctorCompIsoId}\ C\ b\ a\ (by simp [eq_neg_of_add_eq_zero_left h])).\hom.app (\mathrm{G.obj}((F\mathrm.obj X)\langle a \rangle'))) \circ \\ adj.\mathrm{counit}.app ((F\mathrm obj X)\langle a \rangle)$$$$
Lean4
@[reassoc]
theorem iso_hom_app (X : C) :
(iso adj a).hom.app X =
F.map ((adj.unit.app X)⟦a⟧') ≫
F.map (G.map (((shiftFunctorCompIsoId D a b h).inv.app (F.obj X)))⟦a⟧') ≫
F.map (((G.commShiftIso b).hom.app ((F.obj X)⟦a⟧))⟦a⟧') ≫
F.map
((shiftFunctorCompIsoId C b a (by simp [eq_neg_of_add_eq_zero_left h])).hom.app
(G.obj ((F.obj X)⟦a⟧))) ≫
adj.counit.app ((F.obj X)⟦a⟧) :=
by
obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h
simp [iso, iso', shiftEquiv']
