imageSieve

Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.imageSieve

Lean4

/-- For a functor `G : C ⥤ D`, and a morphism `f : G.obj U ⟶ G.obj V`,
`Functor.imageSieve G f` is the sieve of `U`
consisting of those arrows whose composition with `f` has a lift in `G`.

This is the image sieve of `f` under `yonedaMap G V` and hence the name.
See `Functor.imageSieve_eq_imageSieve`.
-/
def imageSieve {U V : C} (f : G.obj U ⟶ G.obj V) : Sieve U
    where
  arrows _ i := ∃ l, G.map l = G.map i ≫ f
  downward_closed := by
    rintro Y₁ Y₂ i₁ ⟨l, hl⟩ i₂
    exact ⟨i₂ ≫ l, by simp [hl]⟩

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

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

Разделы

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

Аффилиация

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