self

Mathlib.CategoryTheory.Preadditive.Projective.Resolution

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ProjectiveResolution.self

Lean4

/-- A projective object admits a trivial projective resolution: itself in degree 0. -/
@[simps]
noncomputable def self [Projective Z] : ProjectiveResolution Z
    where
  complex := (ChainComplex.single₀ C).obj Z
  π := 𝟙 ((ChainComplex.single₀ C).obj Z)
  projective
    n := by
    cases n
    · simpa
    · apply IsZero.projective
      apply HomologicalComplex.isZero_single_obj_X
      simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru