Closed immersions into Proj and properness of the projective bundle of a module

• AlgebraicGeometry.Proj.isClosedImmersion_map_of_surjective: a surjective graded ring map F : A → B induces a closed immersion Proj B ⟶ Proj A [TSPA, Tag 01N0]. On the chart D₊(s) of Proj A the morphism is Spec of the surjection (A_s)₀ → (B_{F s})₀ (Proj.awayι_comp_map, Proj.map_preimage_basicOpen), and being a closed immersion is local on the target.
• AlgebraicGeometry.affineProjectiveBundle.isProper_π: for a finitely generated R-module M, P(M) = Proj (Sym M) ⟶ Spec R is proper: Sym M is generated over R by finitely many elements of degree one, and Mathlib's Proj.toSpecZero is proper for a graded algebra of finite type over its degree-zero part.

theorem HomogeneousLocalization.Away.map_surjective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {σ : Type u_3} {τ : Type u_4} [SetLike σ A] [AddSubgroupClass σ A] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (F : 𝒜 →+*ᵍ ℬ) (hF : Function.Surjective ⇑F) {i : ℕ} {s : A} (hs : s ∈ 𝒜 i) : Function.Surjective ⇑(Away.map F s)

A surjective graded ring map induces surjections of the degree-zero parts of the localizations at homogeneous elements.

theorem AlgebraicGeometry.Proj.isPullback_awayι_map {A B : Type u} [CommRing A] [CommRing B] {σ τ : Type u} [SetLike σ A] [AddSubgroupClass σ A] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (F : 𝒜 →+*ᵍ ℬ) (hF : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map F (HomogeneousIdeal.irrelevant 𝒜)) {i : ℕ} (hi : 0 < i) (s : A) (hs : s ∈ 𝒜 i) : CategoryTheory.IsPullback (awayι ℬ (F s) ⋯ hi) (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.map F s))) (map F hF) (awayι 𝒜 s hs hi)

The chart square of Proj.map: the chart D₊(F s) of Proj B is the preimage of the chart D₊(s) of Proj A, over which the morphism is Spec of (A_s)₀ → (B_{F s})₀.

theorem AlgebraicGeometry.Proj.isClosedImmersion_map_of_surjective {A B : Type u} [CommRing A] [CommRing B] {σ τ : Type u} [SetLike σ A] [AddSubgroupClass σ A] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (F : 𝒜 →+*ᵍ ℬ) (hF : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map F (HomogeneousIdeal.irrelevant 𝒜)) (hsurj : Function.Surjective ⇑F) : IsClosedImmersion (map F hF)

A surjective graded ring map induces a closed immersion Proj B ⟶ Proj A [TSPA, Tag 01N0]. On the chart D₊(s) of Proj A, whose preimage is the chart D₊(F s) of Proj B, the morphism is Spec of the surjection (A_s)₀ → (B_{F s})₀; being a closed immersion is local on the target.

theorem AlgebraicGeometry.affineProjectiveBundle.finiteType_symmetricAlgebra {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Algebra.FiniteType (↥(SymmetricAlgebra.grading R M 0)) (SymmetricAlgebra R M)

For a finitely generated M, Sym M is of finite type over its degree-zero part R: it is generated by the images of finitely many generators of M.

theorem AlgebraicGeometry.affineProjectiveBundle.isProper_π {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] : IsProper (π R M)

The projective bundle of a finitely generated module is proper over Spec R: Sym M is of finite type over R, and Mathlib's Proj.toSpecZero is proper for such graded algebras.