Literal factor categories of finite right-module categories

This file constructs the manuscript's categorical quotient by morphisms factoring through the additive closure of a selected set of indecomposable modules. It deliberately stops before the factor tau-sequences: the quotient category, its linear and additive structures, its finite biproducts, and its surviving skeleton are the reusable substrate for that construction.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SelectedAddCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : Type (u + 1)

The full additive subcategory generated by a set of selected indecomposable labels.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FactorsThroughSelected {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) {X Z : FinitelyGeneratedCategory A} (f : X ⟶ Z) : Prop

A morphism factors through the additive closure of K.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorThroughSelectedMaps {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X Y : S.SelectedAddCategory Set.univ) : Set (X ⟶ Y)

The maps in the complete additive category which factor through the selected additive subcategory.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorThroughSelectedIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal (S.SelectedAddCategory Set.univ)

The additive two-sided Hom ideal of maps factoring through the selected additive subcategory.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FactorCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : Type (u + 1)

The literal factor category add(ind mod A) / [add K].

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCategoryPreadditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : CategoryTheory.Preadditive (S.FactorCategory K)

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : CategoryTheory.Functor (S.SelectedAddCategory Set.univ) (S.FactorCategory K)

The quotient functor from the complete additive category.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorFunctor_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : (S.factorFunctor K).Additive

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCategoryLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : CategoryTheory.Linear k (S.FactorCategory K)

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorFunctor_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : CategoryTheory.Functor.Linear k (S.factorFunctor K)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.selectedAddCategoryHasFiniteBiproducts {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Limits.HasFiniteBiproducts (S.SelectedAddCategory Set.univ)

The complete additive category has finite biproducts.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.selectedAddCategory_hasFiniteBiproducts {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Limits.HasFiniteBiproducts (S.SelectedAddCategory Set.univ)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.selectedAddCategory_isIdempotentComplete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.IsIdempotentComplete (S.SelectedAddCategory Set.univ)

The full additive closure of the skeleton is closed under retracts and is therefore idempotent-complete.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.selectedAddCategory_idempotentComplete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.IsIdempotentComplete (S.SelectedAddCategory Set.univ)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCategoryHasFiniteBiproducts {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : CategoryTheory.Limits.HasFiniteBiproducts (S.FactorCategory K)

The factor category inherits finite biproducts from its source.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCategory_hasFiniteBiproducts {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : CategoryTheory.Limits.HasFiniteBiproducts (S.FactorCategory K)

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCategory_hasBinaryBiproducts {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : CategoryTheory.Limits.HasBinaryBiproducts (S.FactorCategory K)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.inAdd_univ {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : S.almostSplitSkeleton.InAdd Set.univ X

Completeness of the finite skeleton puts every finitely generated module in the additive closure of all skeleton labels.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientAddObject {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : S.SelectedAddCategory Set.univ

A finitely generated module regarded canonically as an object of the complete additive subcategory.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientAddFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor (FinitelyGeneratedCategory A) (S.SelectedAddCategory Set.univ)

The fully faithful inclusion into the explicit additive closure of the finite skeleton.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientAddFunctor_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.ambientAddFunctor.Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientAddFunctor_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor.Linear k S.ambientAddFunctor

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorModuleFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : CategoryTheory.Functor (FinitelyGeneratedCategory A) (S.FactorCategory K)

The literal quotient functor defined on every finitely generated right module.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientAddPoint {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : S.SelectedAddCategory Set.univ

A chosen ambient indecomposable as an object of the complete additive category.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SurvivingLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : Type

Labels which survive the quotient by add K.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorObject {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (x : S.SurvivingLabel K) : S.FactorCategory K

A surviving selected indecomposable in the factor category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorObject_isZero_of_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) {i : Fin S.n} (hi : i ∈ K) : CategoryTheory.Limits.IsZero ((S.factorFunctor K).obj (S.ambientAddPoint i))

A selected label becomes a zero object in the factor category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorObject_not_isZero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (x : S.SurvivingLabel K) : ¬CategoryTheory.Limits.IsZero (S.factorObject K x)

A label outside K remains nonzero in the factor category.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorEndRingHom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (x : S.SurvivingLabel K) : CategoryTheory.End (S.ambientAddPoint ↑x) →+* CategoryTheory.End (S.factorObject K x)

The quotient functor on a surviving object's endomorphisms, bundled as a ring homomorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorObject_end_isLocalRing {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (x : S.SurvivingLabel K) : IsLocalRing (CategoryTheory.End (S.factorObject K x))

A surviving indecomposable retains a local endomorphism ring in the literal factor category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorObject_indecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (x : S.SurvivingLabel K) : CategoryTheory.Indecomposable (S.factorObject K x)

A surviving skeleton object remains indecomposable after quotienting.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.selectedAdd_isRadicalMorphism_of_hom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : S.SelectedAddCategory Set.univ} (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f.hom) : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f

A morphism in the full additive subcategory is radical whenever its underlying module morphism is radical.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorObject_skeletal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) {x y : S.SurvivingLabel K} (e : Nonempty (S.factorObject K x ≅ S.factorObject K y)) : x = y

Distinct surviving skeleton labels remain nonisomorphic in the literal factor category.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCategoryHomFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X Y : S.FactorCategory K) : Module.Finite k (X ⟶ Y)

Hom spaces in the literal factor category remain finite-dimensional.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAmbientPointIsoFactorModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (i : Fin S.n) : (S.factorFunctor K).obj (S.ambientAddPoint i) ≅ (S.factorModuleFunctor K).obj (S.fgObj i)

The two canonical ways to send a skeleton object to the factor category are equal up to the proof carried by the full additive subcategory.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorBiproductIsoSubtypeOfIsZero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {J : Type u_1} [Fintype J] (f : J → S.FactorCategory K) (p : J → Prop) [DecidablePred p] (hzero : ∀ (j : J), ¬p j → CategoryTheory.Limits.IsZero (f j)) : ⨁ f ≅ ⨁ Subtype.restrict p f

Removing the summands outside a decidable subfamily does not change a finite biproduct when all of those summands are zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCategory_obj_decomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : S.FactorCategory K) : ∃ (m : ℕ) (label : Fin m → S.SurvivingLabel K), Nonempty (X ≅ ⨁ fun (i : Fin m) => S.factorObject K (label i))

Every object of the literal factor category is a finite biproduct of the surviving skeleton objects.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCategory_obj_complete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : S.FactorCategory K) (hX : CategoryTheory.Indecomposable X) : ∃ (x : S.SurvivingLabel K), Nonempty (X ≅ S.factorObject K x)

The surviving labels exhaust all indecomposable objects of the literal factor category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorFunctor_kernel_isNilpotent_on_surviving_biproduct {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) {m : ℕ} (label : Fin m → S.SurvivingLabel K) (f : CategoryTheory.End (⨁ fun (i : Fin m) => S.ambientAddPoint ↑(label i))) (hf : (S.factorFunctor K).map f = 0) : IsNilpotent f

On a biproduct of surviving representatives, every endomorphism killed by the quotient functor is nilpotent.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCategory_isIdempotentComplete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : CategoryTheory.IsIdempotentComplete (S.FactorCategory K)

The literal factor category is idempotent-complete.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCategory_idempotentComplete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : CategoryTheory.IsIdempotentComplete (S.FactorCategory K)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAdditiveGenerator {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : S.FactorCategory K

The biproduct of all surviving representatives is an additive generator of the literal factor category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAdditiveGenerator_isFiniteAddGenerator {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : CategoryTheory.IsFiniteAddGenerator (S.factorAdditiveGenerator K)

Every quotient object is a retract of a finite biproduct of copies of the surviving additive generator.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAdditiveGeneratorEndArtinian {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : IsArtinianRing (CategoryTheory.End (S.factorAdditiveGenerator K))

The quotient additive generator has an Artinian endomorphism ring because its endomorphism space is finite-dimensional over the coefficient field.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorNilpotentRadicalData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : QuotientSubmoduleEquidistribution.CategoricalRadical.NilpotentRadicalData (S.FactorCategory K)

The literal factor category has a nilpotent categorical radical.