Theorems · Definition · category theory

CategoryTheory.Limits.weakPullback.snd

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) → [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] → CategoryTheory.Limits.weakPullback f g ⟶ Y

The second projection of the weak pullback of f and g.

Defined in: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
Cited by: 6 results in Mathlib
Foundations: Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Limits.HasWeakPullback

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites7

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

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Limits.cospanproof · cited by 467
CategoryTheory.Limits.WalkingCospan.rightproof · cited by 182
CategoryTheory.Limits.weakPullbackstatement · cited by 8
CategoryTheory.Limits.HasWeakPullbackstatement and proof · cited by 8
CategoryTheory.Limits.weakLimit.πproof · cited by 7

Cited by9

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.weakPullback.conditionstatement · cited by 1
CategoryTheory.Limits.weakPullback.lift_sndstatement · cited by 1
CategoryTheory.Limits.weakLimit.pullbackConeSnd_cone_cospanstatement · cited by 0
CategoryTheory.Limits.weakPullback.condition_assocstatement and proof · cited by 0
CategoryTheory.Limits.weakPullback.exists_liftstatement · cited by 0
CategoryTheory.Limits.weakPullback.lift'statement · cited by 0
CategoryTheory.Limits.weakPullback.lift_snd_assocstatement and proof · cited by 0
CategoryTheory.Limits.weakPullback.mapproof · cited by 0
CategoryTheory.Limits.weakPullbackIsWeakPullbackstatement · cited by 0