Hoshino's primitive-torsion argument

This file formalizes the homological step in Hoshino's reduction. Stable Auslander--Reiten duality kills the relevant Ext¹ group, so every endomorphism of the primitive torsion radical extends to the ambient Auslander--Reiten source. The resulting surjection of endomorphism rings transports locality, and hence indecomposability, to the torsion radical.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.precomp_surjective_of_ext_subsingleton {C : Type u} [CategoryTheory.Category.{u_1, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) [Subsingleton (CategoryTheory.Abelian.Ext S.X₃ Y 1)] : Function.Surjective fun (f : S.X₂ ⟶ Y) => CategoryTheory.CategoryStruct.comp S.f f

In the contravariant long exact sequence of a short exact sequence, vanishing of the following Ext¹ group makes restriction along the kernel surjective on morphisms.

def MagnitudeConjecture.RightModule.primitiveTorsionEndRestriction {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (M : FinitelyGeneratedCategory A) : CategoryTheory.End M →+* CategoryTheory.End (primitiveTorsionFGObj e M)

Restriction of ambient endomorphisms to the primitive torsion radical, as a homomorphism of (possibly noncommutative) rings.

theorem MagnitudeConjecture.RightModule.primitiveTorsionEndRestriction_surjective_of_ext_subsingleton {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] [CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)] (e : A) (M : FinitelyGeneratedCategory A) [Subsingleton (CategoryTheory.Abelian.Ext (primitiveTorsionQuotientFGObj e M) M 1)] : Function.Surjective ⇑(primitiveTorsionEndRestriction e M)

If the torsion-free quotient has no degree-one extensions into the ambient module, every endomorphism of the torsion radical extends to an ambient endomorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightKernelMap_functionExact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom (S.rightKernelMap z)) ⇑(CategoryTheory.ConcreteCategory.hom (S.minimalRightAlmostSplitAt ↑z).map)

The transported kernel inclusion of the chosen right AR map is exact on underlying module elements.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveTorsionFGObj_rightTranslation_nontrivial {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (hN : IsAnnihilatedBy (primitiveIdeal e) (S.fgObj ↑z)) (hNprojective : ¬CategoryTheory.Projective { obj := S.fgObj ↑z, property := hN }) : Nontrivial ↑(primitiveTorsionFGObj e (S.fgObj (S.rightTranslationLabel z)))

Under the manuscript's quotient-nonprojectivity hypothesis, the primitive torsion radical of the ambient AR translate is nonzero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveTorsionQuotient_extOne_rightTranslation_subsingleton {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] [CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)] (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (he : IsIdempotentElem e) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (hN : IsAnnihilatedBy (primitiveIdeal e) (S.fgObj ↑z)) : Subsingleton (CategoryTheory.Abelian.Ext (primitiveTorsionQuotientFGObj e (S.fgObj (S.rightTranslationLabel z))) (S.fgObj (S.rightTranslationLabel z)) 1)

Hoshino's AR-duality vanishing: for a quotient-module endpoint N, the torsion-free quotient of its ambient AR translate has vanishing Ext¹ into that translate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveTorsionEndRestriction_rightTranslation_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (he : IsIdempotentElem e) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (hN : IsAnnihilatedBy (primitiveIdeal e) (S.fgObj ↑z)) : Function.Surjective ⇑(primitiveTorsionEndRestriction e (S.fgObj (S.rightTranslationLabel z)))

The restriction from the endomorphism ring of an ambient AR translate to the endomorphism ring of its primitive torsion radical is surjective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveTorsionFGObj_rightTranslation_end_isLocalRing {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (he : IsIdempotentElem e) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (hN : IsAnnihilatedBy (primitiveIdeal e) (S.fgObj ↑z)) (hNprojective : ¬CategoryTheory.Projective { obj := S.fgObj ↑z, property := hN }) : IsLocalRing (CategoryTheory.End (primitiveTorsionFGObj e (S.fgObj (S.rightTranslationLabel z))))

A nonzero primitive torsion radical of an ambient AR translate inherits a local endomorphism ring.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveTorsionFGObj_rightTranslation_isIndecomposableModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (he : IsIdempotentElem e) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (hN : IsAnnihilatedBy (primitiveIdeal e) (S.fgObj ↑z)) (hNprojective : ¬CategoryTheory.Projective { obj := S.fgObj ↑z, property := hN }) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑(primitiveTorsionFGObj e (S.fgObj (S.rightTranslationLabel z)))

The primitive torsion radical of the ambient AR translate is an indecomposable module under exactly Hoshino's nonprojectivity hypothesis.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveTorsionAmbientTargetMap_rightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (he : IsIdempotentElem e) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (hN : IsAnnihilatedBy (primitiveIdeal e) (S.fgObj ↑z)) (hNprojective : ¬CategoryTheory.Projective { obj := S.fgObj ↑z, property := hN }) : QuotientSubmoduleEquidistribution.IsRightMinimal (primitiveTorsionAmbientTargetMap e (S.minimalRightAlmostSplitAt ↑z).map)

The torsion-restricted ambient AR epimorphism is right minimal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveTorsionTargetMap_minimalRightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (he : IsIdempotentElem e) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (hN : IsAnnihilatedBy (primitiveIdeal e) (S.fgObj ↑z)) (hNprojective : ¬CategoryTheory.Projective { obj := S.fgObj ↑z, property := hN }) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (primitiveTorsionTargetMap e hN (S.minimalRightAlmostSplitAt ↑z).map) ∧ QuotientSubmoduleEquidistribution.IsRightMinimal (primitiveTorsionTargetMap e hN (S.minimalRightAlmostSplitAt ↑z).map)

Hoshino's restricted map is minimal right almost split in the literal primitive-quotient subcategory.