Projective covers in ModuleCat

TauCeti.IsProjectiveCover is the module-level predicate — a surjection from a projective module with superfluous kernel — and TauCeti.IsEssentialEpi is its categorical counterpart, an epimorphism π such that every morphism g into its source with g ≫ π an epimorphism is itself one. This file is the bridge between the two over ModuleCat: a linear map that is a projective cover is an essential epimorphism of ModuleCat from a projective object, and conversely (TauCeti.isProjectiveCover_iff_projective_and_isEssentialEpi), so the existence theorem of TauCeti/Algebra/Module/ProjectiveCover/Existence.lean reads as a statement about objects of ModuleCat.

The two translations used are Mathlib's: an epimorphism of ModuleCat is a surjection (ModuleCat.epi_iff_surjective), and a projective object of ModuleCat is a projective module (IsProjective.iff_projective). The module-level content of essentiality is TauCeti.isProjectiveCover_iff_forall_surjective.

The covering module produced here is a submodule of a free module on the underlying set of the module covered, so it lives in the same universe as that module; this is why the statements below fix a single universe for the ring and the category.

Main results

• TauCeti.IsProjectiveCover.isEssentialEpi: a module-level projective cover is an essential epimorphism of ModuleCat.
• TauCeti.isProjectiveCover_iff_projective_and_isEssentialEpi: the two readings agree — a morphism of ModuleCat is a projective cover of modules exactly when its source is a projective object and it is an essential epimorphism.
• TauCeti.exists_essentialEpi_projective: every object of ModuleCat R over a semiprimary ring receives an essential epimorphism from a projective object.
• TauCeti.exists_projectiveCover: the same for a module over a finite-dimensional algebra, with the two clauses of essentiality written out.

References

See I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.5.

theorem TauCeti.IsProjectiveCover.isEssentialEpi {R : Type u} [Ring R] {P M : ModuleCat R} {π : P ⟶ M} (h : IsProjectiveCover (ModuleCat.Hom.hom π)) : IsEssentialEpi π

A projective cover of modules is an essential epimorphism. The two conditions agree over ModuleCat: surjectivity is Epi and the minimality of a superfluous kernel is exactly the essentiality clause, by TauCeti.isProjectiveCover_iff_forall_surjective.

theorem TauCeti.IsProjectiveCover.projective_obj {R : Type u} [Ring R] {P M : ModuleCat R} {π : P ⟶ M} (h : IsProjectiveCover (ModuleCat.Hom.hom π)) : CategoryTheory.Projective P

A projective cover of modules has a projective source, read in ModuleCat.

theorem TauCeti.isProjectiveCover_iff_projective_and_isEssentialEpi {R : Type u} [Ring R] {P M : ModuleCat R} [Small.{v, u} R] {π : P ⟶ M} : IsProjectiveCover (ModuleCat.Hom.hom π) ↔ CategoryTheory.Projective P ∧ IsEssentialEpi π

The two readings of a projective cover agree. A morphism of ModuleCat is a projective cover of modules exactly when its source is a projective object and it is an essential epimorphism. The backward direction recovers the module-level API — surjectivity and a superfluous kernel — from the categorical data: a map into the source is tested through its range, a submodule of the source and so again an object of ModuleCat.

theorem TauCeti.exists_essentialEpi_projective (R : Type u) [Ring R] [IsSemiprimaryRing R] (M : ModuleCat R) : ∃ (P : ModuleCat R) (π : P ⟶ M), CategoryTheory.Projective P ∧ IsEssentialEpi π

Every object of ModuleCat R over a semiprimary ring has a projective cover: it receives an essential epimorphism from a projective object. Unfolding TauCeti.IsEssentialEpi, this says that π is an epimorphism and that every i : X ⟶ P with i ≫ π an epimorphism is one.

theorem TauCeti.exists_projectiveCover {k : Type v} [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (M : ModuleCat A) : ∃ (P : ModuleCat A) (π : P ⟶ M), CategoryTheory.Projective P ∧ CategoryTheory.Epi π ∧ ∀ (X : ModuleCat A) (i : X ⟶ P), CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp i π) → CategoryTheory.Epi i

Every object of ModuleCat A over a finite-dimensional algebra A has a projective cover. A finite-dimensional algebra is an Artinian ring, hence semiprimary, so this is TauCeti.exists_essentialEpi_projective read through that instance; no finiteness is required of the module. Essentiality is spelled out here as its two clauses, so that the statement is usable without unfolding TauCeti.IsEssentialEpi.