The two defects of a short exact right-module presentation

For a short exact sequence 0 ⟶ A ⟶ B ⟶ C ⟶ 0, Auslander's coherent duality exchanges the contravariant defect

coker(Hom(-, B) ⟶ Hom(-, C))

with the covariant defect

coker(Hom(B, -) ⟶ Hom(A, -)).

This file fixes those two literal cokernel objects on the finite indecomposable skeleton. For a projective cover it identifies them with Hom̲(-, C) and Ext¹(C, -), respectively. The later coherent-duality file will prove that the two exact-presentation constructions form inverse contravariant equivalences on the corresponding defect subcategories.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefect {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : CoveringHom.FiniteDimensionalModuleCategory k

The contravariant defect of a composable two-term module complex. When the complex is short exact, this is the object occurring on the contravariant side of Auslander's exact-presentation duality.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefect {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : CoveringHom.FiniteDimensionalModuleCategory k

The covariant defect of a composable two-term module complex. When the complex is short exact, this is the coherent dual of finiteContravariantDefect.

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

The three representable terms induced by a module short complex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FG} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Mono (S.finiteRestrictedContravariantRepresentableMap f)

Restricted contravariant Yoneda preserves monomorphisms.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantRepresentableComplex_exact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : (S.finiteContravariantRepresentableComplex K).Exact

Restricted contravariant Yoneda carries a short exact module sequence to an exact sequence at its middle representable term.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectSyzygy {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : CoveringHom.FiniteDimensionalModuleCategory k

The first syzygy in the representable resolution of a contravariant defect.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectSyzygyι {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : S.finiteContravariantDefectSyzygy K ⟶ S.finiteRestrictedContravariantRepresentable K.X₃

Exactness lets the second representable map descend through the first cokernel.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectSyzygyπ_comp_ι {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.finiteRestrictedContravariantRepresentableMap K.f)) (S.finiteContravariantDefectSyzygyι K) = S.finiteRestrictedContravariantRepresentableMap K.g

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectSyzygyπ_comp_ι_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) {Z : CoveringHom.FiniteDimensionalModuleCategory k} (h : S.finiteRestrictedContravariantRepresentable K.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.finiteRestrictedContravariantRepresentableMap K.f)) (CategoryTheory.CategoryStruct.comp (S.finiteContravariantDefectSyzygyι K) h) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap K.g) h

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectSyzygyι_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : CategoryTheory.Mono (S.finiteContravariantDefectSyzygyι K)

For a short exact module sequence, the descended map from the first syzygy into the third representable is monic.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectLeftShortComplex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The left short exact sequence obtained by splitting the four-term representable resolution at its first syzygy.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectLeftShortComplex_shortExact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : (S.finiteContravariantDefectLeftShortComplex K).ShortExact

The left syzygy sequence is short exact when the module sequence is.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectRightShortComplex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The right short complex from the first syzygy to the contravariant defect.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectRightShortComplex_shortExact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : (S.finiteContravariantDefectRightShortComplex K).ShortExact

The right syzygy sequence is short exact when the module sequence is.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.IsFiniteContravariantDefect {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.ObjectProperty (CoveringHom.FiniteDimensionalModuleCategory k)

The exact-presentation condition on the contravariant side of Auslander's coherent duality. An object has this property when it is isomorphic to the contravariant defect of some short exact sequence of finitely generated right modules.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FiniteContravariantDefectCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) : Type (u + 1)

The full subcategory of finite contravariant functors admitting an exact representable presentation.

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

The exact-presentation condition on the covariant side of Auslander's coherent duality.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FiniteCovariantDefectCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Type (u + 1)

The full subcategory of finite covariant functors admitting an exact representable presentation.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectIsoProjectiveStable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X : FG} (P : MinimalProjectivePresentation X) : S.finiteContravariantDefect (projectiveCoverShortComplex P) ≅ S.finiteProjectiveStableContravariantRepresentable X

For a projective cover, the contravariant defect is the projective-stable representable of the target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefect_isUniserial_iff_projectiveStable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X : FG} (P : MinimalProjectivePresentation X) : IsUniserialObject (S.finiteContravariantDefect (projectiveCoverShortComplex P)) ↔ IsUniserialObject (S.finiteProjectiveStableContravariantRepresentable X)

Uniseriality of the contravariant defect of a projective cover is equivalent to uniseriality of its stable representable.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableContravariantDefectObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X : FG} (P : MinimalProjectivePresentation X) : S.FiniteContravariantDefectCategory

A projective-stable contravariant representable, equipped with the exact presentation supplied by a projective cover.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectIsoRestrictedExtOne {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.finiteCovariantDefect (projectiveCoverShortComplex P) ≅ S.finiteRestrictedExtOne P

For a projective cover, the covariant defect is the restricted degree-one Ext functor of its target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefect_isUniserial_iff_restrictedExtOne {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) : IsUniserialObject (S.finiteCovariantDefect (projectiveCoverShortComplex P)) ↔ IsUniserialObject (S.finiteRestrictedExtOne P)

Uniseriality of the covariant defect of a projective cover is equivalent to uniseriality of its restricted degree-one Ext functor.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedExtOneCovariantDefectObj {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.FiniteCovariantDefectCategory

The restricted degree-one Ext functor, equipped with the exact presentation supplied by a projective cover.