relative

Mathlib.CategoryTheory.MorphismProperty.Representable

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

Lean4

/-- Given a morphism property `P` in a category `C`, a functor `F : C ⥤ D` and a morphism
`f : X ⟶ Y` in `D`. Then `f` satisfies the morphism property `P.relative` with respect to `F` iff:
* The morphism is representable with respect to `F`
* For any morphism `g : F.obj a ⟶ Y`, the property `P` holds for any represented pullback of
  `f` by `g`. -/
def relative : MorphismProperty D := fun X Y f ↦
  F.relativelyRepresentable f ∧
    ∀ ⦃a b : C⦄ (g : F.obj a ⟶ Y) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd

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

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

Разделы

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

Аффилиация

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