Directedness under fully faithful additive transport

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.hasAcyclicNonzeroNonisomorphisms_of_fullyFaithful {k A B : Type u} [Field k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (T : FiniteIndecomposableSkeleton k B) (H : S.HasAcyclicNonzeroNonisomorphisms) (F : CategoryTheory.Functor (FinitelyGeneratedCategory B) (FinitelyGeneratedCategory A)) [F.Full] [F.Faithful] [F.Additive] (j : Fin T.n → Fin S.n) (e : (i : Fin T.n) → F.obj (T.fgObj i) ≅ S.fgObj (j i)) : T.HasAcyclicNonzeroNonisomorphisms

A fully faithful additive functor into a directed module category preserves cycle-freeness on any selected family identified with ambient indecomposables.