Documentation

TauCeti.Algebra.Bialgebra.ComoduleAlgebra.FixedPointIdeal

Fixed-point ideals of comodule algebras over monoid algebras #

Let M be a monoid and let A be a commutative R-algebra with a right R[M]-comodule structure. The coaction decomposes A into weight submodules. This file defines the fixed-point ideal: the ideal generated by the weight submodules of nontrivial weight. An algebra map out of A kills it exactly when the coaction, pushed forward along that map, is trivial (TauCeti.Comodule.fixedPointIdeal_le_ker_iff).

Geometrically, when M is commutative and the coaction is a comodule algebra structure, this is an action of the diagonalizable monoid scheme D(M) = Spec R[M] on X = Spec A. The fixed-point ideal then cuts out the closed subscheme X^{D(M)} of fixed points, and an algebra-valued point of X lies in it exactly when the action of the universal point of D(M) fixes it.

This is not the subalgebra of coinvariants TauCeti.ComoduleAlgebra.coinvariants: in the geometric setting, the coinvariants are the invariant functions on X, the coordinate ring of the quotient, while the fixed-point ideal defines a closed subscheme.

The main result is that the quotient of a formally smooth comodule algebra over R[M] by its fixed-point ideal is formally smooth (TauCeti.ComoduleAlgebra.formallySmooth_quotient_fixedPointIdeal). The proof is the infinitesimal lifting criterion. An algebra map A → C ⧸ J killing the fixed-point ideal, for a square-zero ideal J, lifts to some algebra map φ : A → C, which need not kill it. Its weight-1 component a ↦ φ(a₁) is again an algebra map. Indeed, pushing the coaction forward along φ gives an algebra map A → C[M] (the orbit map of φ) whose coefficient at m is a ↦ φ(aₘ). The coefficients away from 1 lie in J, because the original map killed the fixed-point ideal, so the coefficient at 1 is multiplicative. The weight-1 component kills the nontrivial weight submodules and still lifts the given map.

No hypothesis on M beyond being a monoid, and no Noetherian or finiteness hypothesis on R or A, is needed for this algebraic statement; it is a statement about fixed-point subschemes when M is commutative. The main application is to centralizers of diagonalizable subgroups of smooth affine groups, which are the fixed points of the conjugation action.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.Comodule.fixedPointIdeal (R : Type u) (M : Type v) (A : Type w) [CommRing R] [Monoid M] [CommRing A] [Algebra R A] [Comodule R (MonoidAlgebra R M) A] :
Ideal A

The fixed-point ideal of a commutative algebra A with a comodule structure over R[M]: the ideal generated by the weight submodules of nontrivial weight. When M is commutative and the comodule structure is a comodule algebra structure, it cuts out the closed subscheme of fixed points of the action of D(M) on Spec A.

Instances For
    source
    theorem TauCeti.Comodule.weightSpace_subset_fixedPointIdeal {R : Type u} {M : Type v} {A : Type w} [CommRing R] [Monoid M] [CommRing A] [Algebra R A] [Comodule R (MonoidAlgebra R M) A] {m : M} (hm : m ≠ 1) :
    ↑(weightSpace R M A m) ⊆ ↑(fixedPointIdeal R M A)

    A weight submodule of nontrivial weight lies in the fixed-point ideal.

    source
    theorem TauCeti.Comodule.weightProj_mem_fixedPointIdeal {R : Type u} {M : Type v} {A : Type w} [CommRing R] [Monoid M] [CommRing A] [Algebra R A] [Comodule R (MonoidAlgebra R M) A] {m : M} (hm : m ≠ 1) (a : A) :
    (weightProj R M A m) a ∈ fixedPointIdeal R M A

    A weight component of nontrivial weight lies in the fixed-point ideal.

    source
    theorem TauCeti.Comodule.sub_weightProj_one_mem_fixedPointIdeal {R : Type u} {M : Type v} {A : Type w} [CommRing R] [Monoid M] [CommRing A] [Algebra R A] [Comodule R (MonoidAlgebra R M) A] (a : A) :
    a - (weightProj R M A 1) a ∈ fixedPointIdeal R M A

    Modulo the fixed-point ideal, a function agrees with its weight-1 component.

    source
    theorem TauCeti.Comodule.fixedPointIdeal_le_ker_iff {R : Type u} {M : Type v} {A : Type w} [CommRing R] [Monoid M] [CommRing A] [Algebra R A] [Comodule R (MonoidAlgebra R M) A] {B : Type x} [CommRing B] [Algebra R B] (f : A →ₐ[R] B) :
    fixedPointIdeal R M A ≤ RingHom.ker f ↔ ∀ (a : A), (Algebra.TensorProduct.map f (AlgHom.id R (MonoidAlgebra R M))) (coact a) = f a ⊗ₜ[R] 1

    An algebra map kills the fixed-point ideal exactly when it is a fixed point of the coaction: pushing the coaction forward along it gives the trivial coaction a ↦ f a ⊗ 1.

    source
    instance TauCeti.ComoduleAlgebra.formallySmooth_quotient_fixedPointIdeal {R : Type u} {M : Type v} {A : Type w} [CommRing R] [Monoid M] [CommRing A] [Algebra R A] [ComoduleAlgebra R (MonoidAlgebra R M) A] [Algebra.FormallySmooth R A] :
    Algebra.FormallySmooth R (A ⧸ Comodule.fixedPointIdeal R M A)

    The quotient of a formally smooth comodule algebra over R[M] by its fixed-point ideal is formally smooth. For commutative M, this says that the fixed points of a diagonalizable action on a formally smooth affine scheme form a formally smooth closed subscheme. No hypothesis on the monoid M or on the base ring is needed.