Theorems · Definition · category theory

CategoryTheory.Limits.weakPullback

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

weakPullback f g computes the weak pullback of a pair of morphisms with the same target.

Defined in: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
Cited by: 8 results in Mathlib
Foundations: Depth 18 from the axioms · uses Classical.choice
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.

Cites5

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.HasWeakPullbackstatement and proof · cited by 8
CategoryTheory.Limits.weakLimitproof · cited by 7

Cited by15

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.weakPullback.fststatement · cited by 6
CategoryTheory.Limits.weakPullback.liftstatement · cited by 6
CategoryTheory.Limits.weakPullback.sndstatement · cited by 6
CategoryTheory.Limits.weakPullback.conditionstatement · cited by 1
CategoryTheory.Limits.weakPullback.lift_fststatement · cited by 1
CategoryTheory.Limits.weakPullback.lift_sndstatement · cited by 1
CategoryTheory.Limits.weakPullback.condition_assocstatement · cited by 0
CategoryTheory.Limits.weakPullback.exists_liftstatement · cited by 0
CategoryTheory.Limits.weakPullback.lift'statement · cited by 0
CategoryTheory.Limits.weakPullback.lift_fst_assocstatement · cited by 0
CategoryTheory.Limits.weakPullback.lift_snd_assocstatement · cited by 0
CategoryTheory.Limits.weakPullback.mapstatement · cited by 0