locallyRingedSpaceObj_presheaf_map'

English

The map on presheaves induced by the Spec construction aligns with the map on the standard structure sheaf.

Русский

Отображение на presheaf, индуцируемое конструктором Spec, совпадает с отображением на стандартной структуре sheaf.

LaTeX

$$$(Spec.locallyRingedSpaceObj R).presheaf.map = (structureSheaf R).1.map$$$

Lean4

theorem locallyRingedSpaceObj_presheaf_map' (R : Type u) [CommRing R] {U V} (i : U ⟶ V) :
    (Spec.locallyRingedSpaceObj <| CommRingCat.of R).presheaf.map i = (structureSheaf R).1.map i :=
  rfl

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