Properties of objects on categories equipped with shift #

Given a predicate P : ObjectProperty C on objects of a category equipped with a shift by A, we define shifted properties of objects P.shift a for all a : A.

source

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

ObjectProperty C

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

P.shift a X = P ((CategoryTheory.shiftFunctor C a).obj X)

source

theorem CategoryTheory.ObjectProperty.prop_shift_iff {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) (X : C) :

P.shift a X ↔ P ((shiftFunctor C a).obj X)

source

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsShift {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) [P.IsClosedUnderIsomorphisms] :

(P.shift a).IsClosedUnderIsomorphisms

source

@[simp]

theorem CategoryTheory.ObjectProperty.shift_zero {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) (A : Type u_2) [AddMonoid A] [HasShift C A] [P.IsClosedUnderIsomorphisms] :

P.shift 0 = P

source

theorem CategoryTheory.ObjectProperty.shift_shift {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a b c : A) (h : a + b = c) [P.IsClosedUnderIsomorphisms] :

(P.shift b).shift a = P.shift c

source

@[deprecated CategoryTheory.ObjectProperty.shift (since := "2025-02-25")]

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

ObjectProperty C

Alias of CategoryTheory.ObjectProperty.shift.

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