pullbackIso — Mathlib

English

There is an isomorphism describing pullback of sheaves of modules along a morphism of topologies.

Русский

Существует изоморфизм, описывающий вытягивание пучков модулей вдоль морфизма топологий.

LaTeX

$$$\mathrm{pullback}(\varphi) \cong \mathrm{forget}(S) \circ \mathrm{pullback}(\varphi_{\mathrm{val}}) \circ \mathrm{sheafification}(\mathrm{id})$$$

Lean4

/-- The pullback functor on sheaves of modules can be described as a composition
of the forget functor to presheaves, the pullback on presheaves of modules, and
the sheafification functor. -/
noncomputable def pullbackIso :
    pullback.{v} φ ≅ forget S ⋙ PresheafOfModules.pullback.{v} φ.val ⋙ PresheafOfModules.sheafification (𝟙 R.val) :=
  Adjunction.leftAdjointUniq (pullbackPushforwardAdjunction φ) (PullbackConstruction.adjunction φ)

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