Yoneda

📁 Source: Mathlib/CategoryTheory/Abelian/Yoneda.lean

Statistics

Metric	Count
Definitions	0
Theorems full_comp_preadditiveCoyonedaObj, preadditiveCoyonedaObj_map_surjective	2
Total	2

CategoryTheory.Abelian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
full_comp_preadditiveCoyonedaObj 📖	mathematical	CategoryTheory.IsSeparator CategoryTheory.Epi CategoryTheory.Functor.obj	CategoryTheory.Functor.Full ModuleCat MulOpposite CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOpposite.instRing CategoryTheory.Preadditive.instRingEnd toPreadditive ModuleCat.moduleCategory CategoryTheory.Functor.comp CategoryTheory.preadditiveCoyonedaObj	—	preadditiveCoyonedaObj_map_surjective CategoryTheory.Functor.map_surjective
preadditiveCoyonedaObj_map_surjective 📖	mathematical	CategoryTheory.IsSeparator	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct ModuleCat MulOpposite CategoryTheory.End MulOpposite.instRing CategoryTheory.Preadditive.instRingEnd toPreadditive ModuleCat.moduleCategory CategoryTheory.Functor.obj CategoryTheory.preadditiveCoyonedaObj CategoryTheory.Functor.map	—	CategoryTheory.additive_coyonedaObj CategoryTheory.Functor.coe_mapAddHom AddCommGrpCat.hom_ofHom AddCommGrpCat.epi_iff_surjective CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.kernel.condition CategoryTheory.ShortComplex.exact_of_f_is_kernel CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.op_mono_of_epi CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj CategoryTheory.ShortComplex.epi_of_mono_of_epi_of_mono CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.additive_yonedaObj' CategoryTheory.Functor.preservesZeroMorphisms_comp CategoryTheory.Functor.op_additive CategoryTheory.ShortComplex.Exact.map_of_mono_of_preservesKernel CategoryTheory.balanced_opposite CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory toIsNormalMonoCategory CategoryTheory.ShortComplex.Exact.op CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.preservesLimits_preadditiveYoneda_obj CategoryTheory.Functor.map_mono CategoryTheory.Functor.preservesMonomorphisms_comp CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.preservesFiniteLimits_op CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective ModuleCat.hom_ext CategoryTheory.Preadditive.add_comp LinearMap.ext_ring_op CategoryTheory.Category.id_comp

---

← Back to Index