The ordinary quiver of a finite right-module category

The vertices are the chosen indecomposable projective right modules. Arrows from x to y index a basis of the radical quotient rad(P_y,P_x) / rad²(P_y,P_x) formed inside the full subcategory on those projectives. Choosing radical lifts realizes this quiver in the projective subcategory.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedModule {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : Module k ↑(S.almostSplitSkeleton.obj i)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedScalarTower {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : IsScalarTower k Aᵐᵒᵖ ↑(S.almostSplitSkeleton.obj i)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.objFinite {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : Module.Finite k ↑(S.almostSplitSkeleton.obj i)

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ProjectiveCategory {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Type

The full category on the selected indecomposable projectives.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCategoryCategory {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Category.{u, 0} S.ProjectiveCategory

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCategoryPreadditive {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Preadditive S.ProjectiveCategory

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCategoryLinear {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Linear k S.ProjectiveCategory

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryProjectiveObj {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) : S.ProjectiveCategory

A projective label regarded as an object of the selected projective subcategory.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryProjectiveFGObj {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) : FinitelyGeneratedCategory A

The selected projective represented by a label, as an ambient finitely generated right module.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCategoryHomFinite {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveCategory) : Module.Finite k (x ⟶ y)

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveInclusion {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor S.ProjectiveCategory (FinitelyGeneratedCategory A)

Inclusion of the selected projective category into finitely generated right modules.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveInclusion_additive {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : S.projectiveInclusion.Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveInclusion_linear {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor.Linear k S.projectiveInclusion

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveInclusion_full {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : S.projectiveInclusion.Full

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveInclusion_faithful {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : S.projectiveInclusion.Faithful

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCategoryEndLocal {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (X : S.ProjectiveCategory) : IsLocalRing (CategoryTheory.End X)

Endomorphism rings in the selected-projective category are local.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRadicalIdeal {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal S.ProjectiveCategory

The categorical radical pulled back to the full subcategory on selected projectives.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_projectiveRadicalIdeal_iff {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : S.ProjectiveCategory} (f : X ⟶ Y) : f ∈ S.projectiveRadicalIdeal.hom X Y ↔ S.projectiveInclusion.map f ∈ S.fgNilpotentRadicalData.ideal.hom (S.projectiveInclusion.obj X) (S.projectiveInclusion.obj Y)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveNilpotentRadicalData {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : QuotientSubmoduleEquidistribution.CategoricalRadical.NilpotentRadicalData S.ProjectiveCategory

The projective radical is nilpotent. Its powers only factor through selected projectives, while their images lie in the corresponding powers of the ambient categorical radical.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRadicalSubmodule {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : Submodule k (S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x)

The projective radical as a linear submodule of a selected-projective Hom-space.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRadicalSquareSubmodule {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : Submodule k (S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x)

The square of the radical formed inside the selected-projective subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRadicalSquare_le_radical {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : S.projectiveRadicalSquareSubmodule x y ≤ S.projectiveRadicalSubmodule x y

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRadicalSquareInRadicalSubmodule {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : Submodule k ↥(S.projectiveRadicalSubmodule x y)

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveIrreducibleHomSpace {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : Type u

The irreducible projective-morphism space used by the ordinary quiver.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrow {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : Type u

The ordinary-quiver arrow type, with direction opposite to module maps.

@[instance_reducible]

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

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowFintype {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : Fintype (S.OrdinaryArrow x y)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowBasis {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : Module.Basis (S.OrdinaryArrow x y) k (S.projectiveIrreducibleHomSpace x y)

The chosen finite basis of an ordinary-quiver arrow space.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowClass {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : S.projectiveIrreducibleHomSpace x y

The irreducible class indexed by a displayed ordinary-quiver arrow.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowClass_linearIndependent {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : LinearIndependent k fun (a : S.OrdinaryArrow x y) => S.ordinaryArrowClass a

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowRadical {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : ↥(S.projectiveRadicalSubmodule x y)

A chosen projective-radical representative of a displayed arrow.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowRadical_mkQ {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : Submodule.Quotient.mk (S.ordinaryArrowRadical a) = S.ordinaryArrowClass a

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowRadical_linearIndependent {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : LinearIndependent k fun (a : S.OrdinaryArrow x y) => S.ordinaryArrowRadical a

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowHom {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x

The projective morphism realizing a displayed ordinary-quiver arrow.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowFGHom {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : S.ordinaryProjectiveFGObj y ⟶ S.ordinaryProjectiveFGObj x

The same displayed arrow in the ambient finitely generated module category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowHom_mem_projectiveRadical {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : S.ordinaryArrowHom a ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowFGHom_mem_radical {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : S.ordinaryArrowFGHom a ∈ S.fgNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveFGObj y) (S.ordinaryProjectiveFGObj x)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryPathMap_mem_radicalPow {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (p : Quiver.Path x y) : LinearPathCategory.pathMap S.ordinaryProjectiveObj (fun {x x_1 : S.ProjectiveLabel} (a : S.OrdinaryArrow x x_1) => S.ordinaryArrowHom a) p ∈ (S.projectiveNilpotentRadicalData.ideal.pow p.length).hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x)

A realized path belongs to the power of the projective radical indexed by its length.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryPathMap_hom {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (p : Quiver.Path x y) : (LinearPathCategory.pathMap S.ordinaryProjectiveObj (fun {x x_1 : S.ProjectiveLabel} (a : S.OrdinaryArrow x x_1) => S.ordinaryArrowHom a) p).hom = LinearPathCategory.pathMap S.ordinaryProjectiveFGObj (fun {x x_1 : S.ProjectiveLabel} (a : S.OrdinaryArrow x x_1) => S.ordinaryArrowFGHom a) p

Taking the underlying ambient module map commutes with reversed path evaluation.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryArrowHom_linearIndependent {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : LinearIndependent k fun (a : S.OrdinaryArrow x y) => S.ordinaryArrowHom a

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryQuiverRealization {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor (LinearPathCategory.Category k S.ProjectiveLabel) S.ProjectiveCategory

The free linear path realization of the selected ordinary quiver.

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

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryFGQuiverRealization {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor (LinearPathCategory.Category k S.ProjectiveLabel) (FinitelyGeneratedCategory A)

The free ordinary-quiver realization in the ambient finitely generated module category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryFGQuiverRealization_map {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : LinearPathCategory.Category k S.ProjectiveLabel} (f : X ⟶ Y) : S.ordinaryFGQuiverRealization.map f = (S.ordinaryQuiverRealization.map f).hom

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryFGQuiverRealization_map_pathHom {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (p : Quiver.Path x y) : S.ordinaryFGQuiverRealization.map (LinearPathCategory.pathHom p) = LinearPathCategory.pathMap S.ordinaryProjectiveFGObj (fun {x x_1 : S.ProjectiveLabel} (a : S.OrdinaryArrow x x_1) => S.ordinaryArrowFGHom a) p

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryQuiverRealization_map_arrow {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : S.ordinaryQuiverRealization.map (LinearPathCategory.pathHom (have this := (have this := a; this).toPath; this)) = S.ordinaryArrowHom a