Linear actions on the projective spectrum of a symmetric algebra

A linear equivalence induces a contravariant isomorphism of projective spectra. Applying this construction to inverse equivalences gives a homomorphism into scheme automorphisms and hence, for any linear group action, an action by continuous translations. These are the translations used in studying projective orbits and homogeneous spaces.

The convention here is Proj(Sym M): M is the module of linear homogeneous coordinates. For the projective space of lines in a finite locally free module V, take M = V∨ and the contragredient representation. No finite generation or freeness is needed here. The point action is selected explicitly, since a scheme can admit many linear actions. This file constructs individual scheme automorphisms; it does not construct a morphism from a product of schemes representing a family of translations.

The construction combines SymmetricAlgebra.gradedMap with Proj.mapIso.

References

• J. S. Milne, Algebraic Groups (2017), §§7.d–7.f, projective representations and orbits.

noncomputable def AlgebraicGeometry.Proj.symmetricAlgebraMapIso (R : Type u) [CommRing R] {M N : Type u} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) : Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule R N) ≅ Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)

A linear equivalence induces a contravariant isomorphism of projective spectra of symmetric algebras.

Equations

• AlgebraicGeometry.Proj.symmetricAlgebraMapIso R e = AlgebraicGeometry.Proj.mapIso (SymmetricAlgebra.gradedMap R ↑e) (SymmetricAlgebra.gradedMap R ↑e.symm) ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Proj.symmetricAlgebraMapIso_hom (R : Type u) [CommRing R] {M N : Type u} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) : (symmetricAlgebraMapIso R e).hom = map (SymmetricAlgebra.gradedMap R ↑e) ⋯

The forward projective map pulls coordinates back by the given linear equivalence.

@[simp]

theorem AlgebraicGeometry.Proj.symmetricAlgebraMapIso_inv (R : Type u) [CommRing R] {M N : Type u} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) : (symmetricAlgebraMapIso R e).inv = map (SymmetricAlgebra.gradedMap R ↑e.symm) ⋯

The inverse projective map pulls coordinates back by the inverse linear equivalence.

@[simp]

theorem AlgebraicGeometry.Proj.symmetricAlgebraMapIso_symm (R : Type u) [CommRing R] {M N : Type u} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) : symmetricAlgebraMapIso R e.symm = (symmetricAlgebraMapIso R e).symm

Inverting a linear equivalence inverts its projective isomorphism.

@[simp]

theorem AlgebraicGeometry.Proj.symmetricAlgebraMapIso_refl (R : Type u) [CommRing R] {M : Type u} [AddCommMonoid M] [Module R M] : symmetricAlgebraMapIso R (LinearEquiv.refl R M) = CategoryTheory.Iso.refl (Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M))

The identity equivalence induces the identity projective isomorphism.

@[simp]

theorem AlgebraicGeometry.Proj.symmetricAlgebraMapIso_trans (R : Type u) [CommRing R] {M N P : Type u} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (e : M ≃ₗ[R] N) (d : N ≃ₗ[R] P) : symmetricAlgebraMapIso R (e ≪≫ₗ d) = symmetricAlgebraMapIso R d ≪≫ symmetricAlgebraMapIso R e

Projective pullback reverses composition of linear equivalences.

noncomputable def AlgebraicGeometry.Proj.symmetricAlgebraAut (R : Type u) [CommRing R] {M : Type u} [AddCommMonoid M] [Module R M] : (M ≃ₗ[R] M) →* CategoryTheory.Aut (Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M))

Inverse pullback turns linear coordinate automorphisms into scheme automorphisms, with the usual (function-composition) multiplication on both groups.

Equations

• AlgebraicGeometry.Proj.symmetricAlgebraAut R = { toFun := fun (e : M ≃ₗ[R] M) => AlgebraicGeometry.Proj.symmetricAlgebraMapIso R e.symm, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AlgebraicGeometry.Proj.symmetricAlgebraAut_apply (R : Type u) [CommRing R] {M : Type u} [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) : (symmetricAlgebraAut R) e = symmetricAlgebraMapIso R e.symm

The automorphism attached to e is projective pullback by e⁻¹.

@[instance_reducible]

noncomputable def AlgebraicGeometry.Proj.symmetricAlgebraMulAction (R : Type u) [CommRing R] {M : Type u} [AddCommMonoid M] [Module R M] {G : Type v} [Monoid G] (ρ : G →* M ≃ₗ[R] M) : MulAction G ↥(Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M))

A linear group action gives an action on Proj(Sym M) by scheme automorphisms. Install this definition as a local instance to select the action.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Proj.symmetricAlgebra_smul_def (R : Type u) [CommRing R] {M : Type u} [AddCommMonoid M] [Module R M] {G : Type v} [Monoid G] (ρ : G →* M ≃ₗ[R] M) (g : G) (x : ↥(Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M))) : g • x = (symmetricAlgebraMapIso R (ρ g).symm).hom x

The selected point action is the underlying map of the projective scheme automorphism.

theorem AlgebraicGeometry.Proj.symmetricAlgebraMulAction_continuousConstSMul (R : Type u) [CommRing R] {M : Type u} [AddCommMonoid M] [Module R M] {G : Type v} [Monoid G] (ρ : G →* M ≃ₗ[R] M) : ContinuousConstSMul G ↥(Proj (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M))

Every translation of the selected projective action is continuous in the Zariski topology.