Stable representables on a finite indecomposable skeleton

For a representation-finite module category, the projective-stable contravariant representable stable Hom(-, C) may be restricted to the finite skeleton of indecomposables. This file bundles that restriction as a finite-dimensional linear module. It is the functor appearing in Auslander--Reiten's uniserial-functor criterion.

def MagnitudeConjecture.ProjectiveStable.precomp {k : Type uk} [Field k] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (Y : D) {X Z : D} (g : X ⟶ Z) : Hom Z Y →ₗ[k] Hom X Y

Precomposition on projective-stable Hom.

@[simp]

theorem MagnitudeConjecture.ProjectiveStable.precomp_mk {k : Type uk} [Field k] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (Y : D) {X Z : D} (g : X ⟶ Z) (f : Z ⟶ Y) : (precomp Y g) (mk f) = mk (CategoryTheory.CategoryStruct.comp g f)

theorem MagnitudeConjecture.ProjectiveStable.factorSubmodule_eq_range_rightComp_of_projective_epi {k : Type uk} [Field k] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {P Y : D} (q : P ⟶ Y) [CategoryTheory.Projective P] [CategoryTheory.Epi q] (X : D) : factorSubmodule X Y = (CategoryTheory.Linear.rightComp k X q).range

If q : P ⟶ Y is an epimorphism from a projective object, then a morphism into Y factors through some projective exactly when it factors through q.

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecCategoryOppositeFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Fintype S.IndecCategoryᵒᵖ

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableContravariantRepresentable {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : CategoryTheory.Functor S.IndecCategoryᵒᵖ (ModuleCat k)

The restriction of stable Hom(-, C) to the opposite finite skeleton of indecomposable right modules.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableContravariantRepresentable_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : (S.projectiveStableContravariantRepresentable C).Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableContravariantRepresentable_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : CategoryTheory.Functor.Linear k (S.projectiveStableContravariantRepresentable C)

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableContravariantRepresentableLinearModule {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : CoveringHom.LinearModuleCategory k

The restricted stable representable as an additive linear module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableContravariantRepresentable_isFiniteDimensional {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : CoveringHom.IsFiniteDimensionalModule k (S.projectiveStableContravariantRepresentableLinearModule C)

On the finite indecomposable skeleton, the stable representable is a finite-dimensional linear module.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableContravariantRepresentable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : CoveringHom.FiniteDimensionalModuleCategory k

The restricted stable representable as an object of the finite functor category.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : CoveringHom.FiniteDimensionalModuleCategory k

The ordinary contravariant representable restricted to the finite indecomposable skeleton.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecOppositeRepresentableFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule (Opposite.op i))

The representable at an object of the opposite indecomposable skeleton is finite-dimensional.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedFgObjOppositeHomLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) (X : S.IndecCategoryᵒᵖ) : (S.inclusion.obj (Opposite.unop X) ⟶ S.inclusion.obj i) ≃ₗ[k] Opposite.op i ⟶ X

Ambient morphisms between chosen skeleton objects are the same as morphisms in the induced skeleton, written in the variance appropriate for the opposite representable.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedContravariantRepresentableFgObjRawIso {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : CoveringHom.restrictedLinearYoneda S.inclusion (S.fgObj i).obj ≅ (CategoryTheory.linearCoyoneda k S.IndecCategoryᵒᵖ).obj (Opposite.op (Opposite.op i))

Restricted ambient Yoneda at a chosen indecomposable agrees naturally with the corresponding representable of the opposite finite skeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedContravariantRepresentableFgObjLinearIso {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : CoveringHom.restrictedLinearYonedaLinearModule S.inclusion (S.fgObj i).obj ≅ CoveringHom.linearCoyonedaLinearModule (Opposite.op i)

Linear-module form of the comparison with the opposite-skeleton representable.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableFgObjIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ≅ CoveringHom.finiteDimensionalLinearCoyoneda (Opposite.op i) ⋯

Finite-module form of the comparison with the opposite-skeleton representable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDimensionalModule_exists_nonzero_restrictedRepresentableMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {M : CoveringHom.FiniteDimensionalModuleCategory k} (hM : ¬CategoryTheory.Limits.IsZero M) : ∃ (i : S.IndecCategory) (f : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ M), f ≠ 0

A nonzero finite functor on the indecomposable skeleton receives a nonzero map from one restricted representable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDimensionalModule_isEssentialMono_of_simple_restrictedRepresentable_factors {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {L F : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple L] (l : L ⟶ F) [CategoryTheory.Mono l] (hfactor : ∀ {T : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple T] (t : T ⟶ F) [CategoryTheory.Mono t] (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T), p ≠ 0 → ∃ (a : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ L), CategoryTheory.CategoryStruct.comp a l = CategoryTheory.CategoryStruct.comp p t) : IsEssentialMono l

To prove a simple finite subfunctor essential, it suffices to factor the composites of its nonzero restricted-representable generators through it.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecCategory_obj_end_isLocalRing {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : IsLocalRing (CategoryTheory.End i)

A chosen object has local endomorphism ring already in the induced indecomposable skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecCategoryOpposite_obj_end_isLocalRing {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : S.IndecCategoryᵒᵖ) : IsLocalRing (CategoryTheory.End X)

Local endomorphism rings pass to objects of the opposite finite indecomposable skeleton.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableFgObj_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : CategoryTheory.Projective (S.finiteRestrictedContravariantRepresentable (S.fgObj i))

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableFgObj_end_isLocalRing {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : IsLocalRing (CategoryTheory.End (S.finiteRestrictedContravariantRepresentable (S.fgObj i)))

The ordinary restricted representable at a chosen indecomposable has local endomorphism ring.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableRadical {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : CoveringHom.FiniteDimensionalModuleCategory k

The categorical radical of the finite representable corresponding to a chosen indecomposable, transported to the restricted ambient representable.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableRadicalInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : S.finiteRestrictedContravariantRepresentableRadical i ⟶ S.finiteRestrictedContravariantRepresentable (S.fgObj i)

The radical inclusion after transporting from the opposite-skeleton representable to the restricted ambient representable.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableRadicalInclusion_app_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) (X : S.IndecCategoryᵒᵖ) (q : ↥(CategoryTheory.radicalHomSubmodule k (Opposite.op i) X)) : (CategoryTheory.ConcreteCategory.hom ((S.finiteRestrictedContravariantRepresentableRadicalInclusion i).hom.hom.app X)) q = (↑q).unop.hom

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableRadicalInclusion_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : CategoryTheory.Mono (S.finiteRestrictedContravariantRepresentableRadicalInclusion i)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableRadicalInclusion_isRightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.finiteRestrictedContravariantRepresentableRadicalInclusion i)

The transported radical inclusion is the right almost-split boundary of the chosen restricted representable.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) {C D : FinitelyGeneratedCategory A} (f : C ⟶ D) : S.finiteRestrictedContravariantRepresentable C ⟶ S.finiteRestrictedContravariantRepresentable D

Postcomposition gives the expected map between two restricted ordinary representables.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_app_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C D : FinitelyGeneratedCategory A} (f : C ⟶ D) (X : S.IndecCategoryᵒᵖ) (g : S.inclusion.obj (Opposite.unop X) ⟶ C.obj) : (CategoryTheory.ConcreteCategory.hom ((S.finiteRestrictedContravariantRepresentableMap f).hom.hom.app X)) g = CategoryTheory.CategoryStruct.comp g f.hom

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_fgObj_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i j : S.IndecCategory) (f : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ S.finiteRestrictedContravariantRepresentable (S.fgObj j)) : have h := CategoryTheory.ObjectProperty.homMk (id ((CategoryTheory.ConcreteCategory.hom (f.hom.hom.app (Opposite.op i))) (CategoryTheory.CategoryStruct.id (S.inclusion.obj i)))); S.finiteRestrictedContravariantRepresentableMap h = f

Restricted Yoneda is full on the chosen indecomposable skeleton: a map between two represented functors is recovered by evaluating it at the identity of its source.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {B C D : FinitelyGeneratedCategory A} (f : B ⟶ C) (g : C ⟶ D) : S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap f) (S.finiteRestrictedContravariantRepresentableMap g)

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_id {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.id C) = CategoryTheory.CategoryStruct.id (S.finiteRestrictedContravariantRepresentable C)

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_isIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C D : FinitelyGeneratedCategory A} (f : C ⟶ D) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (S.finiteRestrictedContravariantRepresentableMap f)

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_add {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C D : FinitelyGeneratedCategory A} (f g : C ⟶ D) : S.finiteRestrictedContravariantRepresentableMap (f + g) = S.finiteRestrictedContravariantRepresentableMap f + S.finiteRestrictedContravariantRepresentableMap g

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (C D : FinitelyGeneratedCategory A) : S.finiteRestrictedContravariantRepresentableMap 0 = 0

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_neg {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C D : FinitelyGeneratedCategory A} (f : C ⟶ D) : S.finiteRestrictedContravariantRepresentableMap (-f) = -S.finiteRestrictedContravariantRepresentableMap f

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_eq_splitMono_add_complement {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y Z : FinitelyGeneratedCategory A} (t : X ⟶ Y) [CategoryTheory.IsSplitMono t] (d : QuotientSubmoduleEquidistribution.SplitMonoComplement t) (f : Y ⟶ Z) : S.finiteRestrictedContravariantRepresentableMap f = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.retraction t)) (S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.comp t f)) + CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap d.projection) (S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.comp d.inclusion f))

A split summand and its chosen complement decompose the restricted representable map induced by any morphism out of the ambient object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_comp_eq_complement {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y Z : FinitelyGeneratedCategory A} (t : X ⟶ Y) [CategoryTheory.IsSplitMono t] (d : QuotientSubmoduleEquidistribution.SplitMonoComplement t) (f : Y ⟶ Z) {G : CoveringHom.FiniteDimensionalModuleCategory k} (p : S.finiteRestrictedContravariantRepresentable Z ⟶ G) (hzero : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.comp t f)) p = 0) : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap f) p = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap d.projection) (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.comp d.inclusion f)) p)

If one split-summand branch is killed after a further map, the whole image is generated by the complementary branch.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_to_fgObj_not_isSplitEpi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (f : C ⟶ S.fgObj i) (hf : ¬CategoryTheory.IsSplitEpi f) : ¬CategoryTheory.IsSplitEpi (S.finiteRestrictedContravariantRepresentableMap f)

A nonsplit epimorphism onto a chosen indecomposable remains nonsplit after applying restricted Yoneda, even when its source is not itself a chosen indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.imageSubobject_finiteRestrictedContravariantRepresentableMap_eq_radical {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (f : C ⟶ S.fgObj i) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) : CategoryTheory.Limits.imageSubobject (S.finiteRestrictedContravariantRepresentableMap f) = CategoryTheory.Subobject.mk (S.finiteRestrictedContravariantRepresentableRadicalInclusion i)

Restricted Yoneda sends a right almost-split map ending at a chosen indecomposable onto the whole radical of the corresponding representable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.imageSubobject_comp_eq_of_epi {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {X Y Z : D} (e : X ⟶ Y) [CategoryTheory.Epi e] (q : Y ⟶ Z) : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp e q) = CategoryTheory.Limits.imageSubobject q

In an abelian category, precomposing a morphism by an epimorphism does not change its image subobject.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.imageSubobjectCompMonoIso {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {X Y Z : D} (q : X ⟶ Y) (m : Y ⟶ Z) [CategoryTheory.Mono m] : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject q) ≅ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp q m))

Postcomposition by a monomorphism preserves the object underlying an image, although it changes the ambient object in which the image sits.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.imageSubobject_radicalInclusion_comp_eq_rightAlmostSplit_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (f : C ⟶ S.fgObj i) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) {G : CoveringHom.FiniteDimensionalModuleCategory k} (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) p) = CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap f) p)

Pushing a representable radical through any further map can equivalently be computed from any right almost-split map ending at that representable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_not_isSplitEpi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {i j : S.IndecCategory} (f : S.fgObj j ⟶ S.fgObj i) (hf : ¬CategoryTheory.IsSplitEpi f) : ¬CategoryTheory.IsSplitEpi (S.finiteRestrictedContravariantRepresentableMap f)

A nonsplit epimorphism between ambient modules remains nonsplit after applying the restricted contravariant representable construction.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_finiteRestrictedContravariantRepresentableRadicalFactor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {i j : S.IndecCategory} (f : S.fgObj j ⟶ S.fgObj i) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) : ∃ (l : S.finiteRestrictedContravariantRepresentable (S.fgObj j) ⟶ S.finiteRestrictedContravariantRepresentableRadical i), CategoryTheory.CategoryStruct.comp l (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) = S.finiteRestrictedContravariantRepresentableMap f

An irreducible map between chosen indecomposables factors, after restricted Yoneda, through the transported radical of its target.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableQuotientLinearModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : (S.finiteRestrictedContravariantRepresentable C).obj ⟶ (S.finiteProjectiveStableContravariantRepresentable C).obj

The objectwise stable-quotient map from the restricted ordinary representable to the restricted projective-stable representable.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableQuotient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : S.finiteRestrictedContravariantRepresentable C ⟶ S.finiteProjectiveStableContravariantRepresentable C

The stable-quotient map in the finite-dimensional functor category.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedToProjectiveStableMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ S.finiteProjectiveStableContravariantRepresentable C

A module morphism out of a chosen indecomposable represents a natural map into the stable representable of its target.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedToProjectiveStableMap_app_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (X : S.IndecCategoryᵒᵖ) (f : S.inclusion.obj (Opposite.unop X) ⟶ S.inclusion.obj i) : (CategoryTheory.ConcreteCategory.hom ((S.finiteRestrictedToProjectiveStableMap i h).hom.hom.app X)) f = ProjectiveStable.mk (CategoryTheory.CategoryStruct.comp f h.hom)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_comp_stableMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} {i j : S.IndecCategory} (f : S.fgObj j ⟶ S.fgObj i) (h : S.fgObj i ⟶ C) : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap f) (S.finiteRestrictedToProjectiveStableMap i h) = S.finiteRestrictedToProjectiveStableMap j (CategoryTheory.CategoryStruct.comp f h)

Precomposing a stable generator by an ordinary morphism agrees with postcomposing the corresponding restricted representable map.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) : CoveringHom.FiniteDimensionalModuleCategory k

The finite functor generated by one stable morphism.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImageInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) : S.finiteProjectiveStableImage i h ⟶ S.finiteProjectiveStableContravariantRepresentable C

The canonical inclusion of a cyclic stable image into the full stable representable.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImageInclusion_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) : CategoryTheory.Mono (S.finiteProjectiveStableImageInclusion i h)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImagePresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ S.finiteProjectiveStableImage i h

The canonical epimorphism from the representing projective onto the stable image generated by a morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImagePresentation_comp_inclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) : CategoryTheory.CategoryStruct.comp (S.finiteProjectiveStableImagePresentation i h) (S.finiteProjectiveStableImageInclusion i h) = S.finiteRestrictedToProjectiveStableMap i h

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImagePresentation_comp_inclusion_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) {Z : CoveringHom.FiniteDimensionalModuleCategory k} (h✝ : S.finiteProjectiveStableContravariantRepresentable C ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.finiteProjectiveStableImagePresentation i h) (CategoryTheory.CategoryStruct.comp (S.finiteProjectiveStableImageInclusion i h) h✝) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedToProjectiveStableMap i h) h✝

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImagePresentation_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) : CategoryTheory.Epi (S.finiteProjectiveStableImagePresentation i h)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImagePresentation_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) : S.finiteProjectiveStableImagePresentation i h ≠ 0

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImageMinimalProjectivePresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) : MinimalProjectivePresentation (S.finiteProjectiveStableImage i h)

Every nonzero cyclic stable image has the expected indecomposable representable as its minimal projective cover.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImageRadical_isRadicalSubobject {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) : IsUniserialObject.IsRadicalSubobject (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h)))

Pushing the representable radical through the minimal cover of a nonzero cyclic stable image gives a radical subobject of that image.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImageRadical_ne_top {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h)) ≠ ⊤

For a nonzero stable generator, its pushed-forward representable radical is a proper subobject of the cyclic stable image.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImageRadicalCokernel_simple {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) : CategoryTheory.Simple (CategoryTheory.Limits.cokernel (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h))).arrow)

The top of every nonzero cyclic stable image is simple: quotienting by the pushed-forward representable radical gives a simple object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImage_isUniserial_of_radical {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hrad : IsUniserialObject (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h))))) : IsUniserialObject (S.finiteProjectiveStableImage i h)

The radical step for cyclic stable images: uniseriality of the proper pushed-forward radical implies uniseriality of the image itself.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImage_isUniserial_of_closedRadicalSuccessors {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (Good : {C : FinitelyGeneratedCategory A} → (i : S.IndecCategory) → (S.fgObj i ⟶ C) → Prop) (hsuccessor : ∀ {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C), Good i h → S.finiteRestrictedToProjectiveStableMap i h ≠ 0 → ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h)))) → ∃ (j : S.IndecCategory) (g : S.fgObj j ⟶ C), Good j g ∧ S.finiteRestrictedToProjectiveStableMap j g ≠ 0 ∧ Nonempty (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h))) ≅ S.finiteProjectiveStableImage j g)) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hgood : Good i h) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) : IsUniserialObject (S.finiteProjectiveStableImage i h)

Finite-length radical induction for a class of cyclic stable images. If the class is closed under taking a nonzero radical stage, then every image in the class is uniserial.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImage_isUniserial_of_radicalSuccessors {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hsuccessor : ∀ {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C), S.finiteRestrictedToProjectiveStableMap i h ≠ 0 → ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h)))) → ∃ (j : S.IndecCategory) (g : S.fgObj j ⟶ C), S.finiteRestrictedToProjectiveStableMap j g ≠ 0 ∧ Nonempty (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h))) ≅ S.finiteProjectiveStableImage j g)) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) : IsUniserialObject (S.finiteProjectiveStableImage i h)

The predicate-free form of finite-length radical induction.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableQuotient_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : CategoryTheory.Epi (S.finiteProjectiveStableQuotient C)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_finiteRestrictedToProjectiveStableMap_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i j : S.IndecCategory) (f : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ S.finiteProjectiveStableContravariantRepresentable (S.fgObj j)) : ∃ (h : S.fgObj i ⟶ S.fgObj j), S.finiteRestrictedToProjectiveStableMap i h = f

Every map from a restricted representable to the stable representable of a chosen indecomposable is induced by an actual module morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableQuotient_fgObj_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) (hi : ¬CategoryTheory.Projective (S.inclusion.obj i)) : S.finiteProjectiveStableQuotient (S.fgObj i) ≠ 0

For a nonprojective indecomposable, the quotient from ordinary to stable Hom is nonzero: otherwise its identity would factor through a projective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableQuotient_fgObj_isRightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) (hi : ¬CategoryTheory.Projective (S.inclusion.obj i)) : QuotientSubmoduleEquidistribution.IsRightMinimal (S.finiteProjectiveStableQuotient (S.fgObj i))

At a nonprojective indecomposable, the stable quotient is the minimal projective cover of the restricted stable representable.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableMinimalProjectivePresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) (hi : ¬CategoryTheory.Projective (S.inclusion.obj i)) : MinimalProjectivePresentation (S.finiteProjectiveStableContravariantRepresentable (S.fgObj i))

The canonical minimal projective presentation of the stable representable at a nonprojective indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedMap_stableQuotient_app_range_eq_ker {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {P C : FinitelyGeneratedCategory A} (q : P ⟶ C) [CategoryTheory.Epi q] (hP : CategoryTheory.Projective P.obj) (X : S.IndecCategoryᵒᵖ) : have J := (CoveringHom.IsFiniteDimensionalModule k).ι; have I := (CoveringHom.IsLinearModule k).ι; (ModuleCat.Hom.hom ((I.map (J.map (S.finiteRestrictedContravariantRepresentableMap q))).app X)).range = (ModuleCat.Hom.hom ((I.map (J.map (S.finiteProjectiveStableQuotient C))).app X)).ker

A projective epimorphism presents the stable representable pointwise: the image of postcomposition with the epimorphism is exactly the kernel of the stable quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedMap_comp_stableQuotient_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {P C : FinitelyGeneratedCategory A} (q : P ⟶ C) (hP : CategoryTheory.Projective P.obj) : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap q) (S.finiteProjectiveStableQuotient C) = 0

Postcomposition through a projective is killed by the stable quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedMap_cokernelMap_exact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U P : FinitelyGeneratedCategory A} (g : U ⟶ P) [CategoryTheory.Mono g] : { X₁ := S.finiteRestrictedContravariantRepresentable U, X₂ := S.finiteRestrictedContravariantRepresentable P, X₃ := S.finiteRestrictedContravariantRepresentable (CategoryTheory.Limits.cokernel g), f := S.finiteRestrictedContravariantRepresentableMap g, g := S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.Limits.cokernel.π g), zero := ⋯ }.Exact

The representables of a monomorphism and its cokernel projection form an exact sequence. This is the left half of the explicit projective presentation used for a quotient by an irreducible projective submodule.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedMap_stableQuotient_exact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {P C : FinitelyGeneratedCategory A} (q : P ⟶ C) [CategoryTheory.Epi q] (hP : CategoryTheory.Projective P.obj) : { X₁ := S.finiteRestrictedContravariantRepresentable P, X₂ := S.finiteRestrictedContravariantRepresentable C, X₃ := S.finiteProjectiveStableContravariantRepresentable C, f := S.finiteRestrictedContravariantRepresentableMap q, g := S.finiteProjectiveStableQuotient C, zero := ⋯ }.Exact

Hence a projective epimorphism gives an exact two-term presentation of the restricted stable representable.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedMap_stableQuotient_isCokernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {P C : FinitelyGeneratedCategory A} (q : P ⟶ C) [CategoryTheory.Epi q] (hP : CategoryTheory.Projective P.obj) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (S.finiteProjectiveStableQuotient C) ⋯)

A projective epimorphism presents the restricted stable representable as the actual cokernel of postcomposition. This upgrades the pointwise exact sequence above to the projective-presentation interface used in the Auslander--Reiten socle argument.