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.
The differential of a differential object.
The differential
dsatisfies thatd² = 0.
@[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.
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
theorem
CategoryTheory.DifferentialObject.Hom.ext_iff
{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}
:
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)
:
@[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 := ⋯ }
@[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)
:
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.
@[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)
:
instance
CategoryTheory.DifferentialObject.categoryOfDifferentialObjects
{S : Type u_1}
[AddMonoidWithOne S]
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
:
Equations
- One or more equations did not get rendered due to their size.
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)
:
theorem
CategoryTheory.DifferentialObject.ext_iff
{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}
:
@[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)
:
@[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)
:
@[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.
instance
CategoryTheory.DifferentialObject.forget_faithful
(S : Type u_1)
[AddMonoidWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
:
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}
:
@[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]
:
Equations
- One or more equations did not get rendered due to their size.
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)
:
An isomorphism of differential objects gives an isomorphism of the underlying objects.
@[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_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_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)
:
An isomorphism of differential objects can be constructed from an isomorphism of the underlying objects that commutes with the differentials.
@[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.
@[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✝)
:
@[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)
:
@[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)
:
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)
Equations
- CategoryTheory.DifferentialObject.hasForgetOfDifferentialObjects S C = { forget := (CategoryTheory.DifferentialObject.forget S C).comp (CategoryTheory.forget C), forget_faithful := ⋯ }
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 := ⋯ }
@[reducible, inline]
abbrev
CategoryTheory.DifferentialObject.HomSubtype
(S : Type u_1)
[AddMonoidWithOne S]
(C : Type (u + 1))
[LargeCategory C]
[Limits.HasZeroMorphisms C]
{FC : C → C → Type u_2}
{CC : C → Type u_3}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasShift C S]
(X Y : DifferentialObject S C)
:
Type u_2
The type of C-morphisms that can be lifted back to morphisms in the category DifferentialObject.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.DifferentialObject.instFunLikeHomSubtypeObj
(S : Type u_1)
[AddMonoidWithOne S]
(C : Type (u + 1))
[LargeCategory C]
[Limits.HasZeroMorphisms C]
{FC : C → C → Type u_2}
{CC : C → Type u_3}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasShift C S]
(X Y : DifferentialObject S C)
:
FunLike (HomSubtype S C X Y) (CC X.obj) (CC Y.obj)
Equations
- CategoryTheory.DifferentialObject.instFunLikeHomSubtypeObj S C X Y = { coe := fun (f : CategoryTheory.DifferentialObject.HomSubtype S C X Y) => ⇑↑f, coe_injective' := ⋯ }
instance
CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects
(S : Type u_1)
[AddMonoidWithOne S]
(C : Type (u + 1))
[LargeCategory C]
[Limits.HasZeroMorphisms C]
{FC : C → C → Type u_2}
{CC : C → Type u_3}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasShift C S]
:
ConcreteCategory (DifferentialObject S C) (HomSubtype S C)
Equations
- One or more equations did not get rendered due to their size.
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.
@[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)
:
@[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✝)
:
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)
:
The shift functor on DifferentialObject S C is additive.
Equations
- One or more equations did not get rendered due to their size.
@[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)
:
@[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)
:
def
CategoryTheory.DifferentialObject.shiftZero
{S : Type u_1}
[AddCommGroupWithOne S]
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroMorphisms C]
[HasShift C S]
:
The shift by zero is naturally isomorphic to the identity.
Equations
- One or more equations did not get rendered due to their size.
@[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)
:
@[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)
:
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.