Structures · Category theory
CategoryTheory.EnoughProjectives
A category "has enough projectives" if for every object X there is a projective object P and
an epimorphism P ↠ X.
- Shape
- One type argument · adds presentation
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- ModuleCat
- Rep
- Profinite
- CompHaus
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by27
- CategoryTheory.Projective.π
- CategoryTheory.Projective.over
- CategoryTheory.Projective.syzygies
- CategoryTheory.Projective.d
- CategoryTheory.ProjectiveResolution.ofComplex
- CategoryTheory.exact_d_f
- Ext
- CategoryTheory.ProjectiveResolution.isoExt
- CategoryTheory.ProjectiveResolution.of
- isZero_Ext_succ_of_projective
- CategoryTheory.Injective.enoughInjectives_of_enoughProjectives_op
- CategoryTheory.Abelian.has_projective_separator
- CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succ
- CategoryTheory.EnoughProjectives.presentation
- CategoryTheory.hasInjectiveDimensionLT_of_enoughProjectives
- CategoryTheory.hasExt_of_enoughProjectives
- CategoryTheory.Functor.mapExt_bijective_of_preservesProjectiveObjects
- CategoryTheory.ProjectiveResolution.instHasProjectiveResolutions
- CategoryTheory.ProjectiveResolution.of_def
- CategoryTheory.Projective.π_epi
- CategoryTheory.Projective.projective_over
- CategoryTheory.Functor.preservesEpimorphisms_of_adjunction_of_preservesProjectiveObjects
- CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex
- CategoryTheory.ProjectiveResolution.ofComplex_d_1_0
- CategoryTheory.ProjectiveResolution.instHasProjectiveResolution
- CategoryTheory.Projective.instSyzygies
- CategoryTheory.Injective.instEnoughInjectivesOppositeOfEnoughProjectives
Ancestors0
No ancestors.