Predicates on categories equipped with shift

Given a predicate P : C → Prop on objects of a category equipped with a shift by A, we define shifted predicates PredicateShift P a for all a : A.

def CategoryTheory.PredicateShift {C : Type u_1} [Category.{u_3, u_1} C] (P : C → Prop) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) : C → Prop

Given a predicate P : C → Prop on objects of a category equipped with a shift by A, this is the predicate which is satisfied by X if P (X⟦a⟧).

Equations

• CategoryTheory.PredicateShift P a X = P ((CategoryTheory.shiftFunctor C a).obj X)

theorem CategoryTheory.predicateShift_iff {C : Type u_1} [Category.{u_3, u_1} C] (P : C → Prop) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) (X : C) : PredicateShift P a X ↔ P ((shiftFunctor C a).obj X)

instance CategoryTheory.predicateShift_closedUnderIsomorphisms {C : Type u_1} [Category.{u_3, u_1} C] (P : C → Prop) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) [ClosedUnderIsomorphisms P] : ClosedUnderIsomorphisms (PredicateShift P a)

@[simp]

theorem CategoryTheory.predicateShift_zero {C : Type u_1} [Category.{u_3, u_1} C] (P : C → Prop) (A : Type u_2) [AddMonoid A] [HasShift C A] [ClosedUnderIsomorphisms P] : PredicateShift P 0 = P

theorem CategoryTheory.predicateShift_predicateShift {C : Type u_1} [Category.{u_3, u_1} C] (P : C → Prop) {A : Type u_2} [AddMonoid A] [HasShift C A] (a b c : A) (h : a + b = c) [ClosedUnderIsomorphisms P] : PredicateShift (PredicateShift P b) a = PredicateShift P c