Transfer Lie brackets along AddEquiv, LinearEquiv and Equiv

Main definitions:

• AddEquiv.lieRing transferring a LieRing structure along an additive equivalence.
• LinearEquiv.lieAlgebra transferring a Lie algebra structure along a linear equivalence.

@[reducible, inline]

abbrev AddEquiv.lieRing {M : Type u_2} {L : Type u_3} [AddCommGroup M] [LieRing L] (e : M ≃+ L) : LieRing M

Transfer LieRing across an AddEquiv

Equations

• e.lieRing = { toAddCommGroup := inst✝¹, bracket := fun (x y : M) => e.symm ⁅e x, e y⁆, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

theorem AddEquiv.bracket_def {M : Type u_2} {L : Type u_3} [AddCommGroup M] [LieRing L] (e : M ≃+ L) (x y : M) : ⁅x, y⁆ = e.symm ⁅e x, e y⁆

@[reducible, inline]

abbrev LinearEquiv.lieAlgebra {R : Type u_1} {M : Type u_2} {L : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [LieRing L] [LieAlgebra R L] (e : M ≃ₗ[R] L) : LieAlgebra R M

Transfer LieAlgebra across a LinearEquiv

Equations

• e.lieAlgebra = { toModule := inst✝², lie_smul := ⋯ }

def LinearEquiv.lieEquiv (R : Type u_1) {M : Type u_2} {L : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [LieRing L] [LieAlgebra R L] (e : M ≃ₗ[R] L) : M ≃ₗ⁅R⁆ L

An equivalence e : M ≃ₗ[R] L gives a Lie algebra equivalence M ≃ₗ⁅R⁆ L where the Lie bracket on M is the one obtained by transporting a Lie Bracket on L back along e.

Equations

• LinearEquiv.lieEquiv R e = { toLinearMap := ↑e, map_lie' := ⋯, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearEquiv.lieEquiv_apply {R : Type u_1} {M : Type u_2} {L : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [LieRing L] [LieAlgebra R L] (e : M ≃ₗ[R] L) (a : M) : (lieEquiv R e) a = e a

@[simp]

theorem LinearEquiv.lieEquiv_symm_apply {R : Type u_1} {M : Type u_2} {L : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [LieRing L] [LieAlgebra R L] (e : M ≃ₗ[R] L) (b : L) : (lieEquiv R e).symm b = e.symm b

@[reducible, inline, deprecated AddEquiv.lieRing (since := "2026-07-30")]

abbrev Equiv.lieRing {L' : Type u_2} {L : Type u_3} [LieRing L] (e : L' ≃ L) : LieRing L'

Transfer LieRing across an Equiv

Equations

• e.lieRing = AddEquiv.lieRing e.addEquiv

@[deprecated AddEquiv.bracket_def (since := "2026-07-30")]

theorem Equiv.bracket_def {L' : Type u_2} {L : Type u_3} [LieRing L] (e : L' ≃ L) (x y : L') : ⁅x, y⁆ = e.symm ⁅e x, e y⁆

@[deprecated LinearEquiv.lieAlgebra (since := "2026-07-30")]

def Equiv.lieAlgebra {R : Type u_1} {M : Type u_2} {L : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [LieRing L] [LieAlgebra R L] (e : M ≃ₗ[R] L) : LieAlgebra R M

Alias of LinearEquiv.lieAlgebra.

---

Transfer LieAlgebra across a LinearEquiv

Equations

• @Equiv.lieAlgebra = @LinearEquiv.lieAlgebra

@[deprecated LinearEquiv.lieEquiv (since := "2026-07-30")]

def Equiv.lieEquiv (R : Type u_1) {M : Type u_2} {L : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [LieRing L] [LieAlgebra R L] (e : M ≃ₗ[R] L) : M ≃ₗ⁅R⁆ L

Alias of LinearEquiv.lieEquiv.

---

An equivalence e : M ≃ₗ[R] L gives a Lie algebra equivalence M ≃ₗ⁅R⁆ L where the Lie bracket on M is the one obtained by transporting a Lie Bracket on L back along e.

Equations

• Equiv.lieEquiv = LinearEquiv.lieEquiv

@[deprecated LinearEquiv.lieEquiv_apply (since := "2026-07-30")]

theorem Equiv.lieEquiv_apply {R : Type u_1} {M : Type u_2} {L : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [LieRing L] [LieAlgebra R L] (e : M ≃ₗ[R] L) (a : M) : (LinearEquiv.lieEquiv R e) a = e a

Alias of LinearEquiv.lieEquiv_apply.

@[deprecated LinearEquiv.lieEquiv_symm_apply (since := "2026-07-30")]

theorem Equiv.lieEquiv_symm_apply {R : Type u_1} {M : Type u_2} {L : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [LieRing L] [LieAlgebra R L] (e : M ≃ₗ[R] L) (b : L) : (LinearEquiv.lieEquiv R e).symm b = e.symm b

Alias of LinearEquiv.lieEquiv_symm_apply.