Projective

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

Statistics

Metric	Count
Definitions	0
Theorems iff_projective, enoughProjectives, projective_of_categoryTheory_projective, projective_of_free, projective_of_module_projective	5
Total	5

IsProjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_projective 📖	mathematical	—	Module.Projective Ring.toSemiring AddCommGroup.toAddCommMonoid CategoryTheory.Projective ModuleCat ModuleCat.moduleCategory ModuleCat.of	—	ModuleCat.projective_of_categoryTheory_projective ModuleCat.projective_of_module_projective

ModuleCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enoughProjectives 📖	mathematical	—	CategoryTheory.EnoughProjectives ModuleCat moduleCategory	—	RingHomInvPair.ids projective_of_free AddMonoid.nat_smulCommClass' RingHomSurjective.ids epi_iff_range_eq_top LinearMap.range_eq_top Module.Basis.constr_apply LinearEquiv.map_zero Finsupp.mapRange_single equivShrink_symm_one Finsupp.sum_single_index zero_smul one_smul
projective_of_categoryTheory_projective 📖	mathematical	—	CategoryTheory.Projective ModuleCat moduleCategory	—	RingHomCompTriple.ids Module.projective_lifting_property epi_iff_surjective hom_ext
projective_of_free 📖	mathematical	—	CategoryTheory.Projective ModuleCat moduleCategory	—	Module.Projective.of_basis projective_of_categoryTheory_projective
projective_of_module_projective 📖	mathematical	—	Module.Projective Ring.toSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule	—	Module.Projective.of_lifting_property epi_iff_surjective RingHomCompTriple.ids hom_ext_iff CategoryTheory.Projective.factorThru_comp

---

← Back to Index