Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.WalkingCospan.one

CategoryTheory.Limits.WalkingCospan

The central point of the walking cospan.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Cited by
31 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.Limits.WalkingCospan.Hom.inl · cited by 24Hom.inlCategoryTheory.Limits.WalkingCospan.Hom.inr · cited by 23Hom.inrCategoryTheory.Limits.diagramIsoCospan · cited by 17Limits.diagramIsoCospanCategoryTheory.Limits.PullbackCone.equalizer_ext · cited by 5PullbackCone.equalizer_extCategoryTheory.Functor.regularEpiOfPreserves · cited by 5Functor.regularEpiOfPrese…CategoryTheory.Limits.cospanHomMk · cited by 4Limits.cospanHomMkCategoryTheory.Limits.cospanIsoMk · cited by 4Limits.cospanIsoMkCategoryTheory.Limits.PullbackCone.isoMk · cited by 4PullbackCone.isoMkCategoryTheory.compatiblePreservingOfFlat · cited by 3CategoryTheory.compatible…CategoryTheory.Limits.PullbackCone.condition_one · cited by 2PullbackCone.condition_oneCategoryTheory.Limits.Cone.ofPullbackCone · cited by 2Cone.ofPullbackConeCategoryTheory.Limits.diagramIsoCospan_hom_app · cited by 2Limits.diagramIsoCospan_h…CategoryTheory.Limits.PullbackCone.ofCone · cited by 2PullbackCone.ofConeCategoryTheory.IsPullback.of_isLimit_cone · cited by 1IsPullback.of_isLimit_coneCategoryTheory.Limits.cospanCompIso_app_one · cited by 0Limits.cospanCompIso_app_…CategoryTheory.Limits.WalkingCospan · cited by 496Limits.WalkingCospanWalkingCospan.oneCITED BYCITES

Cites1

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

Cited by41

Results whose statement or proof uses this declaration.