Structures · Category theory
CategoryTheory.HasProjectiveDimensionLT
An object X in an abelian category has projective dimension < n if
all Ext X Y i vanish when n ≤ i. See also HasProjectiveDimensionLE.
(Do not use the subsingleton' field directly. Use the constructor
HasProjectiveDimensionLT.mk, and the lemmas hasProjectiveDimensionLT_iff and
Ext.eq_zero_of_hasProjectiveDimensionLT.)
- Shape
- 2 explicit arguments · adds subsingleton'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT
- CategoryTheory.HasProjectiveDimensionLT.subsingleton
- CategoryTheory.hasProjectiveDimensionLT_of_ge
- CategoryTheory.Retract.hasProjectiveDimensionLT
- CategoryTheory.hasProjectiveDimensionLT_of_iso
- CategoryTheory.HasProjectiveDimensionLT.subsingleton'
- CategoryTheory.isZero_of_hasProjectiveDimensionLT_zero
- CategoryTheory.instHasProjectiveDimensionLTBiprod
- CategoryTheory.instProjectiveOfHasProjectiveDimensionLTOfNatNat
- CategoryTheory.instHasProjectiveDimensionLTHAddNat
- CategoryTheory.instHasProjectiveDimensionLTSucc
- CategoryTheory.instHasProjectiveDimensionLTHAddNat_1
Ancestors0
No ancestors.