Literal middle-support Cartan data

This file assembles all algebraic and coordinate fields of the manuscript's middle-support Cartan package from the literal complementary-vertex quotient. The only remaining input is the root/Coxeter assertion for the two endpoints of each supported Auslander--Reiten sequence.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceMiddleSupportSkeleton {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : FiniteIndecomposableSkeleton k (P.SupportAlgebra (S.minimalRightAlmostSplitAt ↑z).middle)

The support skeleton attached to the middle term at z.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceMiddleSupportAcyclic {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : (P.rightSequenceMiddleSupportSkeleton hA z).HasAcyclicNonzeroNonisomorphisms

Directedness of the support skeleton attached to the middle term at z.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.middleSupportCartanDataOfRootPairs {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) [IsAlgClosed k] (hA : IsRepresentationFinite k A) (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) (R : ∀ (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }), (P.rightSequenceMiddleSupportSkeleton hA z).SupportCartanRootPairData ⋯ (P.rightSequenceSupportTargetLabel hA z) (P.rightSequenceSupportSourceLabel hA z)) : S.MiddleSupportCartanData D

The literal support quotients provide every field of MiddleSupportCartanData once the sequence-local root pairs are available. This is the internal assembly boundary used by the unconditional constructor.