Base change of the projective bundle of a module

For a ring map φ : R → S and a φ-semilinear map f : M → N that exhibits N as S ⊗_R M (its image spans N, and every φ-semilinear map out of M extends along f to an S-linear map out of N), the square

P(N) ⟶ Spec S
  |        |
P(M) ⟶ Spec R

of projective bundles is cartesian [TSPA, Tag 01N2] (AlgebraicGeometry.affineProjectiveBundle.isPullback_map). P(M) is covered by the charts D₊(ι x) = Spec (Sym M)_(ι x), x ∈ M (the irrelevant ideal is generated by ι(M), SymmetricAlgebra.irrelevant_le_span_ι), the morphism P(N) ⟶ P(M) pulls D₊(ι x) back to D₊(ι (f x)) (Proj.map_preimage_basicOpen), and over a chart the square is Spec of the pushout of rings SymmetricAlgebra.isPushout_away; a square cartesian over an open cover of a corner is cartesian (Mathlib's Scheme.isPullback_of_openCover). This is the argument of AlgebraicGeometry.Proj.isPullback_projMap for polynomial rings.

noncomputable def AlgebraicGeometry.affineProjectiveBundle.chartCover {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] : (affineProjectiveBundle R M).AffineOpenCover

The affine open cover of P(M) by the charts D₊(ι x), x ∈ M.

Equations

• AlgebraicGeometry.affineProjectiveBundle.chartCover = AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpan (SymmetricAlgebra.grading R M) (fun (x : M) => (SymmetricAlgebra.ι R M) x) ⋯ ⋯ ⋯

theorem AlgebraicGeometry.affineProjectiveBundle.awayι_π {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (he : e ∈ SymmetricAlgebra.grading R M 1) : CategoryTheory.CategoryStruct.comp (Proj.awayι (SymmetricAlgebra.grading R M) e he ⋯) (π R M) = Spec.map (CommRingCat.ofHom e.toAway)

The chart D₊(e) = Spec (Sym M)_(e) of P(M) followed by the structure morphism is Spec of the constants R → (Sym M)_(e).

theorem AlgebraicGeometry.affineProjectiveBundle.isPullback_awayι_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) (hspan : Submodule.span S (Set.range ⇑f) = ⊤) (x : M) : CategoryTheory.IsPullback (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.map (SymmetricAlgebra.gradedMap φ f) ((SymmetricAlgebra.ι R M) x)))) (Proj.awayι (SymmetricAlgebra.grading S N) ((SymmetricAlgebra.gradedMap φ f) ((SymmetricAlgebra.ι R M) x)) ⋯ ⋯) (Proj.awayι (SymmetricAlgebra.grading R M) ((SymmetricAlgebra.ι R M) x) ⋯ ⋯) (map φ f hspan)

The chart square of P(N) ⟶ P(M) over D₊(ι x).

theorem AlgebraicGeometry.affineProjectiveBundle.isPullback_map_aux {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) (hspan : Submodule.span S (Set.range ⇑f) = ⊤) (hext : ∀ (T : Type u) [inst : AddCommGroup T] [inst_1 : Module S T] (g : M →ₛₗ[φ] T), ∃ (g' : N →ₗ[S] T), ∀ (x : M), g' (f x) = g x) (x : M) {W' : Scheme} {a : W' ⟶ affineProjectiveBundle S N} {b : W' ⟶ Spec ↧(HomogeneousLocalization.Away (SymmetricAlgebra.grading R M) ((SymmetricAlgebra.ι R M) x))} (hab : CategoryTheory.IsPullback a b (map φ f hspan) (Proj.awayι (SymmetricAlgebra.grading R M) ((SymmetricAlgebra.ι R M) x) ⋯ ⋯)) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp a (π S N)) b (Spec.map (CommRingCat.ofHom φ)) (CategoryTheory.CategoryStruct.comp (Proj.awayι (SymmetricAlgebra.grading R M) ((SymmetricAlgebra.ι R M) x) ⋯ ⋯) (π R M))

The base-change square over the chart D₊(ι x), for any pullback of P(N) ⟶ P(M) along the chart: the square Spec of SymmetricAlgebra.isPushout_away, transported along the identification of the two pullbacks of the chart square.

theorem AlgebraicGeometry.affineProjectiveBundle.isPullback_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) (hspan : Submodule.span S (Set.range ⇑f) = ⊤) (hext : ∀ (T : Type u) [inst : AddCommGroup T] [inst_1 : Module S T] (g : M →ₛₗ[φ] T), ∃ (g' : N →ₗ[S] T), ∀ (x : M), g' (f x) = g x) : CategoryTheory.IsPullback (π S N) (map φ f hspan) (Spec.map (CommRingCat.ofHom φ)) (π R M)

Base change of the projective bundle of a module [TSPA, Tag 01N2]: if f : M → N exhibits N as S ⊗_R M, the square P(N) ⟶ Spec S, P(N) ⟶ P(M), Spec S ⟶ Spec R, P(M) ⟶ Spec R is cartesian. It is cartesian over each chart D₊(ι x) of P(M) (isPullback_map_aux at the canonical pullback), hence cartesian.

theorem AlgebraicGeometry.affineProjectiveBundle.isPullback_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) (hspan : Submodule.span (↑S) (Set.range ⇑f) = ⊤) (hext : ∀ (T : Type u) [inst : AddCommGroup T] [inst_1 : Module (↑S) T] (g : M →ₛₗ[CommRingCat.Hom.hom φ] T), ∃ (g' : N →ₗ[↑S] T), ∀ (x : M), g' (f x) = g x) : CategoryTheory.IsPullback (π (↑S) N) (mapHom φ f hspan) (Spec.map φ) (π (↑R) M)

isPullback_map for a morphism φ : R ⟶ S of CommRingCat.