Cancelling iterated base change for Lie algebras

This file upgrades the linear equivalence TensorProduct.AlgebraTensorModule.cancelBaseChange to a Lie algebra equivalence.

def TauCeti.cancelBaseChange (R : Type u_1) (S : Type u_2) (A : Type u_3) (L : Type u_4) [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [LieRing L] [LieAlgebra R L] : TensorProduct S A (TensorProduct R S L) ≃ₗ⁅A⁆ TensorProduct R A L

Iterating extension of scalars from R through S to A gives the same Lie algebra as extending scalars directly from R to A.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.cancelBaseChange_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) (L : Type u_4) [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [LieRing L] [LieAlgebra R L] (a : A) (s : S) (x : L) : (cancelBaseChange R S A L) (a ⊗ₜ[S] (s ⊗ₜ[R] x)) = (s • a) ⊗ₜ[R] x

@[simp]

theorem TauCeti.cancelBaseChange_symm_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) (L : Type u_4) [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [LieRing L] [LieAlgebra R L] (a : A) (x : L) : (cancelBaseChange R S A L).symm (a ⊗ₜ[R] x) = a ⊗ₜ[S] (1 ⊗ₜ[R] x)