Theorems · Definition · category theory

CategoryTheory.Abelian.Ext

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [CategoryTheory.HasExt C] → C → C → ℕ → Type w

An Ext-group in an abelian category C, defined as a Type w when [HasExt.{w} C].

Defined in

Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Cited by

191 results in Mathlib

Foundations

Depth 95 from the axioms, rests on 2,796 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.HasExt