Documentation

TauCeti.RingTheory.Nilpotent.Conjugation

Conjugating an integral nilpotent exponential by an intertwining automorphism #

Let V be a module over a ℚ-algebra A, let M ≤ V be an additive subgroup, and let θ : V ≃ₗ[ℚ] V be a ℚ-linear automorphism restricting to a bijection of M. If θ carries the action of x : A to the action of y : A, in the sense that θ (x • v) = y • θ v, then it carries every divided power of x to the corresponding divided power of y, and hence conjugates the base-changed divided-power exponential of x into that of y:

θ_R ∘ E_R(x, t) = E_R(y, t) ∘ θ_R,     θ_R = R ⊗ θ|_M.

The intertwining hypothesis is imposed only on x itself. Divided powers divide by factorials in A, so θ must be ℚ-linear for the transported statement to make sense; the conclusion is nonetheless an identity of integral operators on R ⊗[ℤ] M over an arbitrary commutative ring R.

This is a mechanism used to construct graph automorphisms of Chevalley groups: a symmetry of the ambient Lie-algebra data that permutes the distinguished root vectors conjugates the corresponding root subgroups into one another, permuted the same way. Its application to Kostant root subgroups is in TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/RootSubgroup/NumberedSymmetry.lean.

Main definitions and results #

References #

Transporting powers and divided powers #

source
theorem TauCeti.apply_pow_smul_of_intertwines {B : Type u_3} {X : Type u_4} {Y : Type u_5} [Monoid B] [MulAction B X] [MulAction B Y] (f : X → Y) {x y : B} (hxy : ∀ (v : X), f (x • v) = y • f v) (n : ℕ) (v : X) :
f (x ^ n • v) = y ^ n • f v

A map intertwining the actions of x and y intertwines the actions of their powers.

source
theorem TauCeti.apply_dividedPower_smul_of_intertwines {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module ℚ V] [Module A V] [IsScalarTower ℚ A V] (θ : V →ₗ[ℚ] V) {x y : A} (hxy : ∀ (v : V), θ (x • v) = y • θ v) (n : ℕ) (v : V) :
θ (Associative.dividedPower n x • v) = Associative.dividedPower n y • θ v

A linear map intertwining the actions of x and y intertwines the actions of their divided powers.

The divided powers involve division by factorials, which is why the intertwiner is required to be ℚ-linear rather than merely additive.

Conjugating the base-changed exponential #

source
theorem TauCeti.dividedPower_smul_mem_of_intertwines {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module ℚ V] [Module A V] [IsScalarTower ℚ A V] {S : Type u_2} [SetLike S V] {x y : A} (θ : V ≃ₗ[ℚ] V) (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hxy : ∀ (v : V), θ (x • v) = y • θ v) (hx : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (n : ℕ) (v : V) :
v ∈ M → Associative.dividedPower n y • v ∈ M

An invariant equivalence carries preservation of a set by the divided powers of one element to preservation by the divided powers of an intertwined element.

source
theorem TauCeti.baseChange_invariantRestrict_baseChangeExp {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module ℚ V] [Module A V] [IsScalarTower ℚ A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {x y : A} (θ : V ≃ₗ[ℚ] V) {R : Type v} [CommRing R] [Algebra ℤ R] (M : S) (hθ : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hxy : ∀ (v : V), θ (x • v) = y • θ v) (hx : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) {k : ℕ} (hkx : x ^ k = 0) (hky : y ^ k = 0) (t : R) (z : TensorProduct ℤ R ↥M) :
(LinearEquiv.baseChange ℤ R (↥M) (↥M) (θ.toAddEquiv.invariantRestrict M hθ)) ((baseChangeExp x M hx t) z) = (baseChangeExp y M ⋯ t) ((LinearEquiv.baseChange ℤ R (↥M) (↥M) (θ.toAddEquiv.invariantRestrict M hθ)) z)

Conjugating the base-changed divided-power exponential of x by an intertwiner produces the base-changed divided-power exponential of y, with the same parameter.

Both exponentials are truncated at a common bound k; in the intended application, the second bound follows structurally by conjugating the first nilpotent endomorphism.