unit

Mathlib.Topology.Sheaves.Skyscraper

URI: https://scilib.ai/kg/mathlib#StalkSkyscraperPresheafAdjunctionAuxs.unit

Lean4

/-- The unit in `Presheaf.stalkFunctor ⊣ skyscraperPresheafFunctor`
-/
@[simps]
protected def unit : 𝟭 (Presheaf C X) ⟶ Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀
    where
  app _ := toSkyscraperPresheaf _ <| 𝟙 _
  naturality 𝓕 𝓖
    f := by
    ext U; dsimp
    split_ifs with h
    ·
      simp only [Category.id_comp, Category.assoc, eqToHom_trans_assoc, eqToHom_refl,
        Presheaf.stalkFunctor_map_germ_assoc, Presheaf.stalkFunctor_obj]
    · apply ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext

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

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

Разделы

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

Аффилиация

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