HasDerivedCategory

Mathlib.Algebra.Homology.DerivedCategory.Basic

URI: https://scilib.ai/kg/mathlib#HasDerivedCategory

Lean4

/-- The assumption that a localized category for
`(HomologicalComplex.quasiIso C (ComplexShape.up ℤ))` has been chosen, and that the morphisms
in this chosen category are in `Type w`. -/
abbrev HasDerivedCategory :=
  MorphismProperty.HasLocalization.{w} (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))

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

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

Разделы

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

Аффилиация

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