R-linearity of the opposite category

The R-linear counterparts of instPreadditiveOpposite and Functor.op_additive (Mathlib/CategoryTheory/Preadditive/Opposite.lean): Linear R Cᵒᵖ, Functor.op_linear, and the scalar simp lemmas relating op and unop. Mathlib lacks them at the pin; they are written to be upstreamable to Mathlib/CategoryTheory/Linear/. The linearity of the opposite shift is in CategoryTheory/Triangulated/Opposite/Linear.lean.

@[implicit_reducible]

instance CategoryTheory.homModuleOpposite (R : Type u_1) [Semiring R] (C : Type u_2) [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] (X Y : Cᵒᵖ) : Module R (X ⟶ Y)

The R-module structure on X ⟶ Y in Cᵒᵖ, built over the AddCommGroup that Preadditive Cᵒᵖ already installed.

Split out from linearOpposite rather than inlined so that each axiom can be stated with an explicit show: inside a structure instance the smul field is not yet available to simp, which therefore makes no progress on any of the six goals.

Equations

• CategoryTheory.homModuleOpposite R C X Y = { smul := fun (r : R) (f : X ⟶ Y) => (r • f.unop).op, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

instance CategoryTheory.linearOpposite (R : Type u_1) [Semiring R] (C : Type u_2) [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] : Linear R Cᵒᵖ

The opposite of an R-linear category is R-linear.

The R-linear counterpart of Preadditive Cᵒᵖ, and the missing instance ShiftedHom.opEquiv's smul lemmas and the k-linear Yoneda ShiftSequence both need. Scalars act through unop; the two compatibility fields swap pre- and post-composition, because composition in Cᵒᵖ does.

Equations

• CategoryTheory.linearOpposite R C = { homModule := CategoryTheory.homModuleOpposite R C, smul_comp := ⋯, comp_smul := ⋯ }

@[simp]

theorem CategoryTheory.unop_smul {R : Type u_1} [Semiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] {X Y : Cᵒᵖ} (r : R) (f : X ⟶ Y) : (r • f).unop = r • f.unop

@[simp]

theorem CategoryTheory.op_smul {R : Type u_1} [Semiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] {X Y : C} (r : R) (f : X ⟶ Y) : (r • f).op = r • f.op

instance CategoryTheory.Functor.op_linear {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] [Preadditive C] [Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : Functor C D) [Linear R F] : Linear R F.op

The opposite of an R-linear functor is R-linear.

The counterpart of Functor.op_additive, and like it the proof body is empty: with linearOpposite in scope, scalars on both sides are the ones on C and D wrapped in op, so the field is closed by the tactic default.

Two spelling constraints, both worth recording because neither is obvious. Section variables are included in order of first use, so an [F.Linear R] binder introduces R only after [Linear R C] would have had to be included — hence every binder is written out rather than taken from a variable block. And declaring into the Functor namespace makes a bare Linear resolve to Functor.Linear, so the category-level instances have to be qualified.