smoothSheafRing — Mathlib

English

For smooth functions from M to R with R a smooth commutative ring, the presheaf is a presheaf of commutative rings.

Русский

Для гладких функций из M в R, R — гладкое коммутативное кольцо, прешеф является прешефом коммутативных колец.

LaTeX

$$smoothPresheafCommRing IM I M R$$

Lean4

/-- The sheaf of smooth functions from `M` to `R`, for `R` a smooth ring, as a sheaf of
rings. -/
def smoothSheafRing : TopCat.Sheaf RingCat.{u} (TopCat.of M) :=
  { val := smoothPresheafRing IM I M R
    cond := by
      rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _ (CategoryTheory.forget RingCat)]
      exact CategoryTheory.Sheaf.cond (smoothSheaf IM I M R) }

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