Documentation Verification Report

Equalizers

📁 Source: Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean

Statistics

Metric	Count
Definitions `coequalizerCocone`, `coequalizerCoconeIsColimit`, `constructCoequalizer`, `pushoutInl`, `constructEqualizer`, `equalizerCone`, `equalizerConeIsLimit`, `pullbackFst`	8
Theorems `pushoutInl_eq_pushout_inr`, `pullbackFst_eq_pullback_snd`, `hasCoequalizers_of_hasPushouts_and_binary_coproducts`, `hasEqualizers_of_hasPullbacks_and_binary_products`, `preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts`, `preservesEqualizers_of_preservesPullbacks_and_binaryProducts`	6
Total	14

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasCoequalizers_of_hasPushouts_and_binary_coproducts` 📖	mathematical	—	`HasCoequalizers`	—	—
`hasEqualizers_of_hasPullbacks_and_binary_products` 📖	mathematical	—	`HasEqualizers`	—	—
`preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts` 📖	mathematical	—	`PreservesColimitsOfShape` `WalkingParallelPair` `walkingParallelPairHomCategory`	—	`preservesColimit_of_preserves_colimit_cocone` `hasPushout_of_preservesPushout` `PreservesColimitsOfShape.preservesColimit` `hasColimitOfHasColimitsOfShape` `IsColimit.hom_ext` `CategoryTheory.Functor.map_comp_assoc` `coprod.inl_desc` `coprod.inr_desc` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Category.id_comp` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `PreservesPushout.inl_iso_inv_assoc` `pushout.inl_desc` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.eq_inv_comp` `pushout.hom_ext` `PreservesPushout.inl_iso_hom_assoc` `pushout.desc.congr_simp` `PreservesPushout.inr_iso_hom_assoc` `pushout.inr_desc`
`preservesEqualizers_of_preservesPullbacks_and_binaryProducts` 📖	mathematical	—	`PreservesLimitsOfShape` `WalkingParallelPair` `walkingParallelPairHomCategory`	—	`preservesLimit_of_preserves_limit_cone` `hasPullback_of_preservesPullback` `PreservesLimitsOfShape.preservesLimit` `hasLimitOfHasLimitsOfShape` `IsLimit.hom_ext` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `prod.lift_fst` `prod.lift_snd` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Category.comp_id` `PreservesPullback.iso_inv_fst` `pullback.lift_fst` `PreservesPullback.iso_inv_fst_assoc` `pullback.lift_fst_assoc` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.eq_comp_inv` `pullback.hom_ext` `PreservesPullback.iso_hom_fst` `pullback.lift.congr_simp` `PreservesPullback.iso_hom_snd` `pullback.lift_snd`

CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts

Definitions

Name	Category	Theorems
`coequalizerCocone` 📖	CompOp	—
`coequalizerCoconeIsColimit` 📖	CompOp	—
`constructCoequalizer` 📖	CompOp	—
`pushoutInl` 📖	CompOp	1 math math: `pushoutInl_eq_pushout_inr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pushoutInl_eq_pushout_inr` 📖	mathematical	—	`pushoutInl` `CategoryTheory.Limits.pushout.inr` `CategoryTheory.Limits.coprod` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.WalkingParallelPair.one` `CategoryTheory.Limits.WalkingParallelPair.zero` `CategoryTheory.Limits.coprod.desc` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.Limits.WalkingParallelPairHom.left` `CategoryTheory.Limits.WalkingParallelPairHom.right`	—	`CategoryTheory.Limits.coprod.desc_comp` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.colimit.ι_desc` `CategoryTheory.whisker_eq` `CategoryTheory.Limits.pushout.condition`

CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts

Definitions

Name	Category	Theorems
`constructEqualizer` 📖	CompOp	—
`equalizerCone` 📖	CompOp	—
`equalizerConeIsLimit` 📖	CompOp	—
`pullbackFst` 📖	CompOp	1 math math: `pullbackFst_eq_pullback_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pullbackFst_eq_pullback_snd` 📖	mathematical	—	`pullbackFst` `CategoryTheory.Limits.pullback.snd` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.WalkingParallelPair.zero` `CategoryTheory.Limits.prod` `CategoryTheory.Limits.WalkingParallelPair.one` `CategoryTheory.Limits.prod.lift` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.Limits.WalkingParallelPairHom.left` `CategoryTheory.Limits.WalkingParallelPairHom.right`	—	`CategoryTheory.Limits.prod.comp_lift` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.eq_whisker` `CategoryTheory.Limits.pullback.condition`

---

← Back to Index