Injectivity of finite dual corepresentables

Coefficient-dual corepresentables are injective in the category of finite-support pointwise finite-dimensional linear modules. The proof is the dual co-Yoneda lemma followed by extension of a linear functional along the component of a monomorphism.

theorem MagnitudeConjecture.CoveringHom.instInjective_magnitudeConjecture {k : Type v} [Field k] : Module.Injective k k

noncomputable def MagnitudeConjecture.CoveringHom.finiteDualLinearYonedaHomEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (X : C) (hI : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : (M ⟶ finiteDimensionalDualLinearYoneda X hI) ≃ₗ[k] Module.Dual k ↑(M.obj.obj.obj X)

Dual co-Yoneda inside the finite-dimensional module subcategory.

@[simp]

theorem MagnitudeConjecture.CoveringHom.finiteDualLinearYonedaHomEquiv_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (X : C) (hI : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (a : M ⟶ finiteDimensionalDualLinearYoneda X hI) (x : ↑(M.obj.obj.obj X)) : ((finiteDualLinearYonedaHomEquiv M X hI) a) x = ((dualLinearYonedaValueLinearEquiv X X) ((CategoryTheory.ConcreteCategory.hom (a.hom.hom.app X)) x)) (CategoryTheory.CategoryStruct.id X)

theorem MagnitudeConjecture.CoveringHom.finiteDualLinearYonedaHomEquiv_naturality {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : FiniteDimensionalModuleCategory k} (X : C) (hI : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (g : M ⟶ N) (a : N ⟶ finiteDimensionalDualLinearYoneda X hI) (x : ↑(M.obj.obj.obj X)) : ((finiteDualLinearYonedaHomEquiv M X hI) (CategoryTheory.CategoryStruct.comp g a)) x = ((finiteDualLinearYonedaHomEquiv N X hI) a) ((CategoryTheory.ConcreteCategory.hom (g.hom.hom.app X)) x)

Naturality of finite dual co-Yoneda in the source module.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYoneda_injective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) (hI : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : CategoryTheory.Injective (finiteDimensionalDualLinearYoneda X hI)

A finite-dimensional dual corepresentable is injective.

theorem MagnitudeConjecture.CoveringHom.finiteNakayamaRepresentableSum_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)) (Q : CategoryTheory.Mat_ Cᵒᵖ) : CategoryTheory.Injective ((finiteNakayamaRepresentableSumFunctor hI).obj Q)

A literal finite Nakayama sum is injective.