The linear-dual functor on module categories

Mathlib supplies Module.Dual and LinearMap.dualMap, but at the pinned revision it does not bundle them as a functor on ModuleCat. This file is the category-theoretic owner of that functor. In particular it has no dependency on algebraic geometry, so abstract Serre functors can use it.

For k : Type u and modules in universe max u w, algebraic duality stays in the same module category: Module.Dual k V lives in Type (max u w). The older geometric use at ModuleCat.{u + 1} k is the specialization w := u + 1.

Only the functor, its two reduction lemmas, and additivity live here. Exactness over a field remains in Algebra/Category/ModuleCat/LinearDual.lean.

noncomputable def ModuleCat.linearDualFunctor (k : Type u) [Field k] : CategoryTheory.Functor (ModuleCat k)ᵒᵖ (ModuleCat k)

Algebraic linear dual, viewed as a contravariant functor on k-modules.

Equations

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

@[simp]

theorem ModuleCat.linearDualFunctor_obj (k : Type u) [Field k] (V : (ModuleCat k)ᵒᵖ) : (linearDualFunctor k).obj V = of k (Module.Dual k ↑(Opposite.unop V))

@[simp]

theorem ModuleCat.linearDualFunctor_map (k : Type u) [Field k] {V W : (ModuleCat k)ᵒᵖ} (f : V ⟶ W) : (linearDualFunctor k).map f = ofHom (Hom.hom f.unop).dualMap

instance ModuleCat.instAdditiveOppositeLinearDualFunctor (k : Type u) [Field k] : (linearDualFunctor k).Additive