Minimal injective envelopes of finite modules

Coefficient duality turns a finite module into a finite module over the opposite category. A minimal projective cover there dualizes back to a minimal injective envelope. Applying the construction to the first cosyzygy gives a two-step minimal injective presentation.

noncomputable def MagnitudeConjecture.CoveringHom.minimalInjectivePresentationOfDualProjective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (P : MinimalProjectivePresentation (finiteCoefficientDualityEquivalence.functor.obj (Opposite.op M))) : MinimalInjectivePresentation M

A minimal projective cover of the coefficient dual of M dualizes to a minimal injective envelope of M.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_minimalInjectivePresentation_nonempty {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) : Nonempty (MinimalInjectivePresentation M)

Finite representables over the opposite category supply a minimal injective envelope for every finite module.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_twoStepMinimalInjectivePresentation_nonempty {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) : Nonempty (TwoStepMinimalInjectivePresentation M)

Finite representables over the opposite category supply a two-step minimal injective presentation for every finite module.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_isEssentialMono_iff_isLeftMinimal {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M I : FiniteDimensionalModuleCategory k} [CategoryTheory.Injective I] (f : M ⟶ I) [CategoryTheory.Mono f] : IsEssentialMono f ↔ QuotientSubmoduleEquidistribution.IsLeftMinimal f

For finite modules, essential injective monomorphisms and left-minimal injective monomorphisms are equivalent.