id — Mathlib · SciLib

English

The inverse component of the commShiftIso for the composition F ⋙ G is given by the inverse components of G and a mapped inverse of F's commShiftIso.

Русский

Обратная компонента commShiftIso для композиции F ⋙ G задаётся через обратные компоненты G и отображённую через F коммShiftIso.

LaTeX

$$$ (commShiftIso (F ⋙ G) a).inv.app X = (commShiftIso G a).inv.app (F.obj X) ≫ G.map ((commShiftIso F a).inv.app X) $$$

Lean4

instance id : CommShift (𝟭 C) A where iso := fun _ => rightUnitor _ ≪≫ (leftUnitor _).symm

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