Checking shift compatibility of natural transformations at a generator #
For integral shifts, a natural transformation between functors commuting with shifts is
compatible with every shift as soon as it is compatible with the shift by one. Compatibility
is closed under addition by Mathlib's NatTrans.CommShiftCore.add; cancellation of a shift
gives compatibility with negative integers.
theorem
TauCeti.natTrans_commShiftCore_add_right_iff
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Category.{v_2, u_2} D]
{A : Type u_3}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
{F G : CategoryTheory.Functor C D}
[F.CommShift A]
[G.CommShift A]
{τ : F ⟶ G}
{a b : A}
[(CategoryTheory.shiftFunctor D b).Faithful]
:
Compatibility with shifts by b and a + b is equivalent to compatibility with shifts
by b and a. It suffices that the target shift by b is faithful; in particular this holds
for group shifts.
theorem
TauCeti.natTrans_commShift_iff_one
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Category.{v_2, u_2} D]
{F G : CategoryTheory.Functor C D}
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.HasShift D ℤ]
[F.CommShift ℤ]
[G.CommShift ℤ]
{τ : F ⟶ G}
:
A natural transformation is compatible with all integral shifts if and only if it is compatible with the shift by one.