Projective

📁 Source: Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.lean

Statistics

Metric	Count
Definitions Projective	1
Theorems projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj, projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj	2
Total	3

CategoryTheory

Definitions

Name	Category	Theorems
Projective 📖	CompData	51 math math: ModuleCat.projective_of_free, projective_iff_llp_epimorphisms_of_isZero, Projective.iso_iff, Stonean.instProjective, Injective.instProjectiveOppositeOp, Functor.projective_obj, Projective.projective_over, projective_of_preservesFiniteColimits_preadditiveCoyonedaObj, Rep.trivial_projective_of_subsingleton, Rep.free_projective, ProjectiveResolution.instProjectiveXNatOfComplex, Injective.injective_iff_projective_op, projective_iff_subsingleton_ext_one, Rep.diagonal_succ_projective, Rep.instProjective, Functor.projective_of_map_projective, Projective.projective_iff_preservesEpimorphisms_coyoneda_obj, IsProjective.iff_projective, Equivalence.map_projective_iff, projective_iff_llp_epimorphisms_zero, Injective.projective_iff_injective_op, Adjunction.projective_of_map_projective, ProjectivePresentation.projective, Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj, Profinite.projective_ultrafilter, Projective.instSyzygies, Functor.projective_obj_of_projective, Limits.IsZero.projective, ModuleCat.projective_of_categoryTheory_projective, Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj, ProjectiveResolution.instProjectiveXIntCochainComplex, Abelian.has_projective_separator, Projective.of_iso, Projective.zero_projective, Projective.instBiprod, Rep.standardComplex.x_projective, CompHaus.projective_ultrafilter, ModuleCat.instProjectiveObjFree, Profinite.projective_of_extrDisc, Stonean.instProjectiveCompHausCompHaus, Functor.PreservesProjectiveObjects.projective_obj, ProjectiveResolution.projective, CompHaus.Gleason, Rep.leftRegular_projective, Stonean.instProjectiveProfiniteObjToProfinite, Projective.inst, FDRep.instProjectiveOfNeZeroCastCard, Injective.instProjectiveUnopOfOpposite, projective_iff_hasProjectiveDimensionLT_one, Adjunction.map_projective, Projective.instCoprod

CategoryTheory.Projective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj 📖	mathematical	—	CategoryTheory.Projective CategoryTheory.Functor.PreservesEpimorphisms ModuleCat MulOpposite CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOpposite.instRing CategoryTheory.Preadditive.instRingEnd ModuleCat.moduleCategory CategoryTheory.preadditiveCoyonedaObj	—	projective_iff_preservesEpimorphisms_coyoneda_obj CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.instFaithfulForget CategoryTheory.Functor.preservesEpimorphisms_comp ModuleCat.forget_preservesEpimorphisms
projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj 📖	mathematical	—	CategoryTheory.Projective CategoryTheory.Functor.PreservesEpimorphisms AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.preadditiveCoyoneda Opposite.op	—	projective_iff_preservesEpimorphisms_coyoneda_obj CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.instFaithfulForget CategoryTheory.Functor.preservesEpimorphisms_comp AddCommGrpCat.forget_commGrp_preserves_epi

---

← Back to Index