germ_res_apply' — Mathlib

English

Variant of germ_res_apply for op V ⟶ op U; expresses how F.map interacts with germs across the opposite direction.

Русский

Вариант germ_res_apply для op V ⟶ op U; описывает взаимодействие F.map с гермами в противоположном направлении.

LaTeX

$$$F.germ U x hx (F.map i s) = F.germ V x (i.unop.le hx) s$$$

Lean4

theorem germ_res_apply' (F : X.Presheaf C) {U V : Opens X} (i : op V ⟶ op U) (x : X) (hx : x ∈ U)
    [ConcreteCategory C FC] (s) : F.germ U x hx (F.map i s) = F.germ V x (i.unop.le hx) s := by
  rw [← ConcreteCategory.comp_apply, germ_res']

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