HomRel.IsCompatibleWithShift.condition

theorem HomRel.IsCompatibleWithShift.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {r : HomRel C} {A : Type w} [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [self : r.IsCompatibleWithShift A] (a : A) ⦃X Y : C⦄ (f g : X ⟶ Y), r f g → r ((CategoryTheory.shiftFunctor C a).map f) ((CategoryTheory.shiftFunctor C a).map g)

The theorem `HomRel.IsCompatibleWithShift.condition` states that given a category `C`, a `HomRel` (homeomorphism relation) `r` on `C`, and an additive monoid `A` (with `C` having a shift structure with respect to `A`), if `r` is compatible with the shift operation then for any element `a` of `A` and any two morphisms `f` and `g` from `X` to `Y` in `C`, if `f` and `g` are related by `r` then so are their images under the shift functor associated with `a`. This means the relation `r` is preserved when moving objects and morphisms 'up' according to the shift operation.

More concisely: Given a category with a shift structure, a homeomorphism relation compatible with shifts preserves the relation between morphisms when applying the shift functor.