iff_projective — Mathlib

English

A module is projective in the module category iff it is projective in the category-theoretic sense.

Русский

Модуль проектируем в модульной категории тогда и только тогда, когда он проективен в категориальном смысле.

LaTeX

$$$ IsProjective.iff_projective$$$

Lean4

/-- The categorical notion of projective object agrees with the explicit module-theoretic notion. -/
theorem iff_projective [Small.{v} R] (P : Type v) [AddCommGroup P] [Module R P] :
    Module.Projective R P ↔ Projective (of R P) :=
  ⟨fun _ => (of R P).projective_of_categoryTheory_projective, fun _ => (of R P).projective_of_module_projective⟩

Похожие утверждения