Documentation Verification Report

Preserves

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

Statistics

Metric	Count
Definitions `PreservesInjectiveObjects`	1
Theorems `injective_obj`, `injective_obj`, `injective_obj_of_injective`, `preservesInjectiveObjects_comp`, `preservesInjectiveObjects_of_adjunction_of_preservesMonomorphisms`, `preservesInjectiveObjects_of_isEquivalence`, `preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects`	7
Total	8

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`PreservesInjectiveObjects` 📖	CompData	5 math math: `preservesInjectiveObjects_of_isEquivalence`, `preservesInjectiveObjects_comp`, `CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesInjectiveObjects`, `preservesInjectiveObjects_of_adjunction_of_preservesMonomorphisms`, `ModuleCat.instPreservesInjectiveObjectsUliftFunctorOfSmall`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective_obj` 📖	mathematical	—	`CategoryTheory.Injective` `obj`	—	`PreservesInjectiveObjects.injective_obj`
`injective_obj_of_injective` 📖	mathematical	—	`CategoryTheory.Injective` `obj`	—	`PreservesInjectiveObjects.injective_obj`
`preservesInjectiveObjects_comp` 📖	mathematical	—	`PreservesInjectiveObjects` `comp`	—	`injective_obj_of_injective`
`preservesInjectiveObjects_of_adjunction_of_preservesMonomorphisms` 📖	mathematical	—	`PreservesInjectiveObjects`	—	`CategoryTheory.Adjunction.map_injective`
`preservesInjectiveObjects_of_isEquivalence` 📖	mathematical	—	`PreservesInjectiveObjects`	—	`preservesInjectiveObjects_of_adjunction_of_preservesMonomorphisms` `CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `instPreservesLimitsOfSizeOfIsRightAdjoint` `isRightAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_functor`
`preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects` 📖	mathematical	—	`PreservesMonomorphisms`	—	`injective_obj` `CategoryTheory.Injective.injective_under` `CategoryTheory.Injective.comp_factorThru` `map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Adjunction.counit_naturality` `CategoryTheory.Adjunction.left_triangle_components_assoc` `CategoryTheory.mono_of_mono_fac` `CategoryTheory.Injective.ι_mono`

CategoryTheory.Functor.PreservesInjectiveObjects

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective_obj` 📖	mathematical	—	`CategoryTheory.Injective` `CategoryTheory.Functor.obj`	—	—

---

← Back to Index