LeftResolution

📁 Source: Mathlib/Algebra/Category/ModuleCat/LeftResolution.lean

Statistics

Metric	Count
Definitions LeftResolution, LeftResolution, projectiveResolution	3
Theorems instProjectiveObjFree	1
Total	4

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
LeftResolution 📖	CompData	—

CategoryTheory.LocalizerMorphism

Definitions

Name	Category	Theorems
LeftResolution 📖	CompData	14 math math: LeftResolution.opFunctor_map_f, LeftResolution.id_f, LeftResolution.opEquivalence_unitIso, nonempty_rightResolution_iff_op, LeftResolution.opEquivalence_inverse, LeftResolution.opFunctor_obj, HomotopicalAlgebra.CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism, LeftResolution.comp_f_assoc, RightResolution.unopFunctor_obj, LeftResolution.comp_f, nonempty_leftResolution_iff_op, RightResolution.unopFunctor_map_f, LeftResolution.opEquivalence_counitIso, LeftResolution.opEquivalence_functor

ModuleCat

Definitions

Name	Category	Theorems
projectiveResolution 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instProjectiveObjFree 📖	mathematical	—	CategoryTheory.Projective ModuleCat moduleCategory CategoryTheory.Functor.obj CategoryTheory.types free	—	Function.Surjective.hasRightInverse epi_iff_surjective free_hom_ext freeDesc_apply

---

← Back to Index