Preserves

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

Statistics

Metric	Count
Definitions PreservesProjectiveObjects	1
Theorems projective_obj, preservesEpimorphisms_of_adjunction_of_preservesProjectiveObjects, preservesProjectiveObjects_comp, preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms, preservesProjectiveObjects_of_isEquivalence, projective_obj, projective_obj_of_projective	7
Total	8

CategoryTheory.Functor

Definitions

Name	Category	Theorems
PreservesProjectiveObjects 📖	CompData	5 math math: Rep.instPreservesProjectiveObjectsActionModuleCatSubtypeMemSubgroupResSubtype, preservesProjectiveObjects_comp, preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms, preservesProjectiveObjects_of_isEquivalence, ModuleCat.instPreservesProjectiveObjectsUliftFunctorOfSmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesEpimorphisms_of_adjunction_of_preservesProjectiveObjects 📖	mathematical	—	PreservesEpimorphisms	—	projective_obj CategoryTheory.Projective.projective_over CategoryTheory.Category.assoc map_comp CategoryTheory.Projective.factorThru_comp CategoryTheory.Adjunction.unit_naturality_assoc CategoryTheory.Adjunction.right_triangle_components CategoryTheory.Category.comp_id CategoryTheory.epi_of_epi_fac CategoryTheory.Projective.π_epi
preservesProjectiveObjects_comp 📖	mathematical	—	PreservesProjectiveObjects comp	—	projective_obj_of_projective
preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms 📖	mathematical	—	PreservesProjectiveObjects	—	CategoryTheory.Adjunction.map_projective
preservesProjectiveObjects_of_isEquivalence 📖	mathematical	—	PreservesProjectiveObjects	—	preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits instPreservesColimitsOfSizeOfIsLeftAdjoint isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse
projective_obj 📖	mathematical	—	CategoryTheory.Projective obj	—	PreservesProjectiveObjects.projective_obj
projective_obj_of_projective 📖	mathematical	—	CategoryTheory.Projective obj	—	PreservesProjectiveObjects.projective_obj

CategoryTheory.Functor.PreservesProjectiveObjects

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
projective_obj 📖	mathematical	—	CategoryTheory.Projective CategoryTheory.Functor.obj	—	—

---

← Back to Index