Simple socles of stable representables

Pointwise coefficient duality embeds the dual of a stable representable into the dual corepresentable at the same indecomposable. This is the injective envelope used in Auslander--Reiten's socle-series proof of Corollary 3.8.

theorem MagnitudeConjecture.isEssentialMono_of_simple_comp_mono_into_injective_local_end {C₀ : Type u₀} [CategoryTheory.Category.{v₀, u₀} C₀] [CategoryTheory.Abelian C₀] {T H I : C₀} [CategoryTheory.Simple T] [CategoryTheory.Injective I] [IsLocalRing (CategoryTheory.End I)] (t : T ⟶ H) (m : H ⟶ I) [CategoryTheory.Mono m] (s : T ⟶ I) [CategoryTheory.Mono s] (hs : s ≠ 0) (htm : CategoryTheory.CategoryStruct.comp t m = s) : IsEssentialMono t

A simple subobject remains essential after restricting an indecomposable injective to any intermediate subobject containing it.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteReverseCoefficientDualMap {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {M N : CoveringHom.FiniteDimensionalModuleCategory k} (f : M ⟶ N) : CoveringHom.reverseFiniteCoefficientDual N ⟶ CoveringHom.reverseFiniteCoefficientDual M

Pointwise coefficient duality in the direction from modules on the opposite indecomposable skeleton back to modules on the skeleton.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteReverseCoefficientDualMap_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {M N : CoveringHom.FiniteDimensionalModuleCategory k} (f : M ⟶ N) [CategoryTheory.Epi f] : CategoryTheory.Mono (S.finiteReverseCoefficientDualMap f)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteReverseCoefficientDualMap_ne_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {M N : CoveringHom.FiniteDimensionalModuleCategory k} (f : M ⟶ N) (hf : f ≠ 0) : S.finiteReverseCoefficientDualMap f ≠ 0

Over a field, coefficient duality detects whether a natural transformation of finite modules is zero.

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

Dual corepresentables on the finite indecomposable skeleton satisfy the finite-module condition.

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

The reverse coefficient dual of a restricted ambient representable is naturally the dual corepresentable of the corresponding skeleton object.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDualProjectiveStableRepresentable {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 coefficient dual of a stable representable.

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

Dualizing the stable quotient gives its canonical inclusion into the dual of the ordinary restricted representable.

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDualProjectiveStableCorepresentableInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : S.finiteDualProjectiveStableRepresentable (S.fgObj i) ⟶ CoveringHom.finiteDimensionalDualLinearYoneda i ⋯

At a chosen indecomposable, the dual stable representable embeds in the standard dual corepresentable.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDualProjectiveStableCorepresentableInclusion_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : CategoryTheory.Mono (S.finiteDualProjectiveStableCorepresentableInclusion i)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDualProjectiveStableCorepresentableInclusion_ne_zero {k A : Type u} [Field k] [IsAlgClosed 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.finiteDualProjectiveStableCorepresentableInclusion i ≠ 0

The dual stable embedding is nonzero at a nonprojective indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDualProjectiveStableCorepresentableInclusion_isEssential {k A : Type u} [Field k] [IsAlgClosed 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)) : IsEssentialMono (S.finiteDualProjectiveStableCorepresentableInclusion i)

The dual stable representable is an essential subobject of its ambient indecomposable injective dual corepresentable.

@[reducible, inline]

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

The canonical simple socle of the ambient dual corepresentable.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDualProjectiveStableSocleInclusion {k A : Type u} [Field k] [IsAlgClosed 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.finiteDualProjectiveStableSocle i ⟶ S.finiteDualProjectiveStableRepresentable (S.fgObj i)

The canonical ambient socle factors through every nonzero dual stable representable subobject.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDualProjectiveStableSocleInclusion_comp {k A : Type u} [Field k] [IsAlgClosed 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)) : CategoryTheory.CategoryStruct.comp (S.finiteDualProjectiveStableSocleInclusion i hi) (S.finiteDualProjectiveStableCorepresentableInclusion i) = CoveringHom.finiteDimensionalDualLinearYonedaSocleInclusion i ⋯

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDualProjectiveStableSocleInclusion_comp_assoc {k A : Type u} [Field k] [IsAlgClosed 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)) {Z : CoveringHom.FiniteDimensionalModuleCategory k} (h : CoveringHom.finiteDimensionalDualLinearYoneda i ⋯ ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.finiteDualProjectiveStableSocleInclusion i hi) (CategoryTheory.CategoryStruct.comp (S.finiteDualProjectiveStableCorepresentableInclusion i) h) = CategoryTheory.CategoryStruct.comp (CoveringHom.finiteDimensionalDualLinearYonedaSocleInclusion i ⋯) h

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDualProjectiveStableSocleInclusion_mono {k A : Type u} [Field k] [IsAlgClosed 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)) : CategoryTheory.Mono (S.finiteDualProjectiveStableSocleInclusion i hi)

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteDualProjectiveStableSocleInclusion_isEssential {k A : Type u} [Field k] [IsAlgClosed 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)) : IsEssentialMono (S.finiteDualProjectiveStableSocleInclusion i hi)

For a nonprojective indecomposable, the dual stable representable has the canonical ambient simple as an essential socle.