generateFamily

Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

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

Lean4

/-- The sieve of morphisms which factor through a morphism in a given family.
This is equal to `Sieve.generate (Presieve.ofArrows X π)`, but has
more convenient definitional properties.
-/
def generateFamily {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) : Sieve B
    where
  arrows Y := {f | ∃ (a : α) (g : Y ⟶ X a), g ≫ π a = f}
  downward_closed := by
    rintro Y₁ Y₂ g₁ ⟨a, q, rfl⟩ e
    exact ⟨a, e ≫ q, by simp⟩

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

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

Разделы

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

Аффилиация

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