Exact linear duality on modules over a field

Over a field, algebraic linear duality sends a module V to Vᵛ = Hom(V, k). The contravariant additive functor is defined in CategoryTheory/ModuleCat/LinearDual.lean; this file proves that it is exact: it takes short exact sequences to short exact sequences and preserves finite limits and colimits. Its derived lift is Algebra/Homology/DerivedCategory/LinearDual.lean.

theorem ModuleCat.linearDualFunctor_map_shortExact (k : Type u) [Field k] (S : CategoryTheory.ShortComplex (ModuleCat k)ᵒᵖ) (hS : S.ShortExact) : (S.map (linearDualFunctor k)).ShortExact

Linear duality reverses a short exact sequence of vector spaces to a short exact sequence.

theorem ModuleCat.linearDualFunctor_preservesFiniteLimits_and_colimits (k : Type u) [Field k] : CategoryTheory.Limits.PreservesFiniteLimits (linearDualFunctor k) ∧ CategoryTheory.Limits.PreservesFiniteColimits (linearDualFunctor k)

Exactness of algebraic linear duality, in the form Mathlib's derived-functor construction consumes.

theorem ModuleCat.linearDualFunctor_preservesFiniteLimits (k : Type u) [Field k] : CategoryTheory.Limits.PreservesFiniteLimits (linearDualFunctor k)

Linear duality preserves finite limits, being exact.

theorem ModuleCat.linearDualFunctor_preservesFiniteColimits (k : Type u) [Field k] : CategoryTheory.Limits.PreservesFiniteColimits (linearDualFunctor k)

Linear duality preserves finite colimits, being exact.

instance ModuleCat.instPreservesFiniteLimitsOppositeLinearDualFunctor (k : Type u) [Field k] : CategoryTheory.Limits.PreservesFiniteLimits (linearDualFunctor k)

instance ModuleCat.instPreservesFiniteColimitsOppositeLinearDualFunctor (k : Type u) [Field k] : CategoryTheory.Limits.PreservesFiniteColimits (linearDualFunctor k)