Documentation

TauCeti.AlgebraicGeometry.ProjectiveSpectrum.SymmetricAlgebra

The projective spectrum of a finite module #

The coefficient morphism Proj(Sym M) ⟶ Spec R is proper when M is a finite R-module, even when M is not free or projective. Over a Noetherian coefficient ring, its source is a Noetherian scheme. These are the finiteness properties needed to apply Chevalley's theorem to projective orbit morphisms.

The convention is that M consists of homogeneous linear coordinates. For the space of lines in a finite locally free representation V, use M = V∨.

SymmetricAlgebra.projToSpec is the structural morphism over R. Its properness and quasi-compactness instances require only Module.Finite R M; its Noetherianity instance also requires IsNoetherianRing R. The chart formula describes this morphism on the standard affine charts. Its source is Jacobson whenever Spec R is Jacobson.

References #

source
noncomputable def TauCeti.SymmetricAlgebra.projToSpec (R M : Type u) [CommRing R] [AddCommMonoid M] [Module R M] :
AlgebraicGeometry.Proj (homogeneousSubmodule R M) ⟶ AlgebraicGeometry.Spec ↧R

The structural morphism from the projective spectrum of a symmetric algebra to the spectrum of its coefficient ring.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.SymmetricAlgebra.projToSpec_def (R M : Type u) [CommRing R] [AddCommMonoid M] [Module R M] :
    projToSpec R M = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (homogeneousSubmodule R M)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R ↥(homogeneousSubmodule R M 0))))

    The coefficient morphism is Proj.toSpecZero followed by the scalar identification.

    source
    @[simp]
    theorem TauCeti.SymmetricAlgebra.awayι_projToSpec (R M : Type u) [CommRing R] [AddCommMonoid M] [Module R M] {f : SymmetricAlgebra R M} {n : ℕ} (hf : f ∈ homogeneousSubmodule R M n) (hn : 0 < n) :
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι (homogeneousSubmodule R M) f hf hn) (projToSpec R M) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ((HomogeneousLocalization.fromZeroRingHom (homogeneousSubmodule R M) (Submonoid.powers f)).comp (algebraMap R ↥(homogeneousSubmodule R M 0))))

    On a standard affine chart, the coefficient morphism comes from the inclusion of scalars into the homogeneous localization.

    source
    @[simp]
    theorem TauCeti.SymmetricAlgebra.awayι_projToSpec_assoc (R M : Type u) [CommRing R] [AddCommMonoid M] [Module R M] {f : SymmetricAlgebra R M} {n : ℕ} (hf : f ∈ homogeneousSubmodule R M n) (hn : 0 < n) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι (homogeneousSubmodule R M) f hf hn) (CategoryTheory.CategoryStruct.comp (projToSpec R M) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ((HomogeneousLocalization.fromZeroRingHom (homogeneousSubmodule R M) (Submonoid.powers f)).comp (algebraMap R ↥(homogeneousSubmodule R M 0))))) h

    On a standard affine chart, the coefficient morphism comes from the inclusion of scalars into the homogeneous localization.

    source
    instance TauCeti.SymmetricAlgebra.instIsProperProjToSpec (R M : Type u) [CommRing R] [AddCommMonoid M] [Module R M] [Module.Finite R M] :
    AlgebraicGeometry.IsProper (projToSpec R M)

    The projective spectrum of a finite module is proper over the coefficient ring. Freeness and projectivity are not required.

    source
    instance TauCeti.SymmetricAlgebra.instCompactSpaceProj (R M : Type u) [CommRing R] [AddCommMonoid M] [Module R M] [Module.Finite R M] :
    CompactSpace ↥(AlgebraicGeometry.Proj (homogeneousSubmodule R M))

    The projective spectrum of a finite module is quasi-compact, over any coefficient ring.

    source
    instance TauCeti.SymmetricAlgebra.instIsNoetherianProj (R M : Type u) [CommRing R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [IsNoetherianRing R] :
    AlgebraicGeometry.IsNoetherian (AlgebraicGeometry.Proj (homogeneousSubmodule R M))

    Over a Noetherian ring, the projective spectrum of a finite module is Noetherian.

    source
    instance TauCeti.SymmetricAlgebra.instJacobsonSpaceProj (R M : Type u) [CommRing R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [JacobsonSpace ↥(AlgebraicGeometry.Spec ↧R)] :
    JacobsonSpace ↥(AlgebraicGeometry.Proj (homogeneousSubmodule R M))

    The projective spectrum of a finite module over a Jacobson spectrum is Jacobson.