pullbackPushforwardAdjunction — Mathlib

English

Similar to above: the composition SheafOfModules.toSheaf R ⋙ Presheaf preserves finite limits.

Русский

Аналогично: композиция SheafOfModules.toSheaf R ⋙ Presheaf сохраняет конечные пределы.

LaTeX

$$$\operatorname{PreservesFiniteLimits}\big(\mathrm{SheafToPresheaf}\big)$$$

Lean4

/-- Given a continuous functor between sites `F`, and a morphism of sheaves of rings
`S ⟶ (F.sheafPushforwardContinuous RingCat.{u} J K).obj R`, this is the adjunction
between the corresponding pullback and pushforward functors on the categories
of sheaves of modules. -/
noncomputable def pullbackPushforwardAdjunction : pullback.{v} φ ⊣ pushforward.{v} φ :=
  Adjunction.ofIsRightAdjoint (pushforward φ)

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