Exactness consequences of finite coefficient duality

The pointwise coefficient-duality anti-equivalence reverses monomorphisms and epimorphisms. These two small interfaces are the categorical input for the Auslander--Reiten socle-length calculation.

theorem MagnitudeConjecture.CoveringHom.finiteCoefficientDual_map_mono_of_epi {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : FiniteDimensionalModuleCategory k} (f : M ⟶ N) [CategoryTheory.Epi f] : CategoryTheory.Mono (finiteCoefficientDualityEquivalence.functor.map f.op)

Coefficient duality sends an epimorphism of finite modules to a monomorphism.

theorem MagnitudeConjecture.CoveringHom.finiteCoefficientDual_map_epi_of_mono {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : FiniteDimensionalModuleCategory k} (f : M ⟶ N) [CategoryTheory.Mono f] : CategoryTheory.Epi (finiteCoefficientDualityEquivalence.functor.map f.op)

Coefficient duality sends a monomorphism of finite modules to an epimorphism.

theorem MagnitudeConjecture.CoveringHom.finiteCoefficientDual_map_mono_iff_epi {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : FiniteDimensionalModuleCategory k} (f : M ⟶ N) : CategoryTheory.Mono (finiteCoefficientDualityEquivalence.functor.map f.op) ↔ CategoryTheory.Epi f

A finite-module map is epic exactly when its coefficient dual is monic.

theorem MagnitudeConjecture.CoveringHom.finiteCoefficientDual_map_epi_iff_mono {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : FiniteDimensionalModuleCategory k} (f : M ⟶ N) : CategoryTheory.Epi (finiteCoefficientDualityEquivalence.functor.map f.op) ↔ CategoryTheory.Mono f

A finite-module map is monic exactly when its coefficient dual is epic.

theorem MagnitudeConjecture.CoveringHom.finiteCoefficientDual_map_shortExact {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex (FiniteDimensionalModuleCategory k)) (hS : S.ShortExact) : (S.op.map finiteCoefficientDualityEquivalence.functor).ShortExact

Coefficient duality carries a short exact sequence to its reversed short exact sequence.

theorem MagnitudeConjecture.CoveringHom.finiteCoefficientDual_map_shortExact_iff {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex (FiniteDimensionalModuleCategory k)) : (S.op.map finiteCoefficientDualityEquivalence.functor).ShortExact ↔ S.ShortExact

A short complex is short exact exactly when its coefficient-dual reversal is short exact.