Finite-representable coordinates on projective modules

When the representing objects have local endomorphism rings, every indecomposable projective finite module is a covariant representable. Finite indecomposable decomposition therefore puts every projective finite module in literal finite-representable coordinates. Applying this to projective covers produces exact minimal two-step presentations in the matrix model used by the Nakayama push-down comparison.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyoneda_end_isLocalRing {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (X : C) : IsLocalRing (CategoryTheory.End ((finiteDimensionalLinearCoyonedaFunctor hP).obj (Opposite.op X)))

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyoneda_indecomposable {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (X : C) : CategoryTheory.Indecomposable ((finiteDimensionalLinearCoyonedaFunctor hP).obj (Opposite.op X))

theorem MagnitudeConjecture.CoveringHom.indecomposable_projective_iso_finiteDimensionalLinearCoyoneda {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (P : FiniteDimensionalModuleCategory k) [CategoryTheory.Projective P] (hPind : CategoryTheory.Indecomposable P) : ∃ (X : C), Nonempty ((finiteDimensionalLinearCoyonedaFunctor hP).obj (Opposite.op X) ≅ P)

structure MagnitudeConjecture.CoveringHom.FiniteRepresentableCoordinates {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (P : FiniteDimensionalModuleCategory k) : Type (max u v)

Literal finite-representable coordinates on a finite projective module.

• n : ℕ
• X : Fin self.n → C
• isoSource : (⨁ fun (i : Fin self.n) => (finiteDimensionalLinearCoyonedaFunctor hP).obj (Opposite.op (self.X i))) ≅ P

theorem MagnitudeConjecture.CoveringHom.finiteRepresentableCoordinates_nonempty_of_projective {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (P : FiniteDimensionalModuleCategory k) [CategoryTheory.Projective P] : Nonempty (FiniteRepresentableCoordinates hP P)

structure MagnitudeConjecture.CoveringHom.MinimalFiniteRepresentablePresentation {k : Type uK} [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) extends MagnitudeConjecture.CoveringHom.FiniteRepresentablePresentation hP M : Type (max u v)

A minimal projective presentation in literal finite-representable coordinates.

• n : ℕ
• X : Fin self.n → C
• f : (⨁ fun (i : Fin self.n) => (finiteDimensionalLinearCoyonedaFunctor hP).obj (Opposite.op (self.X i))) ⟶ M
• epi : CategoryTheory.Epi self.f
• rightMinimal : QuotientSubmoduleEquidistribution.IsRightMinimal self.f

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.MinimalFiniteRepresentablePresentation.source {k : Type uK} [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 : MinimalFiniteRepresentablePresentation hP M) : FiniteDimensionalModuleCategory k

The finite sum of representables underlying a minimal presentation.

instance MagnitudeConjecture.CoveringHom.MinimalFiniteRepresentablePresentation.instProjectiveFiniteDimensionalModuleCategorySource {k : Type uK} [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 : MinimalFiniteRepresentablePresentation hP M) : CategoryTheory.Projective P.source

instance MagnitudeConjecture.CoveringHom.MinimalFiniteRepresentablePresentation.instEpiFiniteDimensionalModuleCategoryF {k : Type uK} [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 : MinimalFiniteRepresentablePresentation hP M) : CategoryTheory.Epi P.f

noncomputable def MagnitudeConjecture.CoveringHom.MinimalFiniteRepresentablePresentation.toMinimalProjectivePresentation {k : Type uK} [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 : MinimalFiniteRepresentablePresentation hP M) : MinimalProjectivePresentation M

Forgetting the literal representable coordinates gives an ordinary minimal projective presentation.

noncomputable def MagnitudeConjecture.CoveringHom.MinimalFiniteRepresentablePresentation.ofMinimalProjectivePresentation {k : Type uK} [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 : MinimalProjectivePresentation M) (Q : FiniteRepresentableCoordinates hP P.p) : MinimalFiniteRepresentablePresentation hP M

Transport an abstract minimal projective presentation into chosen literal finite-representable coordinates on its source.

theorem MagnitudeConjecture.CoveringHom.minimalFiniteRepresentablePresentation_nonempty {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (M : FiniteDimensionalModuleCategory k) : Nonempty (MinimalFiniteRepresentablePresentation hP M)

Every finite module has a minimal projective presentation whose source is literally a finite sum of representables, provided representing objects have local endomorphism rings.

structure MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation {k : Type uK} [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) : Type (max u v)

A two-step minimal projective presentation in literal finite-representable matrix coordinates.

• augmentation : MinimalFiniteRepresentablePresentation hP M
• syzygyPresentation : MinimalFiniteRepresentablePresentation hP (CategoryTheory.Limits.kernel self.augmentation.f)

def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.toTwoStepFiniteRepresentablePresentation {k : Type uK} [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) : TwoStepFiniteRepresentablePresentation hP M

Forgetting minimality gives the existing literal matrix presentation.

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.toTwoStepMinimalProjectivePresentation {k : Type uK} [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) : TwoStepMinimalProjectivePresentation M

Forgetting coordinates gives the generic two-step minimal projective presentation.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.presentationComplex_exact {k : Type uK} [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.toTwoStepFiniteRepresentablePresentation.presentationComplex.Exact

The literal finite-matrix presentation is exact.

theorem MagnitudeConjecture.CoveringHom.twoStepMinimalFiniteRepresentablePresentation_nonempty {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (M : FiniteDimensionalModuleCategory k) : Nonempty (TwoStepMinimalFiniteRepresentablePresentation hP M)

Every finite module has an exact two-step minimal projective presentation in literal finite-representable matrix coordinates.