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 : obj ⟶ obj⟦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.
structure
CategoryTheory.DifferentialObject
(S : Type u_1)
[AddMonoidWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
:
Type (max u v)
A differential object in a category with zero morphisms and a shift is
an object obj equipped with
a morphism d : obj ⟶ obj⟦1⟧, such that d^2 = 0.
- obj : C
The underlying object of a differential object.
- d : self.obj ⟶ (CategoryTheory.shiftFunctor C 1).obj self.obj
The differential of a differential object.
- d_squared : CategoryStruct.comp self.d ((CategoryTheory.shiftFunctor C 1).map self.d) = 0
The differential
dsatisfies thatd² = 0.
Instances For
@[simp]
theorem
CategoryTheory.DifferentialObject.d_squared_assoc
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(self : DifferentialObject S C)
{Z : C}
(h : (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj self.obj) ⟶ Z)
:
CategoryStruct.comp self.d (CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.d) h) = CategoryStruct.comp 0 h
structure
CategoryTheory.DifferentialObject.Hom
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(X Y : DifferentialObject S C)
:
Type v
A morphism of differential objects is a morphism commuting with the differentials.
- f : X.obj ⟶ Y.obj
The morphism between underlying objects of the two differentiable objects.
- comm : CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map self.f) = CategoryStruct.comp self.f Y.d
Instances For
theorem
CategoryTheory.DifferentialObject.Hom.ext
{S : Type u_1}
{inst✝ : AddMonoidWithOne S}
{C : Type u}
{inst✝¹ : Category.{v, u} C}
{inst✝² : Limits.HasZeroMorphisms C}
{inst✝³ : HasShift C S}
{X Y : DifferentialObject S C}
{x y : X.Hom Y}
(f : x.f = y.f)
:
x = y
@[simp]
theorem
CategoryTheory.DifferentialObject.Hom.comm_assoc
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y : DifferentialObject S C}
(self : X.Hom Y)
{Z : C}
(h : (CategoryTheory.shiftFunctor C 1).obj Y.obj ⟶ Z)
:
CategoryStruct.comp X.d (CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.f) h) = CategoryStruct.comp self.f (CategoryStruct.comp Y.d h)
def
CategoryTheory.DifferentialObject.Hom.id
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(X : DifferentialObject S C)
:
X.Hom X
The identity morphism of a differential object.
Equations
- CategoryTheory.DifferentialObject.Hom.id X = { f := CategoryTheory.CategoryStruct.id X.obj, comm := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.DifferentialObject.Hom.id_f
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(X : DifferentialObject S C)
:
(id X).f = CategoryStruct.id X.obj
def
CategoryTheory.DifferentialObject.Hom.comp
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y Z : DifferentialObject S C}
(f : X.Hom Y)
(g : Y.Hom Z)
:
X.Hom Z
The composition of morphisms of differential objects.
Equations
- f.comp g = { f := CategoryTheory.CategoryStruct.comp f.f g.f, comm := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.DifferentialObject.Hom.comp_f
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y Z : DifferentialObject S C}
(f : X.Hom Y)
(g : Y.Hom Z)
:
(f.comp g).f = CategoryStruct.comp f.f g.f
instance
CategoryTheory.DifferentialObject.categoryOfDifferentialObjects
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
:
theorem
CategoryTheory.DifferentialObject.ext
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{A B : DifferentialObject S C}
{f g : A ⟶ B}
(w : f.f = g.f := by aesop_cat)
:
f = g
@[simp]
theorem
CategoryTheory.DifferentialObject.id_f
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(X : DifferentialObject S C)
:
(CategoryStruct.id X).f = CategoryStruct.id X.obj
@[simp]
theorem
CategoryTheory.DifferentialObject.comp_f
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y Z : DifferentialObject S C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
(CategoryStruct.comp f g).f = CategoryStruct.comp f.f g.f
@[simp]
theorem
CategoryTheory.DifferentialObject.eqToHom_f
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y : DifferentialObject S C}
(h : X = Y)
:
def
CategoryTheory.DifferentialObject.forget
(S : Type u_1)
[AddMonoidWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
:
Functor (DifferentialObject S C) C
The forgetful functor taking a differential object to its underlying object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.DifferentialObject.forget_faithful
(S : Type u_1)
[AddMonoidWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
:
(forget S C).Faithful
instance
CategoryTheory.DifferentialObject.instZeroHom
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
[(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms]
{X Y : DifferentialObject S C}
:
Equations
- CategoryTheory.DifferentialObject.instZeroHom = { zero := { f := 0, comm := ⋯ } }
@[simp]
theorem
CategoryTheory.DifferentialObject.zero_f
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
[(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms]
(P Q : DifferentialObject S C)
:
instance
CategoryTheory.DifferentialObject.hasZeroMorphisms
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
[(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms]
:
def
CategoryTheory.DifferentialObject.isoApp
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y : DifferentialObject S C}
(f : X ≅ Y)
:
X.obj ≅ Y.obj
An isomorphism of differential objects gives an isomorphism of the underlying objects.
Equations
- CategoryTheory.DifferentialObject.isoApp f = { hom := f.hom.f, inv := f.inv.f, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.DifferentialObject.isoApp_hom
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y : DifferentialObject S C}
(f : X ≅ Y)
:
@[simp]
theorem
CategoryTheory.DifferentialObject.isoApp_inv
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y : DifferentialObject S C}
(f : X ≅ Y)
:
@[simp]
theorem
CategoryTheory.DifferentialObject.isoApp_refl
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(X : DifferentialObject S C)
:
@[simp]
theorem
CategoryTheory.DifferentialObject.isoApp_symm
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y : DifferentialObject S C}
(f : X ≅ Y)
:
@[simp]
theorem
CategoryTheory.DifferentialObject.isoApp_trans
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y Z : DifferentialObject S C}
(f : X ≅ Y)
(g : Y ≅ Z)
:
def
CategoryTheory.DifferentialObject.mkIso
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y : DifferentialObject S C}
(f : X.obj ≅ Y.obj)
(hf : CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryStruct.comp 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
- CategoryTheory.DifferentialObject.mkIso f hf = { hom := { f := f.hom, comm := hf }, inv := { f := f.inv, comm := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.DifferentialObject.mkIso_hom_f
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y : DifferentialObject S C}
(f : X.obj ≅ Y.obj)
(hf : CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryStruct.comp f.hom Y.d)
:
@[simp]
theorem
CategoryTheory.DifferentialObject.mkIso_inv_f
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
{X Y : DifferentialObject S C}
(f : X.obj ≅ Y.obj)
(hf : CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryStruct.comp f.hom Y.d)
:
def
CategoryTheory.Functor.mapDifferentialObject
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(D : Type u')
[Category.{v', u'} D]
[Limits.HasZeroMorphisms D]
[HasShift D S]
(F : Functor C D)
(η : (shiftFunctor C 1).comp F ⟶ F.comp (shiftFunctor D 1))
(hF : ∀ (c c' : C), F.map 0 = 0)
:
Functor (DifferentialObject S C) (DifferentialObject S 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 DifferentialObject S C ⥤ DifferentialObject S D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapDifferentialObject_obj_obj
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(D : Type u')
[Category.{v', u'} D]
[Limits.HasZeroMorphisms D]
[HasShift D S]
(F : Functor C D)
(η : (shiftFunctor C 1).comp F ⟶ F.comp (shiftFunctor D 1))
(hF : ∀ (c c' : C), F.map 0 = 0)
(X : DifferentialObject S C)
:
((mapDifferentialObject D F η hF).obj X).obj = F.obj X.obj
@[simp]
theorem
CategoryTheory.Functor.mapDifferentialObject_obj_d
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(D : Type u')
[Category.{v', u'} D]
[Limits.HasZeroMorphisms D]
[HasShift D S]
(F : Functor C D)
(η : (shiftFunctor C 1).comp F ⟶ F.comp (shiftFunctor D 1))
(hF : ∀ (c c' : C), F.map 0 = 0)
(X : DifferentialObject S C)
:
((mapDifferentialObject D F η hF).obj X).d = CategoryStruct.comp (F.map X.d) (η.app X.obj)
@[simp]
theorem
CategoryTheory.Functor.mapDifferentialObject_map_f
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(D : Type u')
[Category.{v', u'} D]
[Limits.HasZeroMorphisms D]
[HasShift D S]
(F : Functor C D)
(η : (shiftFunctor C 1).comp F ⟶ F.comp (shiftFunctor D 1))
(hF : ∀ (c c' : C), F.map 0 = 0)
{X✝ Y✝ : DifferentialObject S C}
(f : X✝ ⟶ Y✝)
:
((mapDifferentialObject D F η hF).map f).f = F.map f.f
instance
CategoryTheory.DifferentialObject.hasZeroObject
(S : Type u_1)
[AddMonoidWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
[(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms]
:
instance
CategoryTheory.DifferentialObject.hasForgetOfDifferentialObjects
(S : Type u_1)
[AddMonoidWithOne S]
(C : Type (u + 1))
[LargeCategory C]
[HasForget C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
:
HasForget (DifferentialObject S C)
instance
CategoryTheory.DifferentialObject.instHasForget₂
(S : Type u_1)
[AddMonoidWithOne S]
(C : Type (u + 1))
[LargeCategory C]
[HasForget C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
:
HasForget₂ (DifferentialObject S C) C
Equations
- CategoryTheory.DifferentialObject.instHasForget₂ S C = { forget₂ := CategoryTheory.DifferentialObject.forget S C, forget_comp := ⋯ }
The category of differential objects itself has a shift functor.
def
CategoryTheory.DifferentialObject.shiftFunctor
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(n : S)
:
Functor (DifferentialObject S C) (DifferentialObject S C)
The shift functor on DifferentialObject S C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.DifferentialObject.shiftFunctor_obj_obj
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(n : S)
(X : DifferentialObject S C)
:
((shiftFunctor C n).obj X).obj = (CategoryTheory.shiftFunctor C n).obj X.obj
@[simp]
theorem
CategoryTheory.DifferentialObject.shiftFunctor_obj_d
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(n : S)
(X : DifferentialObject S C)
:
((shiftFunctor C n).obj X).d = CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map X.d) (shiftComm X.obj 1 n).hom
@[simp]
theorem
CategoryTheory.DifferentialObject.shiftFunctor_map_f
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(n : S)
{X✝ Y✝ : DifferentialObject S C}
(f : X✝ ⟶ Y✝)
:
((shiftFunctor C n).map f).f = (CategoryTheory.shiftFunctor C n).map f.f
def
CategoryTheory.DifferentialObject.shiftFunctorAdd
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(m n : S)
:
shiftFunctor C (m + n) ≅ (shiftFunctor C m).comp (shiftFunctor C n)
The shift functor on DifferentialObject S C is additive.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.DifferentialObject.shiftFunctorAdd_inv_app_f
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(m n : S)
(X : DifferentialObject S C)
:
((shiftFunctorAdd C m n).inv.app X).f = (CategoryTheory.shiftFunctorAdd C m n).inv.app X.obj
@[simp]
theorem
CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(m n : S)
(X : DifferentialObject S C)
:
((shiftFunctorAdd C m n).hom.app X).f = (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj
def
CategoryTheory.DifferentialObject.shiftZero
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
:
shiftFunctor C 0 ≅ Functor.id (DifferentialObject S C)
The shift by zero is naturally isomorphic to the identity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.DifferentialObject.shiftZero_inv_app_f
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(X : DifferentialObject S C)
:
((shiftZero C).inv.app X).f = (shiftFunctorZero C S).inv.app X.obj
@[simp]
theorem
CategoryTheory.DifferentialObject.shiftZero_hom_app_f
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
(X : DifferentialObject S C)
:
((shiftZero C).hom.app X).f = (shiftFunctorZero C S).hom.app X.obj
instance
CategoryTheory.DifferentialObject.instHasShift
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
:
HasShift (DifferentialObject S C) S
Equations
- One or more equations did not get rendered due to their size.