Directedness of primitive quotients and basic representatives

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientFinite_hasAcyclicNonzeroNonisomorphisms {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] : (S.primitiveQuotientFiniteIndecomposableSkeleton D).HasAcyclicNonzeroNonisomorphisms

A primitive quotient of a directed algebra remains directed on its literal finite indecomposable skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moritaBasicSkeleton_hasAcyclicNonzeroNonisomorphisms {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) : S.moritaBasicSkeleton.HasAcyclicNonzeroNonisomorphisms

The canonical basic Morita representative of a directed algebra is directed on the corresponding finite skeleton.