map_app — Mathlib

English

On an open U, the map (Spec.map f).app U is the canonical induced ring map given by the StructureSheaf.

Русский

На открытом U отображение (Spec.map f).app U является канонически индуцированным кольцовым отображением через StructureSheaf.

LaTeX

$$$ (\mathrm{Spec.map} f).\mathrm{app} U = \mathrm{CommRingCat.ofHom} \big( \mathrm{StructureSheaf.comap} f.hom U (\mathrm{Spec.map} f^{-1}\!\! U) \big). $$$

Lean4

theorem map_app (U) : (Spec.map f).app U = CommRingCat.ofHom (StructureSheaf.comap f.hom U (Spec.map f ⁻¹ᵁ U) le_rfl) :=
  rfl

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