instCommShiftPullbackShiftHomFunctorNatIsoComp

English

There is a commuting natural transformation for the opposite-shift construction, giving a CommShift structure on the Hom part of the natIsoComp.

Русский

Существует естественное преобразование для конструкции OppositeShift, задающее структуру CommShift на Hom часть natIsoComp.

LaTeX

$$NatTrans.CommShift((OppositeShift.natIsoComp A F G).hom) A$$

Lean4

instance : NatTrans.CommShift (PullbackShift.natIsoComp φ F G).hom A where
  shift_comm
    _ := by
    ext
    dsimp [PullbackShift.natIsoComp]
    simp only [commShiftPullback_iso_eq φ _ _ _ rfl, Iso.trans_hom, isoWhiskerRight_hom, isoWhiskerLeft_hom,
      Iso.symm_hom, comp_app, comp_obj, whiskerRight_app, Functor.comp_map, commShiftIso_comp_hom_app, whiskerLeft_app,
      assoc, map_id, comp_id, map_comp, id_comp]
    dsimp [PullbackShift.functor]
    slice_rhs 3 4 => rw [← G.map_comp, Iso.inv_hom_id_app]
    simp

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