The k-linear coyoneda functor is homological, and its shift sequence

The companion of Triangulated/LinearYoneda.lean in the other variable. (linearCoyoneda k C).obj A : C ⥤ ModuleCat k is Hom(A, −), and this file gives it IsHomological and ShiftSequence ℤ, so a distinguished triangle in the second argument of Hom also produces a long exact sequence of k-modules.

Why both variables are needed, and why only this one is cheap

A Hom-built Euler form χ(X, Y) = Σᵢ (-1)ⁱ dimₖ Hom(X, Y⟦i⟧) has to be additive in each argument separately before it descends to K₀ C ⊗ K₀ C. LinearYoneda.lean gives the long exact sequence when the triangle is in the first argument; nothing there says anything about the second. This file is that missing half.

The two halves are not symmetric, and the asymmetry is worth stating because it shows up as a hypothesis difference downstream:

• linearYoneda is contravariant, so its source is Cᵒᵖ. Its shift sequence has to move the shift across op, which is what drags in Triangulated/LinearOpposite.lean and, with it, the hypothesis [∀ n, (shiftFunctor C n).Linear k].
• linearCoyoneda is covariant, with source C. Its shift sequence is Functor.ShiftSequence.tautological — literally shiftFunctor C n ⋙ F — so no opposite-category linearity and no shift-linearity hypothesis is required on this side at all.

Mathlib has the preadditiveCoyoneda counterparts of both instances (Triangulated/Yoneda.lean); as with linearYoneda, they cannot serve a k-dimension count because AddCommGrpCat carries no k. The proof here is Mathlib's with ShortComplex.ab_exact_iff replaced by ShortComplex.moduleCat_exact_iff, the same substitution LinearYoneda.lean makes.

What this file does not provide

No Euler form, and no finiteness. Having the long exact sequence in both variables is not having Σᵢ (-1)ⁱ dimₖ Hom(X, Y⟦i⟧): that needs each term finite-dimensional and the sum finitely supported, both of which are supplied data assembled elsewhere.

instance CategoryTheory.Triangulated.linearCoyoneda_isHomological {k : Type u_1} [Ring k] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (A : Cᵒᵖ) : ((linearCoyoneda k C).obj A).IsHomological

The k-linear coyoneda functor is homological.

The ModuleCat k counterpart of Mathlib's instance for preadditiveCoyoneda. As on the Yoneda side the k-action plays no part in the proof, because Triangle.coyoneda_exact₂ is a statement about morphisms in C.

@[implicit_reducible]

noncomputable instance CategoryTheory.Triangulated.linearCoyonedaShiftSequence {k : Type u_1} [Ring k] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (A : Cᵒᵖ) : ((linearCoyoneda k C).obj A).ShiftSequence ℤ

The shifted Hom-groups in the second variable, assembled.

Tautological, and that is the point: (linearCoyoneda k C).obj A is covariant with source C, so shifting the argument is just precomposition with shiftFunctor C n. Contrast LinearYoneda.lean's instance, which has to move a shift across op and needs (shiftFunctor C n).Linear k to do it.

Equations

• CategoryTheory.Triangulated.linearCoyonedaShiftSequence A = CategoryTheory.Functor.ShiftSequence.tautological ((CategoryTheory.linearCoyoneda k C).obj A) ℤ

The long exact sequence

Named specializations of Mathlib's homology-sequence API, matching LinearYoneda.lean's. Unlike those, these are stated for a triangle in C directly — the coyoneda functor's source is C, so no op-triangle is involved.

theorem CategoryTheory.Triangulated.linearCoyoneda_homologySequence_exact₂ {k : Type u_1} [Ring k] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (A : Cᵒᵖ) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (n₀ : ℤ) : { X₁ := (((linearCoyoneda k C).obj A).shift n₀).obj T.obj₁, X₂ := (((linearCoyoneda k C).obj A).shift n₀).obj T.obj₂, X₃ := (((linearCoyoneda k C).obj A).shift n₀).obj T.obj₃, f := (((linearCoyoneda k C).obj A).shift n₀).map T.mor₁, g := (((linearCoyoneda k C).obj A).shift n₀).map T.mor₂, zero := ⋯ }.Exact

Exactness in the middle.

theorem CategoryTheory.Triangulated.linearCoyoneda_homologySequence_exact₃ {k : Type u_1} [Ring k] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (A : Cᵒᵖ) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : { X₁ := (((linearCoyoneda k C).obj A).shift n₀).obj T.obj₂, X₂ := (((linearCoyoneda k C).obj A).shift n₀).obj T.obj₃, X₃ := (((linearCoyoneda k C).obj A).shift n₁).obj T.obj₁, f := (((linearCoyoneda k C).obj A).shift n₀).map T.mor₂, g := ((linearCoyoneda k C).obj A).homologySequenceδ T n₀ n₁ h, zero := ⋯ }.Exact

Exactness at the connecting map's source.

theorem CategoryTheory.Triangulated.linearCoyoneda_homologySequence_exact₁ {k : Type u_1} [Ring k] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (A : Cᵒᵖ) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : { X₁ := (((linearCoyoneda k C).obj A).shift n₀).obj T.obj₃, X₂ := (((linearCoyoneda k C).obj A).shift n₁).obj T.obj₁, X₃ := (((linearCoyoneda k C).obj A).shift n₁).obj T.obj₂, f := ((linearCoyoneda k C).obj A).homologySequenceδ T n₀ n₁ h, g := (((linearCoyoneda k C).obj A).shift n₁).map T.mor₁, zero := ⋯ }.Exact

Exactness at the connecting map's target.