English
Let A be a graded ring with grading 𝒜, X a scheme, and f: A →+* Γ(X, O_X) a ring homomorphism whose image of the irrelevant ideal (under the grading 𝒜) generates the whole ring. Then there exists a canonical morphism X → Proj 𝒜 over R, i.e., a morphism from X to the projective spectrum of the graded algebra 𝒜.
Русский
Пусть A — градуированная кольцо с градациями 𝒜, X — схема, и f: A →+* Γ(X, O_X) такая, что образ нерелевантного идеала под f порождает всё кольцо. Тогда существует канонический морфизм X → Proj 𝒜, то есть отображение X в проективный спектр градации 𝒜.
LaTeX
$$$\text{Let }A\text{ be a graded ring with grading }\mathcal{A}\text{ and }X\text{ a scheme. If }f:A\to\Gamma(X,\mathcal{O}_X)\text{ is a ring homomorphism with }(\mathrm{HomogeneousIdeal}.\mathrm{irrelevant}\;\mathcal{A})^\sim\!\to\!\top\text{ mapped by }f\text{ onto }\top,\text{ then there exists a morphism }X\to\mathrm{Proj}_{\mathcal{A}}.$$$
Lean4
/-- Given a graded ring `A` and a map `f : A →+* Γ(X, ⊤)` such that the image of the
irrelevant ideal under `f` generates the whole ring, we can construct a map `X ⟶ Proj 𝒜`. -/
def fromOfGlobalSections : X ⟶ Proj 𝒜 :=
by
refine
(openCoverOfMapIrrelevantEqTop 𝒜 f hf).glueMorphisms
(fun ri ↦ toBasicOpenOfGlobalSections 𝒜 f rfl ri.2.2.1 ri.2.2.2 ≫ Scheme.Opens.ι _) ?_
rintro x y
let e :
pullback ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≅
(X.basicOpen (f (x.snd.fst * y.snd.fst))) :=
(isPullback_opens_inf _ _).isoPullback.symm ≪≫ X.isoOfEq (by simp)
rw [← cancel_epi e.inv]
trans
toBasicOpenOfGlobalSections 𝒜 f rfl (Nat.add_pos_left x.2.2.1 y.1) (SetLike.mul_mem_graded x.2.2.2 y.2.2.2) ≫
(Scheme.Opens.ι _)
·
simpa [e, openCoverOfMapIrrelevantEqTop, Scheme.isoOfEq_inv] using
homOfLE_toBasicOpenOfGlobalSections_ι _ _ rfl rfl y.2.2.2
·
simpa [e, openCoverOfMapIrrelevantEqTop, Scheme.isoOfEq_inv] using
(homOfLE_toBasicOpenOfGlobalSections_ι _ _ (mul_comm _ _) (add_comm _ _) x.2.2.2).symm
