Theorems · Definition · category theory

CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj

{X Y S : Type v} →
  {f : X ⟶ S} →
    {g : Y ⟶ S} →
      {c : CategoryTheory.Limits.PullbackCone f g} →
        CategoryTheory.Limits.IsLimit c → c.pt ≃ CategoryTheory.Limits.Types.PullbackObj f g

A limit pullback cone in the category of types identifies to the explicit pullback.

Defined in: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Cited by: 7 results in Mathlib
Foundations: Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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

Quiver.Homstatement and proof · cited by 32,603
Equivstatement · cited by 8,337
CategoryTheory.Limits.WalkingPairstatement · cited by 1,319
CategoryTheory.Limits.Cone.ptstatement · cited by 1,298
CategoryTheory.Limits.IsLimitstatement and proof · cited by 664
CategoryTheory.Limits.WalkingCospanstatement · cited by 496
CategoryTheory.Limits.cospanstatement · cited by 467
CategoryTheory.Limits.PullbackConestatement and proof · cited by 136
CategoryTheory.Limits.LimitCone.isLimitproof · cited by 58
CategoryTheory.Limits.IsLimit.conePointUniqueUpToIsoproof · cited by 57
CategoryTheory.Iso.toEquivproof · cited by 32
CategoryTheory.Limits.Types.PullbackObjstatement · cited by 17

Cited by9

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.Types.pullbackIsoPullbackproof · cited by 12
CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fststatement and proof · cited by 3
CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_sndstatement and proof · cited by 3
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.glueproof · cited by 2
CategoryTheory.Limits.Types.exists_of_isPullbackproof · cited by 2
CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_fststatement · cited by 2
CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_sndstatement · cited by 2
CategoryTheory.Limits.PullbackCone.IsLimit.type_extproof · cited by 0
TypeCat.isTrans_of_transitiveRelationproof · cited by 0