Uniserial projective-stable covariant representables

This file formalizes the module-theoretic input used in Auslander--Reiten, Proposition 1.1(a). The first step is the finite-density extension of covariant Yoneda projectivity from chosen indecomposables to arbitrary finitely generated modules.

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

Restricted covariant Yoneda, regarded as an additive functor from the opposite of finitely generated modules.

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentable_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : CategoryTheory.Projective (S.finiteRestrictedCovariantRepresentable C)

Restricted covariant representables of arbitrary finitely generated modules are projective. Decompose the representing module into the chosen indecomposables and apply additivity of covariant Yoneda on the opposite category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableFunctor_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.finiteRestrictedCovariantRepresentableFunctor.Full

Finite additive density upgrades covariant Yoneda fullness on the chosen indecomposables to fullness on all finitely generated modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_eq_finiteRestrictedCovariantRepresentableMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (B C : FinitelyGeneratedCategory A) (p : S.finiteRestrictedCovariantRepresentable B ⟶ S.finiteRestrictedCovariantRepresentable C) : ∃ (h : C ⟶ B), S.finiteRestrictedCovariantRepresentableMap h = p

Every natural map between restricted covariant representables is induced by a unique-variance module map.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedToProjectiveStableCovariantMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) : S.finiteRestrictedCovariantRepresentable Y ⟶ S.finiteProjectiveStableCovariantRepresentable X

A module map f : X ⟶ Y generates a map from covariant Hom(Y,-) to projective-stable Hom(X,-).

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedToProjectiveStableCovariantMap_app_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) (Z : S.IndecCategory) (g : Y.obj ⟶ S.inclusion.obj Z) : (CategoryTheory.ConcreteCategory.hom ((S.finiteRestrictedToProjectiveStableCovariantMap f).hom.hom.app Z)) g = ProjectiveStable.mk (CategoryTheory.CategoryStruct.comp f.hom g)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantImageSubobject {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) : CategoryTheory.Subobject (S.finiteProjectiveStableCovariantRepresentable X)

The stable covariant image subobject generated by a module map.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantImage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) : CoveringHom.FiniteDimensionalModuleCategory k

The object underlying the stable covariant image generated by a module map.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantImageInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) : S.finiteProjectiveStableCovariantImage f ⟶ S.finiteProjectiveStableCovariantRepresentable X

Inclusion of a generated stable covariant image into the represented stable functor.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantImagePresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) : S.finiteRestrictedCovariantRepresentable Y ⟶ S.finiteProjectiveStableCovariantImage f

Presentation of a generated stable covariant image by the corresponding ordinary representable.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantImagePresentation_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) : CategoryTheory.Epi (S.finiteProjectiveStableCovariantImagePresentation f)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantImagePresentation_comp_inclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (S.finiteProjectiveStableCovariantImagePresentation f) (S.finiteProjectiveStableCovariantImageInclusion f) = S.finiteRestrictedToProjectiveStableCovariantMap f

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantImagePresentation_comp_inclusion_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) {Z : CoveringHom.FiniteDimensionalModuleCategory k} (h : S.finiteProjectiveStableCovariantRepresentable X ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.finiteProjectiveStableCovariantImagePresentation f) (CategoryTheory.CategoryStruct.comp (S.finiteProjectiveStableCovariantImageInclusion f) h) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedToProjectiveStableCovariantMap f) h

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_stableFactor_of_covariantImage_le {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} (f : X ⟶ Y) (g : X ⟶ Z) (hfg : S.finiteProjectiveStableCovariantImageSubobject f ≤ S.finiteProjectiveStableCovariantImageSubobject g) : ∃ (t : Z ⟶ Y), S.finiteRestrictedToProjectiveStableCovariantMap (CategoryTheory.CategoryStruct.comp g t) = S.finiteRestrictedToProjectiveStableCovariantMap f

Inclusion of generated image subfunctors lifts to factorization of the generating module maps after passage to projective-stable Hom.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantImages_comparable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X : FinitelyGeneratedCategory A} (hX : IsUniserialObject (S.finiteProjectiveStableCovariantRepresentable X)) {Y Z : FinitelyGeneratedCategory A} (f : X ⟶ Y) (g : X ⟶ Z) : S.finiteProjectiveStableCovariantImageSubobject f ≤ S.finiteProjectiveStableCovariantImageSubobject g ∨ S.finiteProjectiveStableCovariantImageSubobject g ≤ S.finiteProjectiveStableCovariantImageSubobject f

Uniseriality of the represented projective-stable covariant functor makes the images generated by any two maps out of the represented module comparable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorsThroughProjective_of_covariantStableMap_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) (hf : S.finiteRestrictedToProjectiveStableCovariantMap f = 0) : Nonempty (ProjectiveStable.FactorsThroughProjective f.hom)

Vanishing of the restricted natural map into projective-stable covariant Hom detects an actual factorization through a projective module. Finite additive density lets the chosen indecomposables test every target module.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedToProjectiveStableCovariantMap_sub {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f g : X ⟶ Y) : S.finiteRestrictedToProjectiveStableCovariantMap (f - g) = S.finiteRestrictedToProjectiveStableCovariantMap f - S.finiteRestrictedToProjectiveStableCovariantMap g

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorsThroughProjective_of_covariantStableMaps_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f g : X ⟶ Y) (hfg : S.finiteRestrictedToProjectiveStableCovariantMap f = S.finiteRestrictedToProjectiveStableCovariantMap g) : Nonempty (ProjectiveStable.FactorsThroughProjective (f - g).hom)

Equality of the induced stable natural maps means that the difference of the underlying module maps factors through a projective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.stableFactorization_dichotomy_of_covariantUniserial {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X : FinitelyGeneratedCategory A} (hX : IsUniserialObject (S.finiteProjectiveStableCovariantRepresentable X)) {Y Z : FinitelyGeneratedCategory A} (f : X ⟶ Y) (g : X ⟶ Z) : (∃ (t : Z ⟶ Y), Nonempty (ProjectiveStable.FactorsThroughProjective (f - CategoryTheory.CategoryStruct.comp g t).hom)) ∨ ∃ (t : Y ⟶ Z), Nonempty (ProjectiveStable.FactorsThroughProjective (g - CategoryTheory.CategoryStruct.comp f t).hom)

The comparison conclusion used in Auslander--Reiten, Proposition 1.1(a): for two maps out of X, one differs stably from a composite through the other.