Connected

📁 Source: Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean

Statistics

Metric	Count
Definitions pullbackOfHasExactColimitsOfShape, pushoutOfHasExactLimitsOfShape	2
Theorems pullback_hom_ext, pullback_zero_ext, pushout_hom_ext, pushout_zero_ext	4
Total	6

CategoryTheory.Limits.IsColimit

Definitions

Name	Category	Theorems
pullbackOfHasExactColimitsOfShape 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pullback_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd	—	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape hom_ext CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.pullbackObjIso_inv_comp_snd_assoc
pullback_zero_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape pullback_hom_ext CategoryTheory.Limits.comp_zero

CategoryTheory.Limits.IsLimit

Definitions

Name	Category	Theorems
pushoutOfHasExactLimitsOfShape 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pushout_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.pushout CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.pushout.inr	—	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape hom_ext CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Limits.inr_comp_pushoutObjIso_hom
pushout_zero_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.pushout CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.pushout.inr Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape pushout_hom_ext CategoryTheory.Limits.zero_comp

---

← Back to Index