The standard charts of Proj Sym M and their base change

For an R-module M and x₀ ∈ M, the chart D₊(x₀) of Proj (Sym_R M) is Spec of the degree-zero part (Sym M)_(x₀) of the localization at x₀ ∈ Sym¹ M. Every element of it is a fraction a / x₀ⁿ with a ∈ Symⁿ M, and a / x₀ⁿ is the value at a of the dehomogenization SymmetricAlgebra.dehom : Sym M → (Sym M)_(x₀), the ring map with ι x ↦ x / x₀ (SymmetricAlgebra.val_dehom_of_mem, SymmetricAlgebra.dehom_surjective). So a ring map out of the chart is determined by its values on the fractions x / x₀, and every R-linear map g : M → T to a commutative R-algebra with g x₀ = 1 is such a family of values (SymmetricAlgebra.awayLift): the chart is the free commutative R-algebra on M with x₀ = 1.

From this universal property the chart commutes with base change: for a ring map φ : R → S and a φ-semilinear map f : M → N that exhibits N as S ⊗_R M (every φ-semilinear map out of M extends to an S-linear map out of N, and f(M) spans N), the square of rings R → (Sym_R M)_(x₀), S → (Sym_S N)_(f x₀) is a pushout (SymmetricAlgebra.isPushout_away): both corners have the universal property of S-algebras with an R-linear map from M sending x₀ to 1 [TSPA, Tag 01N2].

theorem SymmetricAlgebra.ι_mem_grading_one {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (x : M) : (ι R M) x ∈ grading R M 1

theorem SymmetricAlgebra.algebraMap_mem_grading_zero {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (r : R) : (algebraMap R (SymmetricAlgebra R M)) r ∈ grading R M 0

theorem SymmetricAlgebra.ringHom_ext {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {T : Type u_1} [Semiring T] {F G : SymmetricAlgebra R M →+* T} (h₁ : ∀ (r : R), F ((algebraMap R (SymmetricAlgebra R M)) r) = G ((algebraMap R (SymmetricAlgebra R M)) r)) (h₂ : ∀ (x : M), F ((ι R M) x) = G ((ι R M) x)) : F = G

Two ring maps out of Sym_R M that agree on the constants and on ι(M) are equal.

noncomputable def SymmetricAlgebra.liftₛₗ {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {T : Type u_1} [CommRing T] (ψ : R →+* T) (g : M →+ T) (hg : ∀ (r : R) (x : M), g (r • x) = ψ r * g x) : SymmetricAlgebra R M →+* T

The ring map Sym_R M → T of a ring map ψ : R → T and a ψ-semilinear additive map g : M → T: the lift of g for the R-algebra structure of T along ψ.

Equations

• SymmetricAlgebra.liftₛₗ ψ g hg = (SymmetricAlgebra.lift { toFun := ⇑g, map_add' := ⋯, map_smul' := ⋯ }).toRingHom

theorem SymmetricAlgebra.liftₛₗ_ι {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {T : Type u_1} [CommRing T] (ψ : R →+* T) (g : M →+ T) (hg : ∀ (r : R) (x : M), g (r • x) = ψ r * g x) (x : M) : (liftₛₗ ψ g hg) ((ι R M) x) = g x

theorem SymmetricAlgebra.liftₛₗ_algebraMap {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {T : Type u_1} [CommRing T] (ψ : R →+* T) (g : M →+ T) (hg : ∀ (r : R) (x : M), g (r • x) = ψ r * g x) (r : R) : (liftₛₗ ψ g hg) ((algebraMap R (SymmetricAlgebra R M)) r) = ψ r

theorem SymmetricAlgebra.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) (x : M) : (gradedMap φ f) ((ι R M) x) = (ι S N) (f x)

theorem SymmetricAlgebra.gradedMap_algebraMap {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) (r : R) : (gradedMap φ f) ((algebraMap R (SymmetricAlgebra R M)) r) = (algebraMap S (SymmetricAlgebra S N)) (φ r)

noncomputable def SymmetricAlgebra.toAway {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) : R →+* HomogeneousLocalization.Away (grading R M) e

The constants R → (Sym M)_(e): R ≅ Sym⁰ M followed by r ↦ r / 1.

Equations

• e.toAway = (HomogeneousLocalization.fromZeroRingHom (SymmetricAlgebra.grading R M) (Submonoid.powers e)).comp (algebraMap R ↥(SymmetricAlgebra.grading R M 0))

theorem SymmetricAlgebra.val_toAway {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (r : R) : HomogeneousLocalization.val (e.toAway r) = Localization.mk ((algebraMap R (SymmetricAlgebra R M)) r) 1

theorem SymmetricAlgebra.e_mem_grading_one {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) : e ∈ grading R M 1

noncomputable def SymmetricAlgebra.frac {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) (x : M) : HomogeneousLocalization.Away (grading R M) e

The fraction x / x₀ of the chart (Sym M)_(x₀), for x ∈ M.

Equations

• e.frac x₀ he x = HomogeneousLocalization.Away.mk (SymmetricAlgebra.grading R M) ⋯ 1 ((SymmetricAlgebra.ι R M) x) ⋯

theorem SymmetricAlgebra.val_frac {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) (x : M) : HomogeneousLocalization.val (e.frac x₀ he x) = Localization.mk ((ι R M) x) ⟨e, ⋯⟩

noncomputable def SymmetricAlgebra.dehom {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) : SymmetricAlgebra R M →+* HomogeneousLocalization.Away (grading R M) e

The dehomogenization Sym M → (Sym M)_(x₀), ι x ↦ x / x₀, the ring map whose value at a ∈ Symⁿ M is the fraction a / x₀ⁿ (val_dehom_of_mem).

Equations

• e.dehom x₀ he = SymmetricAlgebra.liftₛₗ e.toAway { toFun := e.frac x₀ he, map_zero' := ⋯, map_add' := ⋯ } ⋯

theorem SymmetricAlgebra.dehom_ι {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) (x : M) : (e.dehom x₀ he) ((ι R M) x) = e.frac x₀ he x

theorem SymmetricAlgebra.dehom_algebraMap {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) (r : R) : (e.dehom x₀ he) ((algebraMap R (SymmetricAlgebra R M)) r) = e.toAway r

theorem SymmetricAlgebra.dehom_e {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) : (e.dehom x₀ he) e = 1

theorem SymmetricAlgebra.val_dehom_of_mem {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) {n : ℕ} {a : SymmetricAlgebra R M} (ha : a ∈ grading R M n) : HomogeneousLocalization.val ((e.dehom x₀ he) a) = Localization.mk a ⟨e ^ n, ⋯⟩

The value of the dehomogenization at a ∈ Symⁿ M is a / x₀ⁿ.

theorem SymmetricAlgebra.dehom_surjective {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) : Function.Surjective ⇑(e.dehom x₀ he)

theorem SymmetricAlgebra.away_ringHom_ext {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) {T : Type u_1} [Semiring T] {F G : HomogeneousLocalization.Away (grading R M) e →+* T} (h₁ : ∀ (r : R), F (e.toAway r) = G (e.toAway r)) (h₂ : ∀ (x : M), F ((e.dehom x₀ he) ((ι R M) x)) = G ((e.dehom x₀ he) ((ι R M) x))) : F = G

Ring maps out of the chart (Sym M)_(x₀) are determined by their values on the fractions x / x₀ and on the constants.

theorem SymmetricAlgebra.awayLift_mk_of_eq_one {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) {T : Type u_1} [CommRing T] (L : SymmetricAlgebra R M →+* T) (hu : L e = 1) (hunit : IsUnit (L e)) (a : SymmetricAlgebra R M) (s : ↥(Submonoid.powers e)) : (Localization.awayLift L e hunit) (Localization.mk a s) = L a

The lift through the localization at e of a ring map sending e to 1 sends a / eⁿ to the image of a.

noncomputable def SymmetricAlgebra.awayLift {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) {T : Type u_1} [CommRing T] (ψ : R →+* T) (g : M →+ T) (hg : ∀ (r : R) (x : M), g (r • x) = ψ r * g x) (h₀ : g x₀ = 1) : HomogeneousLocalization.Away (grading R M) e →+* T

The universal property of the chart: a ring map ψ : R → T and a ψ-semilinear additive map g : M → T with g x₀ = 1 define the ring map (Sym M)_(x₀) → T, x / x₀ ↦ g x: the lift of g to Sym M, which sends x₀ to the unit 1, through the localization at x₀.

Equations

• e.awayLift x₀ he ψ g hg h₀ = (Localization.awayLift (SymmetricAlgebra.liftₛₗ ψ g hg) e ⋯).comp (algebraMap (HomogeneousLocalization.Away (SymmetricAlgebra.grading R M) e) (Localization.Away e))

theorem SymmetricAlgebra.awayLift_dehom {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) {T : Type u_1} [CommRing T] (ψ : R →+* T) (g : M →+ T) (hg : ∀ (r : R) (x : M), g (r • x) = ψ r * g x) (h₀ : g x₀ = 1) (a : SymmetricAlgebra R M) : (e.awayLift x₀ he ψ g hg h₀) ((e.dehom x₀ he) a) = (liftₛₗ ψ g hg) a

theorem SymmetricAlgebra.awayLift_toAway {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) {T : Type u_1} [CommRing T] (ψ : R →+* T) (g : M →+ T) (hg : ∀ (r : R) (x : M), g (r • x) = ψ r * g x) (h₀ : g x₀ = 1) (r : R) : (e.awayLift x₀ he ψ g hg h₀) (e.toAway r) = ψ r

theorem SymmetricAlgebra.awayLift_frac {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (e : SymmetricAlgebra R M) (x₀ : M) (he : (ι R M) x₀ = e) {T : Type u_1} [CommRing T] (ψ : R →+* T) (g : M →+ T) (hg : ∀ (r : R) (x : M), g (r • x) = ψ r * g x) (h₀ : g x₀ = 1) (x : M) : (e.awayLift x₀ he ψ g hg h₀) ((e.dehom x₀ he) ((ι R M) x)) = g x

theorem SymmetricAlgebra.awayMap_toAway {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) (x₀ : M) (r : R) : (HomogeneousLocalization.Away.map (gradedMap φ f) ((ι R M) x₀)) (((ι R M) x₀).toAway r) = ((gradedMap φ f) ((ι R M) x₀)).toAway (φ r)

theorem SymmetricAlgebra.awayMap_frac {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) (x₀ x : M) : (HomogeneousLocalization.Away.map (gradedMap φ f) ((ι R M) x₀)) (((ι R M) x₀).frac x₀ ⋯ x) = ((gradedMap φ f) ((ι R M) x₀)).frac (f x₀) ⋯ (f x)

theorem SymmetricAlgebra.awayMap_dehom {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) (x₀ : M) (a : SymmetricAlgebra R M) : (HomogeneousLocalization.Away.map (gradedMap φ f) ((ι R M) x₀)) ((((ι R M) x₀).dehom x₀ ⋯) a) = (((gradedMap φ f) ((ι R M) x₀)).dehom (f x₀) ⋯) ((gradedMap φ f) a)

The dehomogenizations commute with the graded map of symmetric algebras.

theorem SymmetricAlgebra.isPushout_away {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) (x₀ : M) (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.IsPushout (CommRingCat.ofHom φ) (CommRingCat.ofHom ((ι R M) x₀).toAway) (CommRingCat.ofHom ((gradedMap φ f) ((ι R M) x₀)).toAway) (CommRingCat.ofHom (HomogeneousLocalization.Away.map (gradedMap φ f) ((ι R M) x₀)))

The chart of Proj Sym M commutes with base change [TSPA, Tag 01N2]: if f : M → N is φ-semilinear, its image spans N, and every φ-semilinear map out of M extends along f to an S-linear map out of N (so that N = S ⊗_R M), the square R → S, R → (Sym_R M)_(x₀), S → (Sym_S N)_(f x₀), (Sym_R M)_(x₀) → (Sym_S N)_(f x₀) is a pushout of rings. Both ways round, a ring map out of the corner is a ring map b out of S with an additive map N → T (or M → T), semilinear along b (or b ∘ φ), sending f x₀ (or x₀) to 1 (awayLift); the extension property turns the second kind into the first, and the spanning property makes the extension unique.