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.
• Equiv.lieRing transferring a LieRing structure along an equivalence (transfers the additive structure using Equiv.addCommGroup and then the bracket using AddEquiv.lieRing)
• Equiv.lieAlgebra transferring a Lie algebra structure along an 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]

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

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⁆

@[reducible, inline]

abbrev Equiv.lieAlgebra (R : Type u_1) {L' : Type u_2} {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] (e : L' ≃ L) : LieAlgebra R L'

Transfer LieAlgebra across an Equiv

Equations

• Equiv.lieAlgebra R e = { toModule := Equiv.module R e, lie_smul := ⋯ }

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

An equivalence e : L' ≃ L gives a Lie algebra equivalence L' ≃ₗ⁅R⁆ L where the algebraic structures on L' are obtained by transporting the structures on L back along e.

Equations

• Equiv.lieEquiv R e = { toLinearMap := ↑(Equiv.linearEquiv R e), map_lie' := ⋯, invFun := (Equiv.linearEquiv R e).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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