res_apply — Mathlib

English

On the tilde construction, the restriction map of a section along an inclusion i: V ⟶ U is given by applying i to the base indices. In particular, the restriction respects the underlying fraction representation.

Русский

При построении tilde ограничение секции по включению i: V ⟶ U задаётся применением i к базовым индексам, и ограничение сохраняет дробовую декомпозицию.

LaTeX

$$$\forall i,\; (\tildeInModuleCat M).map i.op$ acts by restricting the index; i.e., the restriction map is given by the base evaluation at i.$$

Lean4

@[simp]
theorem res_apply (U V : Opens (PrimeSpectrum.Top R)) (i : V ⟶ U) (s : (tildeInModuleCat M).obj (op U)) (x : V) :
    ((tildeInModuleCat M).map i.op s).1 x = (s.1 (i x) :) :=
  rfl

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