Euler roots for directed finite module categories

This file identifies the inverse-Cartan quadratic form of a module admitting a length-one projective resolution with its self-Euler characteristic. The degree-one self-Ext vanishing supplied by directedness then makes each such indecomposable dimension vector a positive root.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.differentialPrecompLinear_surjective_of_extOne_self_eq_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (hmono : CategoryTheory.Mono P.differential) (hext : ∀ (xi : CategoryTheory.Abelian.Ext X X 1), xi = 0) : Function.Surjective ⇑(P.differentialPrecompLinear X)

If the first projective differential is monic and Ext¹(X,X) vanishes, then applying Hom(-,X) to the projective presentation is right exact.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.dotProduct_projectiveCartanInverse_mulVec_projectiveHomVectorFGObj {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (M P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : S.projectiveHomVectorFGObj M ⬝ᵥ S.projectiveCartanInverse.mulVec (S.projectiveHomVectorFGObj P) = ↑(Module.finrank k (P ⟶ M))

Pairing a module vector with the inverse-Cartan image of a projective vector computes the corresponding Hom dimension.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.quadraticForm_projectiveHomVectorFGObj_eq_sub {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (hmono : CategoryTheory.Mono P.differential) : CartanCoordinate.quadraticForm S.projectiveCartanInverse (S.projectiveHomVectorFGObj X) = ↑(Module.finrank k (P.augmentation.p ⟶ X)) - ↑(Module.finrank k (P.syzygyPresentation.p ⟶ X))

A length-one projective resolution identifies the inverse-Cartan quadratic form with the alternating Hom dimension of its two projectives.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveHomVector_quadraticForm_eq_one_of_mono_differential {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) [IsAlgClosed k] [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (H : S.HasAcyclicNonzeroNonisomorphisms) (x : Fin S.n) (P : TwoStepMinimalProjectivePresentation (S.fgObj x)) (hmono : CategoryTheory.Mono P.differential) : CartanCoordinate.quadraticForm S.projectiveCartanInverse (S.projectiveHomVector x) = 1

A selected indecomposable with projective dimension at most one has a positive-root projective-Hom vector.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportTarget_quadraticForm_eq_one {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; CartanCoordinate.quadraticForm T.projectiveCartanInverse (T.projectiveHomVector (P.rightSequenceSupportTargetLabel hA z)) = 1

The endpoint of the literal middle-support Auslander--Reiten sequence is a positive root for the support algebra's inverse-Cartan quadratic form.