Theorems · Definition · category theory

CategoryTheory.Limits.widePullback

{J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (B : C) →
        (objs : J → C) → (arrows : (j : J) → objs j ⟶ B) → [CategoryTheory.Limits.HasWidePullback B objs arrows] → C

A choice of wide pullback.

Defined in: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Cited by: 31 results in Mathlib
Foundations: Depth 17 from the axioms · uses Classical.choice
Assumes: CategoryTheory.Category CategoryTheory.Limits.HasWidePullback

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.limitproof · cited by 346
CategoryTheory.Limits.HasWidePullbackstatement and proof · cited by 44
CategoryTheory.Limits.WidePullbackShape.wideCospanproof · cited by 22

Cited by35

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.WidePullback.πstatement · cited by 28
CategoryTheory.Limits.WidePullback.basestatement · cited by 20
CategoryTheory.Arrow.cechNerveproof · cited by 18
CategoryTheory.Limits.WidePullback.liftstatement · cited by 12
CategoryTheory.Limits.WidePullback.lift_basestatement · cited by 2
CategoryTheory.Limits.WidePullback.π_arrowstatement · cited by 2
CategoryTheory.Limits.WidePullback.lift_πstatement · cited by 1
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_basestatement · cited by 1
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0statement · cited by 1
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succstatement · cited by 1
CategoryTheory.Limits.Concrete.widePullback_extstatement and proof · cited by 1
CategoryTheory.Limits.WidePullback.hom_extstatement and proof · cited by 1