Documentation

TauCeti.LinearAlgebra.GeneralLinearGroup.Unipotent

Unipotent linear automorphisms #

A linear automorphism is unipotent when its underlying endomorphism minus the identity is nilpotent. This file records the elementary group-theoretic closure properties needed to use unipotent elements in algebraic groups: inverses, products of commuting elements, powers, and conjugates are unipotent.

It also records the rank-one rigidity statement: over a reduced base, a unipotent automorphism of a free rank-one module is the identity.

Products require commutativity. Indeed, writing g = 1 + x and h = 1 + y, their product is 1 + (x + y + xy); when g and h commute, the three displayed nilpotent endomorphisms commute.

Main declarations #

References #

source
def LinearMap.GeneralLinearGroup.IsUnipotent {K : Type u} {V : Type v} [Semiring K] [AddCommGroup V] [Module K V] (g : GeneralLinearGroup K V) :
Prop

A linear automorphism is unipotent if its difference from the identity is nilpotent.

Equations
Instances For
    source
    theorem LinearMap.GeneralLinearGroup.isUnipotent_def {K : Type u} {V : Type v} [Semiring K] [AddCommGroup V] [Module K V] (g : GeneralLinearGroup K V) :
    g.IsUnipotent ↔ IsNilpotent (↑g - 1)

    Unipotence of a linear automorphism means that its underlying endomorphism minus the identity is nilpotent.

    source
    theorem LinearMap.GeneralLinearGroup.isUnipotent_of_charpoly_eq {F : Type u} {W : Type v} [CommRing F] [AddCommGroup W] [Module F W] [Module.Free F W] [Module.Finite F W] (g : GeneralLinearGroup F W) {n : ℕ} (h : (↑g).charpoly = (Polynomial.X - 1) ^ n) :
    g.IsUnipotent

    An automorphism of a finite free module over a commutative ring is unipotent if its characteristic polynomial is a power of X - 1.

    source
    theorem LinearMap.GeneralLinearGroup.isUnipotent_iff_charpoly {F : Type u} {W : Type v} [CommRing F] [IsDomain F] [AddCommGroup W] [Module F W] [Module.Free F W] [Module.Finite F W] (g : GeneralLinearGroup F W) :
    g.IsUnipotent ↔ (↑g).charpoly = (Polynomial.X - 1) ^ Module.finrank F W

    Over an integral domain, an automorphism of a finite free module is unipotent exactly when its characteristic polynomial is a power of X - 1.

    source
    @[simp]
    theorem LinearMap.GeneralLinearGroup.isUnipotent_one {K : Type u} {V : Type v} [Semiring K] [AddCommGroup V] [Module K V] :
    IsUnipotent 1

    The identity automorphism is unipotent.

    source
    @[simp]
    theorem LinearMap.GeneralLinearGroup.isUnipotent_ofLinearEquiv_iff {K : Type u} {V : Type v} [Semiring K] [AddCommGroup V] [Module K V] (f : V ≃ₗ[K] V) :
    (ofLinearEquiv f).IsUnipotent ↔ IsNilpotent (↑f - 1)

    A linear equivalence is unipotent after conversion to the general linear group exactly when its underlying endomorphism minus the identity is nilpotent.

    source
    theorem LinearMap.GeneralLinearGroup.isUnipotent_congrLinearEquiv_iff {K : Type u} {V : Type v} [Semiring K] [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] (e : V ≃ₗ[K] W) (g : GeneralLinearGroup K V) :
    (ofLinearEquiv (e.symm ≪≫ₗ (g.toLinearEquiv ≪≫ₗ e))).IsUnipotent ↔ g.IsUnipotent

    Unipotence of a linear automorphism is invariant under transport by a linear equivalence.

    source
    theorem LinearMap.GeneralLinearGroup.IsUnipotent.inv {K : Type u} {V : Type v} [Semiring K] [AddCommGroup V] [Module K V] {g : GeneralLinearGroup K V} (hg : g.IsUnipotent) :
    g⁻¹.IsUnipotent

    The inverse of a unipotent linear automorphism is unipotent.

    source
    @[simp]
    theorem LinearMap.GeneralLinearGroup.isUnipotent_inv_iff {K : Type u} {V : Type v} [Semiring K] [AddCommGroup V] [Module K V] (g : GeneralLinearGroup K V) :
    g⁻¹.IsUnipotent ↔ g.IsUnipotent

    A linear automorphism is unipotent if and only if its inverse is unipotent.

    source
    theorem LinearMap.GeneralLinearGroup.IsUnipotent.mul_of_commute {K : Type u} {V : Type v} [Semiring K] [AddCommGroup V] [Module K V] {g h : GeneralLinearGroup K V} (hg : g.IsUnipotent) (hh : h.IsUnipotent) (hcomm : Commute g h) :
    (g * h).IsUnipotent

    The product of two commuting unipotent linear automorphisms is unipotent.

    source
    theorem LinearMap.GeneralLinearGroup.IsUnipotent.pow {K : Type u} {V : Type v} [Semiring K] [AddCommGroup V] [Module K V] {g : GeneralLinearGroup K V} (hg : g.IsUnipotent) (n : ℕ) :
    (g ^ n).IsUnipotent

    Every natural power of a unipotent linear automorphism is unipotent.

    source
    theorem LinearMap.GeneralLinearGroup.IsUnipotent.zpow {K : Type u} {V : Type v} [Semiring K] [AddCommGroup V] [Module K V] {g : GeneralLinearGroup K V} (hg : g.IsUnipotent) (n : ℤ) :
    (g ^ n).IsUnipotent

    Every integer power of a unipotent linear automorphism is unipotent.

    source
    @[simp]
    theorem LinearMap.GeneralLinearGroup.isUnipotent_conj_iff {K : Type u} {V : Type v} [Semiring K] [AddCommGroup V] [Module K V] (g h : GeneralLinearGroup K V) :
    (h * g * h⁻¹).IsUnipotent ↔ g.IsUnipotent

    Unipotence is invariant under conjugation by a linear automorphism.

    source
    theorem LinearMap.GeneralLinearGroup.IsUnipotent.eq_one_of_finrank_eq_one {F : Type u} {W : Type v} [CommRing F] [IsReduced F] [AddCommGroup W] [Module F W] [Module.Free F W] {g : GeneralLinearGroup F W} (hg : g.IsUnipotent) (hdim : Module.finrank F W = 1) :
    g = 1

    A unipotent automorphism of a free rank-one module over a reduced commutative ring is the identity.