sections_property

Mathlib.Algebra.Category.ModuleCat.Presheaf

URI: https://scilib.ai/kg/mathlib#PresheafOfModules.sections_property

English

If s is a global section of a presheaf M and f: X ⟶ Y, then M.map f sends s(X) to s(Y).

Русский

Если s — глобальная секция прешефа M и f: X ⟶ Y, то M.map f отправляет s(X) в s(Y).

LaTeX

$$$ M.map f (s.1 X) = s.1 Y $$$

Lean4

@[simp]
theorem sections_property {M : PresheafOfModules.{v} R} (s : M.sections) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
    M.map f (s.1 X) = s.1 Y :=
  s.2 f

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

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

Разделы

Аффилиация

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