range

Mathlib.CategoryTheory.Subpresheaf.Image

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.range

Lean4

/-- The range of a morphism of presheaves of types, as a subpresheaf of the target. -/
@[simps]
def range (p : F' ⟶ F) : Subpresheaf F where
  obj U := Set.range (p.app U)
  map := by
    rintro U V i _ ⟨x, rfl⟩
    exact ⟨_, FunctorToTypes.naturality _ _ p i x⟩

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

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

Разделы

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

Аффилиация

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