Finite representable projective presentations

Every finite-support finite-dimensional covariant linear module is generated by finitely many elements. Linear coyoneda turns those generators into an epimorphism from a finite sum of representables, and the same construction on its kernel gives an exact two-step projective presentation. Fullness of linear coyoneda records the first differential as a literal finite matrix of representing-object morphisms, matching the Nakayama push-down interface.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_isEssentialEpi_iff_isRightMinimal {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P M : FiniteDimensionalModuleCategory k} [CategoryTheory.Projective P] (f : P ⟶ M) [CategoryTheory.Epi f] : IsEssentialEpi f ↔ QuotientSubmoduleEquidistribution.IsRightMinimal f

For finite modules, essential projective epimorphisms and right-minimal projective epimorphisms are equivalent without an extra Hopfian hypothesis.

noncomputable def MagnitudeConjecture.CoveringHom.linearCoyonedaHom {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) (X : C) (x : ↑(M.obj.obj X)) : linearCoyonedaLinearModule X ⟶ M

The morphism from a covariant linear representable determined by an element at its representing object.

@[simp]

theorem MagnitudeConjecture.CoveringHom.linearCoyonedaHom_app_apply {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) (X Y : C) (x : ↑(M.obj.obj X)) (q : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom ((linearCoyonedaHom M X x).hom.app Y)) q = (CategoryTheory.ConcreteCategory.hom (M.obj.map q)) x

@[simp]

theorem MagnitudeConjecture.CoveringHom.linearCoyonedaHom_app_id {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) (X : C) (x : ↑(M.obj.obj X)) : (CategoryTheory.ConcreteCategory.hom ((linearCoyonedaHom M X x).hom.app X)) (CategoryTheory.CategoryStruct.id X) = x

@[simp]

theorem MagnitudeConjecture.CoveringHom.linearCoyonedaHom_self {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) (X : C) (f : linearCoyonedaLinearModule X ⟶ M) : linearCoyonedaHom M X ((CategoryTheory.ConcreteCategory.hom (f.hom.app X)) (CategoryTheory.CategoryStruct.id X)) = f

noncomputable def MagnitudeConjecture.CoveringHom.linearCoyonedaHomEquiv {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) (X : C) : (linearCoyonedaLinearModule X ⟶ M) ≃ₗ[k] ↑(M.obj.obj X)

Linear Yoneda for covariant modules.

theorem MagnitudeConjecture.CoveringHom.linearCoyonedaHom_comp {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M N : LinearModuleCategory k) (X : C) (x : ↑(M.obj.obj X)) (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (linearCoyonedaHom M X x) f = linearCoyonedaHom N X ((CategoryTheory.ConcreteCategory.hom (f.hom.app X)) x)

instance MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyoneda_projective {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) (hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : CategoryTheory.Projective (finiteDimensionalLinearCoyoneda X hX)

structure MagnitudeConjecture.CoveringHom.FiniteRepresentablePresentation {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 finite projective presentation whose source is literally a finite biproduct of covariant representables.

• 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

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.FiniteRepresentablePresentation.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 : FiniteRepresentablePresentation hP M) : FiniteDimensionalModuleCategory k

The literal finite sum of representables underlying the presentation.

def MagnitudeConjecture.CoveringHom.FiniteRepresentablePresentation.matrixObject {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 : FiniteRepresentablePresentation hP M) : CategoryTheory.Mat_ Cᵒᵖ

The same finite representable sum as an object of Mathlib's matrix envelope.

instance MagnitudeConjecture.CoveringHom.FiniteRepresentablePresentation.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 : FiniteRepresentablePresentation hP M) : CategoryTheory.Projective P.source

noncomputable def MagnitudeConjecture.CoveringHom.FiniteRepresentablePresentation.toProjectivePresentation {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 : FiniteRepresentablePresentation hP M) : CategoryTheory.ProjectivePresentation M

Forgetting the chosen finite matrix coordinates gives an ordinary projective presentation.

noncomputable def MagnitudeConjecture.CoveringHom.FiniteRepresentablePresentation.representingMatrix {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 N : FiniteDimensionalModuleCategory k} (P : FiniteRepresentablePresentation hP M) (Q : FiniteRepresentablePresentation hP N) (f : P.source ⟶ Q.source) : P.matrixObject ⟶ Q.matrixObject

The matrix of representing-object morphisms underlying a map between two finite sums of covariant representables.

theorem MagnitudeConjecture.CoveringHom.FiniteRepresentablePresentation.map_representingMatrix {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 N : FiniteDimensionalModuleCategory k} (P : FiniteRepresentablePresentation hP M) (Q : FiniteRepresentablePresentation hP N) (f : P.source ⟶ Q.source) : (finiteProjectiveRepresentableSumFunctor hP).map (P.representingMatrix Q f) = f

Applying the finite representable functor to the extracted matrix recovers the original map.

theorem MagnitudeConjecture.CoveringHom.finiteRepresentablePresentation_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)) (M : FiniteDimensionalModuleCategory k) : Nonempty (FiniteRepresentablePresentation hP M)

Every finite-support finite-dimensional linear module is an epimorphic image of a finite sum of finite-dimensional covariant representables.

structure MagnitudeConjecture.CoveringHom.TwoStepFiniteRepresentablePresentation {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)

Two explicit finite representable covers give a two-step projective presentation.

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

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepFiniteRepresentablePresentation.differential {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 : TwoStepFiniteRepresentablePresentation hP M) : P.syzygyPresentation.source ⟶ P.augmentation.source

The first differential between the two finite sums of representables.

@[simp]

theorem MagnitudeConjecture.CoveringHom.TwoStepFiniteRepresentablePresentation.differential_comp_augmentation {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 : TwoStepFiniteRepresentablePresentation hP M) : CategoryTheory.CategoryStruct.comp P.differential P.augmentation.f = 0

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepFiniteRepresentablePresentation.matrixDifferential {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 : TwoStepFiniteRepresentablePresentation hP M) : P.syzygyPresentation.matrixObject ⟶ P.augmentation.matrixObject

The differential in literal representing-object matrix coordinates.

theorem MagnitudeConjecture.CoveringHom.TwoStepFiniteRepresentablePresentation.map_matrixDifferential {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 : TwoStepFiniteRepresentablePresentation hP M) : (finiteProjectiveRepresentableSumFunctor hP).map P.matrixDifferential = P.differential

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepFiniteRepresentablePresentation.presentationComplex {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 : TwoStepFiniteRepresentablePresentation hP M) : CategoryTheory.ShortComplex (FiniteDimensionalModuleCategory k)

The associated exact two-term projective complex.

theorem MagnitudeConjecture.CoveringHom.TwoStepFiniteRepresentablePresentation.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 : TwoStepFiniteRepresentablePresentation hP M) : P.presentationComplex.Exact

theorem MagnitudeConjecture.CoveringHom.twoStepFiniteRepresentablePresentation_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)) (M : FiniteDimensionalModuleCategory k) : Nonempty (TwoStepFiniteRepresentablePresentation hP M)

Every finite-support finite-dimensional module has an explicit two-step projective presentation by finite sums of representables.

theorem MagnitudeConjecture.CoveringHom.enoughProjectives_of_finiteRepresentables {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)) : CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)

Finite representables supply enough projectives in the literal finite module category.