English
Variant of germ_res using op V ⟶ op U; expresses how F.map interacts with germs across restriction maps.
Русский
Вариант germ_res с использованием отображения op V ⟶ op U; описывает как F.map взаимодействует с гермами через ограничение.
LaTeX
$$$F.map i ≫ F.germ U x hx = F.germ V x (i.unop.le hx)$$$
Lean4
/-- A variant of `germ_res` with `op V ⟶ op U`
so that the LHS is more general and simp fires more easier. -/
@[reassoc (attr := simp)]
theorem germ_res' (F : X.Presheaf C) {U V : Opens X} (i : op V ⟶ op U) (x : X) (hx : x ∈ U) :
F.map i ≫ F.germ U x hx = F.germ V x (i.unop.le hx) :=
let i' : (⟨U, hx⟩ : OpenNhds x) ⟶ ⟨V, i.unop.le hx⟩ := i.unop
colimit.w ((OpenNhds.inclusion x).op ⋙ F) i'.op
