map_germ_eq_Γgerm — Mathlib

English

Relates the action of map on germs to the canonical Γgerm construction; maps commute with Γgerm.

Русский

Соотношение отображения на гермы и конструкция Γgerm; отображения коммутируют с Γgerm.

LaTeX

$$$F.map i.op ≫ F.germ U x hx = F.Γgerm x$$$

Lean4

@[reassoc]
theorem map_germ_eq_Γgerm (F : X.Presheaf C) {U : Opens X} {i : U ⟶ ⊤} (x : X) (hx : x ∈ U) :
    F.map i.op ≫ F.germ U x hx = F.Γgerm x :=
  germ_res F i x hx

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