germ_skyscraperPresheafStalkOfSpecializes_hom

English

If two global germs s and t agree locally around every point of some supset, then s = t.

Русский

Если два глобальных герма-элемента s и t совпадают локально во всех точках, то они равны.

LaTeX

$$$$\forall x, (\text{germ public})_x(s) = (\text{germ public})_x(t) \Rightarrow s = t.$$$$

Lean4

@[reassoc (attr := simp)]
theorem germ_skyscraperPresheafStalkOfSpecializes_hom [HasColimits C] {y : X} (h : p₀ ⤳ y) (U hU) :
    (skyscraperPresheaf p₀ A).germ U y hU ≫ (skyscraperPresheafStalkOfSpecializes p₀ A h).hom =
      eqToHom (if_pos (h.mem_open U.2 hU)) :=
  colimit.isoColimitCocone_ι_hom _ _

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