whiskerRight — Mathlib

English

If τ: F1 ⟶ F2 is a NatTrans.CommShift A, then whiskering on the right by G preserves CommShift, i.e., NatTrans.CommShift (Functior.whiskerRight τ G) A.

Русский

Если τ: F1 ⟶ F2 — NatTrans.CommShift A, то правый whiskerRight τ G сохраняет CommShift, т.е. NatTrans.CommShift (Functor.whiskerRight τ G) A.

LaTeX

$$$NatTrans.CommShift (Functor.whiskerRight τ G) A$$$

Lean4

instance whiskerRight [NatTrans.CommShift τ A] : NatTrans.CommShift (Functor.whiskerRight τ G) A :=
  ⟨fun a => by
    ext X
    simp only [Functor.whiskerRight_twice, comp_app, Functor.commShiftIso_comp_hom_app, Functor.associator_hom_app,
      Functor.whiskerRight_app, Functor.comp_map, Functor.associator_inv_app, comp_id, id_comp, assoc,
      ← Functor.commShiftIso_hom_naturality, ← G.map_comp_assoc, shift_app_comm, Functor.whiskerLeft_app]⟩

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