mathlib documentation

category_theory.differential_object

Differential objects in a category. #

A differential object in a category with zero morphisms and a shift is an object X equipped with a morphism d : X ⟶ X⟦1⟧, such that d^2 = 0.

We build the category of differential objects, and some basic constructions such as the forgetful functor, zero morphisms and zero objects, and the shift functor on differential objects.

source
@[nolint]
structure category_theory.differential_object (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] :
Type (max u v)

A differential object in a category with zero morphisms and a shift is an object X equipped with a morphism d : X ⟶ X⟦1⟧, such that d^2 = 0.

Instances for category_theory.differential_object
source
@[simp]
theorem category_theory.differential_object.d_squared {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (self : category_theory.differential_object C) :
self.d ≫ (category_theory.shift_functor C 1).map self.d = 0
source
theorem category_theory.differential_object.hom.ext_iff {C : Type u} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.limits.has_zero_morphisms C} {_inst_3 : category_theory.has_shift C ℤ} {X Y : category_theory.differential_object C} (x y : X.hom Y) :
x = y ↔ x.f = y.f
source
theorem category_theory.differential_object.hom.ext {C : Type u} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.limits.has_zero_morphisms C} {_inst_3 : category_theory.has_shift C ℤ} {X Y : category_theory.differential_object C} (x y : X.hom Y) (h : x.f = y.f) :
x = y
source
@[nolint, ext]
structure category_theory.differential_object.hom {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (X Y : category_theory.differential_object C) :
Type v

A morphism of differential objects is a morphism commuting with the differentials.

Instances for category_theory.differential_object.hom
  • category_theory.differential_object.hom.has_sizeof_inst
source
@[simp]
theorem category_theory.differential_object.hom.comm {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y : category_theory.differential_object C} (self : X.hom Y) :
X.d ≫ (category_theory.shift_functor C 1).map self.f = self.f ≫ Y.d
source
@[simp]
theorem category_theory.differential_object.hom.comm_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y : category_theory.differential_object C} (self : X.hom Y) {X' : C} (f' : (category_theory.shift_functor C 1).obj Y.X ⟶ X') :
X.d ≫ (category_theory.shift_functor C 1).map self.f ≫ f' = self.f ≫ Y.d ≫ f'
source
@[simp]
theorem category_theory.differential_object.hom.id_f {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (X : category_theory.differential_object C) :
(category_theory.differential_object.hom.id X).f = 𝟙 X.X
source
def category_theory.differential_object.hom.id {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (X : category_theory.differential_object C) :
X.hom X

The identity morphism of a differential object.

Equations
source
def category_theory.differential_object.hom.comp {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y Z : category_theory.differential_object C} (f : X.hom Y) (g : Y.hom Z) :
X.hom Z

The composition of morphisms of differential objects.

Equations
source
@[simp]
theorem category_theory.differential_object.hom.comp_f {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y Z : category_theory.differential_object C} (f : X.hom Y) (g : Y.hom Z) :
(f.comp g).f = f.f ≫ g.f
source
@[protected, instance]
def category_theory.differential_object.category_of_differential_objects {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] :
category_theory.category (category_theory.differential_object C)
Equations
source
@[simp]
theorem category_theory.differential_object.id_f {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (X : category_theory.differential_object C) :
(𝟙 X).f = 𝟙 X.X
source
@[simp]
theorem category_theory.differential_object.comp_f {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y Z : category_theory.differential_object C} (f : X ⟶ Y) (g : Y ⟶ Z) :
(f ≫ g).f = f.f ≫ g.f
source
@[simp]
theorem category_theory.differential_object.eq_to_hom_f {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y : category_theory.differential_object C} (h : X = Y) :
(category_theory.eq_to_hom h).f = category_theory.eq_to_hom _
source
def category_theory.differential_object.forget (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] :
category_theory.differential_object C ⥤ C

The forgetful functor taking a differential object to its underlying object.

Equations
Instances for category_theory.differential_object.forget
source
@[protected, instance]
def category_theory.differential_object.forget_faithful (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] :
category_theory.faithful (category_theory.differential_object.forget C)
source
@[protected, instance]
def category_theory.differential_object.has_zero_morphisms (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] :
category_theory.limits.has_zero_morphisms (category_theory.differential_object C)
Equations
source
@[simp]
theorem category_theory.differential_object.zero_f {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (P Q : category_theory.differential_object C) :
0.f = 0
source
def category_theory.differential_object.iso_app {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y : category_theory.differential_object C} (f : X ≅ Y) :
X.X ≅ Y.X

An isomorphism of differential objects gives an isomorphism of the underlying objects.

Equations
source
@[simp]
theorem category_theory.differential_object.iso_app_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y : category_theory.differential_object C} (f : X ≅ Y) :
(category_theory.differential_object.iso_app f).inv = f.inv.f
source
@[simp]
theorem category_theory.differential_object.iso_app_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y : category_theory.differential_object C} (f : X ≅ Y) :
(category_theory.differential_object.iso_app f).hom = f.hom.f
source
@[simp]
theorem category_theory.differential_object.iso_app_refl {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (X : category_theory.differential_object C) :
category_theory.differential_object.iso_app (category_theory.iso.refl X) = category_theory.iso.refl X.X
source
@[simp]
theorem category_theory.differential_object.iso_app_symm {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y : category_theory.differential_object C} (f : X ≅ Y) :
category_theory.differential_object.iso_app f.symm = (category_theory.differential_object.iso_app f).symm
source
@[simp]
theorem category_theory.differential_object.iso_app_trans {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y Z : category_theory.differential_object C} (f : X ≅ Y) (g : Y ≅ Z) :
category_theory.differential_object.iso_app (f ≪≫ g) = category_theory.differential_object.iso_app f ≪≫ category_theory.differential_object.iso_app g
source
@[simp]
theorem category_theory.differential_object.mk_iso_hom_f {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y : category_theory.differential_object C} (f : X.X ≅ Y.X) (hf : X.d ≫ (category_theory.shift_functor C 1).map f.hom = f.hom ≫ Y.d) :
(category_theory.differential_object.mk_iso f hf).hom.f = f.hom
source
@[simp]
theorem category_theory.differential_object.mk_iso_inv_f {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y : category_theory.differential_object C} (f : X.X ≅ Y.X) (hf : X.d ≫ (category_theory.shift_functor C 1).map f.hom = f.hom ≫ Y.d) :
(category_theory.differential_object.mk_iso f hf).inv.f = f.inv
source
def category_theory.differential_object.mk_iso {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] {X Y : category_theory.differential_object C} (f : X.X ≅ Y.X) (hf : X.d ≫ (category_theory.shift_functor C 1).map f.hom = f.hom ≫ Y.d) :
X ≅ Y

An isomorphism of differential objects can be constructed from an isomorphism of the underlying objects that commutes with the differentials.

Equations
source
@[simp]
theorem category_theory.functor.map_differential_object_obj_d {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (D : Type u') [category_theory.category D] [category_theory.limits.has_zero_morphisms D] [category_theory.has_shift D ℤ] (F : C ⥤ D) (η : category_theory.shift_functor C 1 ⋙ F ⟶ F ⋙ category_theory.shift_functor D 1) (hF : ∀ (c c' : C), F.map 0 = 0) (X : category_theory.differential_object C) :
((category_theory.functor.map_differential_object D F η hF).obj X).d = F.map X.d ≫ η.app X.X
source
@[simp]
theorem category_theory.functor.map_differential_object_map_f {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (D : Type u') [category_theory.category D] [category_theory.limits.has_zero_morphisms D] [category_theory.has_shift D ℤ] (F : C ⥤ D) (η : category_theory.shift_functor C 1 ⋙ F ⟶ F ⋙ category_theory.shift_functor D 1) (hF : ∀ (c c' : C), F.map 0 = 0) (X Y : category_theory.differential_object C) (f : X ⟶ Y) :
((category_theory.functor.map_differential_object D F η hF).map f).f = F.map f.f
source
def category_theory.functor.map_differential_object {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (D : Type u') [category_theory.category D] [category_theory.limits.has_zero_morphisms D] [category_theory.has_shift D ℤ] (F : C ⥤ D) (η : category_theory.shift_functor C 1 ⋙ F ⟶ F ⋙ category_theory.shift_functor D 1) (hF : ∀ (c c' : C), F.map 0 = 0) :
category_theory.differential_object C ⥤ category_theory.differential_object D

A functor F : C ⥤ D which commutes with shift functors on C and D and preserves zero morphisms can be lifted to a functor differential_object C ⥤ differential_object D.

Equations
source
@[simp]
theorem category_theory.functor.map_differential_object_obj_X {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (D : Type u') [category_theory.category D] [category_theory.limits.has_zero_morphisms D] [category_theory.has_shift D ℤ] (F : C ⥤ D) (η : category_theory.shift_functor C 1 ⋙ F ⟶ F ⋙ category_theory.shift_functor D 1) (hF : ∀ (c c' : C), F.map 0 = 0) (X : category_theory.differential_object C) :
((category_theory.functor.map_differential_object D F η hF).obj X).X = F.obj X.X
source
@[protected, instance]
def category_theory.differential_object.has_zero_object (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] :
category_theory.limits.has_zero_object (category_theory.differential_object C)
source
@[protected, instance]
def category_theory.differential_object.concrete_category_of_differential_objects (C : Type (u+1)) [category_theory.large_category C] [category_theory.concrete_category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] :
category_theory.concrete_category (category_theory.differential_object C)
Equations
source
@[protected, instance]
def category_theory.differential_object.category_theory.has_forget₂ (C : Type (u+1)) [category_theory.large_category C] [category_theory.concrete_category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] :
category_theory.has_forget₂ (category_theory.differential_object C) C
Equations

The category of differential objects itself has a shift functor.

source
@[simp]
theorem category_theory.differential_object.shift_functor_obj_d (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (n : ℤ) (X : category_theory.differential_object C) :
((category_theory.differential_object.shift_functor C n).obj X).d = (category_theory.shift_functor C n).map X.d ≫ (category_theory.shift_comm X.X 1 n).hom
source
@[simp]
theorem category_theory.differential_object.shift_functor_obj_X (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (n : ℤ) (X : category_theory.differential_object C) :
((category_theory.differential_object.shift_functor C n).obj X).X = (category_theory.shift_functor C n).obj X.X
source
@[simp]
theorem category_theory.differential_object.shift_functor_map_f (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (n : ℤ) (X Y : category_theory.differential_object C) (f : X ⟶ Y) :
((category_theory.differential_object.shift_functor C n).map f).f = (category_theory.shift_functor C n).map f.f
source
noncomputable def category_theory.differential_object.shift_functor (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (n : ℤ) :
category_theory.differential_object C ⥤ category_theory.differential_object C

The shift functor on differential_object C.

Equations
source
@[simp]
theorem category_theory.differential_object.shift_functor_add_hom_app_f (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (m n : ℤ) (X : category_theory.differential_object C) :
((category_theory.differential_object.shift_functor_add C m n).hom.app X).f = ((category_theory.shift_monoidal_functor C ℤ).μ_iso {as := m} {as := n}).inv.app X.X
source
noncomputable def category_theory.differential_object.shift_functor_add (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (m n : ℤ) :
category_theory.differential_object.shift_functor C (m + n) ≅ category_theory.differential_object.shift_functor C m ⋙ category_theory.differential_object.shift_functor C n

The shift functor on differential_object C is additive.

Equations
source
@[simp]
theorem category_theory.differential_object.shift_functor_add_inv_app_f (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (m n : ℤ) (X : category_theory.differential_object C) :
((category_theory.differential_object.shift_functor_add C m n).inv.app X).f = ((category_theory.shift_monoidal_functor C ℤ).to_lax_monoidal_functor.μ {as := m} {as := n}).app X.X
source
noncomputable def category_theory.differential_object.shift_ε (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] :
𝟭 (category_theory.differential_object C) ≅ category_theory.differential_object.shift_functor C 0

The shift by zero is naturally isomorphic to the identity.

Equations
source
@[simp]
theorem category_theory.differential_object.shift_ε_hom_app_f (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (X : category_theory.differential_object C) :
((category_theory.differential_object.shift_ε C).hom.app X).f = (category_theory.shift_monoidal_functor C ℤ).to_lax_monoidal_functor.ε.app X.X
source
@[simp]
theorem category_theory.differential_object.shift_ε_inv_app_f (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] (X : category_theory.differential_object C) :
((category_theory.differential_object.shift_ε C).inv.app X).f = (category_theory.shift_monoidal_functor C ℤ).ε_iso.inv.app X.X
source
@[protected, instance]
noncomputable def category_theory.differential_object.int.category_theory.has_shift (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.has_shift C ℤ] :
category_theory.has_shift (category_theory.differential_object C) ℤ
Equations