Coefficient duality for finite modules over a linear category

Pointwise coefficient duality turns a finite covariant module over C into a finite covariant module over Cᵒᵖ. Finite-dimensional biduality upgrades this construction to an anti-equivalence of finite module categories.

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

Pointwise coefficient dual of a covariant module, regarded as a module over the opposite category.

noncomputable def MagnitudeConjecture.CoveringHom.coefficientDualMap {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : LinearModuleCategory k} (f : M ⟶ N) : coefficientDualModule N ⟶ coefficientDualModule M

A module morphism induces the reversed morphism between pointwise coefficient duals.

@[simp]

theorem MagnitudeConjecture.CoveringHom.coefficientDualMap_id {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) : coefficientDualMap (CategoryTheory.CategoryStruct.id M) = CategoryTheory.CategoryStruct.id (coefficientDualModule M)

@[simp]

theorem MagnitudeConjecture.CoveringHom.coefficientDualMap_comp {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {L M N : LinearModuleCategory k} (f : L ⟶ M) (g : M ⟶ N) : coefficientDualMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (coefficientDualMap g) (coefficientDualMap f)

theorem MagnitudeConjecture.CoveringHom.coefficientDualModule_isFiniteDimensionalModule {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) : IsFiniteDimensionalModule k (coefficientDualModule M.obj)

Pointwise coefficient dual preserves the finite-module condition.

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

The coefficient dual as a contravariant functor between finite module categories.

instance MagnitudeConjecture.CoveringHom.finiteCoefficientDualFunctor_additive {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : finiteCoefficientDualFunctor.Additive

theorem MagnitudeConjecture.CoveringHom.coefficientDualModule_isPointwiseThin_iff {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) : IsPointwiseThin (coefficientDualModule M.obj).obj ↔ IsPointwiseThin M.obj.obj

Pointwise coefficient duality preserves and reflects pointwise thinness.

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

Pointwise coefficient dual in the reverse direction, with the double opposite removed.

theorem MagnitudeConjecture.CoveringHom.reverseCoefficientDualModule_isFiniteDimensionalModule {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) : IsFiniteDimensionalModule k (reverseCoefficientDualModule M.obj)

Reverse pointwise coefficient dual preserves finite modules.

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

The same bidual evaluation in the forward order over Cᵒᵖ.

noncomputable def MagnitudeConjecture.CoveringHom.coefficientReverseDoubleDualIso {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) : { obj := coefficientDualModule (reverseCoefficientDualModule M.obj), property := ⋯ } ≅ M

Forward-order bidual evaluation inside the finite module category.

noncomputable def MagnitudeConjecture.CoveringHom.coefficientDualPreimageLinearMap {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : (FiniteDimensionalModuleCategory k)ᵒᵖ} (a : finiteCoefficientDualFunctor.obj M ⟶ finiteCoefficientDualFunctor.obj N) : (Opposite.unop N).obj ⟶ (Opposite.unop M).obj

The morphism recovered from a morphism between coefficient duals by finite-dimensional biduality.

noncomputable def MagnitudeConjecture.CoveringHom.coefficientDualPreimage {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : (FiniteDimensionalModuleCategory k)ᵒᵖ} (a : finiteCoefficientDualFunctor.obj M ⟶ finiteCoefficientDualFunctor.obj N) : M ⟶ N

The recovered morphism, with both full-subcategory layers and the opposite orientation restored.

theorem MagnitudeConjecture.CoveringHom.finiteCoefficientDualFunctor_map_coefficientDualPreimage {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : (FiniteDimensionalModuleCategory k)ᵒᵖ} (a : finiteCoefficientDualFunctor.obj M ⟶ finiteCoefficientDualFunctor.obj N) : finiteCoefficientDualFunctor.map (coefficientDualPreimage a) = a

Dualizing the recovered morphism returns the original morphism.

instance MagnitudeConjecture.CoveringHom.finiteCoefficientDualFunctor_full {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : finiteCoefficientDualFunctor.Full

Pointwise coefficient duality is full on finite modules.

theorem MagnitudeConjecture.CoveringHom.coefficientDualPreimage_finiteCoefficientDualFunctor_map {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) : coefficientDualPreimage (finiteCoefficientDualFunctor.map f) = f

Recovering a dualized morphism returns the original morphism.

instance MagnitudeConjecture.CoveringHom.finiteCoefficientDualFunctor_faithful {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : finiteCoefficientDualFunctor.Faithful

Pointwise coefficient duality is faithful on finite modules.

instance MagnitudeConjecture.CoveringHom.finiteCoefficientDualFunctor_essSurj {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : finiteCoefficientDualFunctor.EssSurj

Every finite module over the opposite category is the coefficient dual of its reverse coefficient dual.

instance MagnitudeConjecture.CoveringHom.finiteCoefficientDualFunctor_isEquivalence {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : finiteCoefficientDualFunctor.IsEquivalence

Pointwise coefficient duality is an anti-equivalence of finite module categories.

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

The finite-module coefficient-duality anti-equivalence.

theorem MagnitudeConjecture.CoveringHom.finiteCoefficientDualFunctor_indec_iff {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) : CategoryTheory.Indecomposable (finiteCoefficientDualFunctor.obj (Opposite.op M)) ↔ CategoryTheory.Indecomposable M

The coefficient-duality anti-equivalence preserves and reflects categorical indecomposability.