English
There is a natural isomorphism between the structure presheaf valued in commutative rings and the Type-valued structure presheaf, compatible with forgetting the ring structure.
Русский
Существует естественное изоморфизм между структурной пресшевой над кольцами и структурной пресшевой над типами, согласованный со стиранием кольцевой структуры.
LaTeX
$$$structurePresheafInCommRing \\; R \\;\u2192\\; forget\\, CommRingCat \\cong (structureSheafInType R).1$$$
Lean4
/-- The predicate saying that a dependent function on an open `U` is realised as a fixed fraction
`r / s` in each of the stalks (which are localizations at various prime ideals).
-/
def IsFraction {U : Opens (PrimeSpectrum.Top R)} (f : ∀ x : U, Localizations R x) : Prop :=
∃ r s : R, ∀ x : U, s ∉ x.1.asIdeal ∧ f x * algebraMap _ _ s = algebraMap _ _ r
