Theorems · Theorem · category theory

CategoryTheory.Functor.relativelyRepresentable.of_diag

∀ {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] [CategoryTheory.Limits.HasPullbacks D]
  [inst_4 : CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {X : D},
  F.relativelyRepresentable (CategoryTheory.Limits.diag X) → ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g

Assume that 1. C has binary products, 2. D has pullbacks, binary products and a terminal object, and 3. F : C ⥤ D is full and preserves binary products. For an object X in a category D, if the diagonal morphism X ⟶ X × X is relatively representable, then every morphism of the form F.obj a ⟶ X is relatively representable with respect to F.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Representable

Cited by

1 results in Mathlib

Foundations

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

Assumes

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