appLE_map — Mathlib

English

The map appLE commutes with pushing forward along a morphism i between opens: applying i then appLE equals applying appLE then the induced map on the source presheaf.

Русский

Отображение appLE коммутирует с переносом вдоль отображения i между открытыми: применение i затем appLE эквивалентно применению appLE затем индуцированному отображению прешфейза источника.

LaTeX

$$$Y.presheaf.map i \circ f.appLE U V e = f.appLE U' V (i.unop.le.trans e)$$$

Lean4

@[reassoc (attr := simp)]
theorem appLE_map (e : V ≤ f ⁻¹ᵁ U) (i : op V ⟶ op V') :
    f.appLE U V e ≫ X.presheaf.map i = f.appLE U V' (i.unop.le.trans e) :=
  by
  rw [Hom.appLE, Category.assoc, ← Functor.map_comp]
  rfl

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