Theorems · Definition · category theory

CategoryTheory.Functor.relativelyRepresentable.pullback

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {X Y : D} → {f : X ⟶ Y} → F.relativelyRepresentable f → {a : C} → (F.obj a ⟶ Y) → C

Let f : X ⟶ Y be a relatively representable morphism in D. Then, for any g : F.obj a ⟶ Y, hf.pullback g denotes the (choice of) a corresponding object in C such that there is a pullback square of the following form `` hf.pullback g --F.map snd--> F.obj a | | fst g | | v v X - f -> Y ``

Defined in

Mathlib.CategoryTheory.MorphismProperty.Representable

Cited by

65 results in Mathlib

Foundations

Depth 9 from the axioms · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.Category