Theorems · Definition · category theory

CategoryTheory.Limits.WidePullback.lift

{J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {B : C} →
        {objs : J → C} →
          {arrows : (j : J) → objs j ⟶ B} →
            [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] →
              {X : C} →
                (f : X ⟶ B) →
                  (fs : (j : J) → X ⟶ objs j) →
                    (∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) →
                      (X ⟶ CategoryTheory.Limits.widePullback B objs arrows)

Lift a collection of morphisms to a morphism to the pullback.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Cited by

12 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasWidePullback