Documentation

Mathlib.CategoryTheory.Shift.Quotient

The shift on a quotient category #

Let C be a category equipped a shift by a monoid A. If we have a relation on morphisms r : HomRel C that is compatible with the shift (i.e. if two morphisms f and g are related, then f⟦a⟧' and g⟦a⟧' are also related for all a : A), then the quotient category Quotient r is equipped with a shift.

The condition r.IsCompatibleWithShift A on the relation r is a class so that the shift can be automatically inferred on the quotient category.

source
class HomRel.IsCompatibleWithShift {C : Type u} [CategoryTheory.Category.{v, u} C] (r : HomRel C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] :
Prop

A relation on morphisms is compatible with the shift by a monoid A when the relation if preserved by the shift.

Instances
    source
    @[irreducible]
    noncomputable instance CategoryTheory.HasShift.quotient {C : Type u} [Category.{v, u} C] (r : HomRel C) (A : Type w) [AddMonoid A] [HasShift C A] [r.IsCompatibleWithShift A] :
    HasShift (Quotient r) A

    The shift by a monoid A induced on a quotient category Quotient r when the relation r is compatible with the shift.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[irreducible]
    noncomputable instance CategoryTheory.Quotient.functor_commShift {C : Type u} [Category.{v, u} C] (r : HomRel C) (A : Type w) [AddMonoid A] [HasShift C A] [r.IsCompatibleWithShift A] :
    (functor r).CommShift A

    The functor Quotient.functor r : C ⥤ Quotient r commutes with the shift.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[irreducible]
    noncomputable def CategoryTheory.Quotient.LiftCommShift.iso {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) (r : HomRel C) {A : Type w} [AddMonoid A] [HasShift C A] [HasShift D A] [r.IsCompatibleWithShift A] [F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (a : A) :
    (shiftFunctor (Quotient r) a).comp (lift r F hF) ≅ (lift r F hF).comp (shiftFunctor D a)

    Auxiliary definition for Quotient.liftCommShift.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Quotient.LiftCommShift.iso_hom_app {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) (r : HomRel C) {A : Type w} [AddMonoid A] [HasShift C A] [HasShift D A] [r.IsCompatibleWithShift A] [F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (a : A) (X : C) :
      (iso F r hF a).hom.app ((functor r).obj X) = CategoryStruct.comp ((lift r F hF).map (((functor r).commShiftIso a).inv.app X)) ((F.commShiftIso a).hom.app X)
      source
      @[simp]
      theorem CategoryTheory.Quotient.LiftCommShift.iso_inv_app {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) (r : HomRel C) {A : Type w} [AddMonoid A] [HasShift C A] [HasShift D A] [r.IsCompatibleWithShift A] [F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (a : A) (X : C) :
      (iso F r hF a).inv.app ((functor r).obj X) = CategoryStruct.comp ((F.commShiftIso a).inv.app X) ((lift r F hF).map (((functor r).commShiftIso a).hom.app X))
      source
      noncomputable instance CategoryTheory.Quotient.liftCommShift {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) (r : HomRel C) (A : Type w) [AddMonoid A] [HasShift C A] [HasShift D A] [r.IsCompatibleWithShift A] [F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) :
      (lift r F hF).CommShift A

      When r : HomRel C is compatible with the shift by an additive monoid, and F : C ⥤ D is a functor which commutes with the shift and is compatible with r, then the induced functor Quotient.lift r F _ : Quotient r ⥤ D also commutes with the shift.

      Equations
      source
      instance CategoryTheory.Quotient.liftCommShift_compatibility {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) (r : HomRel C) (A : Type w) [AddMonoid A] [HasShift C A] [HasShift D A] [r.IsCompatibleWithShift A] [F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) :
      NatTrans.CommShift (lift.isLift r F hF).hom A