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.
@[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)
- X : C
- d : self.X ⟶ (category_theory.shift C ^ 1).functor.obj self.X
- d_squared' : self.d ≫ (category_theory.shift C ^ 1).functor.map self.d = 0 . "obviously"
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.
@[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) :
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) :
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
@[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
- f : X.X ⟶ Y.X
- comm' : X.d ≫ (category_theory.shift C ^ 1).functor.map self.f = self.f ≫ Y.d . "obviously"
A morphism of differential objects is a morphism commuting with the differentials.
@[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) :
@[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 C).functor.obj Y.X ⟶ X') :
@[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) :
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.
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.
@[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) :
@[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] :
Equations
- category_theory.differential_object.category_of_differential_objects = {to_category_struct := {to_quiver := {hom := category_theory.differential_object.hom _inst_3}, id := category_theory.differential_object.hom.id _inst_3, comp := λ (X Y Z : category_theory.differential_object C) (f : X ⟶ Y) (g : Y ⟶ Z), category_theory.differential_object.hom.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}
@[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) :
@[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) :
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] :
The forgetful functor taking a differential object to its underlying object.
Equations
- category_theory.differential_object.forget C = {obj := λ (X : category_theory.differential_object C), X.X, map := λ (X Y : category_theory.differential_object C) (f : X ⟶ Y), f.f, map_id' := _, map_comp' := _}
@[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] :
Equations
- category_theory.differential_object.has_zero_morphisms C = {has_zero := λ (X Y : category_theory.differential_object C), {zero := {f := 0, comm' := _}}, comp_zero' := _, zero_comp' := _}
@[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) :
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) :
An isomorphism of differential objects gives an isomorphism of the underlying objects.
Equations
- category_theory.differential_object.iso_app f = {hom := f.hom.f, inv := f.inv.f, hom_inv_id' := _, inv_hom_id' := _}
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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 C).functor ⋙ F ⟶ F ⋙ (category_theory.shift D).functor)
(hF : ∀ (c c' : C), F.map 0 = 0)
(X : category_theory.differential_object C) :
@[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 C).functor ⋙ F ⟶ F ⋙ (category_theory.shift D).functor)
(hF : ∀ (c c' : C), F.map 0 = 0)
(X Y : category_theory.differential_object C)
(f : X ⟶ Y) :
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 C).functor ⋙ F ⟶ F ⋙ (category_theory.shift D).functor)
(hF : ∀ (c c' : C), F.map 0 = 0) :
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
- category_theory.functor.map_differential_object D F η hF = {obj := λ (X : category_theory.differential_object C), {X := F.obj X.X, d := F.map X.d ≫ η.app X.X, d_squared' := _}, map := λ (X Y : category_theory.differential_object C) (f : X ⟶ Y), {f := F.map f.f, comm' := _}, map_id' := _, map_comp' := _}
@[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 C).functor ⋙ F ⟶ F ⋙ (category_theory.shift D).functor)
(hF : ∀ (c c' : C), F.map 0 = 0)
(X : category_theory.differential_object C) :
@[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] :
Equations
- category_theory.differential_object.has_zero_object C = {zero := {X := 0, d := 0, d_squared' := _}, unique_to := λ (X : category_theory.differential_object C), {to_inhabited := {default := {f := 0, comm' := _}}, uniq := _}, unique_from := λ (X : category_theory.differential_object C), {to_inhabited := {default := {f := 0, comm' := _}}, uniq := _}}
@[instance]
@[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] :
Equations
The category of differential objects itself has a shift functor.
@[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]
(X : category_theory.differential_object C) :
((category_theory.differential_object.shift_functor C).obj X).d = (category_theory.shift C ^ 1).functor.map X.d
@[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]
(X : category_theory.differential_object C) :
((category_theory.differential_object.shift_functor C).obj X).X = (category_theory.shift C ^ 1).functor.obj X.X
@[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]
(X Y : category_theory.differential_object C)
(f : X ⟶ Y) :
((category_theory.differential_object.shift_functor C).map f).f = (category_theory.shift C ^ 1).functor.map f.f
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] :
The shift functor on differential_object C.
Equations
- category_theory.differential_object.shift_functor C = {obj := λ (X : category_theory.differential_object C), {X := (category_theory.shift C ^ 1).functor.obj X.X, d := (category_theory.shift C ^ 1).functor.map X.d, d_squared' := _}, map := λ (X Y : category_theory.differential_object C) (f : X ⟶ Y), {f := (category_theory.shift C ^ 1).functor.map f.f, comm' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.differential_object.shift_inverse_obj_d
(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_inverse_obj C ᾰ).d = (category_theory.shift C ^ -1).functor.map ᾰ.d ≫ (category_theory.shift C).unit_inv.app ᾰ.X ≫ (category_theory.shift C).counit_inv.app ᾰ.X
@[simp]
theorem
category_theory.differential_object.shift_inverse_obj_X
(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_inverse_obj C ᾰ).X = (category_theory.shift C ^ -1).functor.obj ᾰ.X
def
category_theory.differential_object.shift_inverse_obj
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
The inverse shift functor on differential C, at the level of objects.
Equations
- category_theory.differential_object.shift_inverse_obj C = λ (X : category_theory.differential_object C), {X := (category_theory.shift C ^ -1).functor.obj X.X, d := (category_theory.shift C ^ -1).functor.map X.d ≫ (category_theory.shift C).unit_inv.app X.X ≫ (category_theory.shift C).counit_inv.app X.X, d_squared' := _}
def
category_theory.differential_object.shift_inverse
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
The inverse shift functor on differential C.
Equations
- category_theory.differential_object.shift_inverse C = {obj := category_theory.differential_object.shift_inverse_obj C _inst_3, map := λ (X Y : category_theory.differential_object C) (f : X ⟶ Y), {f := (category_theory.shift C ^ -1).functor.map f.f, comm' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.differential_object.shift_inverse_map_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 ⟶ Y) :
((category_theory.differential_object.shift_inverse C).map f).f = (category_theory.shift C ^ -1).functor.map f.f
@[simp]
theorem
category_theory.differential_object.shift_inverse_obj_2
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C]
(ᾰ : category_theory.differential_object C) :
@[simp]
theorem
category_theory.differential_object.shift_unit_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_unit C).app X).f = (category_theory.shift C).unit.app X.X
def
category_theory.differential_object.shift_unit
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
The unit for the shift functor on differential_object C.
Equations
- category_theory.differential_object.shift_unit C = {app := λ (X : category_theory.differential_object C), {f := (category_theory.shift C).unit.app X.X, comm' := _}, naturality' := _}
def
category_theory.differential_object.shift_unit_inv
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
The inverse of the unit for the shift functor on differential_object C.
Equations
- category_theory.differential_object.shift_unit_inv C = {app := λ (X : category_theory.differential_object C), {f := (category_theory.shift C).unit_inv.app X.X, comm' := _}, naturality' := _}
@[simp]
theorem
category_theory.differential_object.shift_unit_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) :
@[simp]
def
category_theory.differential_object.shift_unit_iso
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
The unit isomorphism for the shift functor on differential_object C.
Equations
- category_theory.differential_object.shift_unit_iso C = {hom := category_theory.differential_object.shift_unit C _inst_3, inv := category_theory.differential_object.shift_unit_inv C _inst_3, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
def
category_theory.differential_object.shift_counit
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
The counit for the shift functor on differential_object C.
Equations
- category_theory.differential_object.shift_counit C = {app := λ (X : category_theory.differential_object C), {f := (category_theory.shift C).counit.app X.X, comm' := _}, naturality' := _}
@[simp]
theorem
category_theory.differential_object.shift_counit_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_counit C).app X).f = (category_theory.shift C).counit.app X.X
@[simp]
theorem
category_theory.differential_object.shift_counit_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) :
def
category_theory.differential_object.shift_counit_inv
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
The inverse of the counit for the shift functor on differential_object C.
Equations
- category_theory.differential_object.shift_counit_inv C = {app := λ (X : category_theory.differential_object C), {f := (category_theory.shift C).counit_inv.app X.X, comm' := _}, naturality' := _}
@[simp]
def
category_theory.differential_object.shift_counit_iso
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
The counit isomorphism for the shift functor on differential_object C.
Equations
- category_theory.differential_object.shift_counit_iso C = {hom := category_theory.differential_object.shift_counit C _inst_3, inv := category_theory.differential_object.shift_counit_inv C _inst_3, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.differential_object.shift_counit_iso_inv
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
@[instance]
def
category_theory.differential_object.category_theory.has_shift
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
The category of differential objects in C itself has a shift functor.
Equations
- category_theory.differential_object.category_theory.has_shift C = {shift := {functor := category_theory.differential_object.shift_functor C _inst_3, inverse := category_theory.differential_object.shift_inverse C _inst_3, unit_iso := category_theory.differential_object.shift_unit_iso C _inst_3, counit_iso := category_theory.differential_object.shift_counit_iso C _inst_3, functor_unit_iso_comp' := _}}