Theorems · Theorem · category theory

CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C]
  [inst_3 : CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasBinaryProducts D]
  [inst_5 : CategoryTheory.Limits.HasTerminal D] [F.Full]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {X : D}
  {a : C} [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  (g :
    F.obj a ⟶
      CategoryTheory.Limits.pullback (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from X)),
  F.relativelyRepresentable
    (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id (F.obj a))
      (CategoryTheory.CategoryStruct.id (F.obj a)) ⋯)

Assume that 1. C has binary products and pullbacks, 2. D has pullbacks, binary products and a terminal object, and 3. F : C ⥤ D is full and preserves binary products and pullbacks. For a morphism g : F.obj a ⟶ pullback (terminal.from X) (terminal.from X), the canonical morphism from F.obj a to pullback ((g ≫ pullback.fst _ _) ≫ terminal.from X) ((g ≫ pullback.snd _ _) ≫ terminal.from X) is relatively representable with respect to F.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Representable

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasBinaryProductsCategoryTheory.Limits.HasPullbacksCategoryTheory.Limits.HasBinaryProductsCategoryTheory.Limits.HasTerminalCategoryTheory.Functor.FullCategoryTheory.Limits.PreservesLimitsOfShapeCategoryTheory.Limits.HasPullbacksCategoryTheory.Limits.PreservesLimitsOfShape