Integral exponentials on product lattices #
The product of two additive subgroups stable under divided powers is stable under the componentwise operator. After scalar extension to any commutative ring, its divided-power exponential is the product of the two exponentials. This allows integral representations to be combined without changing the root subgroup actions on their summands.
@[simp]
theorem
Module.End.dividedPower_prodMap
{V : Type u_1}
{W : Type u_2}
[AddCommGroup V]
[Module ℚ V]
[AddCommGroup W]
[Module ℚ W]
(x : End ℚ V)
(y : End ℚ W)
(n : ℕ)
:
Divided powers of a componentwise endomorphism act componentwise.
theorem
Module.End.dividedPower_prodMap_mem_prod
{V : Type u_1}
{W : Type u_2}
[AddCommGroup V]
[Module ℚ V]
[AddCommGroup W]
[Module ℚ W]
(x : End ℚ V)
(y : End ℚ W)
(M : AddSubgroup V)
(N : AddSubgroup W)
(hM : ∀ (n : ℕ), ∀ v ∈ M, TauCeti.Associative.dividedPower n x • v ∈ M)
(hN : ∀ (n : ℕ), ∀ w ∈ N, TauCeti.Associative.dividedPower n y • w ∈ N)
(n : ℕ)
(v : V × W)
(hv : v ∈ M.prod N)
:
A product of divided-power-stable additive subgroups is divided-power-stable.
@[simp]
theorem
Module.End.prodRight_baseChangeExp
{V : Type u_1}
{W : Type u_2}
[AddCommGroup V]
[Module ℚ V]
[AddCommGroup W]
[Module ℚ W]
{R : Type u_3}
[CommRing R]
[Algebra ℤ R]
(x : End ℚ V)
(y : End ℚ W)
(M : AddSubgroup V)
(N : AddSubgroup W)
(hM : ∀ (n : ℕ), ∀ v ∈ M, TauCeti.Associative.dividedPower n x • v ∈ M)
(hN : ∀ (n : ℕ), ∀ w ∈ N, TauCeti.Associative.dividedPower n y • w ∈ N)
(hx : IsNilpotent x)
(hy : IsNilpotent y)
(t : R)
(z : TensorProduct ℤ R ↥(M.prod N))
:
have E := fun (z : TensorProduct ℤ R ↥(M.prod N)) =>
(TensorProduct.prodRight ℤ R R ↥M ↥N)
((LinearEquiv.baseChange ℤ R (↥(M.prod N)) (↥M × ↥N) (M.prodEquiv N).toIntLinearEquiv) z);
E ((TauCeti.baseChangeExp (LinearMap.prodMap x y) (M.prod N) ⋯ t) z) = ((TauCeti.baseChangeExp x M hM t) (E z).1, (TauCeti.baseChangeExp y N hN t) (E z).2)
Scalar extension identifies the integral exponential on a product lattice with the componentwise exponentials. The coefficient ring may have arbitrary characteristic.