Documentation

Mathlib.CategoryTheory.Shift.ShiftedHom

Shifted morphisms #

Given a category C endowed with a shift by an additive monoid M and two objects X and Y in C, we consider the types ShiftedHom X Y m defined as X ⟶ Y⟦m⟧ for all m : M, and the composition on these shifted hom.

source
@[reducible, inline]
abbrev CategoryTheory.ShiftedHom {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] (X Y : C) (m : M) :
Type v_1

In a category C equipped with a shift by an additive monoid, this is the type of morphisms X ⟶ (Y⟦m⟧) for m : M.

Equations
Instances For
    source
    noncomputable def CategoryTheory.ShiftedHom.comp {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} {a b c : M} (f : ShiftedHom X Y a) (g : ShiftedHom Y Z b) (h : b + a = c) :
    ShiftedHom X Z c

    The composition of f : X ⟶ Y⟦a⟧ and g : Y ⟶ Z⟦b⟧, as a morphism X ⟶ Z⟦c⟧ when b + a = c.

    Equations
    Instances For
      source
      theorem CategoryTheory.ShiftedHom.comp_assoc {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z T : C} {a₁ a₂ a₃ a₁₂ a₂₃ a : M} (α : ShiftedHom X Y a₁) (β : ShiftedHom Y Z a₂) (γ : ShiftedHom Z T a₃) (h₁₂ : a₂ + a₁ = a₁₂) (h₂₃ : a₃ + a₂ = a₂₃) (h : a₃ + a₂ + a₁ = a) :
      (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯

      In degree 0 : M, shifted hom ShiftedHom X Y 0 identify to morphisms X ⟶ Y. We generalize this to m₀ : M such that m₀ : 0 as it shall be convenient when we apply this with M := ℤ and m₀ the coercion of 0 : ℕ.

      source
      noncomputable def CategoryTheory.ShiftedHom.mk₀ {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) :
      ShiftedHom X Y m₀

      The element of ShiftedHom X Y m₀ (when m₀ = 0) attached to a morphism X ⟶ Y.

      Equations
      Instances For
        source
        noncomputable def CategoryTheory.ShiftedHom.homEquiv {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) :
        (X ⟶ Y) ≃ ShiftedHom X Y m₀

        The bijection (X ⟶ Y) ≃ ShiftedHom X Y m₀ when m₀ = 0.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.ShiftedHom.homEquiv_apply {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) :
          (homEquiv m₀ hm₀) f = mk₀ m₀ hm₀ f
          source
          theorem CategoryTheory.ShiftedHom.mk₀_comp {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) {a : M} (g : ShiftedHom Y Z a) :
          (mk₀ m₀ hm₀ f).comp g ⋯ = CategoryStruct.comp f g
          source
          @[simp]
          theorem CategoryTheory.ShiftedHom.mk₀_id_comp {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) {a : M} (f : ShiftedHom X Y a) :
          (mk₀ m₀ hm₀ (CategoryStruct.id X)).comp f ⋯ = f
          source
          theorem CategoryTheory.ShiftedHom.comp_mk₀ {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) (g : Y ⟶ Z) :
          f.comp (mk₀ m₀ hm₀ g) ⋯ = CategoryStruct.comp f ((shiftFunctor C a).map g)
          source
          @[simp]
          theorem CategoryTheory.ShiftedHom.comp_mk₀_id {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) :
          f.comp (mk₀ m₀ hm₀ (CategoryStruct.id Y)) ⋯ = f
          source
          @[simp]
          theorem CategoryTheory.ShiftedHom.mk₀_comp_mk₀ {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {a b c : M} (h : b + a = c) (ha : a = 0) (hb : b = 0) :
          (mk₀ a ha f).comp (mk₀ b hb g) h = mk₀ c ⋯ (CategoryStruct.comp f g)
          source
          @[simp]
          theorem CategoryTheory.ShiftedHom.mk₀_comp_mk₀_assoc {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z T : C} (f : X ⟶ Y) (g : Y ⟶ Z) {a : M} (ha : a = 0) {d : M} (h : ShiftedHom Z T d) :
          (mk₀ a ha f).comp ((mk₀ a ha g).comp h ⋯) ⋯ = (mk₀ a ha (CategoryStruct.comp f g)).comp h ⋯
          source
          @[implicit_reducible]
          noncomputable def CategoryTheory.ShiftedHom.precompIsoEquiv {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} (e : X ≅ Y) {a : M} :
          ShiftedHom Y Z a ≃ ShiftedHom X Z a

          The bijection ShiftedHom Y Z a ≃ ShiftedHom X Z a induced by an isomorphism X ≅ Y.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.ShiftedHom.precompIsoEquiv_apply {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} (e : X ≅ Y) {a : M} (x : ShiftedHom Y Z a) :
            (precompIsoEquiv e) x = (mk₀ 0 ⋯ e.hom).comp x ⋯
            source
            @[simp]
            theorem CategoryTheory.ShiftedHom.precompIsoEquiv_symm_apply {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} (e : X ≅ Y) {a : M} (x : ShiftedHom X Z a) :
            (precompIsoEquiv e).symm x = (mk₀ 0 ⋯ e.inv).comp x ⋯
            source
            @[implicit_reducible]
            noncomputable def CategoryTheory.ShiftedHom.postcompIsoEquiv {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} (e : Y ≅ Z) {a : M} :
            ShiftedHom X Y a ≃ ShiftedHom X Z a

            The bijection ShiftedHom X Y a ≃ ShiftedHom X Z a induced by an isomorphism Y ≅ Z.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.ShiftedHom.postcompIsoEquiv_apply {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} (e : Y ≅ Z) {a : M} (x : ShiftedHom X Y a) :
              (postcompIsoEquiv e) x = x.comp (mk₀ 0 ⋯ e.hom) ⋯
              source
              @[simp]
              theorem CategoryTheory.ShiftedHom.postcompIsoEquiv_symm_apply {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} (e : Y ≅ Z) {a : M} (x : ShiftedHom X Z a) :
              (postcompIsoEquiv e).symm x = x.comp (mk₀ 0 ⋯ e.inv) ⋯
              source
              @[simp]
              theorem CategoryTheory.ShiftedHom.mk₀_zero {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] (X Y : C) [Preadditive C] (m₀ : M) (hm₀ : m₀ = 0) :
              mk₀ m₀ hm₀ 0 = 0
              source
              @[simp]
              theorem CategoryTheory.ShiftedHom.mk₀_add {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} [Preadditive C] (m₀ : M) (hm₀ : m₀ = 0) (f g : X ⟶ Y) :
              mk₀ m₀ hm₀ (f + g) = mk₀ m₀ hm₀ f + mk₀ m₀ hm₀ g
              source
              @[simp]
              theorem CategoryTheory.ShiftedHom.mk₀_neg {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} [Preadditive C] (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) :
              mk₀ m₀ hm₀ (-f) = -mk₀ m₀ hm₀ f
              source
              @[simp]
              theorem CategoryTheory.ShiftedHom.comp_add {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} [Preadditive C] [∀ (a : M), (shiftFunctor C a).Additive] {a b c : M} (α : ShiftedHom X Y a) (β₁ β₂ : ShiftedHom Y Z b) (h : b + a = c) :
              α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
              source
              @[simp]
              theorem CategoryTheory.ShiftedHom.add_comp {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} [Preadditive C] {a b c : M} (α₁ α₂ : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) :
              (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
              source
              @[simp]
              theorem CategoryTheory.ShiftedHom.comp_neg {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} [Preadditive C] [∀ (a : M), (shiftFunctor C a).Additive] {a b c : M} (α : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) :
              α.comp (-β) h = -α.comp β h
              source
              @[simp]
              theorem CategoryTheory.ShiftedHom.neg_comp {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} [Preadditive C] {a b c : M} (α : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) :
              (-α).comp β h = -α.comp β h
              source
              @[simp]
              theorem CategoryTheory.ShiftedHom.comp_zero {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} (Z : C) [Preadditive C] [∀ (a : M), (shiftFunctor C a).PreservesZeroMorphisms] {a : M} (β : ShiftedHom X Y a) {b c : M} (h : b + a = c) :
              β.comp 0 h = 0
              source
              @[simp]
              theorem CategoryTheory.ShiftedHom.zero_comp {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] (X : C) {Y Z : C} [Preadditive C] (a : M) {b c : M} (β : ShiftedHom Y Z b) (h : b + a = c) :
              comp 0 β h = 0
              source
              def CategoryTheory.ShiftedHom.map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] {X Y : C} {a : M} (f : ShiftedHom X Y a) (F : Functor C D) [F.CommShift M] :
              ShiftedHom (F.obj X) (F.obj Y) a

              The action on ShiftedHom of a functor which commutes with the shift.

              Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.ShiftedHom.map_mk₀ {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) (F : Functor C D) [F.CommShift M] :
                (mk₀ m₀ hm₀ f).map F = mk₀ m₀ hm₀ (F.map f)
                source
                @[simp]
                theorem CategoryTheory.ShiftedHom.id_map {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} {a : M} (f : ShiftedHom X Y a) :
                f.map (Functor.id C) = f
                source
                theorem CategoryTheory.ShiftedHom.comp_map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {E : Type u_3} [Category.{v_3, u_3} E] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] [HasShift E M] {X Y : C} {a : M} (f : ShiftedHom X Y a) (F : Functor C D) [F.CommShift M] (G : Functor D E) [G.CommShift M] :
                f.map (F.comp G) = (f.map F).map G
                source
                theorem CategoryTheory.ShiftedHom.map_naturality {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] {X Y : C} {a : M} (f : ShiftedHom X Y a) {F G : Functor C D} (τ : F ⟶ G) [F.CommShift M] [G.CommShift M] [NatTrans.CommShift τ M] :
                (f.map F).comp (mk₀ 0 ⋯ (τ.app Y)) ⋯ = (mk₀ 0 ⋯ (τ.app X)).comp (f.map G) ⋯
                source
                @[simp]
                theorem CategoryTheory.ShiftedHom.map_naturality_1 {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] {X Y : C} {a : M} (f : ShiftedHom X Y a) {F G : Functor C D} (e : F ≅ G) [F.CommShift M] [G.CommShift M] [NatTrans.CommShift e.hom M] :
                (mk₀ 0 ⋯ (e.inv.app X)).comp ((f.map F).comp (mk₀ 0 ⋯ (e.hom.app Y)) ⋯) ⋯ = f.map G
                source
                @[simp]
                theorem CategoryTheory.ShiftedHom.map_naturality_2 {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] {X Y : C} {a : M} (f : ShiftedHom X Y a) {F G : Functor C D} (e : F ≅ G) [F.CommShift M] [G.CommShift M] [NatTrans.CommShift e.hom M] :
                (mk₀ 0 ⋯ (e.hom.app X)).comp ((f.map G).comp (mk₀ 0 ⋯ (e.inv.app Y)) ⋯) ⋯ = f.map F
                source
                theorem CategoryTheory.ShiftedHom.map_comp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] {X Y Z : C} {a b c : M} (f : ShiftedHom X Y a) (g : ShiftedHom Y Z b) (h : b + a = c) (F : Functor C D) [F.CommShift M] :
                (f.comp g h).map F = (f.map F).comp (g.map F) h
                source
                @[simp]
                theorem CategoryTheory.ShiftedHom.map_add {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] {X Y : C} [Preadditive C] [Preadditive D] {a : M} (α₁ α₂ : ShiftedHom X Y a) (F : Functor C D) [F.CommShift M] [F.Additive] :
                (α₁ + α₂).map F = α₁.map F + α₂.map F
                source
                @[simp]
                theorem CategoryTheory.ShiftedHom.map_zero {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] {X Y : C} [Preadditive C] [Preadditive D] {a : M} (F : Functor C D) [F.CommShift M] [F.Additive] :
                map 0 F = 0
                source
                @[simp]
                theorem CategoryTheory.ShiftedHom.comp_smul {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} {R : Type u_5} [Ring R] [Preadditive C] [Linear R C] [∀ (a : M), Functor.Linear R (shiftFunctor C a)] (r : R) {a b c : M} (α : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) :
                α.comp (r • β) h = r • α.comp β h
                source
                @[simp]
                theorem CategoryTheory.ShiftedHom.smul_comp {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y Z : C} {R : Type u_5} [Ring R] [Preadditive C] [Linear R C] (r : R) {a b c : M} (α : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) :
                (r • α).comp β h = r • α.comp β h
                source
                @[simp]
                theorem CategoryTheory.ShiftedHom.mk₀_smul {C : Type u_1} [Category.{v_1, u_1} C] {M : Type u_4} [AddMonoid M] [HasShift C M] {X Y : C} {R : Type u_5} [Ring R] [Preadditive C] [Linear R C] (m₀ : M) (hm₀ : m₀ = 0) (r : R) {f : X ⟶ Y} :
                mk₀ m₀ hm₀ (r • f) = r • mk₀ m₀ hm₀ f
                source
                @[simp]
                theorem CategoryTheory.ShiftedHom.map_smul {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {M : Type u_4} [AddMonoid M] [HasShift C M] [HasShift D M] {X Y : C} {R : Type u_5} [Ring R] [Preadditive C] [Linear R C] [Preadditive D] [Linear R D] (r : R) {a : M} (α : ShiftedHom X Y a) (F : Functor C D) [F.CommShift M] [Functor.Linear R F] :
                (r • α).map F = r • α.map F