forgetStalk_hom_comp_evalHom — Mathlib

English

If R is a nontrivial ring, then every stalk of the smooth ring sheaf is nontrivial as a ring; there exist nonzero germs.

Русский

Если R ненулевое кольцо, то каждый stalk гладкого пучка колец ненулевой; существуют ненулевые жёрмы.

LaTeX

$$$$ \\text{If } R \\neq 0 \\text{, then } (\\mathcal{O}_x) \\neq 0 \\text{ for all } x.$$$$

Lean4

@[simp, reassoc, elementwise]
theorem forgetStalk_hom_comp_evalHom (x : TopCat.of M) :
    (smoothSheafCommRing.forgetStalk IM I M R x).hom ≫ (smoothSheaf.evalHom IM I R x) =
      ⇑(smoothSheafCommRing.evalHom _ _ _ _ _) :=
  by
  simp_rw [← CategoryTheory.Iso.eq_inv_comp]
  rw [← smoothSheafCommRing.forgetStalk_inv_comp_eval]

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