Ext from a projective presentation on the finite module skeleton

This file restricts Ext¹(X,-) to the finite indecomposable skeleton and packages the canonical natural epimorphism

Ext¹(X,-) ⟶ \underline{Hom}(ΩX,-).

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FG {A : Type u} [Ring A] : Type (u + 1)

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCoverShortComplex {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {X : FG} (P : MinimalProjectivePresentation X) : CategoryTheory.ShortComplex FG

The short exact sequence defined by a projective cover.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCoverShortComplex_shortExact {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : (projectiveCoverShortComplex P).ShortExact

The projective-cover sequence is short exact.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgMap {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {Y Z : S.IndecCategory} (f : Y ⟶ Z) : S.fgObj Y ⟶ S.fgObj Z

A skeleton morphism bundled in the finitely generated module category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedExtOne {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : CategoryTheory.Functor S.IndecCategory (ModuleCat k)

The restriction of Ext¹(X,-) to the finite skeleton of indecomposable right modules.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedExtOne_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : (S.restrictedExtOne P).Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedExtOne_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : CategoryTheory.Functor.Linear k (S.restrictedExtOne P)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedExtOneLinearModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : CoveringHom.LinearModuleCategory k

Restricted degree-one Ext as a linear module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedExtOne_isFiniteDimensional {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : CoveringHom.IsFiniteDimensionalModule k (S.restrictedExtOneLinearModule P)

Restricted degree-one Ext is pointwise finite-dimensional and has finite support.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedExtOne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : CoveringHom.FiniteDimensionalModuleCategory k

Restricted degree-one Ext in the finite functor category.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgHomLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] (U V : FG) : (U.obj ⟶ V.obj) →ₗ[k] U ⟶ V

Bundle an ambient module morphism between finitely generated objects.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.forgetFGHomLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] (U V : FG) : (U ⟶ V) →ₗ[k] U.obj ⟶ V.obj

Forget the finite-generation property on a morphism, as a linear map.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientConnectingLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) (Y : FG) : ((CategoryTheory.Limits.kernel P.f).obj ⟶ Y.obj) →ₗ[k] CategoryTheory.Abelian.Ext X Y 1

The projective-presentation connecting map, with its source written as ambient module morphisms.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientConnectingLinear_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) (Y : FG) (f : (CategoryTheory.Limits.kernel P.f).obj ⟶ Y.obj) : (ambientConnectingLinear P Y) f = (ProjectivePresentationExt.connectingLinear ⋯ Y) (CategoryTheory.ObjectProperty.homMk f)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientConnectingLinear_postcomp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) {Y Z : FG} (a : Y ⟶ Z) (f : (CategoryTheory.Limits.kernel P.f).obj ⟶ Y.obj) : (ambientConnectingLinear P Z) (CategoryTheory.CategoryStruct.comp f a.hom) = (ProjectivePresentationExt.pushforwardLinear (projectiveCoverShortComplex P) a) ((ambientConnectingLinear P Y) f)

Naturality of the ambient-source connecting map.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantConnecting {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : S.finiteRestrictedCovariantRepresentable (CategoryTheory.Limits.kernel P.f) ⟶ S.finiteRestrictedExtOne P

The connecting morphism Hom(ΩX,-) ⟶ Ext¹(X,-) on the finite indecomposable skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantConnecting_app_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) (Y : S.IndecCategory) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((S.finiteRestrictedCovariantConnecting P).hom.hom.app Y))

The connecting morphism is pointwise surjective.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantConnecting_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : CategoryTheory.Epi (S.finiteRestrictedCovariantConnecting P)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableMap_projectiveCover_comp_kernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedCovariantRepresentableMap P.f) (S.finiteRestrictedCovariantRepresentableMap (CategoryTheory.Limits.kernel.ι P.f)) = 0

The first two maps in the source exact sequence compose to zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantProjectiveCover_exact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : { X₁ := S.finiteRestrictedCovariantRepresentable X, X₂ := S.finiteRestrictedCovariantRepresentable P.p, X₃ := S.finiteRestrictedCovariantRepresentable (CategoryTheory.Limits.kernel P.f), f := S.finiteRestrictedCovariantRepresentableMap P.f, g := S.finiteRestrictedCovariantRepresentableMap (CategoryTheory.Limits.kernel.ι P.f), zero := ⋯ }.Exact

Exactness of Hom(X,-) ⟶ Hom(P,-) ⟶ Hom(ΩX,-) on the finite indecomposable skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableMap_kernel_comp_connecting {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedCovariantRepresentableMap (CategoryTheory.Limits.kernel.ι P.f)) (S.finiteRestrictedCovariantConnecting P) = 0

Precomposition from the projective term lands in the kernel of the connecting morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantConnecting_exact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : { X₁ := S.finiteRestrictedCovariantRepresentable P.p, X₂ := S.finiteRestrictedCovariantRepresentable (CategoryTheory.Limits.kernel P.f), X₃ := S.finiteRestrictedExtOne P, f := S.finiteRestrictedCovariantRepresentableMap (CategoryTheory.Limits.kernel.ι P.f), g := S.finiteRestrictedCovariantConnecting P, zero := ⋯ }.Exact

The connecting morphism realizes Ext¹(X,-) as the cokernel of Hom(P,-) ⟶ Hom(ΩX,-) in the finite functor category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantConnecting_isCokernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (S.finiteRestrictedCovariantConnecting P) ⋯)

The source-shaped cokernel presentation defining the coherent dual of the stable contravariant representable.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.presentationToAmbientProjectiveStable {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X : FG} (P : MinimalProjectivePresentation X) (Y : S.IndecCategory) : (CategoryTheory.Limits.kernel P.f ⟶ S.fgObj Y) ⧸ ProjectivePresentationExt.presentationRange (projectiveCoverShortComplex P) (S.fgObj Y) →ₗ[k] ProjectiveStable.Hom (CategoryTheory.Limits.kernel P.f).obj (S.inclusion.obj Y)

The projective-presentation quotient maps onto stable Hom after forgetting finite generation.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.presentationToAmbientProjectiveStable_mk {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) (Y : S.IndecCategory) (f : CategoryTheory.Limits.kernel P.f ⟶ S.fgObj Y) : (S.presentationToAmbientProjectiveStable P Y) (Submodule.Quotient.mk f) = ProjectiveStable.mk f.hom

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.presentationToAmbientProjectiveStable_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) (Y : S.IndecCategory) : Function.Surjective ⇑(S.presentationToAmbientProjectiveStable P Y)

The presentation-to-ambient-stable map is surjective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.presentationToAmbientProjectiveStable_postcomp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) {Y Z : S.IndecCategory} (a : Y ⟶ Z) (q : (CategoryTheory.Limits.kernel P.f ⟶ S.fgObj Y) ⧸ ProjectivePresentationExt.presentationRange (projectiveCoverShortComplex P) (S.fgObj Y)) : (S.presentationToAmbientProjectiveStable P Z) ((ProjectivePresentationExt.postcompQuotient (projectiveCoverShortComplex P) (S.fgMap a)) q) = (ProjectiveStable.postcomp (CategoryTheory.Limits.kernel P.f).obj (S.inclusion.map a)) ((S.presentationToAmbientProjectiveStable P Y) q)

The presentation-to-ambient-stable map commutes with a skeleton morphism.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.extOneToAmbientProjectiveStable {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) (Y : S.IndecCategory) : CategoryTheory.Abelian.Ext X (S.fgObj Y) 1 →ₗ[k] ProjectiveStable.Hom (CategoryTheory.Limits.kernel P.f).obj (S.inclusion.obj Y)

The objectwise canonical quotient from degree-one Ext to ambient projective-stable Hom.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.extOneToAmbientProjectiveStable_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) (Y : S.IndecCategory) : Function.Surjective ⇑(S.extOneToAmbientProjectiveStable P Y)

The objectwise Ext-to-stable quotient is surjective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.extOneToAmbientProjectiveStable_naturality {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) {Y Z : S.IndecCategory} (a : Y ⟶ Z) (xi : CategoryTheory.Abelian.Ext X (S.fgObj Y) 1) : (S.extOneToAmbientProjectiveStable P Z) ((ProjectivePresentationExt.pushforwardLinear (projectiveCoverShortComplex P) (S.fgMap a)) xi) = (ProjectiveStable.postcomp (CategoryTheory.Limits.kernel P.f).obj (S.inclusion.map a)) ((S.extOneToAmbientProjectiveStable P Y) xi)

Naturality of the Ext-to-ambient-stable quotient.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.extOneToProjectiveStableLinearModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : (S.finiteRestrictedExtOne P).obj ⟶ (S.finiteProjectiveStableCovariantRepresentable (CategoryTheory.Limits.kernel P.f)).obj

The objectwise canonical quotient Ext¹(X,-) ⟶ \underline{Hom}(ΩX,-).

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteExtOneToProjectiveStable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : S.finiteRestrictedExtOne P ⟶ S.finiteProjectiveStableCovariantRepresentable (CategoryTheory.Limits.kernel P.f)

The canonical quotient from degree-one Ext to stable Hom in the finite functor category.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteExtOneToProjectiveStable_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) : CategoryTheory.Epi (S.finiteExtOneToProjectiveStable P)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantRepresentable_isUniserial_of_extOne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] {X : FG} (P : MinimalProjectivePresentation X) (hExt : IsUniserialObject (S.finiteRestrictedExtOne P)) : IsUniserialObject (S.finiteProjectiveStableCovariantRepresentable (CategoryTheory.Limits.kernel P.f))

Uniseriality passes from degree-one Ext to the projective-stable representable of the first syzygy.