Theorems · Definition · category theory

CategoryTheory.Functor.relativelyRepresentable

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → CategoryTheory.MorphismProperty D

A morphism f : X ⟶ Y in D is said to be relatively representable if for any g : F.obj a ⟶ Y, there exists a pullback square of the following form `` F.obj b --F.map snd--> F.obj a | | fst g | | v v X - f --> Y ``

Defined in

Mathlib.CategoryTheory.MorphismProperty.Representable

Cited by

64 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category