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)
Instances For
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]
:
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]
:
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 b c : A)
(h : a + b = c)
[CategoryTheory.ClosedUnderIsomorphisms P]
: