eval_surjective — Mathlib

English

The forgetStalk isomorphism is compatible with the stalk forgetful functor, yielding a natural isomorphism of the corresponding stalks under forgetting the ring structure.

Русский

Изоморфизм forgetStalk совместим с забывающим функтором для stalk, образуя естественный изоморфизм соответствующих stalk после забывания кольцевой структуры.

LaTeX

$$$$ \\text{forgetStalk} : (\\mathcal{O}_x) \\cong (\\text{stalk of types})_x, \\; \\text{compat with forget}.$$$$

Lean4

theorem eval_surjective (x) : Function.Surjective (smoothSheafCommRing.eval IM I M R x) :=
  by
  intro r
  obtain ⟨y, rfl⟩ := smoothSheaf.eval_surjective IM I R x r
  use (smoothSheafCommRing.forgetStalk IM I M R x).inv y
  apply smoothSheafCommRing.forgetStalk_inv_comp_eval_apply

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