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} [CategoryTheory.Category.{u_3, u_1} C] (P : C → Prop) {A : Type u_2} [AddMonoid A] [CategoryTheory.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} [CategoryTheory.Category.{u_3, u_1} C] (P : C → Prop) {A : Type u_2} [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) (X : C) : CategoryTheory.PredicateShift P a X ↔ P ((CategoryTheory.shiftFunctor C a).obj X)

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

Equations

• ⋯ = ⋯

@[simp]

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

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