Theorems · Inductive type · category theory

CategoryTheory.MorphismProperty.IsCompatibleWithShift

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.MorphismProperty C → (A : Type w) → [inst_1 : AddMonoid A] → [CategoryTheory.HasShift C A] → Prop

A morphism property W on a category C is compatible with the shift by a monoid A when for all a : A, a morphism f belongs to W if and only if f⟦a⟧' does.

Defined in

Mathlib.CategoryTheory.Shift.Localization

Cited by

25 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryAddMonoidCategoryTheory.HasShift