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.
- X : C
- d : c.X ⟶ (category_theory.shift C ^ 1).functor.obj c.X
- d_squared' : c.d ≫ (category_theory.shift C ^ 1).functor.map c.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
.
A morphism of differential objects is a morphism commuting with the differentials.
The identity morphism of a differential object.
The composition of morphisms of differential objects.
Equations
- category_theory.differential_object.category_of_differential_objects = {to_category_struct := {to_has_hom := {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' := _}
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' := _}
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' := _}
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' := _}
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' := _}
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 := _}}
Equations
The category of differential objects itself has a shift functor.
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' := _}
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' := _}
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' := _}
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' := _}
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' := _}
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' := _}
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' := _}
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' := _}
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' := _}
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' := _}}