Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.WalkingCospan

Type

The type of objects for the diagram indexing a pullback, defined as a special case of WidePullbackShape.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Cited by
496 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 4 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Limits.cospan · cited by 467Limits.cospanCategoryTheory.Limits.HasPullbacks · cited by 439Limits.HasPullbacksCategoryTheory.Limits.PullbackCone.mk · cited by 203PullbackCone.mkCategoryTheory.Limits.WalkingCospan.left · cited by 190WalkingCospan.leftCategoryTheory.Limits.WalkingCospan.right · cited by 182WalkingCospan.rightCategoryTheory.Limits.PullbackCone.mk_π_app · cited by 120PullbackCone.mk_π_appCategoryTheory.Limits.PullbackCone.fst · cited by 118PullbackCone.fstCategoryTheory.Limits.PullbackCone.snd · cited by 113PullbackCone.sndCategoryTheory.IsPullback.isLimit · cited by 47IsPullback.isLimitCategoryTheory.Limits.PullbackCone.condition · cited by 44PullbackCone.conditionCategoryTheory.Limits.WalkingCospan.one · cited by 31WalkingCospan.oneCategoryTheory.Limits.WalkingCospan.Hom.inl · cited by 24Hom.inlCategoryTheory.Limits.pullback.isLimit · cited by 24pullback.isLimitCategoryTheory.GlueData.mapGlueData · cited by 24GlueData.mapGlueDataCategoryTheory.Limits.WalkingCospan.Hom.inr · cited by 23Hom.inrCategoryTheory.Limits.WalkingPair · cited by 1319Limits.WalkingPairCategoryTheory.Limits.WidePullbackShape · cited by 94Limits.WidePullbackShapeLimits.WalkingCospanCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by685

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 685.