FactorsThru

Mathlib.CategoryTheory.Sites.Coverage

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

Lean4

/-- Given `S T : Presieve X`, we say that `S` factors through `T` if any morphism in `S`
factors through some morphism in `T`.

The lemma `Presieve.isSheafFor_of_factorsThru` gives a *sufficient* condition for a
presheaf to be a sheaf for a presieve `T`, in terms of `S.FactorsThru T`, provided
that the presheaf is a sheaf for `S`.
-/
def FactorsThru {X : C} (S T : Presieve X) : Prop :=
  ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄, S g → ∃ (W : C) (i : Z ⟶ W) (e : W ⟶ X), T e ∧ i ≫ e = g

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

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

Разделы

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

Аффилиация

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