sheafYonedaHom

Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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

Lean4

/-- (Implementation). `sheafCoyonedaHom` but the order of the arguments of the functor are swapped.
-/
noncomputable def sheafYonedaHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) : ℱ ⋙ yoneda ⟶ ℱ'.val ⋙ yoneda
    where
  app
    U :=
    let α := (sheafCoyonedaHom α)
    { app := fun X => (α.app X).app U
      naturality := fun X Y f => by simpa using congr_app (α.naturality f) U }
  naturality U V
    i := by
    ext X x
    exact congr_fun (((sheafCoyonedaHom α).app X).naturality i) x

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

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

Разделы

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

Аффилиация

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