instEnoughProjectives — Mathlib

English

The category Profinite has enough projectives: every object admits a projective presentation.

Русский

У категории Profinite есть достаточно проективных объектов: каждый объект можно представить как образ проективного.

LaTeX

$$$\\text{EnoughProjectives}\\;\\mathrm{Profinite}$$$

Lean4

instance : EnoughProjectives Profinite.{u} where presentation X := ⟨projectivePresentation X⟩

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