Structures · Category theory
CategoryTheory.Projective
An object P is called projective if every morphism out of P factors through every epimorphism.
- Shape
- One type argument · adds factors
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances7
- ModuleCat
- Rep
- Profinite
- FDRep
- CompHaus
- Stonean
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by66
- CategoryTheory.Presheaf.coherentExtensiveEquivalence
- CategoryTheory.Projective.factorThru
- CategoryTheory.Projective.factorThru_comp
- CategoryTheory.Projective.factors
- CategoryTheory.ShortComplex.Exact.liftFromProjective_comp
- CategoryTheory.Abelian.Ext.eq_zero_of_projective
- CategoryTheory.ProjectiveResolution.self
- CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective
- CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ
- CategoryTheory.ShortComplex.Exact.liftFromProjective
- CategoryTheory.Projective.factorThru_comp_assoc
- CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective
- Rep.isZero_Tor_succ_of_projective
- CategoryTheory.regularTopology.isSheafFor_regular_of_projective
- CategoryTheory.Abelian.Ext.subsingleton_of_projective
- DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective
- ModuleCat.projectiveDimension_eq_zero_of_projective
- CategoryTheory.Retract.projective
- CategoryTheory.Abelian.preadditiveCoyonedaObj_map_surjective
- CompHaus.toStonean
- isZero_Ext_succ_of_projective
- CategoryTheory.regularTopology.isSheaf_of_projective
- CategoryTheory.Projective.hasLiftingProperty_of_isZero
- CochainComplex.instIsKProjectiveExtendNatIntEmbeddingDownNatOfProjectiveX
- CategoryTheory.Presheaf.isSheaf_coherent_of_projective_of_comp
- HomologicalComplex.instProjectiveXExtend
- CategoryTheory.Projective.instCoprod
- CategoryTheory.ProjectiveResolution.self_complex
- ChainComplex.quasiIso_iff_of_projective
- CategoryTheory.Projective.instBiproduct
- CochainComplex.isKProjective_of_projective
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_obj
- CategoryTheory.ShortComplex.Exact.liftFromProjective_comp_assoc
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_hom
- CompHaus.instExtremallyDisconnectedCarrierToTopTrueOfProjective
- ModuleCat.projective_of_module_projective
- CategoryTheory.Abelian.full_comp_preadditiveCoyonedaObj
- CategoryTheory.Projective.instBiprod
- CategoryTheory.ShortComplex.Exact.liftFromProjective.congr_simp
- CompHaus.toStonean_toTop
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app
- HomologicalComplex.instProjectiveXObjSingle
- CategoryTheory.Projective.factorThru.congr_simp
- CategoryTheory.isZero_Tor'_succ_of_projective
- CategoryTheory.ProjectiveResolution.self_π
- precomp_extClass_surjective_of_projective_X₂
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app
- CategoryTheory.Projective.instHasLiftingPropertyOfEpi
- CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts
- CategoryTheory.preservesHomology_preadditiveCoyonedaObj_of_projective
Ancestors0
No ancestors.