map_appLE — Mathlib

English

The map on appLE induced by a refinement i: U' ≤ U expresses the compatibility of the appLE maps with Open maps, i.e., a refinement commutes with appLE.

Русский

Карта на appLE, индуцированная сужением i: U' ≤ U, выражает совместимость appLE с отображениями между открытыми подмножествами: уточнение коммутирует с appLE.

LaTeX

$$$\forall i:\, U'\le U,\; f.appLE U V e \circ X.presheaf.map i = f.appLE U' V (i.unop.le.trans e)$$$

Lean4

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

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