SplitEqualizer

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

Statistics

Metric	Count
Definitions IsCosplitPair, HasSplitEqualizer, equalizerOfSplit, equalizerι, isSplitEqualizer, IsSplitEqualizer, asFork, isEqualizer, leftRetraction, map, rightRetraction, instInhabitedIsSplitEqualizerId	12
Theorems splittable, asFork_pt, asFork_ι, bottom_rightRetraction, bottom_rightRetraction_assoc, condition, condition_assoc, map_leftRetraction, map_rightRetraction, top_rightRetraction, top_rightRetraction_assoc, ι_leftRetraction, ι_leftRetraction_assoc, hasEqualizer_of_hasSplitEqualizer, map_is_cosplit_pair	15
Total	27

CategoryTheory

Definitions

Name	Category	Theorems
HasSplitEqualizer 📖	CompData	1 math math: map_is_cosplit_pair
IsSplitEqualizer 📖	CompData	1 math math: HasSplitEqualizer.splittable
instInhabitedIsSplitEqualizerId 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_is_cosplit_pair 📖	mathematical	—	HasSplitEqualizer Functor.obj Functor.map	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsCosplitPair 📖	MathDef	1 math math: CategoryTheory.Comonad.ComonadicityInternal.main_pair_F_cosplit

CategoryTheory.HasSplitEqualizer

Definitions

Name	Category	Theorems
equalizerOfSplit 📖	CompOp	—
equalizerι 📖	CompOp	—
isSplitEqualizer 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
splittable 📖	mathematical	—	CategoryTheory.IsSplitEqualizer	—	—

CategoryTheory.IsSplitEqualizer

Definitions

Name	Category	Theorems
asFork 📖	CompOp	2 math math: asFork_pt, asFork_ι
isEqualizer 📖	CompOp	—
leftRetraction 📖	CompOp	5 math math: ι_leftRetraction, top_rightRetraction, top_rightRetraction_assoc, map_leftRetraction, ι_leftRetraction_assoc
map 📖	CompOp	2 math math: map_rightRetraction, map_leftRetraction
rightRetraction 📖	CompOp	5 math math: bottom_rightRetraction, bottom_rightRetraction_assoc, top_rightRetraction, top_rightRetraction_assoc, map_rightRetraction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asFork_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair asFork	—	—
asFork_ι 📖	mathematical	—	CategoryTheory.Limits.Fork.ι asFork	—	—
bottom_rightRetraction 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightRetraction CategoryTheory.CategoryStruct.id	—	—
bottom_rightRetraction_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightRetraction	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' bottom_rightRetraction
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
map_leftRetraction 📖	mathematical	—	leftRetraction CategoryTheory.Functor.obj CategoryTheory.Functor.map map	—	—
map_rightRetraction 📖	mathematical	—	rightRetraction CategoryTheory.Functor.obj CategoryTheory.Functor.map map	—	—
top_rightRetraction 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightRetraction leftRetraction	—	—
top_rightRetraction_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightRetraction leftRetraction	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' top_rightRetraction
ι_leftRetraction 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftRetraction CategoryTheory.CategoryStruct.id	—	—
ι_leftRetraction_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftRetraction	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ι_leftRetraction

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasEqualizer_of_hasSplitEqualizer 📖	mathematical	—	HasEqualizer	—	—

---

← Back to Index