Differential objects in a category. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_functor C 1).obj self.X
- d_squared' : self.d ≫ (category_theory.shift_functor C 1).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.
Instances for category_theory.differential_object
- category_theory.differential_object.has_sizeof_inst
- category_theory.differential_object.category_of_differential_objects
- category_theory.differential_object.has_zero_morphisms
- category_theory.differential_object.has_zero_object
- category_theory.differential_object.concrete_category_of_differential_objects
- category_theory.differential_object.category_theory.has_forget₂
- category_theory.differential_object.int.category_theory.has_shift
@[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_functor C 1).map self.f = self.f ≫ Y.d . "obviously"
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
@[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_functor C 1).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) :
@[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 ℤ] :
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) :
@[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) :
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' := _}
Instances for category_theory.differential_object.forget
@[protected, instance]
@[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 ℤ] :
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]
@[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.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
@[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
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
- category_theory.differential_object.mk_iso f hf = {hom := {f := f.hom, comm' := hf}, inv := {f := f.inv, comm' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[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) :
@[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) :
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) :
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_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) :
@[protected, instance]
@[protected, instance]
@[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 ℤ] :
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 ℤ]
(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
@[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
@[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
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 : ℤ) :
The shift functor on differential_object C.
Equations
- category_theory.differential_object.shift_functor C n = {obj := λ (X : category_theory.differential_object C), {X := (category_theory.shift_functor C n).obj X.X, d := (category_theory.shift_functor C n).map X.d ≫ (category_theory.shift_comm X.X 1 n).hom, d_squared' := _}, map := λ (X Y : category_theory.differential_object C) (f : X ⟶ Y), {f := (category_theory.shift_functor C n).map f.f, comm' := _}, map_id' := _, map_comp' := _}
@[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_functor_add C m n).hom.app X.X
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 : ℤ) :
The shift functor on differential_object C is additive.
@[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_functor_add C m n).inv.app X.X
@[simp]
noncomputable
def
category_theory.differential_object.shift_zero
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C ℤ] :
The shift by zero is naturally isomorphic to the identity.
@[simp]
@[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 ℤ] :
Equations
- category_theory.differential_object.int.category_theory.has_shift C = category_theory.has_shift_mk (category_theory.differential_object C) ℤ {F := category_theory.differential_object.shift_functor C _inst_3, zero := category_theory.differential_object.shift_zero C _inst_3, add := category_theory.differential_object.shift_functor_add C _inst_3, assoc_hom_app := _, zero_add_hom_app := _, add_zero_hom_app := _}