English
There is a canonical way to produce a section of the structure sheaf on the basic open D(f.den) from a fraction f.num/f.den of a suitable degree, giving a dependent section over that open set.
Русский
Существует канонический способ получить секцию структуры пучка на базовом открытом D(f.den) из дроби f.num/f.den заданной степени, образующей зависимую секцию над этим открытым множеством.
LaTeX
$$$\text{sectionInBasicOpen}_{\mathcal{A}}(x)(f) = \langle f.deg, f.num, f.den, x.2 \rangle$$$
Lean4
/-- Given a point `x` corresponding to a homogeneous prime ideal, there is a (dependent) function
such that, for any `f` in the homogeneous localization at `x`, it returns the obvious section in the
basic open set `D(f.den)`. -/
def sectionInBasicOpen (x : ProjectiveSpectrum.top 𝒜) :
∀ f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl,
(Proj.structureSheaf 𝒜).1.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f.den)) :=
fun f =>
⟨fun y => HomogeneousLocalization.mk ⟨f.deg, f.num, f.den, y.2⟩, fun y =>
⟨ProjectiveSpectrum.basicOpen 𝒜 f.den, y.2, ⟨𝟙 _, ⟨f.deg, ⟨f.num, f.den, _, fun _ => rfl⟩⟩⟩⟩⟩
