Theorems · Theorem · category theory

CategoryTheory.hasExt_of_enoughInjectives

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.EnoughInjectives C], CategoryTheory.HasExt C

If C is a locally w-small abelian category with enough injectives, then HasExt.{w} C holds. We do not make this an instance though: for a given category C, there may be different reasonable choices for the universe w, and if we have two HasExt.{w₁} C and HasExt.{w₂} C instances, we would have to specify the universe explicitly almost everywhere, which would be an inconvenience. Then, we must be very selective regarding HasExt instances.

Defined in

Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Cited by

0 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.LocallySmallCategoryTheory.EnoughInjectives