English
The canonical commShift compatibility for the identity pullback shift natural transformation between 𝟭 C and PullbackShift is well-defined by a single shift_comm condition.
Русский
Каноническое совместимое commShift между единичной натрансформацией 𝟭 C и PullbackShift задаётся через единую условие shift_comm.
LaTeX
$$$\text{NatTrans.CommShift} (PullbackShift.natIsoId\ C\ φ).hom\ A$ with shift_comm: \"ext; \dots\"$$
Lean4
instance commShiftPullback (τ : F ⟶ G) [NatTrans.CommShift τ B] : NatTrans.CommShift (PullbackShift.natTrans φ τ) A
where
shift_comm
_ := by
ext
dsimp [PullbackShift.natTrans]
simp only [commShiftPullback_iso_eq φ _ _ _ rfl, Iso.trans_hom, isoWhiskerRight_hom, isoWhiskerLeft_hom,
Iso.symm_hom, comp_app, comp_obj, whiskerRight_app, whiskerLeft_app, assoc]
rw [← τ.naturality_assoc]
simp [← NatTrans.shift_app_comm_assoc]
