Injective

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

Statistics

Metric	Count
Definitions Injective	1
Theorems injective_iff_preservesEpimorphisms_preadditiveYoneda_obj, injective_iff_preservesEpimorphisms_preadditive_yoneda_obj'	2
Total	3

CategoryTheory

Definitions

Name	Category	Theorems
Injective 📖	CompData	46 math math: InjectiveResolution.injective, AddCommGrpCat.injective_of_divisible, Equivalence.map_injective_iff, Injective.injective_under, Functor.injective_obj_of_injective, Profinite.injective_of_light, Injective.injective_of_adjoint, Functor.PreservesInjectiveObjects.injective_obj, Injective.of_iso, Injective.injective_iff_projective_op, Adjunction.map_injective, Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj', Injective.instUnopOfProjectiveOpposite, Injective.projective_iff_injective_op, LightProfinite.injective, Injective.instOfNonempty, Injective.zero_injective, InjectivePresentation.injective, Injective.instOppositeOpOfProjective, FDRep.instInjectiveOfNeZeroCastCard, injective_iff_rlp_monomorphisms_of_isZero, AddCommGrpCat.injective_as_module_iff, CochainComplex.cm5b.instInjectiveXIntI, Injective.instProd, Module.injective_iff_injective_object, IsGrothendieckAbelian.instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom, Injective.instBiprod, Limits.IsZero.injective, injective_iff_hasInjectiveDimensionLT_one, injective_iff_subsingleton_ext_one, Profinite.injective_of_finite, Injective.injective_iff_preservesEpimorphisms_yoneda_obj, Module.injective_object_of_injective_module, Abelian.has_injective_coseparator, Adjunction.injective_of_map_injective, injective_of_preservesFiniteColimits_preadditiveYonedaObj, CochainComplex.cm5b.instInjectiveXIntMappingConeIdI, Functor.injective_obj, Injective.injective_iff_preservesEpimorphisms_preadditiveYoneda_obj, injective_iff_rlp_monomorphisms_zero, ModuleCat.ulift_injective_of_injective, InjectiveResolution.instInjectiveXIntCochainComplex, InjectiveResolution.instInjectiveXNatOfCocomplex, Injective.iso_iff, Rep.instInjective, Functor.injective_of_map_injective

CategoryTheory.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_iff_preservesEpimorphisms_preadditiveYoneda_obj 📖	mathematical	—	CategoryTheory.Injective CategoryTheory.Functor.PreservesEpimorphisms Opposite CategoryTheory.Category.opposite AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.preadditiveYoneda	—	injective_iff_preservesEpimorphisms_yoneda_obj CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.instFaithfulForget CategoryTheory.Functor.preservesEpimorphisms_comp AddCommGrpCat.forget_commGrp_preserves_epi
injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' 📖	mathematical	—	CategoryTheory.Injective CategoryTheory.Functor.PreservesEpimorphisms Opposite CategoryTheory.Category.opposite ModuleCat CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.Preadditive.instRingEnd ModuleCat.moduleCategory CategoryTheory.preadditiveYonedaObj	—	injective_iff_preservesEpimorphisms_yoneda_obj CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.instFaithfulForget CategoryTheory.Functor.preservesEpimorphisms_comp ModuleCat.forget_preservesEpimorphisms

---

← Back to Index