equalizerSieve

Mathlib.CategoryTheory.Sites.LocallyInjective

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presheaf.equalizerSieve

Lean4

/-- If `F : Cᵒᵖ ⥤ D` is a presheaf with values in a concrete category, if `x` and `y` are
elements in `F.obj X`, this is the sieve of `X.unop` consisting of morphisms `f`
such that `F.map f.op x = F.map f.op y`. -/
@[simps]
def equalizerSieve {F : Cᵒᵖ ⥤ D} {X : Cᵒᵖ} (x y : ToType (F.obj X)) : Sieve X.unop
    where
  arrows _ f := F.map f.op x = F.map f.op y
  downward_closed {X Y} f hf
    g := by
    dsimp at hf ⊢
    simp [hf]

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

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

Разделы

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

Аффилиация

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