Finite-dimensional minimal injective copresentations

Every finite-dimensional module over a finite-dimensional algebra admits a minimal injective copresentation 0 → M → Q₀ → Q₁ with finite-dimensional injective terms. The first term is an injective envelope of M, and the second is an injective envelope of its cokernel. Together with uniqueness of minimal copresentations, this provides the first two terms of a minimal injective resolution, as needed for the inverse Auslander–Reiten construction Tr D.

Both injective terms can be taken in the universe of the field and algebra, independently of the universe of M. No algebraic closedness or self-injectivity assumption is required.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Sections I.5 and IV.1.

theorem TauCeti.exists_isMinimalInjectiveCopresentation_finiteDimensional {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (M : Type w) [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] [FiniteDimensional k M] : ∃ (Q₀ : Type (max u v)) (x : AddCommGroup Q₀) (x_1 : Module A Q₀) (x_2 : Module k Q₀) (_ : IsScalarTower k A Q₀) (_ : FiniteDimensional k Q₀) (Q₁ : Type (max u v)) (x_5 : AddCommGroup Q₁) (x_6 : Module A Q₁) (x_7 : Module k Q₁) (_ : IsScalarTower k A Q₁) (_ : FiniteDimensional k Q₁) (i₀ : M →ₗ[A] Q₀) (i₁ : Q₀ →ₗ[A] Q₁), IsMinimalInjectiveCopresentation i₀ i₁

A finite-dimensional module over a finite-dimensional algebra has a minimal injective copresentation with both injective terms finite-dimensional, in the universe of the field and algebra.

theorem TauCeti.exists_isMinimalInjectiveCopresentation_of_finite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (M : Type w) [AddCommGroup M] [Module A M] [Module.Finite A M] : ∃ (Q₀ : Type (max u v)) (x : AddCommGroup Q₀) (x_1 : Module A Q₀) (x_2 : Module k Q₀) (_ : IsScalarTower k A Q₀) (_ : FiniteDimensional k Q₀) (Q₁ : Type (max u v)) (x_5 : AddCommGroup Q₁) (x_6 : Module A Q₁) (x_7 : Module k Q₁) (_ : IsScalarTower k A Q₁) (_ : FiniteDimensional k Q₁) (i₀ : M →ₗ[A] Q₀) (i₁ : Q₀ →ₗ[A] Q₁), IsMinimalInjectiveCopresentation i₀ i₁

A finitely generated module over a finite-dimensional algebra has a finite-dimensional minimal injective copresentation. The source's field action is induced through the algebra map.