Finite indecomposable skeletons under coefficient duality

Pointwise coefficient duality transports a duplicate-free complete skeleton of finite modules over a linear category to one over the opposite category. The labels are unchanged, while the anti-equivalence reverses morphisms.

noncomputable def MagnitudeConjecture.CoveringHom.reverseFiniteCoefficientDual {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) : FiniteDimensionalModuleCategory k

The reverse pointwise coefficient dual, bundled as a finite module over the original category.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCoefficientDualReverseIso {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) : finiteCoefficientDualFunctor.obj (Opposite.op (reverseFiniteCoefficientDual M)) ≅ M

Dualizing the reverse coefficient dual recovers the original finite module.

theorem MagnitudeConjecture.CoveringHom.reverseFiniteCoefficientDual_injective_iff_projective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) : CategoryTheory.Injective (reverseFiniteCoefficientDual M) ↔ CategoryTheory.Projective M

The reverse coefficient dual is injective exactly when the original finite module is projective. The reversal is forced by the intervening opposite category; coefficient duality is an anti-equivalence.

theorem MagnitudeConjecture.CoveringHom.reverseFiniteCoefficientDual_projective_iff_injective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) : CategoryTheory.Projective (reverseFiniteCoefficientDual M) ↔ CategoryTheory.Injective M

Dually, the reverse coefficient dual is projective exactly when the original finite module is injective.

noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.coefficientDual {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) : FiniteDimensionalModuleIndecomposableSkeleton

Transport a finite complete indecomposable skeleton through pointwise coefficient duality. This is an anti-equivalence, so the target is the finite-module category over Cᵒᵖ.