Abelian

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

Statistics

Metric	Count
Definitions	0
Theorems has_injective_coseparator, has_projective_separator	2
Total	2

CategoryTheory.Abelian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_injective_coseparator 📖	mathematical	CategoryTheory.IsSeparator	CategoryTheory.Injective CategoryTheory.IsCoseparator	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasProductsOfShape_of_small CategoryTheory.small_subobject CategoryTheory.instLocallySmallOpposite CategoryTheory.locallySmall_of_univLE UnivLE.self wellPowered_opposite CategoryTheory.wellPowered_of_isDetector CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits hasFiniteLimits CategoryTheory.IsSeparator.isDetector CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory toIsNormalMonoCategory CategoryTheory.Limits.hasProductsOfShape_of_hasProducts CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Injective.injective_under CategoryTheory.Preadditive.isCoseparator_iff CategoryTheory.Preadditive.isSeparator_iff CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations instHasStrongEpiMonoFactorisations CategoryTheory.op_mono_of_epi CategoryTheory.Limits.instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair hasEqualizers CategoryTheory.Limits.isSplitEpi_pi_π CategoryTheory.Limits.zero_of_comp_mono CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.section_isSplitMono CategoryTheory.Injective.ι_mono CategoryTheory.Limits.instMonoι CategoryTheory.Injective.comp_factorThru CategoryTheory.Limits.image.fac_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.comp_zero CategoryTheory.Limits.image.fac CategoryTheory.Limits.zero_comp
has_projective_separator 📖	mathematical	CategoryTheory.IsCoseparator	CategoryTheory.Projective CategoryTheory.IsSeparator	—	has_injective_coseparator CategoryTheory.Limits.hasLimits_op_of_hasColimits CategoryTheory.Injective.instEnoughInjectivesOppositeOfEnoughProjectives CategoryTheory.isSeparator_op_iff CategoryTheory.Injective.instProjectiveUnopOfOpposite CategoryTheory.isSeparator_unop_iff

---

← Back to Index