Uniseriality under finite-dimensional coefficient duality

This leaf module keeps abelian and uniserial structure out of the foundational coefficient-duality files.

theorem MagnitudeConjecture.IsUniserialObject.unop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : Cᵒᵖ} (hX : IsUniserialObject X) : IsUniserialObject (Opposite.unop X)

Passing back from the opposite category preserves uniseriality.

theorem MagnitudeConjecture.IsUniserialObject.of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (hX : IsUniserialObject X) (f : X ⟶ Y) [CategoryTheory.Epi f] : IsUniserialObject Y

An epimorphic image of a uniserial object in an abelian category is uniserial. Opposite-category duality realizes the target as a subobject of the opposite of the source.

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

Finite-dimensional coefficient duality preserves and reflects uniseriality.

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

Reverse coefficient duality preserves and reflects uniseriality.