pushforward_eq'

Mathlib.Topology.Sheaves.Presheaf

URI: https://scilib.ai/kg/mathlib#TopCat.Presheaf.pushforward_eq'

English

If f = g, then the pushforward along f equals the pushforward along g for presheaves.

Русский

Если f = g, тогда pushforward по f = pushforward по g для пресшефов.

LaTeX

$$pushforward_eq' {X} {F} {f g} (h : f = g) : f_* F = g_* F$$

Lean4

theorem pushforward_eq' {X Y : TopCat.{w}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.Presheaf C) : f _* ℱ = g _* ℱ := by rw [h]

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

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

Разделы

Аффилиация

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