presheafToTypes_map — Mathlib

English

If i: U ⟶ V is a morphism of opens (in the opposite category), then the restriction map of presheafToTypes X T is given by precomposition with i.unop, i.e., (presheafToTypes X T).map i f = f ∘ i.unop.

Русский

Если i: U ⟶ V — морфизм открытых множеств, то ограничение пресsheafToTypes есть предобразная композиция с i.unop: (presheafToTypes X T).map i f = f ∘ i.unop.

LaTeX

$$$(\\mathrm{presheafToTypes}\\ X\\ T).map\\ i\\ f = f \\circ i.unop$$$

Lean4

@[simp]
theorem presheafToTypes_map {T : X → Type*} {U V : (Opens X)ᵒᵖ} {i : U ⟶ V} {f} :
    (presheafToTypes X T).map i f = fun x => f (i.unop x) :=
  rfl

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