R-linearity of the opposite shift

The R-linear counterparts of the (shiftFunctor Cᵒᵖ n).Additive instance (Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean) and of the scalar behaviour of ShiftedHom.opEquiv (Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean). The opposite shift is defined with the opposite of a pretriangulated category, so this file lives at that definition site; the bare Linear R Cᵒᵖ instance it builds on is in CategoryTheory/Linear/Opposite.lean.

instance CategoryTheory.shiftFunctorOppositeLinear (R : Type u_1) [Semiring R] (C : Type u_2) [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] [HasShift C ℤ] [∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)] (n : ℤ) : Functor.Linear R (shiftFunctor Cᵒᵖ n)

The shift functors on Cᵒᵖ are R-linear when those on C are.

The R-linear counterpart of Mathlib's (shiftFunctor Cᵒᵖ n).Additive instance, and the piece that makes Linear R Cᵒᵖ more than a bare module structure: without it the opposite category is linear but its shift is not known to respect scalars, which is exactly what the k-linear Yoneda shift sequence needs.

Shifting by n on Cᵒᵖ is shifting by -n on C, opposed -- shiftFunctorOpIso witnesses this as an eqToIso of a definitional equality -- so Functor.op_linear applied to shiftFunctor C (-n) is already the instance, and inferInstanceAs is the whole proof.

@[simp]

theorem CategoryTheory.ShiftedHom.opEquiv_symm_smul {C : Type u_1} [Category.{u_3, u_1} C] [HasShift C ℤ] {X Y : C} {R : Type u_2} [Ring R] [Preadditive C] [Linear R C] [∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)] {n : ℤ} (r : R) (x : ShiftedHom (Opposite.op Y) (Opposite.op X) n) : (opEquiv n).symm (r • x) = r • (opEquiv n).symm x

The smul counterpart of ShiftedHom.opEquiv_symm_add.

The set_option mirrors Mathlib's on the additive twin, and is load-bearing for the same reason: dsimp on an opposite-category shift leaves the goal not type-correct at instances transparency, and the rewrite then cannot match.

@[simp]

theorem CategoryTheory.ShiftedHom.opEquiv'_symm_smul {C : Type u_1} [Category.{u_3, u_1} C] [HasShift C ℤ] {X Y : C} {R : Type u_2} [Ring R] [Preadditive C] [Linear R C] [∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)] {n a : ℤ} (r : R) (x : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) (a' : ℤ) (h : n + a = a') : (opEquiv' n a a' h).symm (r • x) = r • (opEquiv' n a a' h).symm x

The smul counterpart of ShiftedHom.opEquiv'_symm_add.