Sincerity detection in a literal support algebra

An ambient indecomposable whose projective support is the whole chosen support quotient supplies the two map-detection properties used in Ringel's global-dimension cycle argument.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportLabel_sincereDetectionData {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) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (hM : CategoryTheory.Indecomposable M.obj) (hfull : S.projectiveSupport M = S.projectiveSupport X) : let T := P.supportAlgebraSkeleton hA X; T.SincereDetectionData (P.supportLabel hA X M hsub hM)

A supported indecomposable with the full chosen support detects the maps from the injective cogenerator and into finite projectives that occur in Ringel's proof of global dimension at most two.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_rightSequenceSupport_sincereDetectionData {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 : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : have T := P.rightSequenceMiddleSupportSkeleton hA z; ∃ (w : Fin T.n), T.SincereDetectionData w

The support algebra of a chosen right almost-split middle term contains an actual selected indecomposable with the sincerity detection data.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceMiddleSupport_projectiveCartanInverse_weaklyPositive {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) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : have T := P.rightSequenceMiddleSupportSkeleton hA z; ∀ (x : T.ProjectiveLabel → ℤ), CartanCoordinate.IsPositive x → 1 ≤ CartanCoordinate.quadraticForm T.projectiveCartanInverse x

The Euler quadratic form of the literal middle-support algebra is weakly positive, with no imported Ringel theorem assumption remaining.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportCartanRootPairData {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) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : let T := P.rightSequenceMiddleSupportSkeleton hA z; T.SupportCartanRootPairData ⋯ (P.rightSequenceSupportTargetLabel hA z) (P.rightSequenceSupportSourceLabel hA z)

The two endpoints of a supported Auslander--Reiten sequence form the literal positive-root/Coxeter pair required by the coordinate argument.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.middleSupportCartanData {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) : S.MiddleSupportCartanData D

The literal middle-support Cartan package is available directly from representation-finiteness, directedness, and algebraic closedness.