English
Let F be a presheaf on X. For any open U ⊆ X, any x ∈ U with hx witnessing x ∈ U, any morphism i: U → ⊤, and any s in the appropriate object, the germ at U of x applied to F.map i.op s equals the germ along x of s; i.e., F.germ U x hx (F.map i.op s) = F.Γgerm x s.
Русский
Пусть F — пресшеф над X. Для любого открытого множества U ⊆ X, для любого x ∈ U с доказательством hx, для любого морфизма i: U → ⊤ и любого элемента s в соответствующем объекте, зародок в точке U, применённый к F.map i.op s, равен зародку вдоль x применённому к s; то есть F.germ U x hx (F.map i.op s) = F.Γgerm x s.
LaTeX
$$$F.germ\ U\ x\ hx\ (F.map\ i.op\ s) = F.\Gamma g\erm\ x\ s$$$
Lean4
theorem Γgerm_res_apply (F : X.Presheaf C) {U : Opens X} {i : U ⟶ ⊤} (x : X) (hx : x ∈ U) [ConcreteCategory C FC] (s) :
F.germ U x hx (F.map i.op s) = F.Γgerm x s :=
F.germ_res_apply i x hx s
