Minimal realizations for weak positivity

Every nonnegative projective-coordinate vector has a module realization. Among all realizations choose one with least endomorphism dimension. Ringel's endomorphism-drop lemma then forces the degree-one extensions between all indecomposable summands of a minimal realization to vanish.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.not_isSplitMono_of_extClass_ne_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {Q : CategoryTheory.ShortComplex C} (hQ : Q.ShortExact) (hne : hQ.extClass ≠ 0) : ¬CategoryTheory.IsSplitMono Q.f

A short exact sequence with nonzero extension class cannot split at its left map.

theorem MagnitudeConjecture.CategoryTheory.extOne_biproduct_eq_zero_of_pairwise {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type u_1} [Fintype J] (F : J → C) (hpair : ∀ (i j : J) (xi : CategoryTheory.Abelian.Ext (F i) (F j) 1), xi = 0) (xi : CategoryTheory.Abelian.Ext (⨁ F) (⨁ F) 1) : xi = 0

Pairwise vanishing of degree-one extensions between all summands implies vanishing of the degree-one self-extension group of their finite biproduct.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SincereDetectionData {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (S : FiniteIndecomposableSkeleton k B) (w : Fin S.n) : Prop

The two map-detection consequences of sincerity used in Ringel's cycle proof. They say that the chosen indecomposable detects every nonzero map out of the standard injective cogenerator, and every nonzero map into a finite projective.

• precomp_injectiveCogenerator {T : FGModuleCat Bᵐᵒᵖ} (q : injectiveCogeneratorFGObj ⟶ T) : q ≠ 0 → ∃ (y : Fin S.n), (∃ (f : S.fgObj w ⟶ S.fgObj y), f ≠ 0) ∧ ∃ (g : S.fgObj y ⟶ T), g ≠ 0
• postcomp_projective (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] {T : FGModuleCat Bᵐᵒᵖ} (i : T ⟶ P) : i ≠ 0 → ∃ (y : Fin S.n), (∃ (f : T ⟶ S.fgObj y), f ≠ 0) ∧ ∃ (g : S.fgObj y ⟶ S.fgObj w), g ≠ 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finrank_end_eq_of_iso {k B : Type u} [Field k] [Ring B] [Algebra k B] {M N : FGModuleCat Bᵐᵒᵖ} (e : M ≅ N) : Module.finrank k (M ⟶ M) = Module.finrank k (N ⟶ N)

Endomorphism dimension is invariant under isomorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_projectiveVectorRealization_minimal_end {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) (v : S.ProjectiveLabel → ℕ) : ∃ (M : FGModuleCat Bᵐᵒᵖ), (S.projectiveHomVectorFGObj M = fun (p : S.ProjectiveLabel) => ↑(v p)) ∧ ∀ (N : FGModuleCat Bᵐᵒᵖ), (S.projectiveHomVectorFGObj N = fun (p : S.ProjectiveLabel) => ↑(v p)) → Module.finrank k (M ⟶ M) ≤ Module.finrank k (N ⟶ N)

Every nonnegative coordinate vector has a realization with the least possible endomorphism dimension among all its realizations.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.hasProjectiveDimensionLE_two_of_sincereDetection {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) (w : Fin S.n) (D : S.SincereDetectionData w) (x : Fin S.n) : CategoryTheory.HasProjectiveDimensionLE (S.fgObj x) 2

Ringel 2.4(7), in the selected-skeleton form needed below: the existence of a sincere directing indecomposable forces every selected indecomposable to have projective dimension at most two.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.hasProjectiveDimensionLE_two_fgObj_of_sincereDetection {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) (w : Fin S.n) (D : S.SincereDetectionData w) (M : FGModuleCat Bᵐᵒᵖ) : CategoryTheory.HasProjectiveDimensionLE M 2

The selected bound extends to every finitely generated module by its finite indecomposable decomposition.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.extOne_decomposition_eq_zero_of_minimal_end {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) {M : FGModuleCat Bᵐᵒᵖ} (hminimal : ∀ (N : FGModuleCat Bᵐᵒᵖ), S.projectiveHomVectorFGObj N = S.projectiveHomVectorFGObj M → Module.finrank k (M ⟶ M) ≤ Module.finrank k (N ⟶ N)) {n : ℕ} (label : Fin n → Fin S.n) (e : M ≅ ⨁ fun (t : Fin n) => S.fgObj (label t)) (i j : Fin n) (xi : CategoryTheory.Abelian.Ext (S.fgObj (label i)) (S.fgObj (label j)) 1) : xi = 0

The indecomposable summands of an endomorphism-minimal realization have no degree-one extensions between them. A nonzero extension would replace two summands by its middle term without changing the coordinate vector, but would strictly lower the endomorphism dimension.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_projectiveVectorRealization_extOne_self_eq_zero {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) (v : S.ProjectiveLabel → ℕ) : ∃ (M : FGModuleCat Bᵐᵒᵖ), (S.projectiveHomVectorFGObj M = fun (p : S.ProjectiveLabel) => ↑(v p)) ∧ ∀ (xi : CategoryTheory.Abelian.Ext M M 1), xi = 0

Every nonnegative projective-coordinate vector has a finite realization with vanishing degree-one self-extensions.

theorem MagnitudeConjecture.LinearMap.finrank_le_alternating_of_exact_of_exact_of_injective {k : Type u} [Field k] {E V₀ V₁ V₂ : Type v} [AddCommGroup E] [AddCommGroup V₀] [AddCommGroup V₁] [AddCommGroup V₂] [Module k E] [Module k V₀] [Module k V₁] [Module k V₂] [FiniteDimensional k V₀] [FiniteDimensional k V₁] [FiniteDimensional k V₂] (a : E →ₗ[k] V₀) (b : V₀ →ₗ[k] V₁) (c : V₁ →ₗ[k] V₂) (hab : Function.Exact ⇑a ⇑b) (hbc : Function.Exact ⇑b ⇑c) (ha : Function.Injective ⇑a) : ↑(Module.finrank k E) ≤ ↑(Module.finrank k V₀) - ↑(Module.finrank k V₁) + ↑(Module.finrank k V₂)

The Euler characteristic of an exact four-term cochain beginning with an injection is at least the dimension of its first term.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyPresentation_kernel_projective {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (hX : CategoryTheory.HasProjectiveDimensionLE X 2) : CategoryTheory.Projective (CategoryTheory.Limits.kernel P.syzygyPresentation.f)

If the presented module has projective dimension at most two, the kernel of the chosen projective cover of its first syzygy is projective.

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyKernelPrecompLinear {k B : Type u} [Field k] [Ring B] [Algebra k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) : (P.syzygyPresentation.p ⟶ Y) →ₗ[k] CategoryTheory.Limits.kernel P.syzygyPresentation.f ⟶ Y

Restriction along the kernel of the projective cover of the first syzygy.

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

If Ext¹(X,X) vanishes, applying Hom(-,X) to the first three projectives of the chosen resolution is exact at Hom(P₁,X).

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finrank_end_le_quadraticForm_projectiveHomVectorFGObj {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) {M : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation M) (hpd : CategoryTheory.HasProjectiveDimensionLE M 2) (hext : ∀ (xi : CategoryTheory.Abelian.Ext M M 1), xi = 0) : ↑(Module.finrank k (M ⟶ M)) ≤ CartanCoordinate.quadraticForm S.projectiveCartanInverse (S.projectiveHomVectorFGObj M)

For a module of projective dimension at most two with vanishing Ext¹(M,M), its inverse-Cartan quadratic value is at least the dimension of its endomorphism space.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCartanInverse_weaklyPositive_of_sincereDetection {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) (w : Fin S.n) (D : S.SincereDetectionData w) (x : S.ProjectiveLabel → ℤ) : CartanCoordinate.IsPositive x → 1 ≤ CartanCoordinate.quadraticForm S.projectiveCartanInverse x

Ringel 2.4(9): the inverse-Cartan Euler quadratic form of a directed finite module category with a sincere indecomposable is weakly positive.