Multiequalizer

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Shapes/Multiequalizer.lean

Statistics

Metric	Count
Definitions isColimitMapEquiv, isColimitMapOfPreserves, map, map, multispanMapIso	5
Theorems map_pt, map_ι_app, map_fst, map_left, map_right, map_snd, multispanMapIso_hom_app, multispanMapIso_inv_app	8
Total	13

CategoryTheory.Limits.Multicofork

Definitions

Name	Category	Theorems
isColimitMapEquiv 📖	CompOp	—
isColimitMapOfPreserves 📖	CompOp	—
map 📖	CompOp	2 math math: map_pt, map_ι_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.MultispanIndex.map map CategoryTheory.Functor.obj	—	—
map_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.MultispanIndex.map CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.MultispanIndex.left CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.MultispanShape.fst CategoryTheory.Functor.map CategoryTheory.Limits.MultispanIndex.fst π	—	—

CategoryTheory.Limits.MultispanIndex

Definitions

Name	Category	Theorems
map 📖	CompOp	22 math math: SSet.horn₃₁.desc.multicofork_π_two, SSet.horn₃₂.desc.multicofork_π_one, map_fst, SSet.horn₃₁.desc.multicofork_pt, multispanMapIso_inv_app, SSet.horn₃₁.desc.multicofork_π_two_assoc, SSet.horn₃₁.desc.multicofork_π_zero_assoc, CategoryTheory.Limits.Multicofork.map_pt, map_snd, CategoryTheory.Limits.Multicofork.map_ι_app, map_left, SSet.horn₃₂.desc.multicofork_π_zero_assoc, multispanMapIso_hom_app, map_right, SSet.horn₃₁.desc.multicofork_π_three_assoc, SSet.horn₃₁.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three, SSet.horn₃₂.desc.multicofork_pt, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, SSet.horn₃₁.desc.multicofork_π_three
multispanMapIso 📖	CompOp	2 math math: multispanMapIso_inv_app, multispanMapIso_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_fst 📖	mathematical	—	fst map CategoryTheory.Functor.map left right CategoryTheory.Limits.MultispanShape.fst	—	—
map_left 📖	mathematical	—	left map CategoryTheory.Functor.obj	—	—
map_right 📖	mathematical	—	right map CategoryTheory.Functor.obj	—	—
map_snd 📖	mathematical	—	snd map CategoryTheory.Functor.map left right CategoryTheory.Limits.MultispanShape.snd	—	—
multispanMapIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory multispan map CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category multispanMapIso CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl left right	—	—
multispanMapIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Functor.comp multispan map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category multispanMapIso CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl left right	—	—

---

← Back to Index