id_inv_app

Mathlib.Topology.Sheaves.Presheaf

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

English

Another form of equality of pushforwards given equality of morphisms.

Русский

Другая форма равенства pushforward при равенстве морфизмов.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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