Enough injectives in the finite functor category

A finite-support module embeds into a finite sum of coefficient-dual corepresentables. For every supported object we take a basis of the dual of the module value and assemble the corresponding dual co-Yoneda maps. The identity component detects every vector, so the resulting natural map is pointwise injective.

structure MagnitudeConjecture.CoveringHom.FiniteDualCorepresentableCopresentation {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (M : FiniteDimensionalModuleCategory k) : Type (max u v)

An explicit monomorphism from a finite module to a finite nested biproduct of coefficient-dual corepresentables. The chosen Fintype structure is stored so the target remains available as explicit data.

• supportFintype : Fintype ↑(moduleSupport k M.obj.obj)
• d : ↑(moduleSupport k M.obj.obj) → ℕ
• f : M ⟶ ⨁ fun (X : ↑(moduleSupport k M.obj.obj)) => ⨁ fun (x : Fin (self.d X)) => finiteDimensionalDualLinearYoneda ↑X ⋯
• mono_f : CategoryTheory.Mono self.f

@[reducible, inline]

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

The finite injective target of an explicit dual-corepresentable copresentation.

instance MagnitudeConjecture.CoveringHom.FiniteDualCorepresentableCopresentation.target_injective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)} {M : FiniteDimensionalModuleCategory k} (P : FiniteDualCorepresentableCopresentation hI M) : CategoryTheory.Injective P.target

theorem MagnitudeConjecture.CoveringHom.finiteDualCorepresentableCopresentation_nonempty {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (M : FiniteDimensionalModuleCategory k) : Nonempty (FiniteDualCorepresentableCopresentation hI M)

The explicit finite dual-corepresentable copresentation exists for every finite-support pointwise finite-dimensional module.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModuleCategoryEnoughInjectives {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : CategoryTheory.EnoughInjectives (FiniteDimensionalModuleCategory k)

Finite dual corepresentables provide enough injectives in the category of finite-support pointwise finite-dimensional modules.