The finite-functor-category Auslander transpose copresentation

For a literal two-step finite-representable presentation, applying the finite-matrix Nakayama functor produces a map between injectives. Its kernel therefore has a concrete short injective presentation, and degree-one Ext is the corresponding quotient of a Hom space.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.representingDifferential {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : P.syzygyPresentation.matrixObject ⟶ P.augmentation.matrixObject

The literal representing-object matrix of the first differential.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaDifferential {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : (finiteNakayamaRepresentableSumFunctor hI).obj P.syzygyPresentation.matrixObject ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj P.augmentation.matrixObject

The first differential after applying the finite-matrix Nakayama functor.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaKernel {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : FiniteDimensionalModuleCategory k

The presentation-dependent Auslander--Reiten translate object.

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaInjectivePresentation {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : CategoryTheory.InjectivePresentation (nakayamaKernel hI P)

The inclusion of the Nakayama kernel in the first Nakayama projective, packaged as an injective presentation.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaCokernel {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : FiniteDimensionalModuleCategory k

The quotient of the first Nakayama projective by the Nakayama kernel.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaCokernelπ {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : (finiteNakayamaRepresentableSumFunctor hI).obj P.syzygyPresentation.matrixObject ⟶ nakayamaCokernel hI P

The quotient map from the first Nakayama projective.

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaCokernelι {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : nakayamaCokernel hI P ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj P.augmentation.matrixObject

The Nakayama differential descends to the quotient by its kernel.

@[simp]

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaCokernelπ_comp_ι {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : CategoryTheory.CategoryStruct.comp (nakayamaCokernelπ hI P) (nakayamaCokernelι hI P) = nakayamaDifferential hI P

instance MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaCokernelι_mono {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : CategoryTheory.Mono (nakayamaCokernelι hI P)

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaExtShortComplex {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : CategoryTheory.ShortComplex (FiniteDimensionalModuleCategory k)

The short exact sequence computing Ext from the Nakayama kernel.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaExtPresentationRange {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : Submodule k (Y ⟶ nakayamaCokernel hI P)

Coboundaries in the concrete injective presentation.

@[simp]

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.mem_nakayamaExtPresentationRange_iff {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) (f : Y ⟶ nakayamaCokernel hI P) : f ∈ nakayamaExtPresentationRange hI P Y ↔ ∃ (a : Y ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj P.syzygyPresentation.matrixObject), CategoryTheory.CategoryStruct.comp a (nakayamaCokernelπ hI P) = f

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaExtOneQuotientLinearEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : ((Y ⟶ nakayamaCokernel hI P) ⧸ nakayamaExtPresentationRange hI P Y) ≃ₗ[k] CategoryTheory.Abelian.Ext Y (nakayamaKernel hI P) 1

The concrete quotient presentation of degree-one Ext.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaPrecompQuotient {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) {Y Z : FiniteDimensionalModuleCategory k} (g : Y ⟶ Z) : (Z ⟶ nakayamaCokernel hI P) ⧸ nakayamaExtPresentationRange hI P Z →ₗ[k] (Y ⟶ nakayamaCokernel hI P) ⧸ nakayamaExtPresentationRange hI P Y

Pullback on the concrete Ext presentation quotient.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaExtOneQuotientLinearEquiv_symm_pullback {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) {Y Z : FiniteDimensionalModuleCategory k} (g : Y ⟶ Z) (xi : CategoryTheory.Abelian.Ext Z (nakayamaKernel hI P) 1) : (nakayamaExtOneQuotientLinearEquiv hI P Y).symm ((CategoryTheory.Abelian.Ext.mk₀ g).comp xi ⋯) = (nakayamaPrecompQuotient hI P g) ((nakayamaExtOneQuotientLinearEquiv hI P Z).symm xi)

Inverse-form pullback naturality of the Ext quotient.