Multiplicative Jordan–Chevalley decomposition

Over a perfect field, every linear automorphism of a finite-dimensional vector space factors uniquely as the product of a semisimple automorphism and a unipotent automorphism that commute. This is the multiplicative Jordan–Chevalley decomposition.

The construction converts Mathlib's additive decomposition f = n + s into f = s * (1 + s⁻¹n). The semisimple summand s is invertible because it differs from the invertible map f by a commuting nilpotent map. Uniqueness is reduced in the opposite direction to Module.End.isNilpotent_isSemisimple_unique.

This is the general-linear-group case of the Jordan decomposition requested in Layer 4 of the ReductiveGroups roadmap. It is the linear-algebra input for transporting Jordan decompositions through faithful representations of affine algebraic groups.

Main declarations

• LinearMap.GeneralLinearGroup.IsSemisimple: a linear automorphism is semisimple when its underlying endomorphism is semisimple.
• LinearMap.GeneralLinearGroup.IsSemisimple.inv and .zpow: semisimple automorphisms are closed under inverses and integer powers.
• LinearMap.GeneralLinearGroup.IsSemisimple.mul_of_commute: commuting semisimple automorphisms have semisimple product.
• LinearMap.GeneralLinearGroup.jordanDecomposition: the canonical commuting semisimple and unipotent factors.
• LinearMap.GeneralLinearGroup.eq_jordanDecomposition_iff: the existence and uniqueness characterization of those factors.
• LinearMap.GeneralLinearGroup.unipotentPart_eq_semisimplePart_inv_mul: the unipotent factor is the product of the inverse semisimple factor with the original automorphism.
• LinearMap.GeneralLinearGroup.coe_semisimplePart_mem_adjoin: the semisimple factor belongs to the algebra generated by the original automorphism.

References

• T. A. Springer, Linear Algebraic Groups, §2.4.
• Mathlib.LinearAlgebra.JordanChevalley, whose additive existence and uniqueness theorems are used here.

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

A linear automorphism is semisimple if its underlying linear endomorphism is semisimple.

Equations

• g.IsSemisimple = Module.End.IsSemisimple ↑g

theorem LinearMap.GeneralLinearGroup.isSemisimple_def {K : Type u} {V : Type v} [CommRing K] [AddCommGroup V] [Module K V] (g : GeneralLinearGroup K V) : g.IsSemisimple ↔ Module.End.IsSemisimple ↑g

Semisimplicity of a linear automorphism means semisimplicity of its underlying endomorphism.

@[simp]

theorem LinearMap.GeneralLinearGroup.isSemisimple_one {K : Type u} {V : Type v} [CommRing K] [AddCommGroup V] [Module K V] [IsSemisimpleModule K V] : IsSemisimple 1

The identity automorphism is semisimple.

theorem LinearMap.GeneralLinearGroup.IsSemisimple.inv {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {g : GeneralLinearGroup K V} (hg : g.IsSemisimple) : g⁻¹.IsSemisimple

The inverse of a semisimple linear automorphism is semisimple.

@[simp]

theorem LinearMap.GeneralLinearGroup.isSemisimple_inv_iff {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : g⁻¹.IsSemisimple ↔ g.IsSemisimple

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

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

Every natural power of a semisimple linear automorphism is semisimple.

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

Every integer power of a semisimple linear automorphism is semisimple.

theorem LinearMap.GeneralLinearGroup.IsSemisimple.mul_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [PerfectField K] {g h : GeneralLinearGroup K V} (hg : g.IsSemisimple) (hh : h.IsSemisimple) (hcomm : Commute g h) : (g * h).IsSemisimple

The product of two commuting semisimple linear automorphisms is semisimple.

theorem LinearMap.GeneralLinearGroup.isSemisimple_isUnipotent_unique {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {s₁ u₁ s₂ u₂ : GeneralLinearGroup K V} (hs₁ : s₁.IsSemisimple) (hu₁ : u₁.IsUnipotent) (hc₁ : Commute s₁ u₁) (hs₂ : s₂.IsSemisimple) (hu₂ : u₂.IsUnipotent) (hc₂ : Commute s₂ u₂) (h : s₁ * u₁ = s₂ * u₂) : s₁ = s₂ ∧ u₁ = u₂

Two commuting semisimple–unipotent factorizations of the same linear automorphism have the same factors.

noncomputable def LinearMap.GeneralLinearGroup.jordanDecomposition {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : GeneralLinearGroup K V × GeneralLinearGroup K V

The canonical multiplicative Jordan–Chevalley decomposition of a linear automorphism. The first factor is semisimple, the second is unipotent, and the two factors commute.

Equations

• g.jordanDecomposition = Classical.choose ⋯

theorem LinearMap.GeneralLinearGroup.jordanDecomposition_spec {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : g.jordanDecomposition.1.IsSemisimple ∧ g.jordanDecomposition.2.IsUnipotent ∧ Commute g.jordanDecomposition.1 g.jordanDecomposition.2 ∧ g = g.jordanDecomposition.1 * g.jordanDecomposition.2

The canonical Jordan decomposition has the defining semisimple, unipotent, commutation, and product properties.

theorem LinearMap.GeneralLinearGroup.eq_jordanDecomposition_iff {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g s u : GeneralLinearGroup K V) : (s, u) = g.jordanDecomposition ↔ s.IsSemisimple ∧ u.IsUnipotent ∧ Commute s u ∧ g = s * u

A pair is the canonical Jordan decomposition exactly when it is a commuting semisimple–unipotent factorization.

noncomputable def LinearMap.GeneralLinearGroup.semisimplePart {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : GeneralLinearGroup K V

The semisimple factor of the multiplicative Jordan–Chevalley decomposition.

Equations

• g.semisimplePart = g.jordanDecomposition.1

theorem LinearMap.GeneralLinearGroup.semisimplePart_def {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : g.semisimplePart = g.jordanDecomposition.1

The semisimple part is the first factor of the canonical Jordan decomposition.

noncomputable def LinearMap.GeneralLinearGroup.unipotentPart {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : GeneralLinearGroup K V

The unipotent factor of the multiplicative Jordan–Chevalley decomposition.

Equations

• g.unipotentPart = g.jordanDecomposition.2

theorem LinearMap.GeneralLinearGroup.unipotentPart_def {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : g.unipotentPart = g.jordanDecomposition.2

The unipotent part is the second factor of the canonical Jordan decomposition.

theorem LinearMap.GeneralLinearGroup.isSemisimple_semisimplePart {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : g.semisimplePart.IsSemisimple

The semisimple factor is semisimple.

theorem LinearMap.GeneralLinearGroup.isUnipotent_unipotentPart {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : g.unipotentPart.IsUnipotent

The unipotent factor is unipotent.

theorem LinearMap.GeneralLinearGroup.commute_semisimplePart_unipotentPart {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : Commute g.semisimplePart g.unipotentPart

The semisimple and unipotent factors commute.

@[simp]

theorem LinearMap.GeneralLinearGroup.semisimplePart_mul_unipotentPart {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : g.semisimplePart * g.unipotentPart = g

Multiplying the semisimple and unipotent factors recovers the original automorphism.

theorem LinearMap.GeneralLinearGroup.unipotentPart_eq_semisimplePart_inv_mul {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : g.unipotentPart = g.semisimplePart⁻¹ * g

The unipotent factor is the product of the inverse semisimple factor with the original automorphism.

theorem LinearMap.GeneralLinearGroup.jordanDecomposition_map₂ {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {W : Type w} {U : Type x} [AddCommGroup W] [Module K W] [FiniteDimensional K W] [AddCommGroup U] [Module K U] [FiniteDimensional K U] (F : GeneralLinearGroup K V → GeneralLinearGroup K W → GeneralLinearGroup K U) (map_mul : ∀ (a c : GeneralLinearGroup K V) (b d : GeneralLinearGroup K W), F (a * c) (b * d) = F a b * F c d) (map_isSemisimple : ∀ {a : GeneralLinearGroup K V} {b : GeneralLinearGroup K W}, a.IsSemisimple → b.IsSemisimple → (F a b).IsSemisimple) (map_isUnipotent : ∀ {a : GeneralLinearGroup K V} {b : GeneralLinearGroup K W}, a.IsUnipotent → b.IsUnipotent → (F a b).IsUnipotent) (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) : (F g h).jordanDecomposition = (F g.semisimplePart h.semisimplePart, F g.unipotentPart h.unipotentPart)

A binary operation preserving multiplication, semisimplicity, and unipotence preserves the multiplicative Jordan decomposition.

theorem LinearMap.GeneralLinearGroup.coe_semisimplePart_mem_adjoin {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] (g : GeneralLinearGroup K V) : ↑g.semisimplePart ∈ K[↑g]

The semisimple factor of an automorphism is a polynomial in that automorphism.

@[simp]

theorem LinearMap.GeneralLinearGroup.semisimplePart_eq_self {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g : GeneralLinearGroup K V} (hg : g.IsSemisimple) : g.semisimplePart = g

A semisimple automorphism is its own semisimple part.

@[simp]

theorem LinearMap.GeneralLinearGroup.unipotentPart_eq_one_of_isSemisimple {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g : GeneralLinearGroup K V} (hg : g.IsSemisimple) : g.unipotentPart = 1

A semisimple automorphism has trivial unipotent part.

@[simp]

theorem LinearMap.GeneralLinearGroup.semisimplePart_eq_one_of_isUnipotent {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g : GeneralLinearGroup K V} (hg : g.IsUnipotent) : g.semisimplePart = 1

A unipotent automorphism has trivial semisimple part.

@[simp]

theorem LinearMap.GeneralLinearGroup.unipotentPart_eq_self {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g : GeneralLinearGroup K V} (hg : g.IsUnipotent) : g.unipotentPart = g

A unipotent automorphism is its own unipotent part.