Base change of integral nilpotent exponentials

Let V be an A-module for a ℚ-algebra A, let M ≤ V be an additive subgroup, and suppose that every divided power of an element x : A preserves M. Restricting those divided powers gives integral endomorphisms of M. After extension of scalars to any commutative ring R, the finite sum

E_R(t) = ∑ n, tⁿ (x⁽ⁿ⁾|_M)_R

is therefore defined without dividing by a factorial in R. The divided-power multiplication law proves E_R(t + u) = E_R(t) E_R(u), so E_R(-t) is its inverse. Consequently the additive group of every commutative ring acts on R ⊗[ℤ] M by R-linear automorphisms.

This is the base-ring-valued form of a root subgroup action in the Chevalley--Demazure construction, and an arbitrary-ring analogue of the earlier integer exponential from TauCeti/RingTheory/Nilpotent/Exp.lean. The new content here is that the integral divided-power operators make the same family available over every parameter ring, even when the ring has positive characteristic.

Main definitions and results

• TauCeti.integralDividedPower: a divided-power operator restricted to an invariant additive subgroup.
• TauCeti.mul_integralDividedPower: multiplication formula for restricted divided powers.
• TauCeti.baseChange_integralDividedPower_eq_zero_of_le: a restricted divided power vanishes on base change above the nilpotency index.
• TauCeti.baseChangeExp: the finite divided-power exponential on R ⊗[ℤ] M for an element of A.
• TauCeti.map_baseChangeExp: naturality of the exponential under a map of parameter rings.
• TauCeti.baseChangeExp_add: its one-parameter group law.
• TauCeti.baseChangeExpLinearEquiv: the resulting linear automorphism.
• TauCeti.baseChangeExpHom: the additive one-parameter subgroup over R.
• TauCeti.integralUnitRestrict: a unit of A preserving M restricted to an integral automorphism of M.
• TauCeti.dividedPower_conj_smul_mem: conjugating by such a unit preserves the stability of M under divided powers.
• TauCeti.baseChangeExp_intCast: at an integer parameter the exponential is the base change of a single integral automorphism.
• TauCeti.baseChange_integralUnitRestrict_conj_baseChangeExp: conjugating a one-parameter subgroup by such a unit gives the one-parameter subgroup of the conjugated element.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§26--27.
• R. W. Carter, Simple Groups of Lie Type, §4.4.
• The proof of sum_pow_smul_mul_sum_pow_smul adapts Mathlib's IsNilpotent.exp_add_of_commute in Mathlib/RingTheory/Nilpotent/Exp.lean (Janos Wolosz), replacing powers/factorials by integral divided powers.

Integral divided-power operators

noncomputable def TauCeti.integralDividedPower {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (x : A) (M : S) (n : ℕ) (hM : ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) : Module.End ℤ ↥M

The restriction to M of the n-th divided power of x, given that this divided power maps M into M.

This is an integral linear map: the rational division by n! has already taken place in the ambient representation, while the preservation hypothesis says that its value lands back in M.

Equations

• TauCeti.integralDividedPower x M n hM = { toFun := fun (v : ↥M) => ⟨TauCeti.Associative.dividedPower n x • ↑v, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.coe_integralDividedPower_apply {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (x : A) (M : S) (n : ℕ) (hM : ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (v : ↥M) : ↑((integralDividedPower x M n hM) v) = Associative.dividedPower n x • ↑v

The value of integralDividedPower x M n hM v coerced to V is Associative.dividedPower n x • v.

@[simp]

theorem TauCeti.integralDividedPower_zero {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (x : A) (M : S) (hM0 : ∀ v ∈ M, Associative.dividedPower 0 x • v ∈ M) : integralDividedPower x M 0 hM0 = 1

The zeroth restricted divided power is the identity.

theorem TauCeti.mul_integralDividedPower {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (x : A) (M : S) (m n : ℕ) (hm : ∀ v ∈ M, Associative.dividedPower m x • v ∈ M) (hn : ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hmn : ∀ v ∈ M, Associative.dividedPower (m + n) x • v ∈ M) : integralDividedPower x M m hm * integralDividedPower x M n hn = (m + n).choose m • integralDividedPower x M (m + n) hmn

Multiplication formula for restricted divided powers.

theorem TauCeti.integralDividedPower_eq_zero_of_le {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (x : A) (M : S) (n : ℕ) (hn : ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) {k : ℕ} (hk : x ^ k = 0) (hkn : k ≤ n) : integralDividedPower x M n hn = 0

The restricted divided power vanishes for degrees greater than or equal to a nilpotency bound.

Restricting a unit to an invariant additive subgroup

noncomputable def TauCeti.integralUnitRestrict {A : Type u_1} [Ring A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (u : Aˣ) (M : S) (hu : ∀ v ∈ M, ↑u • v ∈ M) (hu' : ∀ v ∈ M, ↑u⁻¹ • v ∈ M) : ↥M ≃ₗ[ℤ] ↥M

The restriction to M of the action of a unit of A that preserves M together with its inverse, as an integral linear automorphism.

Scalar multiplication by a ring element is additive, and an additive map of abelian groups is exactly a ℤ-linear map, so no divisibility is involved: this automorphism survives base change to an arbitrary commutative ring.

Equations

• TauCeti.integralUnitRestrict u M hu hu' = { toFun := fun (v : ↥M) => ⟨↑u • ↑v, ⋯⟩, invFun := fun (v : ↥M) => ⟨↑u⁻¹ • ↑v, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }.toIntLinearEquiv

@[simp]

theorem TauCeti.coe_integralUnitRestrict_apply {A : Type u_1} [Ring A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (u : Aˣ) (M : S) (hu : ∀ v ∈ M, ↑u • v ∈ M) (hu' : ∀ v ∈ M, ↑u⁻¹ • v ∈ M) (v : ↥M) : ↑((integralUnitRestrict u M hu hu') v) = ↑u • ↑v

@[simp]

theorem TauCeti.coe_integralUnitRestrict_symm_apply {A : Type u_1} [Ring A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (u : Aˣ) (M : S) (hu : ∀ v ∈ M, ↑u • v ∈ M) (hu' : ∀ v ∈ M, ↑u⁻¹ • v ∈ M) (v : ↥M) : ↑((integralUnitRestrict u M hu hu').symm v) = ↑u⁻¹ • ↑v

theorem TauCeti.dividedPower_conj_smul_mem {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] (x : A) (M : S) (u : Aˣ) (hu : ∀ v ∈ M, ↑u • v ∈ M) (hu' : ∀ v ∈ M, ↑u⁻¹ • v ∈ M) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (n : ℕ) (v : V) : v ∈ M → Associative.dividedPower n (↑u * x * ↑u⁻¹) • v ∈ M

A unit preserving M together with its inverse also transports the stability of M under the divided powers of x to stability under the divided powers of the conjugate u x u⁻¹.

Conjugation passes through a divided power, so the conjugated operator acts by u⁻¹, then a divided power of x, then u, and each of the three maps M into M.

noncomputable def TauCeti.integralExpZSMul {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : ℤ) : ↥M ≃ₗ[ℤ] ↥M

The restriction to M of the exponential exp (t • x) of an integral multiple of a nilpotent element whose divided powers preserve M.

The coefficients of the divided-power expansion of exp (t • x) are the integers tⁿ, so this automorphism is defined over ℤ even though the exponential itself divides by factorials.

Equations

• TauCeti.integralExpZSMul x M hM hx t = TauCeti.integralUnitRestrict (TauCeti.nilpotentExpUnit ⋯) M ⋯ ⋯

@[simp]

theorem TauCeti.coe_integralExpZSMul_apply {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : ℤ) (v : ↥M) : ↑((integralExpZSMul x M hM hx t) v) = IsNilpotent.exp (t • x) • ↑v

@[simp]

theorem TauCeti.coe_integralExpZSMul_symm_apply {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : ℤ) (v : ↥M) : ↑((integralExpZSMul x M hM hx t).symm v) = IsNilpotent.exp (-(t • x)) • ↑v

The inverse of the integral exponential is the exponential of the negated element.

theorem TauCeti.integralDividedPower_neg_of_even {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (x : A) (M : S) {n : ℕ} (hn : Even n) (hM' : ∀ v ∈ M, Associative.dividedPower n (-x) • v ∈ M) (hM : ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) : integralDividedPower (-x) M n hM' = integralDividedPower x M n hM

Negating the element leaves the even restricted divided powers unchanged.

theorem TauCeti.integralDividedPower_neg_of_odd {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (x : A) (M : S) {n : ℕ} (hn : Odd n) (hM' : ∀ v ∈ M, Associative.dividedPower n (-x) • v ∈ M) (hM : ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) : integralDividedPower (-x) M n hM' = -integralDividedPower x M n hM

Negating the element negates the odd restricted divided powers.

theorem TauCeti.integralExpZSMul_eq_sum {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) {k : ℕ} (hk : x ^ k = 0) (t : ℤ) : ↑(integralExpZSMul x M hM hx t) = ∑ n ∈ Finset.range k, t ^ n • integralDividedPower x M n ⋯

The integral exponential expanded over any truncation bound.

The divided-power exponential after base change

noncomputable def TauCeti.baseChangeExp {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (t : R) : Module.End R (TensorProduct ℤ R ↥M)

The finite integral divided-power exponential on the scalar extension R ⊗[ℤ] M for an element x.

Although x acts on a rational vector space, this definition uses only the integral operators on M and therefore makes sense over an arbitrary commutative parameter ring R.

Equations

• TauCeti.baseChangeExp x M hM t = ∑ n ∈ Finset.range (nilpotencyClass x), t ^ n • LinearMap.baseChange R (TauCeti.integralDividedPower x M n ⋯)

@[simp]

theorem TauCeti.baseChangeExp_tmul {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (t r : R) (v : ↥M) : (baseChangeExp x M hM t) (r ⊗ₜ[ℤ] v) = ∑ n ∈ Finset.range (nilpotencyClass x), (t ^ n * r) ⊗ₜ[ℤ] (integralDividedPower x M n ⋯) v

The base-changed exponential acts on a pure tensor by the expected finite divided-power formula.

theorem TauCeti.map_baseChangeExp_algHom {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] {T : Type u_3} [CommRing T] [Algebra ℤ T] (φ : R →ₐ[ℤ] T) (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (t : R) (z : TensorProduct ℤ R ↥M) : (TensorProduct.map φ.toLinearMap LinearMap.id) ((baseChangeExp x M hM t) z) = (baseChangeExp x M hM (φ t)) ((TensorProduct.map φ.toLinearMap LinearMap.id) z)

The base-changed divided-power exponential is natural under maps of parameter rings carrying explicit ℤ-algebra structures.

theorem TauCeti.baseChange_integralDividedPower_eq_zero_of_le {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) {n : ℕ} (hn : ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) {k : ℕ} (hk : x ^ k = 0) (hkn : k ≤ n) : LinearMap.baseChange R (integralDividedPower x M n hn) = 0

A restricted divided power vanishes on base change above the nilpotency index. If x ^ k = 0 and k ≤ n, the base change of integralDividedPower x M n is the zero map.

This is the truncation fact every finite expansion of baseChangeExp needs: it is what makes the terms outside the truncation bound drop out.

theorem TauCeti.forall_baseChange_integralDividedPower_eq_zero_of_le {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) {k : ℕ} (hk : x ^ k = 0) (n : ℕ) : k ≤ n → LinearMap.baseChange R (integralDividedPower x M n ⋯) = 0

The base-changed divided powers vanish from the nilpotency index on. The ∀-form of baseChange_integralDividedPower_eq_zero_of_le, stated for the family hM : ∀ n, ∀ v ∈ M, Associative.dividedPower n x • v ∈ M that baseChangeExp carries, rather than for one index at a time.

This is the hzero shape that sum_pow_smul_mul_sum_pow_smul and the normal-ordering combinators consume: each wants the vanishing as one hypothesis about the whole tail, supplied once per element, before case-splitting on which factor of a reordered product falls outside its truncation bound.

theorem TauCeti.baseChangeExp_of_pow_eq_zero {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) {k : ℕ} (hk : x ^ k = 0) (t : R) : baseChangeExp x M hM t = ∑ n ∈ Finset.range k, t ^ n • LinearMap.baseChange R (integralDividedPower x M n ⋯)

The base-changed exponential expanded over any truncation bound k satisfying x ^ k = 0.

theorem TauCeti.baseChangeExp_tmul_of_pow_eq_zero {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) {k : ℕ} (hk : x ^ k = 0) (t r : R) (v : ↥M) : (baseChangeExp x M hM t) (r ⊗ₜ[ℤ] v) = ∑ n ∈ Finset.range k, (t ^ n * r) ⊗ₜ[ℤ] (integralDividedPower x M n ⋯) v

The base-changed exponential acts on a pure tensor by the divided-power formula over any truncation bound k satisfying x ^ k = 0.

theorem TauCeti.baseChangeExp_tmul_of_pow_smul_eq_zero {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) {k : ℕ} (t r : R) (v : ↥M) (hk : x ^ k • ↑v = 0) : (baseChangeExp x M hM t) (r ⊗ₜ[ℤ] v) = ∑ n ∈ Finset.range k, (t ^ n * r) ⊗ₜ[ℤ] (integralDividedPower x M n ⋯) v

The base-changed exponential on a pure tensor may be truncated at any power that annihilates that tensor's module vector. This only requires pointwise nilpotence at v; the separate IsNilpotent x hypothesis supplies a global bound used to expand baseChangeExp.

@[simp]

theorem TauCeti.baseChangeExp_add {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t u : R) : baseChangeExp x M hM (t + u) = baseChangeExp x M hM t * baseChangeExp x M hM u

The integral divided-power exponential satisfies the additive one-parameter group law over every commutative base ring.

@[simp]

theorem TauCeti.baseChangeExp_zero {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) : baseChangeExp x M hM 0 = 1

The base-changed divided-power exponential at zero is the identity.

noncomputable def TauCeti.baseChangeExpLinearEquiv {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : R) : TensorProduct ℤ R ↥M ≃ₗ[R] TensorProduct ℤ R ↥M

The base-changed divided-power exponential as a linear equivalence, with inverse given by the negative parameter.

Equations

• TauCeti.baseChangeExpLinearEquiv x M hM hx t = LinearEquiv.ofLinearMap (TauCeti.baseChangeExp x M hM t) (TauCeti.baseChangeExp x M hM (-t)) ⋯ ⋯

@[simp]

theorem TauCeti.baseChangeExpLinearEquiv_toLinearMap {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : R) : ↑(baseChangeExpLinearEquiv x M hM hx t) = baseChangeExp x M hM t

The linear map underlying baseChangeExpLinearEquiv is baseChangeExp.

@[simp]

theorem TauCeti.coe_baseChangeExpLinearEquiv {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : R) : ⇑(baseChangeExpLinearEquiv x M hM hx t) = ⇑(baseChangeExp x M hM t)

Coercing baseChangeExpLinearEquiv to a function yields baseChangeExp.

@[simp]

theorem TauCeti.baseChangeExpLinearEquiv_symm {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : R) : (baseChangeExpLinearEquiv x M hM hx t).symm = baseChangeExpLinearEquiv x M hM hx (-t)

The inverse of baseChangeExpLinearEquiv is given by the negative parameter.

noncomputable def TauCeti.baseChangeExpHom {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) : Multiplicative R →* TensorProduct ℤ R ↥M ≃ₗ[R] TensorProduct ℤ R ↥M

The additive group of a commutative ring acts on the scalar extension of a divided-power-stable additive subgroup by the integral nilpotent exponential.

Equations

• TauCeti.baseChangeExpHom x M hM hx = { toFun := fun (t : Multiplicative R) => TauCeti.baseChangeExpLinearEquiv x M hM hx (Multiplicative.toAdd t), map_one' := ⋯, map_mul' := ⋯ }

theorem TauCeti.baseChangeExpHom_toLinearMap {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : Multiplicative R) : ↑((baseChangeExpHom x M hM hx) t) = baseChangeExp x M hM (Multiplicative.toAdd t)

The linear map underlying the base-changed one-parameter subgroup is the corresponding divided-power exponential.

@[simp]

theorem TauCeti.baseChangeExpHom_apply {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : Multiplicative R) : (baseChangeExpHom x M hM hx) t = baseChangeExpLinearEquiv x M hM hx (Multiplicative.toAdd t)

Evaluating baseChangeExpHom at t yields baseChangeExpLinearEquiv at toAdd t.

theorem TauCeti.coe_baseChangeExpHom {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : Multiplicative R) : ⇑((baseChangeExpHom x M hM hx) t) = ⇑(baseChangeExp x M hM (Multiplicative.toAdd t))

Coercing baseChangeExpHom to a function yields baseChangeExp.

theorem TauCeti.baseChangeExp_congr {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] {x y : A} (hxy : x = y) (M : S) (hMx : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hMy : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n y • v ∈ M) (t : R) : baseChangeExp x M hMx t = baseChangeExp y M hMy t

The base-changed exponential depends only on the element, not on the stability proof.

theorem TauCeti.baseChangeExp_neg {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM' : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n (-x) • v ∈ M) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : R) : baseChangeExp (-x) M hM' t = baseChangeExp x M hM (-t)

Negating the element inverts the parameter: E_{-x}(t) = E_x(-t).

Conjugating the exponential by an integral unit

theorem TauCeti.baseChangeExp_intCast {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : ℤ) : baseChangeExp x M hM ↑t = LinearMap.baseChange R ↑(integralExpZSMul x M hM hx t)

At an integer parameter the base-changed exponential is the base change of a single integral automorphism of M, namely the restriction of exp (t • x).

This is what makes a Chevalley group element defined over ℤ: its value at an integral parameter does not depend on the ring the points are taken in.

theorem TauCeti.baseChange_integralUnitRestrict_conj_baseChangeExp {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] (x : A) (M : S) (u : Aˣ) (hu : ∀ v ∈ M, ↑u • v ∈ M) (hu' : ∀ v ∈ M, ↑u⁻¹ • v ∈ M) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hx : IsNilpotent x) (t : R) : LinearMap.baseChange R ↑(integralUnitRestrict u M hu hu') * baseChangeExp x M hM t * LinearMap.baseChange R ↑(integralUnitRestrict u M hu hu').symm = baseChangeExp (↑u * x * ↑u⁻¹) M ⋯ t

Conjugating a base-changed exponential by an integral unit. If a unit u of A preserves M together with its inverse, then conjugating the one-parameter subgroup of x by the induced automorphism of R ⊗[ℤ] M gives the one-parameter subgroup of the conjugate u x u⁻¹.

For the Weyl element n_α and a root vector eα this is Chevalley's relation n_α x_α(t) n_α⁻¹ = x_{-α}(-t), obtained from the Lie-algebra identity n_α eα n_α⁻¹ = -e_{-α} alone: conjugation is an algebra automorphism, so it passes through the divided powers.

theorem TauCeti.map_baseChangeExp {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] {T : Type u_3} [CommRing T] (φ : R →+* T) (x : A) (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (t : R) (z : TensorProduct ℤ R ↥M) : (TensorProduct.map φ.toIntAlgHom.toLinearMap LinearMap.id) ((baseChangeExp x M hM t) z) = (baseChangeExp x M hM (φ t)) ((TensorProduct.map φ.toIntAlgHom.toLinearMap LinearMap.id) z)

The base-changed divided-power exponential is natural under every map of parameter rings.