English
The canonical map sending an element f∈R into the ring of sections over an open U equals the constant section with denominator 1 and numerator f.
Русский
Каноническое отображение элемента f∈R в кольцо секций над открытым множеством совпадает с константной секцией с знаменателем 1 и числителем f.
LaTeX
$$$ toOpen R U f = const R f 1 U (\\text{one_mem}) $$$
Lean4
/-- The canonical ring homomorphism interpreting an element of `R` as
a section of the structure sheaf. -/
def toOpen (U : Opens (PrimeSpectrum.Top R)) : CommRingCat.of R ⟶ (structureSheaf R).1.obj (op U) :=
CommRingCat.ofHom
{ toFun
f :=
⟨fun _ => algebraMap R _ f, fun x =>
⟨U, x.2, 𝟙 _, f, 1, fun y => ⟨(Ideal.ne_top_iff_one _).1 y.1.2.1, by simp [RingHom.map_one, mul_one]⟩⟩⟩
map_one' := Subtype.eq <| funext fun _ => RingHom.map_one _
map_mul' _ _ := Subtype.eq <| funext fun _ => RingHom.map_mul _ _ _
map_zero' := Subtype.eq <| funext fun _ => RingHom.map_zero _
map_add' _ _ := Subtype.eq <| funext fun _ => RingHom.map_add _ _ _ }
