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
    theorem HomRel.IsCompatibleWithShift.condition {C : Type u} :
    ∀ {inst : CategoryTheory.Category.{v, u} C} {r : HomRel C} {A : Type w} {inst_1 : AddMonoid A} {inst_2 : CategoryTheory.HasShift C A} [self : r.IsCompatibleWithShift A] (a : A) ⦃X Y : C⦄ (f g : X ⟶ Y), r f g → r ((CategoryTheory.shiftFunctor C a).map f) ((CategoryTheory.shiftFunctor C a).map g)

    the condition that the relation is preserved by the shift

    source
    @[irreducible]
    noncomputable instance CategoryTheory.HasShift.quotient {C : Type u} [CategoryTheory.Category.{v, u} C] (r : HomRel C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [r.IsCompatibleWithShift A] :
    CategoryTheory.HasShift (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (r : HomRel C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [r.IsCompatibleWithShift A] :
    (CategoryTheory.Quotient.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (r : HomRel C) {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.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) :
    (CategoryTheory.shiftFunctor (CategoryTheory.Quotient r) a).comp (CategoryTheory.Quotient.lift r F hF) ≅ (CategoryTheory.Quotient.lift r F hF).comp (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (r : HomRel C) {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.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) :
      (CategoryTheory.Quotient.LiftCommShift.iso F r hF a).hom.app ((CategoryTheory.Quotient.functor r).obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Quotient.lift r F hF).map (((CategoryTheory.Quotient.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (r : HomRel C) {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.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) :
      (CategoryTheory.Quotient.LiftCommShift.iso F r hF a).inv.app ((CategoryTheory.Quotient.functor r).obj X) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).inv.app X) ((CategoryTheory.Quotient.lift r F hF).map (((CategoryTheory.Quotient.functor r).commShiftIso a).hom.app X))
      source
      noncomputable instance CategoryTheory.Quotient.liftCommShift {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (r : HomRel C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.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₂) :
      (CategoryTheory.Quotient.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (r : HomRel C) (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.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₂) :
      CategoryTheory.NatTrans.CommShift (CategoryTheory.Quotient.lift.isLift r F hF).hom A
      Equations
      • ⋯ = ⋯