Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.pullbackIsPullback

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.Limits.HasPullback f g] →
            CategoryTheory.Limits.IsLimit
              (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.fst f g)
                (CategoryTheory.Limits.pullback.snd f g) ⋯)

The pullback cone built from the pullback projections is a pullback.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Cited by
14 results in Mathlib
Foundations
Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.CategoryCategoryTheory.Limits.HasPullback
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.Limits.pullbackSymmetry · cited by 61Limits.pullbackSymmetryCategoryTheory.Limits.hasPullback_symmetry · cited by 22Limits.hasPullback_symmet…CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst · cited by 18Limits.pullbackSymmetry_h…CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd · cited by 13Limits.pullbackSymmetry_h…CategoryTheory.Limits.Types.pullbackIsoPullback · cited by 12Types.pullbackIsoPullbackCategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit · cited by 7Limits.isLimitOfHasPullba…limitConeOfTerminalAndPullbacks · cited by 6limitConeOfTerminalAndPul…CategoryTheory.Limits.hasPullback_of_preservesPullback · cited by 5Limits.hasPullback_of_pre…CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst · cited by 3Types.pullbackIsoPullback…CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd · cited by 3Types.pullbackIsoPullback…CategoryTheory.Limits.pullbackPullbackLeftIsPullback · cited by 3Limits.pullbackPullbackLe…CategoryTheory.Limits.pullbackPullbackRightIsPullback · cited by 3Limits.pullbackPullbackRi…CategoryTheory.regularTopology.EqualizerCondition.mk · cited by 2EqualizerCondition.mkCategoryTheory.JointlyReflectIsomorphisms.mono · cited by 1JointlyReflectIsomorphism…CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst · cited by 1Types.pullbackIsoPullback…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Limits.WalkingPair · cited by 1319Limits.WalkingPairCategoryTheory.Limits.pullback · cited by 864Limits.pullbackCategoryTheory.Limits.IsLimit · cited by 664Limits.IsLimitCategoryTheory.Limits.pullback.fst · cited by 639pullback.fstCategoryTheory.Limits.pullback.snd · cited by 637pullback.sndCategoryTheory.Limits.WalkingCospan · cited by 496Limits.WalkingCospanCategoryTheory.Limits.cospan · cited by 467Limits.cospanCategoryTheory.Limits.HasPullback · cited by 434Limits.HasPullbackCategoryTheory.Limits.PullbackCone.mk · cited by 203PullbackCone.mkCategoryTheory.Limits.pullback.condition · cited by 122pullback.conditionCategoryTheory.Limits.pullback.isLimit · cited by 24pullback.isLimitCategoryTheory.Limits.PullbackCone.mkSelfIsLimit · cited by 0PullbackCone.mkSelfIsLimitLimits.pullbackIsPullbackCITED BYCITES

Cites14

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

Cited by22

Results whose statement or proof uses this declaration.