The projective bundle of a module

For an R-module M, the projective bundle P(M) = Proj (Sym_R M) over Spec R [TSPA, Tag 01OB] is AlgebraicGeometry.affineProjectiveBundle R M, with structure morphism affineProjectiveBundle.π (Proj.toSpecZero followed by R ≅ Sym⁰ M). A ring map φ : R → S and a φ-semilinear map f : M → N whose image spans N induce the morphism affineProjectiveBundle.map φ f : P(N) ⟶ P(M), Mathlib's Proj.map of the graded map Sym_R M → Sym_S N; spanning is the hypothesis of Proj.map, that the irrelevant ideal of Sym_S N, generated by ι(N), lies in the ideal generated by the image of that of Sym_R M. These are the pieces of the projective bundle P(E) of a quasi-coherent sheaf, glued over the affine opens [TSPA, Tag 01OB].

theorem SymmetricAlgebra.irrelevant_le_span_ι {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] : (HomogeneousIdeal.irrelevant (grading R M)).toIdeal ≤ Ideal.span (Set.range ⇑(ι R M))

The irrelevant ideal of Sym M is generated by ι(M): an element of Symⁱ M = ι(M)ⁱ, i > 0, is a sum of products with a factor in ι(M).

theorem SymmetricAlgebra.irrelevant_le_map_gradedMap {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {S N : Type u} [CommRing S] [AddCommGroup N] [Module S N] (φ : R →+* S) (f : M →ₛₗ[φ] N) (hf : Submodule.span S (Set.range ⇑f) = ⊤) : HomogeneousIdeal.irrelevant (grading S N) ≤ HomogeneousIdeal.map (gradedMap φ f) (HomogeneousIdeal.irrelevant (grading R M))

The hypothesis of Proj.map for the graded map of symmetric algebras: if f(M) spans N, the irrelevant ideal of Sym_S N lies in the ideal generated by the image of that of Sym_R M.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.affineProjectiveBundle (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : Scheme

The projective bundle of a module [TSPA, Tag 01OB]: P(M) = Proj (Sym_R M). An abbrev, so that Mathlib's instances on Proj apply to it.

Equations

• AlgebraicGeometry.affineProjectiveBundle R M = AlgebraicGeometry.Proj (SymmetricAlgebra.grading R M)

noncomputable def AlgebraicGeometry.affineProjectiveBundle.π (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : affineProjectiveBundle R M ⟶ Spec ↧R

The structure morphism P(M) ⟶ Spec R: Proj.toSpecZero followed by Spec of the identification R ≅ Sym⁰ M.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.affineProjectiveBundle.map {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {S N : Type u} [CommRing S] [AddCommGroup N] [Module S N] (φ : R →+* S) (f : M →ₛₗ[φ] N) (hf : Submodule.span S (Set.range ⇑f) = ⊤) : affineProjectiveBundle S N ⟶ affineProjectiveBundle R M

The morphism of projective bundles P(N) ⟶ P(M) induced by a ring map φ : R → S and a φ-semilinear map f : M → N whose image spans N: Proj.map of the graded map Sym_R M → Sym_S N.

Equations

• AlgebraicGeometry.affineProjectiveBundle.map φ f hf = AlgebraicGeometry.Proj.map (SymmetricAlgebra.gradedMap φ f) ⋯

noncomputable def AlgebraicGeometry.affineProjectiveBundle.mapHom {R S : CommRingCat} {M N : Type u} [AddCommGroup M] [Module (↑R) M] [AddCommGroup N] [Module (↑S) N] (φ : R ⟶ S) (f : M →ₛₗ[CommRingCat.Hom.hom φ] N) (hf : Submodule.span (↑S) (Set.range ⇑f) = ⊤) : affineProjectiveBundle (↑S) N ⟶ affineProjectiveBundle (↑R) M

affineProjectiveBundle.map for a morphism φ : R ⟶ S of CommRingCat. Applied to a restriction map Γ(X, V) ⟶ Γ(X, U) of a scheme, the form with a ring homomorphism makes Lean unify the ring structures of ↑Γ(X, U) obtained by two routes, which unfolds the presheaf and times out; passing the rings as objects of CommRingCat avoids it (as for affineBlowUp.mapHom).

Equations

• AlgebraicGeometry.affineProjectiveBundle.mapHom φ f hf = AlgebraicGeometry.affineProjectiveBundle.map (CommRingCat.Hom.hom φ) f hf