Flat base change of projective spectra

The projective spectrum of a graded algebra commutes with flat extension of its coefficient ring. The comparison identifies the scheme fiber product, including its structure sheaf, rather than only its points. Over a field, every coefficient extension is flat. This permits projective linear transformations to be assembled into algebraic families.

The construction combines Proj.map for coefficient inclusion, the homogeneous chart comparison HomogeneousLocalization.Away.baseChangeEquiv, and Mathlib's pullbackSpecIso and local criterion Scheme.isPullback_of_openCover.

References

• Stacks Project, Lemma 27.11.6, base change of projective spectra via standard affine charts.

noncomputable def AlgebraicGeometry.Proj.toSpecCoeff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : Proj 𝒜 ⟶ Spec ↧R

The structural morphism to the spectrum of the coefficient ring of a graded algebra.

Equations

• AlgebraicGeometry.Proj.toSpecCoeff 𝒜 = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero 𝒜) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R ↥(𝒜 0))))

theorem AlgebraicGeometry.Proj.toSpecCoeff_def {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : toSpecCoeff 𝒜 = CategoryTheory.CategoryStruct.comp (toSpecZero 𝒜) (Spec.map (CommRingCat.ofHom (algebraMap R ↥(𝒜 0))))

The coefficient structure map factors through the degree-zero spectrum.

@[simp]

theorem AlgebraicGeometry.Proj.awayι_toSpecCoeff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {n : ℕ} (hf : f ∈ 𝒜 n) (hn : 0 < n) : CategoryTheory.CategoryStruct.comp (awayι 𝒜 f hf hn) (toSpecCoeff 𝒜) = Spec.map (CommRingCat.ofHom (algebraMap R (HomogeneousLocalization.Away 𝒜 f)))

The coefficient morphism on a standard affine chart is the chart's coefficient map.

@[simp]

theorem AlgebraicGeometry.Proj.awayι_toSpecCoeff_assoc {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {n : ℕ} (hf : f ∈ 𝒜 n) (hn : 0 < n) {Z : Scheme} (h : Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (awayι 𝒜 f hf hn) (CategoryTheory.CategoryStruct.comp (toSpecCoeff 𝒜) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (algebraMap R (HomogeneousLocalization.Away 𝒜 f)))) h

The coefficient morphism on a standard affine chart is the chart's coefficient map.

noncomputable def AlgebraicGeometry.Proj.baseChangeProjection {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] : (Proj fun (n : ℕ) => Submodule.baseChange S (𝒜 n)) ⟶ Proj 𝒜

The projective projection induced by coefficient extension. Flatness is not needed to construct this map.

Equations

• AlgebraicGeometry.Proj.baseChangeProjection 𝒜 S = AlgebraicGeometry.Proj.map (TauCeti.GradedAlgebra.baseChangeMap S 𝒜) ⋯

theorem AlgebraicGeometry.Proj.baseChangeProjection_def {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] : baseChangeProjection 𝒜 S = map (TauCeti.GradedAlgebra.baseChangeMap S 𝒜) ⋯

The coefficient projection is the projective map of graded coefficient inclusion.

@[simp]

theorem AlgebraicGeometry.Proj.baseChangeProjection_preimage_basicOpen {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] (f : A) : (TopologicalSpace.Opens.map (baseChangeProjection 𝒜 S).base).obj (basicOpen 𝒜 f) = basicOpen (fun (n : ℕ) => Submodule.baseChange S (𝒜 n)) (1 ⊗ₜ[R] f)

The preimage of a standard open is the standard open of the extended element.

@[simp]

theorem AlgebraicGeometry.Proj.awayι_baseChangeProjection {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] {f : A} {n : ℕ} (hf : f ∈ 𝒜 n) (hn : 0 < n) : CategoryTheory.CategoryStruct.comp (awayι (fun (n : ℕ) => Submodule.baseChange S (𝒜 n)) (1 ⊗ₜ[R] f) ⋯ hn) (baseChangeProjection 𝒜 S) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.baseChangeMap 𝒜 S f))) (awayι 𝒜 f hf hn)

On standard affine charts, the projective projection is coefficient extension of homogeneous fractions.

@[simp]

theorem AlgebraicGeometry.Proj.awayι_baseChangeProjection_assoc {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] {f : A} {n : ℕ} (hf : f ∈ 𝒜 n) (hn : 0 < n) {Z : Scheme} (h : Proj 𝒜 ⟶ Z) : CategoryTheory.CategoryStruct.comp (awayι (fun (n : ℕ) => Submodule.baseChange S (𝒜 n)) (1 ⊗ₜ[R] f) ⋯ hn) (CategoryTheory.CategoryStruct.comp (baseChangeProjection 𝒜 S) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.baseChangeMap 𝒜 S f))) (CategoryTheory.CategoryStruct.comp (awayι 𝒜 f hf hn) h)

On standard affine charts, the projective projection is coefficient extension of homogeneous fractions.

@[simp]

theorem AlgebraicGeometry.Proj.baseChangeProjection_toSpecCoeff {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] : CategoryTheory.CategoryStruct.comp (baseChangeProjection 𝒜 S) (toSpecCoeff 𝒜) = CategoryTheory.CategoryStruct.comp (toSpecCoeff fun (n : ℕ) => Submodule.baseChange S (𝒜 n)) (Spec.map (CommRingCat.ofHom (algebraMap R S)))

Coefficient extension gives a commutative square over the base spectra.

@[simp]

theorem AlgebraicGeometry.Proj.baseChangeProjection_toSpecCoeff_assoc {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] {Z : Scheme} (h : Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeProjection 𝒜 S) (CategoryTheory.CategoryStruct.comp (toSpecCoeff 𝒜) h) = CategoryTheory.CategoryStruct.comp (toSpecCoeff fun (n : ℕ) => Submodule.baseChange S (𝒜 n)) (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (algebraMap R S))) h)

Coefficient extension gives a commutative square over the base spectra.

theorem AlgebraicGeometry.Proj.isPullback_away_baseChange {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] [Module.Flat R S] {f : A} {n : ℕ} (hf : f ∈ 𝒜 n) : CategoryTheory.IsPullback (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.baseChangeMap 𝒜 S f))) (Spec.map (CommRingCat.ofHom (algebraMap S (HomogeneousLocalization.Away (fun (n : ℕ) => Submodule.baseChange S (𝒜 n)) (1 ⊗ₜ[R] f))))) (Spec.map (CommRingCat.ofHom (algebraMap R (HomogeneousLocalization.Away 𝒜 f)))) (Spec.map (CommRingCat.ofHom (algebraMap R S)))

The affine standard-chart square of flat coefficient extension is cartesian.

theorem AlgebraicGeometry.Proj.isPullback_baseChangeProjection {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] [Module.Flat R S] : CategoryTheory.IsPullback (baseChangeProjection 𝒜 S) (toSpecCoeff fun (n : ℕ) => Submodule.baseChange S (𝒜 n)) (toSpecCoeff 𝒜) (Spec.map (CommRingCat.ofHom (algebraMap R S)))

Flat extension of coefficients makes the projective structural square cartesian. No finite-generation hypothesis on the graded algebra is needed.

noncomputable def AlgebraicGeometry.Proj.baseChangeIso {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] [Module.Flat R S] : (Proj fun (n : ℕ) => Submodule.baseChange S (𝒜 n)) ≅ CategoryTheory.Limits.pullback (toSpecCoeff 𝒜) (Spec.map (CommRingCat.ofHom (algebraMap R S)))

The canonical identification of the projective spectrum after flat coefficient extension with the fiber product over the original coefficient spectrum.

Equations

• AlgebraicGeometry.Proj.baseChangeIso 𝒜 S = ⋯.isoPullback

@[simp]

theorem AlgebraicGeometry.Proj.baseChangeIso_hom_fst {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] [Module.Flat R S] : CategoryTheory.CategoryStruct.comp (baseChangeIso 𝒜 S).hom (CategoryTheory.Limits.pullback.fst (toSpecCoeff 𝒜) (Spec.map (CommRingCat.ofHom (algebraMap R S)))) = baseChangeProjection 𝒜 S

The first projection of the comparison is the projective coefficient projection.

@[simp]

theorem AlgebraicGeometry.Proj.baseChangeIso_hom_fst_assoc {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] [Module.Flat R S] {Z : Scheme} (h : Proj 𝒜 ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeIso 𝒜 S).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (toSpecCoeff 𝒜) (Spec.map (CommRingCat.ofHom (algebraMap R S)))) h) = CategoryTheory.CategoryStruct.comp (baseChangeProjection 𝒜 S) h

The first projection of the comparison is the projective coefficient projection.

@[simp]

theorem AlgebraicGeometry.Proj.baseChangeIso_hom_snd {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] [Module.Flat R S] : CategoryTheory.CategoryStruct.comp (baseChangeIso 𝒜 S).hom (CategoryTheory.Limits.pullback.snd (toSpecCoeff 𝒜) (Spec.map (CommRingCat.ofHom (algebraMap R S)))) = toSpecCoeff fun (n : ℕ) => Submodule.baseChange S (𝒜 n)

The second projection of the comparison is the extended coefficient structure map.

@[simp]

theorem AlgebraicGeometry.Proj.baseChangeIso_hom_snd_assoc {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (S : Type u) [CommRing S] [Algebra R S] [Module.Flat R S] {Z : Scheme} (h : Spec ↧S ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeIso 𝒜 S).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (toSpecCoeff 𝒜) (Spec.map (CommRingCat.ofHom (algebraMap R S)))) h) = CategoryTheory.CategoryStruct.comp (toSpecCoeff fun (n : ℕ) => Submodule.baseChange S (𝒜 n)) h

The second projection of the comparison is the extended coefficient structure map.