The additive group is unipotent

Let R be a commutative ring and let R[x] = SymmetricAlgebra R R be the coordinate Hopf algebra of the additive group 𝔾ₐ, with primitive generator x = ι(1). This file proves that every point of 𝔾ₐ is unipotent: for every commutative R-algebra A, every point g : R[x] →ₐ[R] A acts on the scalar extension of every finitely generated comodule by an automorphism whose difference from the identity is nilpotent. Over a field this says that 𝔾ₐ acts unipotently in every finite-dimensional representation, which is the geometric definition of a unipotent group; together with the smoothness of R[x] it exhibits 𝔾ₐ as a smooth unipotent affine algebraic group.

The proof is the classical divided-power argument. The monomials xⁿ form a basis of R[x] (monomialBasis), so the coaction of a comodule V can be written ρ v = ∑ₙ Nₙ v ⊗ xⁿ for a family of endomorphisms Nₙ of V (coactComponent), only finitely many of which are nonzero on any given vector. The counit axiom says N₀ = id, and coassociativity, combined with the binomial expansion Δ(xⁿ) = ∑ₖ (n choose k) xᵏ ⊗ xⁿ⁻ᵏ of the primitive generator, says that Nᵢ ∘ Nⱼ = (i + j choose i) Nᵢ₊ⱼ. A point g then acts by a ⊗ v ↦ ∑ᵢ a (g x)ⁱ ⊗ Nᵢ v, so its difference from the identity involves only the components of positive index. Filtering V by the submodules Vₚ on which every Nᵢ with i > p vanishes (coactFiltration), that difference carries Vₚ into Vₚ₋₁ and annihilates V₀; since a finitely generated comodule is V_d for some d, the (d + 1)-st power of the difference vanishes.

Main definitions

• TauCeti.AdditiveGroup.monomialBasis: the monomials xⁿ as a basis of R[x], with TauCeti.AdditiveGroup.coeff its coordinate functionals.
• TauCeti.AdditiveGroup.coactComponent: the n-th divided-power component Nₙ of the coaction of an R[x]-comodule, and TauCeti.AdditiveGroup.coactDecomposition the family of all of them.
• TauCeti.AdditiveGroup.coactFiltration: the divided-power filtration of an R[x]-comodule.

Main results

• TauCeti.AdditiveGroup.coactComponent_coactComponent: the divided-power components compose by the binomial rule Nᵢ ∘ Nⱼ = (i + j choose i) Nᵢ₊ⱼ.
• TauCeti.AdditiveGroup.exists_coactFiltration_eq_top: the filtration of a finitely generated comodule is exhausted at a finite stage.
• TauCeti.AdditiveGroup.exists_ne_zero_coact_eq_tmul_one: Kolchin's theorem for 𝔾ₐ, every nonzero comodule over R[x] contains a nonzero fixed vector.
• TauCeti.AdditiveGroup.isNilpotent_endOfPoint_sub_one and TauCeti.AdditiveGroup.isUnipotentPoint: every point of 𝔾ₐ is unipotent.
• TauCeti.AdditiveGroup.smoothUnipotentCommHopfAlgProperty_coordinateHopfAlgebra: 𝔾ₐ over a field is a smooth unipotent affine group, together with the geometric-point form TauCeti.AdditiveGroup.geometricallyUnipotentPointsCommHopfAlgProperty_coordinateHopfAlgebra.

Implementation notes

The component calculations reuse the coefficient-functional API in TauCeti.Algebra.Coalgebra.Comodule.Basic. The same API underlies the weight decomposition of a comodule over a monoid algebra. The coalgebra-specific calculations differ: group-like basis elements give orthogonal idempotents there, while the primitive generator here gives the binomial composition rule and hence a filtration rather than a splitting.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2 and I.7.8.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §8.3.
• T. A. Springer, Linear Algebraic Groups, §2.4.

noncomputable def TauCeti.AdditiveGroup.monomialBasis (R : Type u) [CommSemiring R] : Module.Basis ℕ R (SymmetricAlgebra R R)

The monomials xⁿ in the coordinate x = ι(1) form a basis of the coordinate algebra R[x] = SymmetricAlgebra R R of the additive group.

Equations

• TauCeti.AdditiveGroup.monomialBasis R = (Module.Basis.singleton Unit R).symmetricAlgebra.reindex (Finsupp.uniqueEquiv ())

@[simp]

theorem TauCeti.AdditiveGroup.monomialBasis_apply (R : Type u) [CommSemiring R] (n : ℕ) : (monomialBasis R) n = (SymmetricAlgebra.ι R R) 1 ^ n

noncomputable def TauCeti.AdditiveGroup.coeff (R : Type u) [CommSemiring R] (n : ℕ) : SymmetricAlgebra R R →ₗ[R] R

The n-th coefficient functional of the coordinate algebra of 𝔾ₐ: the coefficient of the monomial xⁿ.

Equations

• TauCeti.AdditiveGroup.coeff R n = (TauCeti.AdditiveGroup.monomialBasis R).coord n

@[simp]

theorem TauCeti.AdditiveGroup.coeff_pow (R : Type u) [CommSemiring R] (m n : ℕ) : (coeff R n) ((SymmetricAlgebra.ι R R) 1 ^ m) = if m = n then 1 else 0

theorem TauCeti.AdditiveGroup.coeff_zero_eq_counit (R : Type u) [CommSemiring R] : coeff R 0 = CoalgebraStruct.counit

The coefficient of x⁰ is the counit.

noncomputable def TauCeti.AdditiveGroup.coactComponent (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] (n : ℕ) : V →ₗ[R] V

The n-th divided-power component of the coaction of a comodule over the coordinate algebra of 𝔾ₐ: writing the coaction as ρ v = ∑ₙ Nₙ v ⊗ xⁿ, this is Nₙ.

Equations

• TauCeti.AdditiveGroup.coactComponent R V n = TauCeti.Comodule.coactComponent (TauCeti.AdditiveGroup.coeff R n)

theorem TauCeti.AdditiveGroup.coactComponent_apply (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] (n : ℕ) (v : V) : (coactComponent R V n) v = (coeff R n).tensorComponent (Comodule.coact v)

@[simp]

theorem TauCeti.AdditiveGroup.coactComponent_zero (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] : coactComponent R V 0 = LinearMap.id

The zeroth divided-power component is the identity: this is the counit axiom.

@[simp]

theorem TauCeti.AdditiveGroup.coactComponent_coactComponent (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] (i j : ℕ) (v : V) : (coactComponent R V i) ((coactComponent R V j) v) = (i + j).choose i • (coactComponent R V (i + j)) v

The divided-power components compose by the binomial rule Nᵢ ∘ Nⱼ = (i + j choose i) Nᵢ₊ⱼ. This is coassociativity of the coaction, read off in the monomial basis.

noncomputable def TauCeti.AdditiveGroup.coactDecomposition (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] : V →ₗ[R] ℕ →₀ V

The divided-power decomposition of the coaction, as a finitely supported family: writing ρ v = ∑ₙ Nₙ v ⊗ xⁿ, this collects the vectors Nₙ v, only finitely many of which are nonzero.

Equations

• TauCeti.AdditiveGroup.coactDecomposition R V = ↑(TensorProduct.equivFinsuppOfBasisRight (TauCeti.AdditiveGroup.monomialBasis R)) ∘ₗ TauCeti.Comodule.coact

@[simp]

theorem TauCeti.AdditiveGroup.coactDecomposition_apply (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] (v : V) (n : ℕ) : ((coactDecomposition R V) v) n = (coactComponent R V n) v

theorem TauCeti.AdditiveGroup.coact_eq_sum (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] (v : V) : Comodule.coact v = ((coactDecomposition R V) v).sum fun (i : ℕ) (w : V) => w ⊗ₜ[R] ((SymmetricAlgebra.ι R R) 1 ^ i)

The coaction is recovered from its divided-power components: ρ v = ∑ₙ Nₙ v ⊗ xⁿ.

noncomputable def TauCeti.AdditiveGroup.coactFiltration (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] (p : ℕ) : Submodule R V

The divided-power filtration of a 𝔾ₐ-comodule: the p-th step consists of the vectors whose divided-power components above p all vanish. Equivalently, it is the preimage under the coaction of V ⊗ (R ⊕ Rx ⊕ ⋯ ⊕ Rxᵖ).

Equations

• TauCeti.AdditiveGroup.coactFiltration R V p = ⨅ i ∈ Set.Ioi p, (TauCeti.AdditiveGroup.coactComponent R V i).ker

@[simp]

theorem TauCeti.AdditiveGroup.mem_coactFiltration (R : Type u) [CommSemiring R] {V : Type v} [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] {p : ℕ} {v : V} : v ∈ coactFiltration R V p ↔ ∀ (i : ℕ), p < i → (coactComponent R V i) v = 0

theorem TauCeti.AdditiveGroup.coactFiltration_mono (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] {p q : ℕ} (h : p ≤ q) : coactFiltration R V p ≤ coactFiltration R V q

The filtration is monotone.

theorem TauCeti.AdditiveGroup.coactComponent_mem_coactFiltration (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] {p i : ℕ} (hi : 0 < i) {v : V} (hv : v ∈ coactFiltration R V (p + 1)) : (coactComponent R V i) v ∈ coactFiltration R V p

The positive divided-power components lower the filtration by one step.

theorem TauCeti.AdditiveGroup.exists_coactFiltration_eq_top (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] [Module.Finite R V] : ∃ (d : ℕ), coactFiltration R V d = ⊤

The divided-power filtration of a finitely generated comodule is exhaustive. Each vector has only finitely many nonzero divided-power components, and finitely many generators bound them all at once.

theorem TauCeti.AdditiveGroup.mem_coactFiltration_zero_iff (R : Type u) [CommSemiring R] {V : Type v} [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] {v : V} : v ∈ coactFiltration R V 0 ↔ Comodule.coact v = v ⊗ₜ[R] 1

The zeroth step of the divided-power filtration is the set of fixed vectors: a vector has coaction v ↦ v ⊗ 1 exactly when all its positive divided-power components vanish.

theorem TauCeti.AdditiveGroup.exists_ne_zero_coact_eq_tmul_one (R : Type u) [CommSemiring R] {V : Type v} [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] {v : V} (hv : v ≠ 0) : ∃ (w : V), w ≠ 0 ∧ Comodule.coact w = w ⊗ₜ[R] 1

Kolchin's theorem for 𝔾ₐ: every nonzero vector of a comodule over the coordinate algebra of the additive group produces a nonzero fixed vector, over an arbitrary base and with no finiteness hypothesis. The witness is the top nonvanishing divided-power component Nᵢ v: by the binomial composition rule each further component of it is a component of v of strictly larger index, which vanishes by maximality.

theorem TauCeti.AdditiveGroup.endOfPoint_tmul_eq_sum (R : Type u) [CommSemiring R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] {A : Type w} [CommSemiring A] [Algebra R A] (g : SymmetricAlgebra R R →ₐ[R] A) (a : A) (v : V) : (Comodule.endOfPoint V g) (a ⊗ₜ[R] v) = ((coactDecomposition R V) v).sum fun (i : ℕ) (w : V) => (a * g ((SymmetricAlgebra.ι R R) 1) ^ i) ⊗ₜ[R] w

A point of 𝔾ₐ acts through the divided-power components of the coaction. A point with parameter g x sends a ⊗ v to ∑ᵢ a (g x)ⁱ ⊗ Nᵢ v.

theorem TauCeti.AdditiveGroup.endOfPoint_sub_one_tmul (R : Type u) [CommRing R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] {A : Type w} [CommRing A] [Algebra R A] (g : SymmetricAlgebra R R →ₐ[R] A) (a : A) (v : V) : (Comodule.endOfPoint V g - 1) (a ⊗ₜ[R] v) = ∑ i ∈ ((coactDecomposition R V) v).support.erase 0, (a * g ((SymmetricAlgebra.ι R R) 1) ^ i) ⊗ₜ[R] (coactComponent R V i) v

The action of a point, minus the identity, involves only the positive divided-power components.

theorem TauCeti.AdditiveGroup.endOfPoint_sub_one_tmul_eq_zero (R : Type u) [CommRing R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] {A : Type w} [CommRing A] [Algebra R A] (g : SymmetricAlgebra R R →ₐ[R] A) (a : A) {v : V} (hv : v ∈ coactFiltration R V 0) : (Comodule.endOfPoint V g - 1) (a ⊗ₜ[R] v) = 0

A point acts as the identity on the bottom step of the filtration.

theorem TauCeti.AdditiveGroup.endOfPoint_sub_one_tmul_mem (R : Type u) [CommRing R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] {A : Type w} [CommRing A] [Algebra R A] (g : SymmetricAlgebra R R →ₐ[R] A) (a : A) {p : ℕ} {v : V} (hv : v ∈ coactFiltration R V (p + 1)) : (Comodule.endOfPoint V g - 1) (a ⊗ₜ[R] v) ∈ Submodule.baseChange A (coactFiltration R V p)

A point moves the base change of one step of the filtration into the base change of the previous step.

theorem TauCeti.AdditiveGroup.pow_endOfPoint_sub_one_apply_eq_zero (R : Type u) [CommRing R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] {A : Type w} [CommRing A] [Algebra R A] (g : SymmetricAlgebra R R →ₐ[R] A) (p : ℕ) {z : TensorProduct R A V} (hz : z ∈ Submodule.baseChange A (coactFiltration R V p)) : ((Comodule.endOfPoint V g - 1) ^ (p + 1)) z = 0

The action of a point is unipotent on each step of the filtration: on the base change of the p-th step, the (p + 1)-st power of the action minus the identity vanishes.

theorem TauCeti.AdditiveGroup.isNilpotent_endOfPoint_sub_one (R : Type u) [CommRing R] (V : Type v) [AddCommMonoid V] [Module R V] [Comodule R (SymmetricAlgebra R R) V] {A : Type w} [CommRing A] [Algebra R A] [Module.Finite R V] (g : SymmetricAlgebra R R →ₐ[R] A) : IsNilpotent (Comodule.endOfPoint V g - 1)

Every point of 𝔾ₐ acts unipotently on every finitely generated comodule.

theorem TauCeti.AdditiveGroup.isUnipotentPoint (R : Type u) [CommRing R] {A : Type w} [CommRing A] [Algebra R A] (g : WithConv (SymmetricAlgebra R R →ₐ[R] A)) : HopfAlgebra.IsUnipotentPoint g

Every point of the additive group is unipotent. A point of 𝔾ₐ valued in a commutative R-algebra acts on every finitely generated comodule, over a field on every finite-dimensional representation, by a unipotent automorphism.

theorem TauCeti.AdditiveGroup.geometricallyUnipotentPointsCommHopfAlgProperty_coordinateHopfAlgebra (k : Type u) [Field k] : geometricallyUnipotentPointsCommHopfAlgProperty k (coordinateHopfAlgebra k)

The additive group has only unipotent geometric points.

theorem TauCeti.AdditiveGroup.smoothUnipotentCommHopfAlgProperty_coordinateHopfAlgebra (k : Type u) [Field k] : smoothUnipotentCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.of k (SymmetricAlgebra k k))

The additive group 𝔾ₐ is a smooth unipotent affine group.