sheafCompose

Mathlib.CategoryTheory.Sites.Whiskering

URI: https://scilib.ai/kg/mathlib#CategoryTheory.sheafCompose

Lean4

/-- Composing a functor which `HasSheafCompose`, yields a functor between sheaf categories. -/
@[simps]
def sheafCompose : Sheaf J A ⥤ Sheaf J B
    where
  obj G := ⟨G.val ⋙ F, GrothendieckTopology.HasSheafCompose.isSheaf G.val G.2⟩
  map η := ⟨whiskerRight η.val _⟩
  map_id _ := Sheaf.Hom.ext <| whiskerRight_id _
  map_comp _ _ := Sheaf.Hom.ext <| whiskerRight_comp _ _ _

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

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

Разделы

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

Аффилиация

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