germ_stalkSpecializes — Mathlib

English

The reflexivity of specialization at any point x: the specialization from x to itself yields identity on the stalk.

Русский

Рефлексивность специализации в точке x: специализация от x к x даёт тождественный отображение на стэле.

LaTeX

$$stalkSpecializes (specializes_refl x) = 𝟙 _$$

Lean4

@[reassoc (attr := simp), elementwise nosimp]
theorem germ_stalkSpecializes (F : X.Presheaf C) {U : Opens X} {y : X} (hy : y ∈ U) {x : X} (h : x ⤳ y) :
    F.germ U y hy ≫ F.stalkSpecializes h = F.germ U x (h.mem_open U.isOpen hy) :=
  colimit.ι_desc _ _

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