Theorems · Theorem · category theory

CategoryTheory.Functor.relativelyRepresentable.map

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full] [CategoryTheory.Limits.HasPullbacks C] {a b : C} (f : a ⟶ b)
  [∀ (c : C) (g : c ⟶ b), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F],
  F.relativelyRepresentable (F.map f)

When C has pullbacks, then F.map f is representable with respect to F for any f : a ⟶ b in C.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Representable

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.FullCategoryTheory.Limits.HasPullbacksCategoryTheory.Limits.PreservesLimit