generateSingleton

Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sieve.generateSingleton

Lean4

/-- The sieve of morphisms which factor through a given morphism `f`.
This is equal to `Sieve.generate (Presieve.singleton f)`, but has
more convenient definitional properties.
-/
def generateSingleton {X Y : C} (f : Y ⟶ X) : Sieve X
    where
  arrows Z := {g | ∃ (e : Z ⟶ Y), e ≫ f = g}
  downward_closed := by
    rintro W Z g ⟨e, rfl⟩ q
    exact ⟨q ≫ e, by simp⟩

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

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

Разделы

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

Аффилиация

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