shiftFunctorZero_inv_app_shift — Mathlib

English

The inverse component of the zero-shift functor behaves compatibly with shifting by n, distributing through the shift-commutation structure.

Русский

Обратная компонента нулевого сдвигового функторa совместима со сдвигом на n, распределяясь через структуру коммутатии сдвигов.

LaTeX

$$$ (shiftFunctorZero C A).inv.app (X⟦n⟧) = ((shiftFunctorZero C A).inv.app X)⟦n⟧' ≫ (shiftFunctorComm C n 0).inv.app X $$$

Lean4

theorem shiftFunctorZero_inv_app_shift (n : A) :
    (shiftFunctorZero C A).inv.app (X⟦n⟧) =
      ((shiftFunctorZero C A).inv.app X)⟦n⟧' ≫ (shiftFunctorComm C n 0).inv.app X :=
  by
  rw [← cancel_mono ((shiftFunctorZero C A).hom.app (X⟦n⟧)), Category.assoc, Iso.inv_hom_id_app,
    shiftFunctorZero_hom_app_shift, Iso.inv_hom_id_app_assoc, ← Functor.map_comp, Iso.inv_hom_id_app]
  dsimp
  rw [Functor.map_id]

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