Theorems · Theorem · category theory

CategoryTheory.Presieve.HasPairwisePullbacks.has_pullbacks

∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X : C} {R : CategoryTheory.Presieve X}
  [self : R.HasPairwisePullbacks] {Y Z : C} {f : Y ⟶ X},
  R f → ∀ {g : Z ⟶ X}, R g → CategoryTheory.Limits.HasPullback f g

For all arrows f and g in R, the pullback of f and g exists.

Defined in: Mathlib.CategoryTheory.Sites.Sieves
Cited by: 3 results in Mathlib
Foundations: Depth 18 from the axioms · uses no axioms
Assumes: CategoryTheory.Presieve.HasPairwisePullbacks

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 · cited by 32,603
CategoryTheory.Presievestatement and proof · cited by 449
CategoryTheory.Limits.HasPullbackstatement · cited by 434
CategoryTheory.Presieve.HasPairwisePullbacksstatement and proof · cited by 25

Cited by3

Results whose statement or proof uses this declaration.

CategoryTheory.Equalizer.Presieve.wproof · cited by 2
CategoryTheory.Presieve.HasPairwisePullbacks.map_of_preservesPairwisePullbacksproof · cited by 1
CategoryTheory.Presieve.pullbackCompatible_iffproof · cited by 1