Dehomogenization: the standard chart of ℙ^{r-1}_R is a polynomial ring

The exceptional divisor of the blow-up of a smooth scheme along a smooth centre Z of codimension r is locally (Z ∩ U) ×_k ℙ^{r-1}_k; establishing this needs the base change of Proj along k → B for the polynomial ring k[u_0, …, u_{r-1}] with its standard grading [TSPA, Tag 01MX], which Mathlib does not provide. Its local form on the standard chart D₊(u_j) is the ring statement of this file: the degree-zero part of the localization R[u]_{u_j} is the polynomial ring R[u_i/u_j : i ≠ j], naturally in R, so that B ⊗_k (k[u]_{u_j})₀ ≅ (B[u]_{u_j})₀.

Why the theorems hold. Every element of (R[u]_{u_j})₀ is a fraction p/u_j^m with p homogeneous of degree m, and p/u_j^m = p(u_i/u_j) is the polynomial p(u_j ↦ 1, u_i ↦ y_i) in the variables y_i = u_i/u_j (dehomogenization); conversely a polynomial q(y) is recovered from q(u_i/u_j) ∈ R[u]_{u_j} by the ring map u_j ↦ 1, u_i ↦ y_i, which is defined on the localization because it sends u_j to a unit. So q ↦ q(u_i/u_j) is an isomorphism R[y_i : i ≠ j] ≅ (R[u]_{u_j})₀; it commutes with the coefficient maps R → S, and S ⊗_R R[y] = S[y] (Mathlib's MvPolynomial.algebraTensorAlgEquiv) gives the tensor identity.

Main declarations

• AlgebraicGeometry.Proj.dehom R j : MvPolynomial {i // i ≠ j} R ≃ₐ[R] Away (𝒜 R) (X j) — y_i ↦ u_i/u_j, for 𝒜 R = homogeneousSubmodule σ R the standard grading of R[u].
• AlgebraicGeometry.Proj.gradedMap R S : homogeneousSubmodule σ R →+*ᵍ homogeneousSubmodule σ S — the coefficient map R[u] → S[u] as a graded ring homomorphism; awayMap_dehomAux is the naturality of dehom.
• AlgebraicGeometry.Proj.tensorEquiv R j S : S ⊗[R] Away (𝒜 R) (X j) ≃ₐ[S] Away (𝒜 S) (X j) and the pushout square isPushout_away in CommRingCat.

Conventions

The variable type σ lives in Type (the applications use Fin r), so that MvPolynomial σ R stays in the universe of R for CommRingCat. The chart element is carried as a variable f with hf : f = X j, because the base-changed chart is Away (𝒜 S) (gradedMap R S (X j)) (the image of X j, equal but not definitionally equal to X j).

theorem AlgebraicGeometry.Proj.val_fromZeroRingHom {ι : Type u_1} {σ' : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [SetLike σ' A] [AddSubgroupClass σ' A] (𝒜 : ι → σ') [GradedRing 𝒜] (x : Submonoid A) (f : ↥(𝒜 0)) : ((HomogeneousLocalization.fromZeroRingHom 𝒜 x) f).val = (algebraMap A (Localization x)) ↑f

val on the constants of degree zero: f/1.

@[reducible, inline]

abbrev AlgebraicGeometry.Proj.valRingHom {ι : Type u_1} {σ' : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [SetLike σ' A] [AddSubgroupClass σ' A] (𝒜 : ι → σ') [GradedRing 𝒜] (x : Submonoid A) : HomogeneousLocalization 𝒜 x →+* Localization x

val as a ring homomorphism (the algebraMap of Mathlib's algebra instance).

Equations

• AlgebraicGeometry.Proj.valRingHom 𝒜 x = algebraMap (HomogeneousLocalization 𝒜 x) (Localization x)

theorem AlgebraicGeometry.Proj.valRingHom_apply {ι : Type u_1} {σ' : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [SetLike σ' A] [AddSubgroupClass σ' A] (𝒜 : ι → σ') [GradedRing 𝒜] (x : Submonoid A) (y : HomogeneousLocalization 𝒜 x) : (valRingHom 𝒜 x) y = y.val

theorem AlgebraicGeometry.Proj.X_mem_one {σ : Type} (R : Type u) [CommRing R] (i : σ) : MvPolynomial.X i ∈ MvPolynomial.homogeneousSubmodule σ R 1

The variables are homogeneous of degree one.

theorem AlgebraicGeometry.Proj.X_mem_one_smul {σ : Type} (R : Type u) [CommRing R] (i : σ) : MvPolynomial.X i ∈ MvPolynomial.homogeneousSubmodule σ R (1 • 1)

@[instance_reducible]

noncomputable def AlgebraicGeometry.Proj.instAlgebraAway {σ : Type} (R : Type u) [CommRing R] (f : MvPolynomial σ R) : Algebra R (HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) f)

The R-algebra structure on (R[u]_f)₀: Mathlib's scalar action of R on the homogeneous localization (through the numerators) with the constants R → (R[u])₀ → (R[u]_f)₀ as algebraMap — the composite of Mathlib's Algebra (𝒜 0) (HomogeneousLocalization 𝒜 x) with the grade-zero Algebra R (𝒜 0) (the scalar tower instIsScalarTowerAway below). Scoped to Hironaka.Proj, as an instance on a Mathlib type.

Equations

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

theorem AlgebraicGeometry.Proj.algebraMap_away_apply {σ : Type} (R : Type u) [CommRing R] (f : MvPolynomial σ R) (r : R) : (algebraMap R (HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) f)) r = (HomogeneousLocalization.fromZeroRingHom (MvPolynomial.homogeneousSubmodule σ R) (Submonoid.powers f)) ((algebraMap R ↥(MvPolynomial.homogeneousSubmodule σ R 0)) r)

theorem AlgebraicGeometry.Proj.instIsScalarTowerAway {σ : Type} (R : Type u) [CommRing R] (f : MvPolynomial σ R) : IsScalarTower R (↥(MvPolynomial.homogeneousSubmodule σ R 0)) (HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) f)

The R-algebra structure on (R[u]_f)₀ is compatible with Mathlib's (R[u])₀-algebra structure.

theorem AlgebraicGeometry.Proj.val_algebraMap_away {σ : Type} (R : Type u) [CommRing R] (f : MvPolynomial σ R) (r : R) : HomogeneousLocalization.val ((algebraMap R (HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) f)) r) = (algebraMap (MvPolynomial σ R) (Localization (Submonoid.powers f))) (MvPolynomial.C r)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Proj.fpow {σ : Type} (R : Type u) [CommRing R] (f : MvPolynomial σ R) (n : ℕ) : ↥(Submonoid.powers f)

f ^ n as an element of the submonoid powers f.

Equations

• AlgebraicGeometry.Proj.fpow R f n = ⟨f ^ n, ⋯⟩

The chart of u_j: f is the variable u_j (as an element, up to the equation hf)

theorem AlgebraicGeometry.Proj.f_mem_one {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) : f ∈ MvPolynomial.homogeneousSubmodule σ R 1

noncomputable def AlgebraicGeometry.Proj.mkX {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) (i : σ) : HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) f

u_i / u_j.

Equations

• AlgebraicGeometry.Proj.mkX R j f hf i = HomogeneousLocalization.Away.mk (MvPolynomial.homogeneousSubmodule σ R) ⋯ 1 (MvPolynomial.X i) ⋯

theorem AlgebraicGeometry.Proj.val_mkX {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) (i : σ) : HomogeneousLocalization.val (mkX R j f hf i) = Localization.mk (MvPolynomial.X i) (fpow R f 1)

theorem AlgebraicGeometry.Proj.mkX_self {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) : mkX R j f hf j = 1

noncomputable def AlgebraicGeometry.Proj.dehomAux {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) : MvPolynomial { i : σ // i ≠ j } R →ₐ[R] HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) f

R[y_i : i ≠ j] → (R[u]_{u_j})₀, y_i ↦ u_i/u_j.

Equations

• AlgebraicGeometry.Proj.dehomAux R j f hf = MvPolynomial.aeval fun (i : { i : σ // i ≠ j }) => AlgebraicGeometry.Proj.mkX R j f hf ↑i

noncomputable def AlgebraicGeometry.Proj.dehomogenize {σ : Type} (R : Type u) [CommRing R] (j : σ) : MvPolynomial σ R →ₐ[R] MvPolynomial { i : σ // i ≠ j } R

Dehomogenization u_j ↦ 1, u_i ↦ y_i.

Equations

• AlgebraicGeometry.Proj.dehomogenize R j = MvPolynomial.aeval fun (i : σ) => if h : i = j then 1 else MvPolynomial.X ⟨i, h⟩

theorem AlgebraicGeometry.Proj.dehomogenize_X_self {σ : Type} (R : Type u) [CommRing R] (j : σ) : (dehomogenize R j) (MvPolynomial.X j) = 1

theorem AlgebraicGeometry.Proj.dehomogenize_X_of_ne {σ : Type} (R : Type u) [CommRing R] (j : σ) {i : σ} (h : i ≠ j) : (dehomogenize R j) (MvPolynomial.X i) = MvPolynomial.X ⟨i, h⟩

theorem AlgebraicGeometry.Proj.eval₂_mul_right_of_isHomogeneous {σ : Type} (R : Type u) [CommRing R] {S : Type u_1} [CommRing S] (φ : R →+* S) (g : σ → S) (u : S) {p : MvPolynomial σ R} {m : ℕ} (hp : p.IsHomogeneous m) : MvPolynomial.eval₂ φ (fun (i : σ) => g i * u) p = u ^ m * MvPolynomial.eval₂ φ g p

For p homogeneous of degree m, p(g_i · u) = u^m · p(g_i).

theorem AlgebraicGeometry.Proj.aeval_mkX_of_mem {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) {p : MvPolynomial σ R} {m : ℕ} (hp : p ∈ MvPolynomial.homogeneousSubmodule σ R m) : (MvPolynomial.aeval (mkX R j f hf)) p = HomogeneousLocalization.Away.mk (MvPolynomial.homogeneousSubmodule σ R) ⋯ m p ⋯

The chart computation: a homogeneous p of degree m evaluated at u_i/u_j is the fraction p/u_j^m.

theorem AlgebraicGeometry.Proj.dehomAux_dehomogenize {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) (p : MvPolynomial σ R) : (dehomAux R j f hf) ((dehomogenize R j) p) = (MvPolynomial.aeval (mkX R j f hf)) p

theorem AlgebraicGeometry.Proj.dehomAux_surjective {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) : Function.Surjective ⇑(dehomAux R j f hf)

theorem AlgebraicGeometry.Proj.isUnit_dehomogenize {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) : IsUnit ((dehomogenize R j) f)

noncomputable def AlgebraicGeometry.Proj.dehomLoc {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) : Localization (Submonoid.powers f) →+* MvPolynomial { i : σ // i ≠ j } R

The map R[u]_{u_j} → R[y], u_j ↦ 1, u_i ↦ y_i, on the localization.

Equations

• AlgebraicGeometry.Proj.dehomLoc R j f hf = IsLocalization.Away.lift f ⋯

theorem AlgebraicGeometry.Proj.dehomLoc_val_dehomAux {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) (q : MvPolynomial { i : σ // i ≠ j } R) : (dehomLoc R j f hf) (HomogeneousLocalization.val ((dehomAux R j f hf) q)) = q

theorem AlgebraicGeometry.Proj.dehomAux_injective {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) : Function.Injective ⇑(dehomAux R j f hf)

noncomputable def AlgebraicGeometry.Proj.dehom {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) : MvPolynomial { i : σ // i ≠ j } R ≃ₐ[R] HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) f

The dehomogenization isomorphism R[y_i : i ≠ j] ≅ (R[u]_{u_j})₀, y_i ↦ u_i/u_j: the standard chart of projective space is an affine space [TSPA, Tag 01MX].

Equations

• AlgebraicGeometry.Proj.dehom R j f hf = AlgEquiv.ofBijective (AlgebraicGeometry.Proj.dehomAux R j f hf) ⋯

theorem AlgebraicGeometry.Proj.dehom_apply {σ : Type} (R : Type u) [CommRing R] (j : σ) (f : MvPolynomial σ R) (hf : f = MvPolynomial.X j) (q : MvPolynomial { i : σ // i ≠ j } R) : (dehom R j f hf) q = (dehomAux R j f hf) q

noncomputable def AlgebraicGeometry.Proj.gradedMap {σ : Type} (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] : MvPolynomial.homogeneousSubmodule σ R →+*ᵍ MvPolynomial.homogeneousSubmodule σ S

The coefficient map R[u] → S[u] as a graded ring homomorphism.

Equations

• AlgebraicGeometry.Proj.gradedMap R S = { toRingHom := MvPolynomial.map (algebraMap R S), map_mem := ⋯ }

theorem AlgebraicGeometry.Proj.gradedMap_apply {σ : Type} (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] (p : MvPolynomial σ R) : (gradedMap R S) p = (MvPolynomial.map (algebraMap R S)) p

theorem AlgebraicGeometry.Proj.gradedMap_X {σ : Type} (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] (i : σ) : (gradedMap R S) (MvPolynomial.X i) = MvPolynomial.X i

theorem AlgebraicGeometry.Proj.awayMap_dehomAux {σ : Type} (R : Type u) [CommRing R] (j : σ) (S : Type u) [CommRing S] [Algebra R S] (q : MvPolynomial { i : σ // i ≠ j } R) : (HomogeneousLocalization.Away.map (gradedMap R S) (MvPolynomial.X j)) ((dehomAux R j (MvPolynomial.X j) ⋯) q) = (dehomAux S j ((gradedMap R S) (MvPolynomial.X j)) ⋯) ((MvPolynomial.map (algebraMap R S)) q)

Naturality of dehomogenization in the coefficients.

noncomputable def AlgebraicGeometry.Proj.tensorEquiv {σ : Type} (R : Type u) [CommRing R] (j : σ) (S : Type u) [CommRing S] [Algebra R S] : TensorProduct R S (HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) (MvPolynomial.X j)) ≃ₐ[S] HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ S) ((gradedMap R S) (MvPolynomial.X j))

S ⊗_R (R[u]_{u_j})₀ ≅ (S[u]_{u_j})₀: the base change of the standard chart.

Equations

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

theorem AlgebraicGeometry.Proj.tensorEquiv_tmul {σ : Type} (R : Type u) [CommRing R] (j : σ) (S : Type u) [CommRing S] [Algebra R S] (s : S) (z : HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) (MvPolynomial.X j)) : (tensorEquiv R j S) (s ⊗ₜ[R] z) = (algebraMap S (HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ S) ((gradedMap R S) (MvPolynomial.X j)))) s * (HomogeneousLocalization.Away.map (gradedMap R S) (MvPolynomial.X j)) z

theorem AlgebraicGeometry.Proj.isPushout_away {σ : Type} (R : Type u) [CommRing R] (j : σ) (S : Type u) [CommRing S] [Algebra R S] : CategoryTheory.IsPushout (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R (HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) (MvPolynomial.X j)))) (CommRingCat.ofHom (algebraMap S (HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ S) ((gradedMap R S) (MvPolynomial.X j))))) (CommRingCat.ofHom (HomogeneousLocalization.Away.map (gradedMap R S) (MvPolynomial.X j)))

The standard chart of ℙ^{r-1} commutes with base change: the square R → S, R → (R[u]_{u_j})₀, S → (S[u]_{u_j})₀, (R[u]_{u_j})₀ → (S[u]_{u_j})₀ is a pushout of rings — the chart form of the base change of projective space [TSPA, Tag 01MX].