mapPresheaf

Mathlib.Geometry.RingedSpace.PresheafedSpace

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

Lean4

/-- We can apply a functor `F : C ⥤ D` to the values of the presheaf in any `PresheafedSpace C`,
giving a functor `PresheafedSpace C ⥤ PresheafedSpace D` -/
def mapPresheaf (F : C ⥤ D) : PresheafedSpace C ⥤ PresheafedSpace D
    where
  obj
    X :=
    { carrier := X.carrier
      presheaf := X.presheaf ⋙ F }
  map
    f :=
    { base := f.base
      c := whiskerRight f.c F }
      -- Porting note: these proofs were automatic in mathlib3

  map_id X := by ext <;> cat_disch
  map_comp f g := by ext <;> cat_disch

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

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

Разделы

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

Аффилиация

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