enoughProjectives — Mathlib

English

The category Type (of types) has enough projectives: for every type X, there is a projective presentation given by X with identity on X.

Русский

Категория типов имеет достаточно проективных объектов: для каждого типа X существует проективная презентация, задаваемая X с идентичностью на X.

LaTeX

$$$ \\text{EnoughProjectives } (\\mathrm{Type}) \\quad \\text{presentation } X := \\langle\\langle X, \\mathrm{id}_X \\rangle\\rangle $$$

Lean4

instance enoughProjectives : EnoughProjectives (Type u) where presentation X := ⟨⟨X, 𝟙 X⟩⟩

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