English
The category of modules has enough projectives since every module is a quotient of a free module.
Русский
Категория модулей имеет достаточно проективных объектов, так как каждый модуль является образцом свободного модуля.
LaTeX
$$$ \text{ModuleCat.enoughProjectives}$$$
Lean4
/-- The category of modules has enough projectives, since every module is a quotient of a free
module. -/
instance enoughProjectives [Small.{v} R] : EnoughProjectives (ModuleCat.{v} R) where
presentation
M :=
let e : Basis M R (M →₀ Shrink.{v} R) := ⟨Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R)⟩
⟨{ p := ModuleCat.of R (M →₀ Shrink.{v} R)
projective := projective_of_free e
f := ofHom <| e.constr ℕ _root_.id
epi := by
rw [epi_iff_range_eq_top, LinearMap.range_eq_top]
refine fun m ↦ ⟨Finsupp.single m 1, ?_⟩
simp [e, Basis.constr_apply] }⟩
