restrict_presheaf_map — Mathlib

English

The restriction of the presheaf along an open embedding h respects composition: the restricted presheaf map equals the composition of the global presheaf map with the adjunction counit.

Русский

Ограничение прешефа вдоль открытого отображения сохраняет композицию: отображение прешефа ограниченного пространства равно композиции общего прешефа с суточением адъункции.

LaTeX

$$$$ (X.restrict h).presheaf.map i = X.presheaf.map (homOfLE (\dots)).op $$$$

Lean4

@[simp]
theorem restrict_presheaf_map (V W) (i : V ⟶ W) :
    (X.restrict h).presheaf.map i =
      X.presheaf.map
        (homOfLE (show X.ofRestrict h ''ᵁ W.unop ≤ X.ofRestrict h ''ᵁ V.unop from Set.image_mono i.unop.le)).op :=
  rfl

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