Almost-split maps from a finite module skeleton

Finite radical evaluation over a complete indecomposable skeleton constructs a right almost-split map at every label. Minimalizing its finite-dimensional source produces the chosen labelwise maps needed for downstream right-tau data.

theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.isRightAlmostSplit_of_factors_obj {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) {z : Fin S.n} {E : FiniteDimensionalModuleCategory k} (f : E ⟶ S.obj z) (hnosplit : ¬CategoryTheory.IsSplitEpi f) (hfac : ∀ (x : Fin S.n) (g : S.obj x ⟶ S.obj z), ¬CategoryTheory.IsSplitEpi g → ∃ (h : S.obj x ⟶ E), CategoryTheory.CategoryStruct.comp h f = g) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f

To prove a map into a chosen finite-module skeleton representative is right almost split, it is enough to factor nonsplit maps from the chosen indecomposable representatives.

theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.exists_rightAlmostSplit {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) (y : Fin S.n) : ∃ (E : FiniteDimensionalModuleCategory k) (f : E ⟶ S.obj y), QuotientSubmoduleEquidistribution.IsRightAlmostSplit f

Finite radical evaluation over all skeleton labels gives a right almost-split morphism ending at every chosen indecomposable.

structure MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.MinimalRightAlmostSplitAt {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) (y : Fin S.n) : Type (max (max u uK) (v + 1))

A chosen right-minimal right almost-split morphism ending at a skeleton label.

• source : FiniteDimensionalModuleCategory k
• map : self.source ⟶ S.obj y
• rightAlmostSplit : QuotientSubmoduleEquidistribution.IsRightAlmostSplit self.map
• rightMinimal : QuotientSubmoduleEquidistribution.IsRightMinimal self.map

noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.minimalRightAlmostSplitAt {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) (y : Fin S.n) : S.MinimalRightAlmostSplitAt y

Choose a right-minimal right almost-split morphism at every skeleton label.