Kupisch's one-sided uniserial alternative

This file upgrades distributive Hom-bimodule chains to the exact condition used by Skowroński--Waschbüsch. Finite-dimensionality first supplies a largest principal two-sided span. Kupisch cyclicity orients that generator to one endpoint. On endomorphism rings the same construction gives a generator of the Jacobson radical; nilpotence and the algebraically closed residue character make the endpoint regular modules uniserial.

theorem MagnitudeConjecture.exists_postcomposition_of_mem_twoSidedEndomorphismSpan {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Y : C} {f g : X ⟶ Y} (ht : AllowsTransit f) (hg : g ∈ twoSidedEndomorphismSpan f) : ∃ (b : CategoryTheory.End Y), g = CategoryTheory.CategoryStruct.comp f b.asHom

Transit collapses a principal two-sided span to target-endomorphism multiples of its generator.

theorem MagnitudeConjecture.exists_precomposition_of_mem_twoSidedEndomorphismSpan {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Y : C} {f g : X ⟶ Y} (hc : AllowsCotransit f) (hg : g ∈ twoSidedEndomorphismSpan f) : ∃ (a : CategoryTheory.End X), g = CategoryTheory.CategoryStruct.comp a.asHom f

Cotransit collapses a principal two-sided span to source-endomorphism multiples of its generator.

theorem MagnitudeConjecture.exists_twoSidedEndomorphismSpan_eq {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Y : C} [Module.Finite k (X ⟶ Y)] (T : Submodule k (X ⟶ Y)) (hT : IsHomSubbimodule T) (hcomparable : ∀ (U V : Submodule k (X ⟶ Y)), IsHomSubbimodule U → IsHomSubbimodule V → U ≤ V ∨ V ≤ U) : ∃ f ∈ T, twoSidedEndomorphismSpan f = T

A finite-dimensional endpoint-stable subspace whose endpoint-stable subspaces are comparable has a single two-sided generator.

theorem MagnitudeConjecture.transit_or_cotransit_of_homSubbimodule_comparable_local {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [IsAlgClosed k] {X Y : C} [Module.Finite k (CategoryTheory.End X)] [Module.Finite k (CategoryTheory.End Y)] [IsLocalRing (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End Y)] (f : X ⟶ Y) (hcomparable : ∀ (U V : Submodule k (X ⟶ Y)), IsHomSubbimodule U → IsHomSubbimodule V → U ≤ V ∨ V ≤ U) : AllowsTransit f ∨ AllowsCotransit f

The algebraically closed residue map supplies the hypotheses of the generic Kupisch cyclicity theorem.

theorem MagnitudeConjecture.end_regular_and_opposite_uniserial_of_homSubbimodule_comparable {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [IsAlgClosed k] (X : C) [Module.Finite k (X ⟶ X)] [Module.Finite k (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End X)] (hcomparable : ∀ (U V : Submodule k (CategoryTheory.End X)), IsHomSubbimodule U → IsHomSubbimodule V → U ≤ V ∨ V ≤ U) : IsUniserialModule (CategoryTheory.End X) (CategoryTheory.End X) ∧ IsUniserialModule (CategoryTheory.End X)ᵐᵒᵖ (CategoryTheory.End X)ᵐᵒᵖ

Comparable endomorphism subbimodules make both regular endpoint modules uniserial. The zero-radical case is division-like; otherwise a maximal radical generator, Kupisch orientation, and polynomial generation give the power normal form.

theorem MagnitudeConjecture.uniserialModule_or_opposite_of_homSubbimodule_comparable {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [IsAlgClosed k] [∀ (X Y : C), Module.Finite k (X ⟶ Y)] [∀ (X : C), Module.Finite k (CategoryTheory.End X)] [∀ (X : C), IsLocalRing (CategoryTheory.End X)] (hcomparable : ∀ {X Y : C} (U V : Submodule k (X ⟶ Y)), IsHomSubbimodule U → IsHomSubbimodule V → U ≤ V ∨ V ≤ U) (X Y : C) : IsUniserialModule (CategoryTheory.End Y) (X ⟶ Y) ∨ IsUniserialModule (CategoryTheory.End X)ᵐᵒᵖ (X ⟶ Y)

Kupisch's condition (K)(2): in a finite-dimensional linear category with local endpoints and comparable Hom subbimodules, every Hom space is uniserial as a module over its target endomorphism ring or over the opposite of its source endomorphism ring.