Additive structures on graded objects

This file equips Mathlib's canonical category CategoryTheory.GradedObject β C with the pointwise preadditive, linear, and abelian structures inherited from C, with morphisms added and scaled componentwise (CategoryTheory.GradedObject.add_apply, CategoryTheory.GradedObject.smul_apply). It also records that the canonical reindexing and shift functors are additive and linear, and that totalizing a graded object, X ↦ ∐ᵢ Xᵢ, is left adjoint to the constant graded object (TauCeti.gradedObjectTotalAdjunction).

Mathlib provides the category of graded objects and its grading shift, but not these structures. They are what homological algebra needs: Ext groups, and hence the graded Ext-Euler form χ_q(X, Y) = ∑ n, j, (-1)ⁿ q⁻ʲ dim Extⁿ(X, Y{j}), are only defined in an abelian category, and the q-Euler form uses the grading shift as a linear autoequivalence. With these instances, categories of graded objects such as graded vector spaces GradedObjectWithShift (-1) (ModuleCat k) become examples of the graded Ext-Euler formalism.

@[instance_reducible]

instance TauCeti.gradedObjectHomAdd {C : Type u} [CategoryTheory.Category.{v, u} C] (β : Type w) [CategoryTheory.Preadditive C] (X Y : CategoryTheory.GradedObject β C) : Add (X ⟶ Y)

Pointwise addition of morphisms of graded objects.

Equations

• TauCeti.gradedObjectHomAdd β X Y = { add := fun (f g : X ⟶ Y) (i : β) => f i + g i }

@[instance_reducible]

instance TauCeti.gradedObjectHomNeg {C : Type u} [CategoryTheory.Category.{v, u} C] (β : Type w) [CategoryTheory.Preadditive C] (X Y : CategoryTheory.GradedObject β C) : Neg (X ⟶ Y)

Pointwise negation of morphisms of graded objects.

Equations

• TauCeti.gradedObjectHomNeg β X Y = { neg := fun (f : X ⟶ Y) (i : β) => -f i }

@[instance_reducible]

instance TauCeti.gradedObjectPreadditive {C : Type u} [CategoryTheory.Category.{v, u} C] (β : Type w) [CategoryTheory.Preadditive C] : CategoryTheory.Preadditive (CategoryTheory.GradedObject β C)

The pointwise preadditive structure on Mathlib's category of graded objects.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.gradedObjectLinear {C : Type u} [CategoryTheory.Category.{v, u} C] (β : Type w) (R : Type t) [Semiring R] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] : CategoryTheory.Linear R (CategoryTheory.GradedObject β C)

The pointwise linear structure on Mathlib's category of graded objects.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.GradedObject.add_apply {C : Type u} [Category.{v, u} C] {β : Type w} [Preadditive C] {X Y : GradedObject β C} (f g : X ⟶ Y) (i : β) : (f + g) i = f i + g i

Morphisms of graded objects are added componentwise.

@[simp]

theorem CategoryTheory.GradedObject.neg_apply {C : Type u} [Category.{v, u} C] {β : Type w} [Preadditive C] {X Y : GradedObject β C} (f : X ⟶ Y) (i : β) : (-f) i = -f i

Morphisms of graded objects are negated componentwise.

@[simp]

theorem CategoryTheory.GradedObject.sub_apply {C : Type u} [Category.{v, u} C] {β : Type w} [Preadditive C] {X Y : GradedObject β C} (f g : X ⟶ Y) (i : β) : (f - g) i = f i - g i

Morphisms of graded objects are subtracted componentwise.

@[simp]

theorem CategoryTheory.GradedObject.smul_apply {C : Type u} [Category.{v, u} C] {β : Type w} {R : Type t} [Semiring R] [Preadditive C] [Linear R C] {X Y : GradedObject β C} (r : R) (f : X ⟶ Y) (i : β) : (r • f) i = r • f i

Morphisms of graded objects are scaled componentwise.

instance TauCeti.gradedObjectComapAdditive {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u_1} {J : Type u_2} [CategoryTheory.Preadditive C] (f : J → I) : (CategoryTheory.GradedObject.comap C f).Additive

Reindexing a graded object is additive.

instance TauCeti.gradedObjectComapLinear {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u_1} {J : Type u_2} [CategoryTheory.Preadditive C] (R : Type t) [Semiring R] [CategoryTheory.Linear R C] (f : J → I) : CategoryTheory.Functor.Linear R (CategoryTheory.GradedObject.comap C f)

Reindexing a graded object is linear.

instance TauCeti.gradedObjectShiftFunctorAdditive {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} [AddCommGroup β] [CategoryTheory.Preadditive C] (s : β) (n : ℤ) : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift s C) n).Additive

Mathlib's canonical shift functor on graded objects is additive.

instance TauCeti.gradedObjectShiftFunctorLinear {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} [AddCommGroup β] [CategoryTheory.Preadditive C] (R : Type t) [Semiring R] [CategoryTheory.Linear R C] (s : β) (n : ℤ) : CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift s C) n)

Mathlib's canonical shift functor on graded objects is linear.

instance TauCeti.gradedObjectShiftEquivFunctorAdditive {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} [AddCommGroup β] [CategoryTheory.Preadditive C] (s : β) (n : ℤ) : (CategoryTheory.shiftEquiv (CategoryTheory.GradedObjectWithShift s C) n).functor.Additive

The functor of Mathlib's canonical shift autoequivalence on graded objects is additive. This is gradedObjectShiftFunctorAdditive, restated because shiftEquiv' is not reducible, so instance search does not see that its functor is shiftFunctor.

instance TauCeti.gradedObjectShiftEquivFunctorLinear {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} [AddCommGroup β] [CategoryTheory.Preadditive C] (R : Type t) [Semiring R] [CategoryTheory.Linear R C] (s : β) (n : ℤ) : CategoryTheory.Functor.Linear R (CategoryTheory.shiftEquiv (CategoryTheory.GradedObjectWithShift s C) n).functor

The functor of Mathlib's canonical shift autoequivalence on graded objects is linear. This is gradedObjectShiftFunctorLinear, restated because shiftEquiv' is not reducible, so instance search does not see that its functor is shiftFunctor.

instance TauCeti.gradedObjectHasFiniteLimits {C : Type u} [CategoryTheory.Category.{v, u} C] (β : Type w) [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.GradedObject β C)

Graded objects in a category with finite limits have finite limits, computed pointwise.

@[instance_reducible]

noncomputable instance TauCeti.gradedObjectAbelian {C : Type u} [CategoryTheory.Category.{v, u} C] (β : Type w) [CategoryTheory.Abelian C] : CategoryTheory.Abelian (CategoryTheory.GradedObject β C)

The pointwise abelian structure on Mathlib's category of graded objects.

Equations

• TauCeti.gradedObjectAbelian β = CategoryTheory.abelianOfEquivalence (CategoryTheory.piEquivalenceFunctorDiscrete β C).functor

noncomputable def TauCeti.gradedObjectTotalAdjunction (β : Type) (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] : CategoryTheory.GradedObject.total β C ⊣ CategoryTheory.Functor.pi' fun (x : β) => CategoryTheory.Functor.id C

Totalizing a graded object is left adjoint to the constant graded object: morphisms ∐ᵢ Xᵢ ⟶ Y correspond to families of morphisms Xᵢ ⟶ Y.

Equations

• One or more equations did not get rendered due to their size.