self

Mathlib.CategoryTheory.Preadditive.Injective.Resolution

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

Lean4

/-- An injective object admits a trivial injective resolution: itself in degree 0. -/
@[simps]
def self [Injective Z] : InjectiveResolution Z
    where
  cocomplex := (CochainComplex.single₀ C).obj Z
  ι := 𝟙 ((CochainComplex.single₀ C).obj Z)
  injective
    n := by
    cases n
    · simpa
    · apply IsZero.injective
      apply HomologicalComplex.isZero_single_obj_X
      simp

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

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

Разделы

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

Аффилиация

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