Graded maps out of the symmetric algebra #
For a graded R-algebra A = ⨁ₙ Aₙ and an R-linear map g : M → A₁, the lift
Sym_R M → A of g is a graded ring map (SymmetricAlgebra.gradedLift): it sends
Symⁿ M = ι(M)ⁿ into Aⁿ since A₁ⁿ ⊆ Aₙ. This is the surjection Sym(I) → ⨁ₙ Iⁿ of the
symmetric algebra of an ideal onto its Rees algebra, which embeds a blow-up in a projective bundle
[TSPA, Tag 02NS].
noncomputable def
SymmetricAlgebra.gradedLift
{R M : Type u}
[CommRing R]
[AddCommGroup M]
[Module R M]
{A : Type u}
[CommRing A]
[Algebra R A]
(𝒜 : ℕ → Submodule R A)
[GradedAlgebra 𝒜]
(g : M →ₗ[R] A)
(hg : ∀ (x : M), g x ∈ 𝒜 1)
:
The graded lift Sym_R M → A of an R-linear map g : M → A into degree one.
Equations
- SymmetricAlgebra.gradedLift 𝒜 g hg = { toRingHom := (SymmetricAlgebra.lift g).toRingHom, map_mem := ⋯ }
Instances For
theorem
SymmetricAlgebra.gradedLift_apply
{R M : Type u}
[CommRing R]
[AddCommGroup M]
[Module R M]
{A : Type u}
[CommRing A]
[Algebra R A]
(𝒜 : ℕ → Submodule R A)
[GradedAlgebra 𝒜]
(g : M →ₗ[R] A)
(hg : ∀ (x : M), g x ∈ 𝒜 1)
(a : SymmetricAlgebra R M)
: