English
There exists a natural transformation commuting with Shift structures on PullbackShift induced by φ and the identity, i.e., the canonical CommShift structure aligns with the pullback of the base CommShift.
Русский
Существует натуральное преобразование, совмещающее структуры Shift на PullbackShift, индуцируемые φ и единичностью; каноническая структура CommShift согласуется с вытяжкой базовой CommShift.
LaTeX
$$$\text{NatTrans.CommShift} (\text{PullbackShift.natIsoId } C φ).hom A$$$
Lean4
/-- This expresses the compatibility between two `CommShift` structures by `A` on (synonyms of)
`𝟭 C`: the canonical `CommShift` structure on `𝟭 (PullbackShift C φ)`, and the `CommShift`
structure on `PullbackShift.functor (𝟭 C) φ` (i.e the pullback of the canonical `CommShift`
structure on `𝟭 C`).
-/
instance : NatTrans.CommShift (PullbackShift.natIsoId C φ).hom A where
shift_comm
_ := by
ext
simp [PullbackShift.natIsoId, Functor.commShiftPullback_iso_eq]
