English
Under finitary generation hypotheses, Proj instantiates a locally finite type morphism to SpecZero; more precisely, Proj instantiates a LocallyOfFiniteType object at SpecZero when the finite-type condition holds on the base piece 𝒜(0).
Русский
При конечном типе основания, Proj реализует отображение локального типа на SpecZero; формулировка: LocallyOfFiniteType при SpecZero, если 𝒜(0) имеет конечный тип.
LaTeX
$$$\mathrm{LocallyOfFiniteType}(\mathrm{Proj.toSpecZero}(\mathcal A))$ under finite type on 𝒜(0)$$
Lean4
instance [Algebra.FiniteType (𝒜 0) A] : LocallyOfFiniteType (Proj.toSpecZero 𝒜) :=
by
obtain ⟨x, hx, hx'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜
choose d hd hxd using hx'
rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := @LocallyOfFiniteType) _
(Proj.iSup_basicOpen_eq_top' 𝒜 (ι := x) (↑) (fun i ↦ ⟨_, hxd _ i.2⟩) (by simpa using hx))]
intro i
rw [←
MorphismProperty.cancel_left_of_respectsIso (P := @LocallyOfFiniteType)
(Proj.basicOpenIsoSpec 𝒜 i (hxd _ i.2) (hd _ i.2).bot_lt).inv,
← Category.assoc, ← Proj.awayι, Proj.awayι_toSpecZero, HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)]
exact HomogeneousLocalization.Away.finiteType _ _ (hxd _ i.2)
