SplitCoequalizer

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

Statistics

Metric	Count
Definitions IsSplitPair, HasSplitCoequalizer, coequalizerOfSplit, coequalizerπ, isSplitCoequalizer, IsSplitCoequalizer, asCofork, isCoequalizer, leftSection, map, rightSection, instInhabitedIsSplitCoequalizerId	12
Theorems splittable, asCofork_pt, asCofork_π, condition, condition_assoc, leftSection_bottom, leftSection_bottom_assoc, leftSection_top, leftSection_top_assoc, map_leftSection, map_rightSection, rightSection_π, rightSection_π_assoc, hasCoequalizer_of_hasSplitCoequalizer, map_is_split_pair	15
Total	27

CategoryTheory

Definitions

Name	Category	Theorems
HasSplitCoequalizer 📖	CompData	1 math math: map_is_split_pair
IsSplitCoequalizer 📖	CompData	1 math math: HasSplitCoequalizer.splittable
instInhabitedIsSplitCoequalizerId 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_is_split_pair 📖	mathematical	—	HasSplitCoequalizer Functor.obj Functor.map	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsSplitPair 📖	MathDef	1 math math: CategoryTheory.Monad.MonadicityInternal.main_pair_G_split

CategoryTheory.HasSplitCoequalizer

Definitions

Name	Category	Theorems
coequalizerOfSplit 📖	CompOp	—
coequalizerπ 📖	CompOp	—
isSplitCoequalizer 📖	CompOp	—

Theorems

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

CategoryTheory.IsSplitCoequalizer

Definitions

Name	Category	Theorems
asCofork 📖	CompOp	2 math math: asCofork_pt, asCofork_π
isCoequalizer 📖	CompOp	—
leftSection 📖	CompOp	5 math math: leftSection_bottom_assoc, leftSection_top, leftSection_bottom, leftSection_top_assoc, map_leftSection
map 📖	CompOp	2 math math: map_leftSection, map_rightSection
rightSection 📖	CompOp	5 math math: leftSection_top, leftSection_top_assoc, rightSection_π, rightSection_π_assoc, map_rightSection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asCofork_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair asCofork	—	—
asCofork_π 📖	mathematical	—	CategoryTheory.Limits.Cofork.π asCofork	—	—
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
leftSection_bottom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftSection CategoryTheory.CategoryStruct.id	—	—
leftSection_bottom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftSection	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' leftSection_bottom
leftSection_top 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftSection rightSection	—	—
leftSection_top_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftSection rightSection	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftSection_top
map_leftSection 📖	mathematical	—	leftSection CategoryTheory.Functor.obj CategoryTheory.Functor.map map	—	—
map_rightSection 📖	mathematical	—	rightSection CategoryTheory.Functor.obj CategoryTheory.Functor.map map	—	—
rightSection_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightSection CategoryTheory.CategoryStruct.id	—	—
rightSection_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightSection	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' rightSection_π

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCoequalizer_of_hasSplitCoequalizer 📖	mathematical	—	HasCoequalizer	—	—

---

← Back to Index