id_hom_app

Mathlib.Topology.Sheaves.Presheaf

URI: https://scilib.ai/kg/mathlib#TopCat.Presheaf.Pushforward.id_hom_app

English

If f = g as morphisms, the pushforward along f equals the pushforward along g (on presheaves).

Русский

Если f = g как морфизмы, то pushforward по f равен pushforward по g (на пресшевах).

LaTeX

$$f = g → f_* F = g_* F$$

Lean4

@[simp]
theorem id_hom_app {X : TopCat.{w}} (ℱ : X.Presheaf C) (U) : (id ℱ).hom.app U = 𝟙 _ :=
  rfl

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

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

Разделы

Аффилиация

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