CategoryTheory.MorphismProperty.IsCompatibleWithShift.condition

theorem CategoryTheory.MorphismProperty.IsCompatibleWithShift.condition : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {A : Type w} [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [self : W.IsCompatibleWithShift A] (a : A), W.inverseImage (CategoryTheory.shiftFunctor C a) = W

This theorem states that for any category `C`, any property `W` of morphisms in `C`, and any element `a` from an additive monoid `A` (where `C` has a shift structure with respect to `A`), the property `W` remains invariant under the action of the shift functor by `a`. In other words, taking the inverse image of `W` by the shift functor induced by `a` yields the same morphism property `W`. This is a condition for `W` to be compatible with the shift structure in `C`.

More concisely: For any category `C` with a shift structure with respect to an additive monoid `A`, and any morphism property `W` in `C`, the shift functor by an element `a` in `A` preserves `W`, i.e., the inverse image of `W` under the shift functor is equal to `W`.