Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.WalkingCospan.left

CategoryTheory.Limits.WalkingCospan

The left point of the walking cospan.

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

Around this declaration

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

CategoryTheory.Limits.pullback.fst · cited by 639pullback.fstCategoryTheory.Limits.PullbackCone.fst · cited by 118PullbackCone.fstCategoryTheory.Limits.pullback.lift_fst · cited by 40pullback.lift_fstCategoryTheory.Limits.WalkingCospan.Hom.inl · cited by 24Hom.inlCategoryTheory.Limits.pullbackSymmetry_hom_comp_fst · cited by 18Limits.pullbackSymmetry_h…CategoryTheory.Limits.diagramIsoCospan · cited by 17Limits.diagramIsoCospanCategoryTheory.Limits.pullbackSymmetry_hom_comp_snd · cited by 13Limits.pullbackSymmetry_h…CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst · cited by 12IsLimit.lift_fstCategoryTheory.IsPullback.isoPullback_hom_fst · cited by 10IsPullback.isoPullback_ho…CategoryTheory.Limits.PreservesPullback.iso_hom_fst · cited by 7PreservesPullback.iso_hom…CategoryTheory.Limits.pullback.congrHom_inv · cited by 7pullback.congrHom_invAlgebraicGeometry.pullbackSpecIso_inv_fst · cited by 7AlgebraicGeometry.pullbac…CategoryTheory.Limits.weakPullback.fst · cited by 6weakPullback.fstCategoryTheory.Limits.pullbackAssoc_inv_fst_fst · cited by 6Limits.pullbackAssoc_inv_…CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst · cited by 5Limits.pullbackRightPullb…CategoryTheory.Limits.WalkingCospan · cited by 496Limits.WalkingCospanWalkingCospan.leftCITED BYCITES

Cites1

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

Cited by206

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 206.