shiftFunctorComm_zero_hom_app — Mathlib

English

The hom component of the commuting-shift isomorphism with zero shift aligns with the zero-shift homomorphism.

Русский

Гомоморфизм компонента изоморфизма коммутативности сдвигов с нулевым сдвигом согласуется с гомоморфизмом нулевого сдвига.

LaTeX

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

Lean4

theorem shiftFunctorComm_zero_hom_app (a : A) :
    (shiftFunctorComm C a 0).hom.app X =
      (shiftFunctorZero C A).hom.app (X⟦a⟧) ≫ ((shiftFunctorZero C A).inv.app X)⟦a⟧' :=
  by
  simp only [shiftFunctorZero_hom_app_shift, Category.assoc, ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id,
    Functor.comp_obj, Category.comp_id]

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