The grading of the symmetric algebra

Mathlib's SymmetricAlgebra R M, the free commutative R-algebra on an R-module M, carries no grading. Its n-th graded piece Symⁿ M is the n-th power of the submodule ι(M) (SymmetricAlgebra.grading R M n), and SymmetricAlgebra.gradedAlgebra makes it a graded R-algebra, by the argument of Mathlib's TensorAlgebra.gradedAlgebra: the lift of the inclusion of M in degree one into the direct sum ⨁ₙ ι(M)ⁿ, a commutative algebra, splits the inclusion of the direct sum. The degree-zero piece is R (SymmetricAlgebra.gradingZeroEquiv).

A ring map φ : R → S and a φ-semilinear map f : M → N induce the graded ring map SymmetricAlgebra.gradedMap φ f : Sym_R M → Sym_S N, ι m ↦ ι (f m); these are the transition maps of the projective bundle P(E) = Proj_X (Sym E) of a quasi-coherent sheaf [TSPA, Tag 01OB].

def SymmetricAlgebra.grading (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) : Submodule R (SymmetricAlgebra R M)

The graded pieces of the symmetric algebra: Symⁿ M = ι(M)ⁿ, the n-th power of the R-submodule spanned by the image of M.

Equations

• SymmetricAlgebra.grading R M n = (SymmetricAlgebra.ι R M).range ^ n

instance SymmetricAlgebra.gradedMonoid (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : SetLike.GradedMonoid (grading R M)

The pieces multiply as powers of one submodule do.

def SymmetricAlgebra.gradedι (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : M →ₗ[R] DirectSum ℕ fun (i : ℕ) => ↥(grading R M i)

The inclusion M → ⨁ₙ Symⁿ M in degree one, the auxiliary map of SymmetricAlgebra.gradedAlgebra.

Equations

• SymmetricAlgebra.gradedι R M = DirectSum.lof R ℕ (fun (i : ℕ) => ↥(SymmetricAlgebra.grading R M i)) 1 ∘ₗ LinearMap.codRestrict (SymmetricAlgebra.grading R M 1) (SymmetricAlgebra.ι R M) ⋯

theorem SymmetricAlgebra.gradedι_apply (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] (m : M) : (gradedι R M) m = (DirectSum.of (fun (i : ℕ) => ↥(grading R M i)) 1) ⟨(ι R M) m, ⋯⟩

@[instance_reducible]

instance SymmetricAlgebra.gradedAlgebra (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : GradedAlgebra (grading R M)

The symmetric algebra is graded by the powers of ι(M).

Equations

• SymmetricAlgebra.gradedAlgebra R M = GradedAlgebra.ofAlgHom (SymmetricAlgebra.grading R M) (SymmetricAlgebra.lift (SymmetricAlgebra.gradedι R M)) ⋯ ⋯

theorem SymmetricAlgebra.algebraMap_bijective_gradingZero {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] : Function.Bijective ⇑(algebraMap R ↥(grading R M 0))

The constants have degree zero, and only they: Sym⁰ M = R.

noncomputable def SymmetricAlgebra.gradingZeroEquiv (R M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : R ≃+* ↥(grading R M 0)

The degree-zero piece of the symmetric algebra is R: R ≃+* Sym⁰ M, the algebra map.

Equations

• SymmetricAlgebra.gradingZeroEquiv R M = RingEquiv.ofBijective (algebraMap R ↥(SymmetricAlgebra.grading R M 0)) ⋯

@[reducible, inline]

noncomputable abbrev SymmetricAlgebra.algebraOfRingHom {R : Type u} [CommRing R] {S N : Type u} [CommRing S] [AddCommGroup N] [Module S N] (φ : R →+* S) : Algebra R (SymmetricAlgebra S N)

The R-algebra structure of Sym_S N along φ : R → S, under which a φ-semilinear map M → N followed by ι is R-linear; the auxiliary structure of SymmetricAlgebra.gradedMap.

Equations

• SymmetricAlgebra.algebraOfRingHom φ = ((algebraMap S (SymmetricAlgebra S N)).comp φ).toAlgebra

noncomputable def SymmetricAlgebra.ιₛₗ {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) : M →ₗ[R] SymmetricAlgebra S N

The R-linear map M → Sym_S N, m ↦ ι (f m), for the algebra structure SymmetricAlgebra.algebraOfRingHom φ.

Equations

• SymmetricAlgebra.ιₛₗ φ f = { toFun := fun (m : M) => (SymmetricAlgebra.ι S N) (f m), map_add' := ⋯, map_smul' := ⋯ }

noncomputable def 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) : grading R M →+*ᵍ grading S N

The graded map of symmetric algebras induced by a ring map φ : R → S and a φ-semilinear map f : M → N: the ring map Sym_R M → Sym_S N with ι m ↦ ι (f m) and r ↦ φ r, which sends Symⁿ M into Symⁿ N.

Equations

• SymmetricAlgebra.gradedMap φ f = { toRingHom := (SymmetricAlgebra.lift (SymmetricAlgebra.ιₛₗ φ f)).toRingHom, map_mem := ⋯ }