Documentation

Mathlib.CategoryTheory.ObjectProperty.Shift

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
Instances For
    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
    Instances For
      source
      @[deprecated CategoryTheory.ObjectProperty.prop_shift_iff (since := "2025-02-25")]
      theorem CategoryTheory.predicateShift_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)

      Alias of CategoryTheory.ObjectProperty.prop_shift_iff.

      source
      @[deprecated CategoryTheory.ObjectProperty.shift_zero (since := "2025-02-25")]
      theorem CategoryTheory.predicateShift_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

      Alias of CategoryTheory.ObjectProperty.shift_zero.

      source
      @[deprecated CategoryTheory.ObjectProperty.shift_shift (since := "2025-02-25")]
      theorem CategoryTheory.predicateShift_predicateShift {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

      Alias of CategoryTheory.ObjectProperty.shift_shift.