The primitive torsion radical

For a primitive idempotent e, the Hoshino torsion radical sends a right A-module M to its largest submodule annihilated by AeA. In the right-module convention this is the idempotent-torsion submodule for MulOpposite.op e in the left Aᵐᵒᵖ-module M.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.primitiveTorsionSubmodule {A : Type u} [Ring A] (e : A) (M : FinitelyGeneratedCategory A) : Submodule Aᵐᵒᵖ ↑M

The largest ambient submodule annihilated by the primitive quotient ideal AeA.

def MagnitudeConjecture.RightModule.primitiveTorsionFGObj {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (M : FinitelyGeneratedCategory A) : FinitelyGeneratedCategory A

The primitive torsion radical as a finitely generated ambient right module.

def MagnitudeConjecture.RightModule.primitiveTorsionInclusion {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (M : FinitelyGeneratedCategory A) : primitiveTorsionFGObj e M ⟶ M

The canonical inclusion of the primitive torsion radical.

def MagnitudeConjecture.RightModule.primitiveTorsionQuotientFGObj {A : Type u} [Ring A] (e : A) (M : FinitelyGeneratedCategory A) : FinitelyGeneratedCategory A

The quotient of a module by its maximal AeA-annihilated submodule.

def MagnitudeConjecture.RightModule.primitiveTorsionQuotientMk {A : Type u} [Ring A] (e : A) (M : FinitelyGeneratedCategory A) : M ⟶ primitiveTorsionQuotientFGObj e M

The canonical projection onto the primitive torsion-free quotient.

theorem MagnitudeConjecture.RightModule.primitiveTorsionInclusion_comp_quotientMk {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (M : FinitelyGeneratedCategory A) : CategoryTheory.CategoryStruct.comp (primitiveTorsionInclusion e M) (primitiveTorsionQuotientMk e M) = 0

theorem MagnitudeConjecture.RightModule.primitiveTorsionQuotient_shortExact {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (M : FinitelyGeneratedCategory A) : { X₁ := (primitiveTorsionFGObj e M).obj, X₂ := M.obj, X₃ := (primitiveTorsionQuotientFGObj e M).obj, f := (primitiveTorsionInclusion e M).hom, g := (primitiveTorsionQuotientMk e M).hom, zero := ⋯ }.ShortExact

The torsion radical, ambient module, and torsion-free quotient form the canonical short exact sequence.

theorem MagnitudeConjecture.RightModule.primitiveTorsionQuotient_fg_shortExact {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (M : FinitelyGeneratedCategory A) : { X₁ := primitiveTorsionFGObj e M, X₂ := M, X₃ := primitiveTorsionQuotientFGObj e M, f := primitiveTorsionInclusion e M, g := primitiveTorsionQuotientMk e M, zero := ⋯ }.ShortExact

The same canonical torsion sequence, retained inside the finitely generated module category.

theorem MagnitudeConjecture.RightModule.primitiveTorsionQuotient_torsionSubmodule_eq_bot {A : Type u} [Ring A] {e : A} (he : IsIdempotentElem e) (M : FinitelyGeneratedCategory A) : primitiveTorsionSubmodule e (primitiveTorsionQuotientFGObj e M) = ⊥

Quotienting by the primitive torsion radical leaves no nonzero primitive torsion.

theorem MagnitudeConjecture.RightModule.primitiveTorsionFGObj_isAnnihilatedBy {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (M : FinitelyGeneratedCategory A) : IsAnnihilatedBy (primitiveIdeal e) (primitiveTorsionFGObj e M)

The torsion radical is annihilated by AeA, hence is an object of the primitive quotient subcategory.

def MagnitudeConjecture.RightModule.primitiveTorsionSubcategoryObj {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (M : FinitelyGeneratedCategory A) : PrimitiveQuotientSubcategory e

The torsion radical bundled in the full primitive-quotient subcategory.

def MagnitudeConjecture.RightModule.primitiveTorsionMap {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {M N : FinitelyGeneratedCategory A} (f : M ⟶ N) : primitiveTorsionFGObj e M ⟶ primitiveTorsionFGObj e N

A morphism of ambient modules restricts to their primitive torsion radicals.

@[simp]

theorem MagnitudeConjecture.RightModule.primitiveTorsionMap_apply {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {M N : FinitelyGeneratedCategory A} (f : M ⟶ N) (x : ↑(primitiveTorsionFGObj e M)) : ↑((CategoryTheory.ConcreteCategory.hom (primitiveTorsionMap e f)) x) = (CategoryTheory.ConcreteCategory.hom f) ↑x

theorem MagnitudeConjecture.RightModule.primitiveTorsionMap_comp_inclusion {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {M N : FinitelyGeneratedCategory A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (primitiveTorsionMap e f) (primitiveTorsionInclusion e N) = CategoryTheory.CategoryStruct.comp (primitiveTorsionInclusion e M) f

Restriction to the primitive torsion radical commutes with the canonical inclusions into the ambient modules.

def MagnitudeConjecture.RightModule.primitiveTorsionFunctor {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : CategoryTheory.Functor (FinitelyGeneratedCategory A) (FinitelyGeneratedCategory A)

The primitive torsion radical is functorial on finitely generated ambient modules.

instance MagnitudeConjecture.RightModule.primitiveTorsionFunctor_additive {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : (primitiveTorsionFunctor e).Additive

The primitive torsion radical is additive on morphisms.

instance MagnitudeConjecture.RightModule.primitiveTorsionFunctor_preservesBinaryBiproducts {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : CategoryTheory.Limits.PreservesBinaryBiproducts (primitiveTorsionFunctor e)

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.primitiveTorsionBiprodIso {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (M N : FinitelyGeneratedCategory A) : (primitiveTorsionFunctor e).obj (M ⊞ N) ≅ (primitiveTorsionFunctor e).obj M ⊞ (primitiveTorsionFunctor e).obj N

Primitive torsion carries a binary biproduct to the biproduct of the primitive torsion radicals.

def MagnitudeConjecture.RightModule.primitiveTorsionInclusionNatTrans {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : primitiveTorsionFunctor e ⟶ CategoryTheory.Functor.id (FinitelyGeneratedCategory A)

The torsion inclusions form a natural transformation to the identity functor.

def MagnitudeConjecture.RightModule.primitiveTorsionLift {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {X M : FinitelyGeneratedCategory A} (hX : IsAnnihilatedBy (primitiveIdeal e) X) (f : X ⟶ M) : X ⟶ primitiveTorsionFGObj e M

Any map from an AeA-annihilated module factors canonically through the primitive torsion radical.

@[simp]

theorem MagnitudeConjecture.RightModule.primitiveTorsionLift_comp_inclusion {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {X M : FinitelyGeneratedCategory A} (hX : IsAnnihilatedBy (primitiveIdeal e) X) (f : X ⟶ M) : CategoryTheory.CategoryStruct.comp (primitiveTorsionLift e hX f) (primitiveTorsionInclusion e M) = f

theorem MagnitudeConjecture.RightModule.hom_to_primitiveTorsionQuotient_eq_zero {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) {X M : FinitelyGeneratedCategory A} (hX : IsAnnihilatedBy (primitiveIdeal e) X) (f : X ⟶ primitiveTorsionQuotientFGObj e M) : f = 0

Every morphism from an AeA-annihilated module to the torsion-free quotient is zero.

def MagnitudeConjecture.RightModule.primitiveTorsionIsoOfIsAnnihilated {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) : primitiveTorsionFGObj e M ≅ M

On an AeA-annihilated module the torsion inclusion is an isomorphism.

def MagnitudeConjecture.RightModule.primitiveTorsionTargetMap {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {E N : FinitelyGeneratedCategory A} (hN : IsAnnihilatedBy (primitiveIdeal e) N) (q : E ⟶ N) : primitiveTorsionSubcategoryObj e E ⟶ { obj := N, property := hN }

Restrict an ambient map to the primitive torsion radical of its source, when its target is already annihilated by AeA.

theorem MagnitudeConjecture.RightModule.primitiveTorsionTargetMap_isRightAlmostSplit {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {E N : FinitelyGeneratedCategory A} (hN : IsAnnihilatedBy (primitiveIdeal e) N) (q : E ⟶ N) (hq : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (primitiveTorsionTargetMap e hN q)

Hoshino's factorization step: applying the primitive torsion radical to an ambient right almost-split map gives a right almost-split map in the full primitive-quotient subcategory.

theorem MagnitudeConjecture.RightModule.primitiveQuotientSubcategory_enoughProjectives {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : CategoryTheory.EnoughProjectives (PrimitiveQuotientSubcategory e)

The primitive-quotient full subcategory has enough projectives, by transport from the literal module category of A/AeA.

theorem MagnitudeConjecture.RightModule.primitiveTorsionTargetMap_epi_of_not_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {E N : FinitelyGeneratedCategory A} (hN : IsAnnihilatedBy (primitiveIdeal e) N) (q : E ⟶ N) (hq : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) (hNprojective : ¬CategoryTheory.Projective { obj := N, property := hN }) : CategoryTheory.Epi (primitiveTorsionTargetMap e hN q)

The restricted right almost-split map is epic when its target is nonprojective in the primitive-quotient category.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.primitiveTorsionAmbientTargetMap {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {E N : FinitelyGeneratedCategory A} (q : E ⟶ N) : primitiveTorsionFGObj e E ⟶ N

The underlying ambient map of primitiveTorsionTargetMap.

theorem MagnitudeConjecture.RightModule.primitiveTorsionAmbientTargetMap_surjective_of_not_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {E N : FinitelyGeneratedCategory A} (hN : IsAnnihilatedBy (primitiveIdeal e) N) (q : E ⟶ N) (hq : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) (hNprojective : ¬CategoryTheory.Projective { obj := N, property := hN }) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (primitiveTorsionAmbientTargetMap e q))

Quotient nonprojectivity makes the restricted target map surjective on the underlying ambient modules.

theorem MagnitudeConjecture.RightModule.primitiveTorsion_functionExact {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {Q E N : FinitelyGeneratedCategory A} (i : Q ⟶ E) (q : E ⟶ N) (hi : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom i)) (hexact : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom i) ⇑(CategoryTheory.ConcreteCategory.hom q)) : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom (primitiveTorsionMap e i)) ⇑(CategoryTheory.ConcreteCategory.hom (primitiveTorsionAmbientTargetMap e q))

The primitive torsion radical is left exact on an ambient exact pair. This is the kernel part of Hoshino's comparison and uses only the maximal annihilated-submodule construction.

theorem MagnitudeConjecture.RightModule.primitiveTorsionFGObj_nontrivial_of_not_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {Q E N : FinitelyGeneratedCategory A} (hN : IsAnnihilatedBy (primitiveIdeal e) N) (i : Q ⟶ E) (q : E ⟶ N) (hi : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom i)) (hexact : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom i) ⇑(CategoryTheory.ConcreteCategory.hom q)) (hq : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) (hNprojective : ¬CategoryTheory.Projective { obj := N, property := hN }) : Nontrivial ↑(primitiveTorsionFGObj e Q)

In Hoshino's situation the torsion part of the ambient kernel is nonzero. Once quotient nonprojectivity makes the restricted right almost-split map epic, a zero torsion kernel would make that map an isomorphism, contradicting right almost-splitness.

theorem MagnitudeConjecture.RightModule.primitiveTorsion_comp_eq_zero {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {Q E N : FinitelyGeneratedCategory A} (i : Q ⟶ E) (q : E ⟶ N) (hi : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom i)) (hexact : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom i) ⇑(CategoryTheory.ConcreteCategory.hom q)) : CategoryTheory.CategoryStruct.comp (primitiveTorsionMap e i) (primitiveTorsionAmbientTargetMap e q) = 0

theorem MagnitudeConjecture.RightModule.primitiveTorsion_comp_eq_zero_hom {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {Q E N : FinitelyGeneratedCategory A} (i : Q ⟶ E) (q : E ⟶ N) (hi : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom i)) (hexact : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom i) ⇑(CategoryTheory.ConcreteCategory.hom q)) : CategoryTheory.CategoryStruct.comp (primitiveTorsionMap e i).hom (primitiveTorsionAmbientTargetMap e q).hom = 0

theorem MagnitudeConjecture.RightModule.primitiveTorsion_shortExact {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {Q E N : FinitelyGeneratedCategory A} (i : Q ⟶ E) (q : E ⟶ N) (hi : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom i)) (hexact : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom i) ⇑(CategoryTheory.ConcreteCategory.hom q)) (hsurj : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (primitiveTorsionAmbientTargetMap e q))) : { X₁ := (primitiveTorsionFGObj e Q).obj, X₂ := (primitiveTorsionFGObj e E).obj, X₃ := N.obj, f := (primitiveTorsionMap e i).hom, g := (primitiveTorsionAmbientTargetMap e q).hom, zero := ⋯ }.ShortExact

If the torsion-restricted target map is surjective, the left-exact torsion pair is a short exact sequence of ambient modules.

theorem MagnitudeConjecture.RightModule.primitiveTorsion_shortExact_of_not_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {Q E N : FinitelyGeneratedCategory A} (hN : IsAnnihilatedBy (primitiveIdeal e) N) (i : Q ⟶ E) (q : E ⟶ N) (hi : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom i)) (hexact : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom i) ⇑(CategoryTheory.ConcreteCategory.hom q)) (hq : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) (hNprojective : ¬CategoryTheory.Projective { obj := N, property := hN }) : { X₁ := (primitiveTorsionFGObj e Q).obj, X₂ := (primitiveTorsionFGObj e E).obj, X₃ := N.obj, f := (primitiveTorsionMap e i).hom, g := (primitiveTorsionAmbientTargetMap e q).hom, zero := ⋯ }.ShortExact

Hoshino's restricted sequence is short exact whenever the quotient target is nonprojective.

theorem MagnitudeConjecture.RightModule.primitiveTorsion_fg_shortExact_of_not_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {Q E N : FinitelyGeneratedCategory A} (hN : IsAnnihilatedBy (primitiveIdeal e) N) (i : Q ⟶ E) (q : E ⟶ N) (hi : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom i)) (hexact : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom i) ⇑(CategoryTheory.ConcreteCategory.hom q)) (hq : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) (hNprojective : ¬CategoryTheory.Projective { obj := N, property := hN }) : { X₁ := primitiveTorsionFGObj e Q, X₂ := primitiveTorsionFGObj e E, X₃ := N, f := primitiveTorsionMap e i, g := primitiveTorsionAmbientTargetMap e q, zero := ⋯ }.ShortExact

Hoshino's restricted short exact sequence retained in the finitely generated ambient module category.