presheaf

Mathlib.CategoryTheory.Subobject.Presheaf

URI: https://scilib.ai/kg/mathlib#Subobject.presheaf

Lean4

/-- This is the presheaf that sends every object `X : C` to its type of subobjects `Subobject X`,
and every morphism `f : X ⟶ Y` to the function `Subobject Y → Subobject X` that maps every
subobject of `Y` to its pullback along `f`. -/
@[simps]
noncomputable def presheaf : Cᵒᵖ ⥤ Type max u v
    where
  obj X := Subobject X.unop
  map f := (pullback f.unop).obj
  map_id _ := by ext : 1; simp [pullback_id]
  map_comp _ _ := by ext : 1; simp [pullback_comp]

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

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

Разделы

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

Аффилиация

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