Documentation Verification Report

WideEqualizers

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean

Statistics

Metric	Count
Definitions `ofCotrident`, `ofTrident`, `Cotrident`, `desc'`, `homIso`, `mk`, `mk'`, `ext`, `mkHom`, `ofCocone`, `ofπ`, `π`, `HasWideCoequalizer`, `HasWideCoequalizers`, `HasWideEqualizer`, `HasWideEqualizers`, `Trident`, `homIso`, `lift'`, `mk`, `mk'`, `ext`, `mkHom`, `ofCone`, `ofι`, `ι`, `WalkingParallelFamily`, `comp`, `arrowEquiv`, `category`, `instDecidableEqHom`, `decEq`, `diagramIsoParallelFamily`, `instDecidableEqWalkingParallelFamily`, `instInhabitedHomZero`, `instInhabitedWalkingParallelFamily`, `default`, `parallelFamily`, `walkingParallelFamilyEquivWalkingParallelPair`, `wideCoequalizer`, `cotrident`, `desc`, `desc'`, `π`, `wideCoequalizerIsWideCoequalizer`, `wideEqualizer`, `lift'`, `trident`, `ι`, `wideEqualizerIsWideEqualizer`	50
Theorems `ofCotrident_ι`, `ofTrident_π`, `homIso_apply_coe`, `homIso_natural`, `homIso_symm_apply`, `hom_ext`, `app_one`, `app_one_assoc`, `coequalizer_ext`, `condition`, `condition_assoc`, `mkHom_hom`, `ofCocone_ι`, `ofπ_pt`, `ofπ_ι_app`, `π_eq_app_one`, `π_ofπ`, `homIso_apply_coe`, `homIso_natural`, `homIso_symm_apply`, `hom_ext`, `app_zero`, `app_zero_assoc`, `condition`, `condition_assoc`, `equalizer_ext`, `ext_hom`, `ext_inv`, `mkHom_hom`, `ofCone_π`, `ofι_pt`, `ofι_π_app`, `ι_eq_app_zero`, `ι_ofι`, `hom_id`, `diagramIsoParallelFamily_hom_app`, `diagramIsoParallelFamily_inv_app`, `epi_of_isColimit_parallelFamily`, `hasCoequalizers_of_hasWideCoequalizers`, `hasEqualizers_of_hasWideEqualizers`, `hasWideCoequalizers_of_hasColimit_parallelFamily`, `hasWideEqualizers_of_hasLimit_parallelFamily`, `mono_of_isLimit_parallelFamily`, `parallelFamily_map_left`, `parallelFamily_obj_one`, `parallelFamily_obj_zero`, `walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app`, `walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app`, `walkingParallelFamilyEquivWalkingParallelPair_functor_map`, `walkingParallelFamilyEquivWalkingParallelPair_functor_obj`, `walkingParallelFamilyEquivWalkingParallelPair_inverse_map`, `walkingParallelFamilyEquivWalkingParallelPair_inverse_obj`, `walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app`, `walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app`, `condition`, `condition_assoc`, `cotrident_ι_app_one`, `cotrident_π`, `hom_ext`, `hom_ext_iff`, `π_desc`, `π_desc_assoc`, `π_epi`, `condition`, `condition_assoc`, `hom_ext`, `hom_ext_iff`, `lift_ι`, `lift_ι_assoc`, `trident_ι`, `trident_π_app_zero`, `ι_mono`	72
Total	122

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`Cotrident` 📖	CompOp	—
`HasWideCoequalizer` 📖	MathDef	—
`HasWideCoequalizers` 📖	MathDef	1 math math: `hasWideCoequalizers_of_hasColimit_parallelFamily`
`HasWideEqualizer` 📖	MathDef	—
`HasWideEqualizers` 📖	MathDef	1 math math: `hasWideEqualizers_of_hasLimit_parallelFamily`
`Trident` 📖	CompOp	2 math math: `Trident.ext_hom`, `Trident.ext_inv`
`WalkingParallelFamily` 📖	CompData	43 math math: `Trident.condition_assoc`, `parallelFamily_obj_zero`, `Cotrident.ofCocone_ι`, `Trident.app_zero`, `Cone.ofTrident_π`, `mono_of_isLimit_parallelFamily`, `walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app`, `diagramIsoParallelFamily_inv_app`, `Cocone.ofCotrident_ι`, `Cotrident.π_eq_app_one`, `Trident.ofι_pt`, `Cotrident.IsColimit.homIso_natural`, `Trident.condition`, `Cotrident.ofπ_pt`, `Cotrident.condition_assoc`, `walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app`, `CategoryTheory.hasCardinalLT_arrow_walkingParallelFamily`, `walkingParallelFamilyEquivWalkingParallelPair_functor_map`, `walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app`, `walkingParallelFamilyEquivWalkingParallelPair_inverse_obj`, `parallelFamily_obj_one`, `walkingParallelFamilyEquivWalkingParallelPair_inverse_map`, `Trident.IsLimit.homIso_apply_coe`, `walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app`, `Cotrident.IsColimit.homIso_symm_apply`, `Trident.ofCone_π`, `WalkingParallelFamily.hom_id`, `Trident.ofι_π_app`, `diagramIsoParallelFamily_hom_app`, `Trident.ι_eq_app_zero`, `Cotrident.app_one`, `Trident.IsLimit.homIso_symm_apply`, `wideCoequalizer.cotrident_ι_app_one`, `Cotrident.condition`, `epi_of_isColimit_parallelFamily`, `Trident.app_zero_assoc`, `Cotrident.ofπ_ι_app`, `walkingParallelFamilyEquivWalkingParallelPair_functor_obj`, `Cotrident.app_one_assoc`, `wideEqualizer.trident_π_app_zero`, `parallelFamily_map_left`, `Trident.IsLimit.homIso_natural`, `Cotrident.IsColimit.homIso_apply_coe`
`diagramIsoParallelFamily` 📖	CompOp	2 math math: `diagramIsoParallelFamily_inv_app`, `diagramIsoParallelFamily_hom_app`
`instDecidableEqWalkingParallelFamily` 📖	CompOp	—
`instInhabitedHomZero` 📖	CompOp	—
`instInhabitedWalkingParallelFamily` 📖	CompOp	—
`parallelFamily` 📖	CompOp	37 math math: `Trident.condition_assoc`, `parallelFamily_obj_zero`, `Cotrident.ofCocone_ι`, `Trident.app_zero`, `Cone.ofTrident_π`, `mono_of_isLimit_parallelFamily`, `walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app`, `diagramIsoParallelFamily_inv_app`, `Cocone.ofCotrident_ι`, `Cotrident.π_eq_app_one`, `Trident.ofι_pt`, `Cotrident.IsColimit.homIso_natural`, `Trident.condition`, `Cotrident.ofπ_pt`, `Cotrident.condition_assoc`, `walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app`, `walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app`, `parallelFamily_obj_one`, `Trident.IsLimit.homIso_apply_coe`, `walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app`, `Cotrident.IsColimit.homIso_symm_apply`, `Trident.ofCone_π`, `Trident.ofι_π_app`, `diagramIsoParallelFamily_hom_app`, `Trident.ι_eq_app_zero`, `Cotrident.app_one`, `Trident.IsLimit.homIso_symm_apply`, `wideCoequalizer.cotrident_ι_app_one`, `Cotrident.condition`, `epi_of_isColimit_parallelFamily`, `Trident.app_zero_assoc`, `Cotrident.ofπ_ι_app`, `Cotrident.app_one_assoc`, `wideEqualizer.trident_π_app_zero`, `parallelFamily_map_left`, `Trident.IsLimit.homIso_natural`, `Cotrident.IsColimit.homIso_apply_coe`
`walkingParallelFamilyEquivWalkingParallelPair` 📖	CompOp	8 math math: `walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app`, `walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app`, `walkingParallelFamilyEquivWalkingParallelPair_functor_map`, `walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app`, `walkingParallelFamilyEquivWalkingParallelPair_inverse_obj`, `walkingParallelFamilyEquivWalkingParallelPair_inverse_map`, `walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app`, `walkingParallelFamilyEquivWalkingParallelPair_functor_obj`
`wideCoequalizer` 📖	CompOp	6 math math: `wideCoequalizer.π_epi`, `wideCoequalizer.condition`, `wideCoequalizer.condition_assoc`, `wideCoequalizer.π_desc_assoc`, `wideCoequalizer.π_desc`, `wideCoequalizer.hom_ext_iff`
`wideCoequalizerIsWideCoequalizer` 📖	CompOp	—
`wideEqualizer` 📖	CompOp	6 math math: `wideEqualizer.condition_assoc`, `wideEqualizer.lift_ι_assoc`, `wideEqualizer.ι_mono`, `wideEqualizer.lift_ι`, `wideEqualizer.hom_ext_iff`, `wideEqualizer.condition`
`wideEqualizerIsWideEqualizer` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diagramIsoParallelFamily_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `WalkingParallelFamily` `WalkingParallelFamily.category` `parallelFamily` `CategoryTheory.Functor.obj` `WalkingParallelFamily.zero` `WalkingParallelFamily.one` `CategoryTheory.Functor.map` `WalkingParallelFamily.Hom.line` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `diagramIsoParallelFamily` `CategoryTheory.eqToHom` `CategoryTheory.Category.toCategoryStruct`	—	—
`diagramIsoParallelFamily_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `WalkingParallelFamily` `WalkingParallelFamily.category` `parallelFamily` `CategoryTheory.Functor.obj` `WalkingParallelFamily.zero` `WalkingParallelFamily.one` `CategoryTheory.Functor.map` `WalkingParallelFamily.Hom.line` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `diagramIsoParallelFamily` `CategoryTheory.eqToHom` `CategoryTheory.Category.toCategoryStruct`	—	—
`epi_of_isColimit_parallelFamily` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `WalkingParallelFamily` `WalkingParallelFamily.category` `parallelFamily` `WalkingParallelFamily.one` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `Cocone.pt` `CategoryTheory.NatTrans.app` `Cocone.ι`	—	`Cotrident.IsColimit.hom_ext`
`hasCoequalizers_of_hasWideCoequalizers` 📖	mathematical	`HasWideCoequalizers`	`HasCoequalizers`	—	`hasColimitsOfShape_of_equivalence`
`hasEqualizers_of_hasWideEqualizers` 📖	mathematical	`HasWideEqualizers`	`HasEqualizers`	—	`hasLimitsOfShape_of_equivalence`
`hasWideCoequalizers_of_hasColimit_parallelFamily` 📖	mathematical	`HasColimit` `WalkingParallelFamily` `WalkingParallelFamily.category` `parallelFamily`	`HasWideCoequalizers`	—	`hasColimit_of_iso`
`hasWideEqualizers_of_hasLimit_parallelFamily` 📖	mathematical	`HasLimit` `WalkingParallelFamily` `WalkingParallelFamily.category` `parallelFamily`	`HasWideEqualizers`	—	`hasLimit_of_iso`
`mono_of_isLimit_parallelFamily` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `WalkingParallelFamily` `WalkingParallelFamily.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `Cone.pt` `parallelFamily` `WalkingParallelFamily.zero` `Trident.ι`	—	`Trident.IsLimit.hom_ext`
`parallelFamily_map_left` 📖	mathematical	—	`CategoryTheory.Functor.map` `WalkingParallelFamily` `WalkingParallelFamily.category` `parallelFamily` `WalkingParallelFamily.zero` `WalkingParallelFamily.one` `WalkingParallelFamily.Hom.line`	—	—
`parallelFamily_obj_one` 📖	mathematical	—	`CategoryTheory.Functor.obj` `WalkingParallelFamily` `WalkingParallelFamily.category` `parallelFamily` `WalkingParallelFamily.one`	—	—
`parallelFamily_obj_zero` 📖	mathematical	—	`CategoryTheory.Functor.obj` `WalkingParallelFamily` `WalkingParallelFamily.category` `parallelFamily` `WalkingParallelFamily.zero`	—	—
`walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `WalkingParallelPair` `walkingParallelPairHomCategory` `CategoryTheory.Functor.comp` `WalkingParallelFamily` `WalkingParallelFamily.category` `parallelPair` `WalkingParallelFamily.zero` `WalkingParallelFamily.one` `WalkingParallelFamily.Hom.line` `parallelFamily` `WalkingParallelPair.zero` `WalkingParallelPair.one` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `WalkingParallelPairHom.left` `WalkingParallelPairHom.right` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `walkingParallelFamilyEquivWalkingParallelPair` `CategoryTheory.eqToHom` `CategoryTheory.Functor.obj`	—	—
`walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `WalkingParallelPair` `walkingParallelPairHomCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `WalkingParallelFamily` `WalkingParallelFamily.category` `parallelPair` `WalkingParallelFamily.zero` `WalkingParallelFamily.one` `WalkingParallelFamily.Hom.line` `parallelFamily` `WalkingParallelPair.zero` `WalkingParallelPair.one` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `WalkingParallelPairHom.left` `WalkingParallelPairHom.right` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `walkingParallelFamilyEquivWalkingParallelPair` `CategoryTheory.eqToHom` `CategoryTheory.Functor.obj`	—	—
`walkingParallelFamilyEquivWalkingParallelPair_functor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `WalkingParallelFamily` `WalkingParallelFamily.category` `WalkingParallelPair` `walkingParallelPairHomCategory` `CategoryTheory.Equivalence.functor` `walkingParallelFamilyEquivWalkingParallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `WalkingParallelPair.zero` `WalkingParallelPair.one` `CategoryTheory.CategoryStruct.id` `WalkingParallelPairHom.left` `WalkingParallelPairHom.right`	—	—
`walkingParallelFamilyEquivWalkingParallelPair_functor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `WalkingParallelFamily` `WalkingParallelFamily.category` `WalkingParallelPair` `walkingParallelPairHomCategory` `CategoryTheory.Equivalence.functor` `walkingParallelFamilyEquivWalkingParallelPair` `WalkingParallelPair.zero` `WalkingParallelPair.one`	—	—
`walkingParallelFamilyEquivWalkingParallelPair_inverse_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `WalkingParallelPair` `walkingParallelPairHomCategory` `WalkingParallelFamily` `WalkingParallelFamily.category` `CategoryTheory.Equivalence.inverse` `walkingParallelFamilyEquivWalkingParallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `WalkingParallelFamily.zero` `WalkingParallelFamily.one` `CategoryTheory.CategoryStruct.id` `WalkingParallelFamily.Hom.line`	—	—
`walkingParallelFamilyEquivWalkingParallelPair_inverse_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `WalkingParallelPair` `walkingParallelPairHomCategory` `WalkingParallelFamily` `WalkingParallelFamily.category` `CategoryTheory.Equivalence.inverse` `walkingParallelFamilyEquivWalkingParallelPair` `WalkingParallelFamily.zero` `WalkingParallelFamily.one`	—	—
`walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `WalkingParallelFamily` `WalkingParallelFamily.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `WalkingParallelPair` `walkingParallelPairHomCategory` `parallelFamily` `WalkingParallelPair.zero` `WalkingParallelPair.one` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `WalkingParallelPairHom.left` `WalkingParallelPairHom.right` `parallelPair` `WalkingParallelFamily.zero` `WalkingParallelFamily.one` `WalkingParallelFamily.Hom.line` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `walkingParallelFamilyEquivWalkingParallelPair` `CategoryTheory.eqToHom` `CategoryTheory.Functor.obj`	—	—
`walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `WalkingParallelFamily` `WalkingParallelFamily.category` `CategoryTheory.Functor.comp` `WalkingParallelPair` `walkingParallelPairHomCategory` `parallelFamily` `WalkingParallelPair.zero` `WalkingParallelPair.one` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `WalkingParallelPairHom.left` `WalkingParallelPairHom.right` `parallelPair` `WalkingParallelFamily.zero` `WalkingParallelFamily.one` `WalkingParallelFamily.Hom.line` `CategoryTheory.Functor.id` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `walkingParallelFamilyEquivWalkingParallelPair` `CategoryTheory.eqToHom` `CategoryTheory.Functor.obj`	—	—

CategoryTheory.Limits.Cocone

Definitions

Name	Category	Theorems
`ofCotrident` 📖	CompOp	1 math math: `ofCotrident_ι`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofCotrident_ι` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `pt` `ofCotrident` `ι` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.zero` `CategoryTheory.Limits.WalkingParallelFamily.one` `CategoryTheory.Functor.map` `CategoryTheory.Limits.WalkingParallelFamily.Hom.line` `CategoryTheory.eqToHom`	—	—

CategoryTheory.Limits.Cone

Definitions

Name	Category	Theorems
`ofTrident` 📖	CompOp	1 math math: `ofTrident_π`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofTrident_π` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `pt` `ofTrident` `π` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.zero` `CategoryTheory.Limits.WalkingParallelFamily.one` `CategoryTheory.Functor.map` `CategoryTheory.Limits.WalkingParallelFamily.Hom.line` `CategoryTheory.eqToHom`	—	—

CategoryTheory.Limits.Cotrident

Definitions

Name	Category	Theorems
`ext` 📖	CompOp	—
`mkHom` 📖	CompOp	1 math math: `mkHom_hom`
`ofCocone` 📖	CompOp	1 math math: `ofCocone_ι`
`ofπ` 📖	CompOp	3 math math: `ofπ_pt`, `π_ofπ`, `ofπ_ι_app`
`π` 📖	CompOp	7 math math: `π_eq_app_one`, `condition_assoc`, `CategoryTheory.Limits.wideCoequalizer.cotrident_π`, `IsColimit.homIso_symm_apply`, `condition`, `π_ofπ`, `IsColimit.homIso_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`app_one` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.one` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Limits.WalkingParallelFamily.zero`	—	`CategoryTheory.Limits.Cocone.w` `CategoryTheory.Limits.parallelFamily_map_left`
`app_one_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.one` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Limits.WalkingParallelFamily.zero`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `app_one`
`coequalizer_ext` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.one` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `π`	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`app_one` `CategoryTheory.Category.assoc`
`condition` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.one` `π`	—	`app_one`
`condition_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.one` `π`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `condition`
`mkHom_hom` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.one` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `π`	`CategoryTheory.Limits.CoconeMorphism.hom` `mkHom`	—	—
`ofCocone_ι` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily.zero` `CategoryTheory.Limits.WalkingParallelFamily.one` `CategoryTheory.Functor.map` `CategoryTheory.Limits.WalkingParallelFamily.Hom.line` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `ofCocone` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eqToHom`	—	—
`ofπ_pt` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `ofπ`	—	—
`ofπ_ι_app` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.ι` `ofπ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.WalkingParallelFamily.zero` `Classical.arbitrary`	—	—
`π_eq_app_one` 📖	mathematical	—	`π` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Limits.WalkingParallelFamily.one`	—	—
`π_ofπ` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`π` `ofπ`	—	—

CategoryTheory.Limits.Cotrident.IsColimit

Definitions

Name	Category	Theorems
`desc'` 📖	CompOp	1 math math: `homIso_symm_apply`
`homIso` 📖	CompOp	3 math math: `homIso_natural`, `homIso_symm_apply`, `homIso_apply_coe`
`mk` 📖	CompOp	—
`mk'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homIso_apply_coe` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `DFunLike.coe` `Equiv` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `EquivLike.toFunLike` `Equiv.instEquivLike` `homIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.WalkingParallelFamily.one` `CategoryTheory.Limits.Cotrident.π`	—	—
`homIso_natural` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `DFunLike.coe` `Equiv` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `EquivLike.toFunLike` `Equiv.instEquivLike` `homIso` `CategoryTheory.CategoryStruct.comp`	—	`CategoryTheory.Category.assoc`
`homIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homIso` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily.one` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cotrident.π` `desc'`	—	—
`hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.one` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.Cotrident.π`	—	—	`CategoryTheory.Limits.IsColimit.hom_ext` `CategoryTheory.Limits.Cotrident.coequalizer_ext`

CategoryTheory.Limits.Trident

Definitions

Name	Category	Theorems
`ext` 📖	CompOp	2 math math: `ext_hom`, `ext_inv`
`mkHom` 📖	CompOp	3 math math: `ext_hom`, `ext_inv`, `mkHom_hom`
`ofCone` 📖	CompOp	1 math math: `ofCone_π`
`ofι` 📖	CompOp	3 math math: `ι_ofι`, `ofι_pt`, `ofι_π_app`
`ι` 📖	CompOp	8 math math: `condition_assoc`, `ι_ofι`, `CategoryTheory.Limits.mono_of_isLimit_parallelFamily`, `condition`, `CategoryTheory.Limits.wideEqualizer.trident_ι`, `IsLimit.homIso_apply_coe`, `ι_eq_app_zero`, `IsLimit.homIso_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`app_zero` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.zero` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π` `CategoryTheory.Limits.WalkingParallelFamily.one`	—	`CategoryTheory.Limits.Cone.w` `CategoryTheory.Limits.parallelFamily_map_left`
`app_zero_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.zero` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π` `CategoryTheory.Limits.WalkingParallelFamily.one`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `app_zero`
`condition` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.zero` `ι`	—	`app_zero`
`condition_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.zero` `ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `condition`
`equalizer_ext` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily.zero` `ι`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.π`	—	`app_zero` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'`
`ext_hom` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily.zero` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Iso.hom` `ι`	`CategoryTheory.Limits.Trident` `CategoryTheory.Limits.Cone.category` `ext` `mkHom`	—	—
`ext_inv` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily.zero` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Iso.hom` `ι`	`CategoryTheory.Iso.inv` `CategoryTheory.Limits.Trident` `CategoryTheory.Limits.Cone.category` `ext` `mkHom`	—	—
`mkHom_hom` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily.zero` `CategoryTheory.CategoryStruct.comp` `ι`	`CategoryTheory.Limits.ConeMorphism.hom` `mkHom`	—	—
`ofCone_π` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.zero` `CategoryTheory.Limits.WalkingParallelFamily.one` `CategoryTheory.Functor.map` `CategoryTheory.Limits.WalkingParallelFamily.Hom.line` `ofCone` `CategoryTheory.Limits.Cone.π` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eqToHom`	—	—
`ofι_pt` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `ofι`	—	—
`ofι_π_app` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.Cone.π` `ofι` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.WalkingParallelFamily.one` `Classical.arbitrary`	—	—
`ι_eq_app_zero` 📖	mathematical	—	`ι` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Limits.Cone.π` `CategoryTheory.Limits.WalkingParallelFamily.zero`	—	—
`ι_ofι` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`ι` `ofι`	—	—

CategoryTheory.Limits.Trident.IsLimit

Definitions

Name	Category	Theorems
`homIso` 📖	CompOp	3 math math: `homIso_apply_coe`, `homIso_symm_apply`, `homIso_natural`
`lift'` 📖	CompOp	1 math math: `homIso_symm_apply`
`mk` 📖	CompOp	—
`mk'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homIso_apply_coe` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `DFunLike.coe` `Equiv` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `EquivLike.toFunLike` `Equiv.instEquivLike` `homIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Limits.Trident.ι`	—	—
`homIso_natural` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `DFunLike.coe` `Equiv` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `EquivLike.toFunLike` `Equiv.instEquivLike` `homIso` `CategoryTheory.CategoryStruct.comp`	—	`CategoryTheory.Category.assoc`
`homIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homIso` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily.zero` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Limits.Trident.ι` `lift'`	—	—
`hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelFamily.zero` `CategoryTheory.Limits.Trident.ι`	—	—	`CategoryTheory.Limits.IsLimit.hom_ext` `CategoryTheory.Limits.Trident.equalizer_ext`

CategoryTheory.Limits.WalkingParallelFamily

Definitions

Name	Category	Theorems
`arrowEquiv` 📖	CompOp	—
`category` 📖	CompOp	43 math math: `CategoryTheory.Limits.Trident.condition_assoc`, `CategoryTheory.Limits.parallelFamily_obj_zero`, `CategoryTheory.Limits.Cotrident.ofCocone_ι`, `CategoryTheory.Limits.Trident.app_zero`, `CategoryTheory.Limits.Cone.ofTrident_π`, `CategoryTheory.Limits.mono_of_isLimit_parallelFamily`, `CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app`, `CategoryTheory.Limits.diagramIsoParallelFamily_inv_app`, `CategoryTheory.Limits.Cocone.ofCotrident_ι`, `CategoryTheory.Limits.Cotrident.π_eq_app_one`, `CategoryTheory.Limits.Trident.ofι_pt`, `CategoryTheory.Limits.Cotrident.IsColimit.homIso_natural`, `CategoryTheory.Limits.Trident.condition`, `CategoryTheory.Limits.Cotrident.ofπ_pt`, `CategoryTheory.Limits.Cotrident.condition_assoc`, `CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app`, `CategoryTheory.hasCardinalLT_arrow_walkingParallelFamily`, `CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_functor_map`, `CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app`, `CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_inverse_obj`, `CategoryTheory.Limits.parallelFamily_obj_one`, `CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_inverse_map`, `CategoryTheory.Limits.Trident.IsLimit.homIso_apply_coe`, `CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app`, `CategoryTheory.Limits.Cotrident.IsColimit.homIso_symm_apply`, `CategoryTheory.Limits.Trident.ofCone_π`, `hom_id`, `CategoryTheory.Limits.Trident.ofι_π_app`, `CategoryTheory.Limits.diagramIsoParallelFamily_hom_app`, `CategoryTheory.Limits.Trident.ι_eq_app_zero`, `CategoryTheory.Limits.Cotrident.app_one`, `CategoryTheory.Limits.Trident.IsLimit.homIso_symm_apply`, `CategoryTheory.Limits.wideCoequalizer.cotrident_ι_app_one`, `CategoryTheory.Limits.Cotrident.condition`, `CategoryTheory.Limits.epi_of_isColimit_parallelFamily`, `CategoryTheory.Limits.Trident.app_zero_assoc`, `CategoryTheory.Limits.Cotrident.ofπ_ι_app`, `CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_functor_obj`, `CategoryTheory.Limits.Cotrident.app_one_assoc`, `CategoryTheory.Limits.wideEqualizer.trident_π_app_zero`, `CategoryTheory.Limits.parallelFamily_map_left`, `CategoryTheory.Limits.Trident.IsLimit.homIso_natural`, `CategoryTheory.Limits.Cotrident.IsColimit.homIso_apply_coe`
`instDecidableEqHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_id` 📖	mathematical	—	`Hom.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Category.toCategoryStruct` `category`	—	—

CategoryTheory.Limits.WalkingParallelFamily.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	—

CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

CategoryTheory.Limits.instInhabitedWalkingParallelFamily

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

CategoryTheory.Limits.wideCoequalizer

Definitions

Name	Category	Theorems
`cotrident` 📖	CompOp	2 math math: `cotrident_π`, `cotrident_ι_app_one`
`desc` 📖	CompOp	2 math math: `π_desc_assoc`, `π_desc`
`desc'` 📖	CompOp	—
`π` 📖	CompOp	8 math math: `π_epi`, `condition`, `cotrident_π`, `condition_assoc`, `π_desc_assoc`, `π_desc`, `hom_ext_iff`, `cotrident_ι_app_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`condition` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.wideCoequalizer` `π`	—	`CategoryTheory.Limits.Cotrident.condition`
`condition_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.wideCoequalizer` `π`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `condition`
`cotrident_ι_app_one` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Limits.parallelFamily` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `cotrident` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Limits.WalkingParallelFamily.one` `π`	—	—
`cotrident_π` 📖	mathematical	—	`CategoryTheory.Limits.Cotrident.π` `cotrident` `π`	—	—
`hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.wideCoequalizer` `π`	—	—	`CategoryTheory.Limits.Cotrident.IsColimit.hom_ext`
`hom_ext_iff` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.wideCoequalizer` `π`	—	`hom_ext`
`π_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Limits.wideCoequalizer` `π` `desc`	—	`CategoryTheory.Limits.colimit.ι_desc`
`π_desc_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Limits.wideCoequalizer` `π` `desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `π_desc`
`π_epi` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Limits.wideCoequalizer` `π`	—	`hom_ext`

CategoryTheory.Limits.wideEqualizer

Definitions

Name	Category	Theorems
`lift'` 📖	CompOp	—
`trident` 📖	CompOp	2 math math: `trident_ι`, `trident_π_app_zero`
`ι` 📖	CompOp	8 math math: `condition_assoc`, `lift_ι_assoc`, `trident_ι`, `ι_mono`, `lift_ι`, `trident_π_app_zero`, `hom_ext_iff`, `condition`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`condition` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.wideEqualizer` `ι`	—	`CategoryTheory.Limits.Trident.condition`
`condition_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.wideEqualizer` `ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `condition`
`hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.wideEqualizer` `ι`	—	—	`CategoryTheory.Limits.Trident.IsLimit.hom_ext`
`hom_ext_iff` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.wideEqualizer` `ι`	—	`hom_ext`
`lift_ι` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Limits.wideEqualizer` `lift` `ι`	—	`CategoryTheory.Limits.limit.lift_π`
`lift_ι_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Limits.wideEqualizer` `lift` `ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_ι`
`trident_ι` 📖	mathematical	—	`CategoryTheory.Limits.Trident.ι` `trident` `ι`	—	—
`trident_π_app_zero` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelFamily` `CategoryTheory.Limits.WalkingParallelFamily.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.parallelFamily` `trident` `CategoryTheory.Limits.Cone.π` `CategoryTheory.Limits.WalkingParallelFamily.zero` `ι`	—	—
`ι_mono` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Limits.wideEqualizer` `ι`	—	`hom_ext`

---

← Back to Index