presheaf

Mathlib.CategoryTheory.MorphismProperty.Representable

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.presheaf

Lean4

/-- Given a morphism property `P` in a category `C`, a morphism `f : F ⟶ G` of presheaves in the
category `Cᵒᵖ ⥤ Type v` satisfies the morphism property `P.presheaf` iff:
* The morphism is representable.
* For any morphism `g : F.obj a ⟶ G`, the property `P` holds for any represented pullback of
  `f` by `g`.
This is implemented as a special case of the more general notion of `P.relative`, to the case when
the functor `F` is `yoneda`. -/
abbrev presheaf : MorphismProperty (Cᵒᵖ ⥤ Type v₁) :=
  P.relative yoneda

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru