FactorsThruAlong

Mathlib.CategoryTheory.Sites.Coverage

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presieve.FactorsThruAlong

Lean4

/-- Given a morphism `f : Y ⟶ X`, a presieve `S` on `Y` and presieve `T` on `X`,
we say that *`S` factors through `T` along `f`*, written `S.FactorsThruAlong T f`,
provided that for any morphism `g : Z ⟶ Y` in `S`, there exists some
morphism `e : W ⟶ X` in `T` and some morphism `i : Z ⟶ W` such that the obvious
square commutes: `i ≫ e = g ≫ f`.

This is used in the definition of a coverage.
-/
def FactorsThruAlong {X Y : C} (S : Presieve Y) (T : Presieve X) (f : Y ⟶ X) : Prop :=
  ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄, S g → ∃ (W : C) (i : Z ⟶ W) (e : W ⟶ X), T e ∧ i ≫ e = g ≫ f

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

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

Разделы

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

Аффилиация

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