CategoryTheory.DifferentialObject.ext
theorem CategoryTheory.DifferentialObject.ext :
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
{A B : CategoryTheory.DifferentialObject S C} {f g : A ⟶ B}, autoParam (f.f = g.f) _auto✝ → f = g
This theorem, named `CategoryTheory.DifferentialObject.ext`, states that for any type `S` equipped with an `AddMonoidWithOne` structure, and any category `C` that has zero morphisms and a shift structure with respect to `S`, if `A` and `B` are differential objects in `C` with respect to `S`, then any two morphisms `f` and `g` from `A` to `B` are equal if their underlying morphisms `f.f` and `g.f` are equal. The equality of `f.f` and `g.f` is provided as an automatically inferred parameter (`autoParam`) with a certain tactic (`_auto✝`).
More concisely: If `S` is a type with an `AddMonoidWithOne` structure, and `C` is a category with zero morphisms and a shift structure with respect to `S`, then for any differential objects `A` and `B` in `C` with respect to `S`, any two morphisms `f` and `g` from `A` to `B` are equal if their underlying morphisms are equal.
|
CategoryTheory.DifferentialObject.Hom.ext
theorem CategoryTheory.DifferentialObject.Hom.ext :
∀ {S : Type u_1} {inst : AddMonoidWithOne S} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
{inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.HasShift C S}
{X Y : CategoryTheory.DifferentialObject S C} (x y : X.Hom Y), x.f = y.f → x = y
This theorem states that in the category of differential objects over a category `C` with zero morphisms and a shift operation, and with coefficients in an additive monoid with one `S`, any two morphisms `x` and `y` between the same differential objects `X` and `Y` are equal if their underlying morphisms `x.f` and `y.f` are equal.
More concisely: In the category of differential objects over a category with zero morphisms and a shift operation, and with coefficients in an additive monoid, any two morphisms between the same objects with equal underlying morphisms are equal.
|
CategoryTheory.DifferentialObject.d_squared
theorem CategoryTheory.DifferentialObject.d_squared :
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
(self : CategoryTheory.DifferentialObject S C),
CategoryTheory.CategoryStruct.comp self.d ((CategoryTheory.shiftFunctor C 1).map self.d) = 0
This theorem states that for any differential object in a category, the differential operator `d` is nilpotent of degree 2. More specifically, given any type `S` that is an additive monoid with a distinguished one element, any type `C` that forms a category with zero morphisms, and any shift functor on `C` using `S`, for any differential object `self` in this context, if you apply the differential operator `d` twice to `self` (in the category-theoretic sense of composition), you get the zero morphism. This mirrors the mathematical property that the differential of the differential of a differential form is zero (often written as `d² = 0` in differential geometry).
More concisely: For any differential object in a category with shift functor, the differential operator's composition is equal to the zero morphism. (d ^ 2 = 0)
|