mathlib docs: category_theory.differential

@[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 : 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.

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) :

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] :

category_theory.differential_object C → category_theory.differential_object C → Type v

f : X.X ⟶ Y.X
comm' : X.d ≫ (category_theory.shift C ^ 1).functor.map c.f = c.f ≫ Y.d . "obviously"

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

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

category_theory.differential_object.hom.id X = {f := 𝟙 X.X, comm' := _}

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} :

X.hom Y → Y.hom Z → X.hom Z

The composition of morphisms of differential objects.

Equations

f.comp g = {f := f.f ≫ g.f, comm' := _}

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

@[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

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' := _}

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

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

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' := _}

source

@[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

@[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

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' := _}

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

@[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)

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 := _}}

source

@[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

category_theory.differential_object.concrete_category_of_differential_objects C = category_theory.concrete_category.mk (category_theory.differential_object.forget C ⋙ category_theory.forget C)

source

@[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

category_theory.differential_object.category_theory.has_forget₂ C = {forget₂ := category_theory.differential_object.forget C _inst_4, forget_comp := _}

mathlib documentation

Differential objects in a category.