Directedness for the finite right-module skeleton

This file adapts the representation-directed order kernel from the clean subcat-research-mathlib-only formalization to the magnitude package's literal finite right-module skeleton. It retains only the part needed here: cycle-freeness makes nonzero endomorphisms invertible, hence scalar over an algebraically closed field, and the scalar conclusion descends to every literal factor object.

Donor provenance is recorded in the magnitude formalization thread. The implementation is expressed entirely in the local right-module vocabulary and introduces no dependency on the donor repository.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.NonzeroNonisomorphism {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i j : Fin S.n) : Prop

A nonzero nonisomorphism between two selected indecomposable right modules.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.HasAcyclicNonzeroNonisomorphisms {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Prop

The cycle-free part of representation-directedness on the finite duplicate-free skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.HasAcyclicNonzeroNonisomorphisms.isIso_of_ne_zero_endomorphism {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (i : Fin S.n) (f : S.fgObj i ⟶ S.fgObj i) (hf : f ≠ 0) : CategoryTheory.IsIso f

In a directed skeleton every nonzero indecomposable endomorphism is an isomorphism: otherwise it is a one-edge cycle.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.HasAcyclicNonzeroNonisomorphisms.finrank_endomorphism_eq_one {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (i : Fin S.n) : Module.finrank k (S.fgObj i ⟶ S.fgObj i) = 1

Algebraic closedness and directedness make every selected indecomposable endomorphism space one-dimensional.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.HasAcyclicNonzeroNonisomorphisms.endomorphism_eq_smul_id {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (i : Fin S.n) (f : S.fgObj i ⟶ S.fgObj i) : ∃ (c : k), c • CategoryTheory.CategoryStruct.id (S.fgObj i) = f

Constructive Schur form: every selected indecomposable endomorphism is a scalar multiple of its identity.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.HasAcyclicNonzeroNonisomorphisms.factorObject_endomorphism_eq_smul_id {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (K : Set (Fin S.n)) (x : S.SurvivingLabel K) (f : S.factorObject K x ⟶ S.factorObject K x) : ∃ (c : k), c • CategoryTheory.CategoryStruct.id (S.factorObject K x) = f

Directed scalar endomorphisms descend through the literal quotient functor to every surviving factor object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.HasAcyclicNonzeroNonisomorphisms.factorObject_label_eq_of_two_way {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (K : Set (Fin S.n)) (x y : S.SurvivingLabel K) (f : S.factorObject K x ⟶ S.factorObject K y) (hf : f ≠ 0) (g : S.factorObject K y ⟶ S.factorObject K x) (hg : g ≠ 0) : x = y

Two surviving factor indecomposables admitting nonzero maps in both directions have the same label. Any pair of distinct labels would lift to a two-edge cycle of nonzero nonisomorphisms in the ambient directed skeleton.