shift_app — Mathlib

English

Let τ: F1 ⇒ F2 be a natural transformation between functors with shift structure. Then the following equality holds: (τ.app X)⟦a⟧' = (F1.commShiftIso a).inv.app X ≫ τ.app (X⟦a⟧) ≫ (F2.commShiftIso a).hom.app X.

Русский

Пусть τ: F1 ⇒ F2 — натрансформация между функтороми сдвига. Тогда: (τ.app X)⟦a⟧' = (F1.commShiftIso a).inv.app X ≫ τ.app (X⟦a⟧) ≫ (F2.commShiftIso a).hom.app X.

LaTeX

$$$(\\tau.app X)\\,⟦a⟧' = (F_1.commShiftIso a).inv.app X \\\\; \\circ \\\\; \\tau.app (X⟦a⟧) \\\\; \\circ \\\\; (F_2.commShiftIso a).hom.app X$$$

Lean4

@[reassoc]
theorem shift_app (a : A) (X : C) :
    (τ.app X)⟦a⟧' = (F₁.commShiftIso a).inv.app X ≫ τ.app (X⟦a⟧) ≫ (F₂.commShiftIso a).hom.app X := by
  rw [← shift_app_comm, Iso.inv_hom_id_app_assoc]

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