Lie algebras #

This file defines Lie rings and Lie algebras over a commutative ring together with their modules, morphisms and equivalences, as well as various lemmas to make these definitions usable.

Main definitions #

Notation #

Working over a fixed commutative ring R, we introduce the notations:

L →ₗ⁅R⁆ L' for a morphism of Lie algebras,
L ≃ₗ⁅R⁆ L' for an equivalence of Lie algebras,
M →ₗ⁅R,L⁆ N for a morphism of Lie algebra modules M, N over a Lie algebra L,
M ≃ₗ⁅R,L⁆ N for an equivalence of Lie algebra modules M, N over a Lie algebra L.

Implementation notes #

Lie algebras are defined as modules with a compatible Lie ring structure and thus, like modules, are partially unbundled.

References #

N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1--3

Tags #

lie bracket, jacobi identity, lie ring, lie algebra, lie module

source

class LieRing (L : Type v) extends AddCommGroup L, Bracket L L :

Type v

A Lie ring is an additive group with compatible product, known as the bracket, satisfying the Jacobi identity.

add : L → L → L
add_assoc (a b c : L) : a + b + c = a + (b + c)
zero : L
zero_add (a : L) : 0 + a = a
add_zero (a : L) : a + 0 = a
nsmul : ℕ → L → L
nsmul_zero (x : L) : AddMonoid.nsmul 0 x = 0
nsmul_succ (n : ℕ) (x : L) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
neg : L → L
sub : L → L → L
sub_eq_add_neg (a b : L) : a - b = a + -b
zsmul : ℤ → L → L
zsmul_zero' (a : L) : SubNegMonoid.zsmul 0 a = 0
zsmul_succ' (n : ℕ) (a : L) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
zsmul_neg' (n : ℕ) (a : L) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
neg_add_cancel (a : L) : -a + a = 0
add_comm (a b : L) : a + b = b + a
bracket : L → L → L
add_lie (x y z : L) : ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
A Lie ring bracket is additive in its first component.
lie_add (x y z : L) : ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
A Lie ring bracket is additive in its second component.
lie_self (x : L) : ⁅x, x⁆ = 0
A Lie ring bracket vanishes on the diagonal in L × L.
leibniz_lie (x y z : L) : ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
A Lie ring bracket satisfies a Leibniz / Jacobi identity.

Instances

source

class LieAlgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] extends Module R L :

Type (max u v)

A Lie algebra is a module with compatible product, known as the bracket, satisfying the Jacobi identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring.

smul : R → L → L
one_smul (b : L) : 1 • b = b
mul_smul (x y : R) (b : L) : (x * y) • b = x • y • b
smul_zero (a : R) : a • 0 = 0
smul_add (a : R) (x y : L) : a • (x + y) = a • x + a • y
add_smul (r s : R) (x : L) : (r + s) • x = r • x + s • x
zero_smul (x : L) : 0 • x = 0
lie_smul (t : R) (x y : L) : ⁅x, t • y⁆ = t • ⁅x, y⁆
A Lie algebra bracket is compatible with scalar multiplication in its second argument.
The compatibility in the first argument is not a class property, but follows since every Lie algebra has a natural Lie module action on itself, see LieModule.

Instances

source

theorem LieAlgebra.ext {R : Type u} {L : Type v} {inst✝ : CommRing R} {inst✝¹ : LieRing L} {x y : LieAlgebra R L} (smul : SMul.smul = SMul.smul) :

x = y

source

class LieRingModule (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] extends Bracket L M :

Type (max v w)

A Lie ring module is an additive group, together with an additive action of a Lie ring on this group, such that the Lie bracket acts as the commutator of endomorphisms. (For representations of Lie algebras see LieModule.)

bracket : L → M → M
add_lie (x y : L) (m : M) : ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
A Lie ring module bracket is additive in its first component.
lie_add (x : L) (m n : M) : ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆
A Lie ring module bracket is additive in its second component.
leibniz_lie (x y : L) (m : M) : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
A Lie ring module bracket satisfies a Leibniz / Jacobi identity.

Instances

source

class LieModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Prop

A Lie module is a module over a commutative ring, together with a linear action of a Lie algebra on this module, such that the Lie bracket acts as the commutator of endomorphisms.

smul_lie (t : R) (x : L) (m : M) : ⁅t • x, m⁆ = t • ⁅x, m⁆
A Lie module bracket is compatible with scalar multiplication in its first argument.
lie_smul (t : R) (x : L) (m : M) : ⁅x, t • m⁆ = t • ⁅x, m⁆
A Lie module bracket is compatible with scalar multiplication in its second argument.

Instances

source

class IsLieTower (L₁ : Type u_1) (L₂ : Type u_2) (M : Type u_3) [Bracket L₁ L₂] [Bracket L₁ M] [Bracket L₂ M] [Add M] :

Prop

A tower of Lie bracket actions encapsulates the Leibniz rule for Lie bracket actions.

More precisely, it does so in a relative setting: Let L₁ and L₂ be two types with Lie bracket actions on a type M endowed with an addition, and additionally assume a Lie bracket action of L₁ on L₂. Then the Leibniz rule asserts for all x : L₁, y : L₂, and m : M that ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ holds.

Common examples include the case where L₁ is a Lie subalgebra of L₂ and the case where L₂ is a Lie ideal of L₁.

leibniz_lie (x : L₁) (y : L₂) (m : M) : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆

Instances

source

theorem leibniz_lie {L₁ : Type u_1} {L₂ : Type u_2} {M : Type u_3} [Bracket L₁ L₂] [Bracket L₁ M] [Bracket L₂ M] [Add M] [IsLieTower L₁ L₂ M] (x : L₁) (y : L₂) (m : M) :

⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆

source

theorem lie_swap_lie {L₁ : Type u_1} {L₂ : Type u_2} {M : Type u_3} [Bracket L₁ L₂] [Bracket L₁ M] [Bracket L₂ M] [Bracket L₂ L₁] [AddCommGroup M] [IsLieTower L₁ L₂ M] [IsLieTower L₂ L₁ M] (x : L₁) (y : L₂) (m : M) :

⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆

source

theorem LieAlgebra.toModule_injective (L : Type u_1) [LieRing L] :

Function.Injective (@toModule ℚ L Rat.commRing inst✝)

source

instance instSubsingletonLieAlgebraRat (L : Type u_1) [LieRing L] :

Subsingleton (LieAlgebra ℚ L)

source

@[simp]

theorem add_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x y : L) (m : M) :

⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆

source

@[simp]

theorem lie_add {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m n : M) :

⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆

source

@[simp]

theorem smul_lie {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (t : R) (x : L) (m : M) :

⁅t • x, m⁆ = t • ⁅x, m⁆

source

@[simp]

theorem lie_smul {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (t : R) (x : L) (m : M) :

⁅x, t • m⁆ = t • ⁅x, m⁆

source

instance instIsLieTower {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] :

IsLieTower L L M

source

@[simp]

theorem lie_zero {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) :

⁅x, 0⁆ = 0

source

@[simp]

theorem zero_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (m : M) :

⁅0, m⁆ = 0

source

@[simp]

theorem lie_self {L : Type v} [LieRing L] (x : L) :

⁅x, x⁆ = 0

source

instance lieRingSelfModule {L : Type v} [LieRing L] :

LieRingModule L L

Equations

lieRingSelfModule = LieRingModule.mk ⋯ ⋯ ⋯

source

@[simp]

theorem lie_skew {L : Type v} [LieRing L] (x y : L) :

-⁅y, x⁆ = ⁅x, y⁆

source

instance lieAlgebraSelfModule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :

LieModule R L L

Every Lie algebra is a module over itself.

source

@[simp]

theorem neg_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) :

⁅-x, m⁆ = -⁅x, m⁆

source

@[simp]

theorem lie_neg {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) :

⁅x, -m⁆ = -⁅x, m⁆

source

@[simp]

theorem sub_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x y : L) (m : M) :

⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆

source

@[simp]

theorem lie_sub {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m n : M) :

⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆

source

@[simp]

theorem nsmul_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (n : ℕ) :

⁅n • x, m⁆ = n • ⁅x, m⁆

source

@[simp]

theorem lie_nsmul {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (n : ℕ) :

⁅x, n • m⁆ = n • ⁅x, m⁆

source

theorem zsmul_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (a : ℤ) :

⁅a • x, m⁆ = a • ⁅x, m⁆

source

theorem lie_zsmul {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (a : ℤ) :

⁅x, a • m⁆ = a • ⁅x, m⁆

source

@[simp]

theorem lie_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x y : L) (m : M) :

⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

source

theorem lie_jacobi {L : Type v} [LieRing L] (x y z : L) :

⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0

source

instance LieRing.instLieAlgebra {L : Type v} [LieRing L] :

LieAlgebra ℤ L

Equations

LieRing.instLieAlgebra = LieAlgebra.mk ⋯

source

instance instLieModuleInt {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] :

LieModule ℤ L M

source

instance LinearMap.instLieRingModule {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] :

LieRingModule L (M →ₗ[R] N)

Equations

LinearMap.instLieRingModule = LieRingModule.mk ⋯ ⋯ ⋯

source

@[simp]

theorem LieHom.lie_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ[R] N) (x : L) (m : M) :

⁅x, f⁆ m = ⁅x, f m⁆ - f ⁅x, m⁆

source

instance LinearMap.instLieModule {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] :

LieModule R L (M →ₗ[R] N)

source

instance Module.Dual.instLieRingModule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

LieRingModule L (M →ₗ[R] R)

We could avoid defining this by instead defining a LieRingModule L R instance with a zero bracket and relying on LinearMap.instLieRingModule. We do not do this because in the case that L = R we would have a non-defeq diamond via Ring.instBracket.

Equations

Module.Dual.instLieRingModule = LieRingModule.mk ⋯ ⋯ ⋯

source

@[simp]

theorem Module.Dual.lie_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) (f : M →ₗ[R] R) :

⁅x, f⁆ m = -f ⁅x, m⁆

source

instance Module.Dual.instLieModule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

LieModule R L (M →ₗ[R] R)

source

def LieRing.toNonUnitalNonAssocRing (L : Type v) [LieRing L] :

NonUnitalNonAssocRing L

It is sometimes useful to regard a LieRing as a NonUnitalNonAssocRing.

Equations

LieRing.toNonUnitalNonAssocRing L = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

Instances For

source

theorem sum_lie {L : Type v} [LieRing L] {ι : Type u_1} (s : Finset ι) (f : ι → L) (a : L) :

⁅∑ i ∈ s, f i, a⁆ = ∑ i ∈ s, ⁅f i, a⁆

source

theorem lie_sum {L : Type v} [LieRing L] {ι : Type u_1} (s : Finset ι) (f : ι → L) (a : L) :

⁅a, ∑ i ∈ s, f i⁆ = ∑ i ∈ s, ⁅a, f i⁆

source

theorem sum_lie_sum {L : Type v} [LieRing L] {ι : Type u_1} {κ : Type u_3} (s : Finset ι) (t : Finset κ) (f : ι → L) (g : κ → L) :

⁅∑ i ∈ s, f i, ∑ j ∈ t, g j⁆ = ∑ i ∈ s, ∑ j ∈ t, ⁅f i, g j⁆

source

structure LieHom (R : Type u_1) (L : Type u_2) (L' : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] extends L →ₗ[R] L' :

Type (max u_2 u_3)

A morphism of Lie algebras (denoted as L₁ →ₗ⁅R⁆ L₂) is a linear map respecting the bracket operations.

toFun : L → L'
map_add' (x y : L) : (↑self).toFun (x + y) = (↑self).toFun x + (↑self).toFun y
map_smul' (m : R) (x : L) : (↑self).toFun (m • x) = (RingHom.id R) m • (↑self).toFun x
map_lie' {x y : L} : (↑self).toFun ⁅x, y⁆ = ⁅(↑self).toFun x, (↑self).toFun y⁆
A morphism of Lie algebras is compatible with brackets.

Instances For

source

def «term_→ₗ⁅_⁆_» :

Lean.TrailingParserDescr

A morphism of Lie algebras (denoted as L₁ →ₗ⁅R⁆ L₂) is a linear map respecting the bracket operations.

Equations

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

Instances For

source

instance LieHom.instCoeLinearMapId {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

Coe (L₁ →ₗ⁅R⁆ L₂) (L₁ →ₗ[R] L₂)

Equations

LieHom.instCoeLinearMapId = { coe := LieHom.toLinearMap }

source

instance LieHom.instFunLike {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

FunLike (L₁ →ₗ⁅R⁆ L₂) L₁ L₂

Equations

LieHom.instFunLike = { coe := fun (f : L₁ →ₗ⁅R⁆ L₂) => (↑f).toFun, coe_injective' := ⋯ }

source

@[simp]

theorem LieHom.coe_toLinearMap {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) :

⇑↑f = ⇑f

source

@[simp]

theorem LieHom.toFun_eq_coe {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) :

(↑f).toFun = ⇑f

source

@[simp]

theorem LieHom.map_smul {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (c : R) (x : L₁) :

f (c • x) = c • f x

source

@[simp]

theorem LieHom.map_add {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) :

f (x + y) = f x + f y

source

@[simp]

theorem LieHom.map_sub {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) :

f (x - y) = f x - f y

source

@[simp]

theorem LieHom.map_neg {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) :

f (-x) = -f x

source

@[simp]

theorem LieHom.map_lie {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) :

f ⁅x, y⁆ = ⁅f x, f y⁆

source

@[simp]

theorem LieHom.map_zero {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) :

f 0 = 0

source

def LieHom.id {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :

L₁ →ₗ⁅R⁆ L₁

The identity map is a morphism of Lie algebras.

Equations

LieHom.id = { toLinearMap := LinearMap.id, map_lie' := ⋯ }

Instances For

source

@[simp]

theorem LieHom.coe_id {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :

⇑id = _root_.id

source

theorem LieHom.id_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) :

id x = x

source

instance LieHom.instZero {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

Zero (L₁ →ₗ⁅R⁆ L₂)

The constant 0 map is a Lie algebra morphism.

Equations

LieHom.instZero = { zero := let __src := 0; { toLinearMap := __src, map_lie' := ⋯ } }

source

@[simp]

theorem LieHom.coe_zero {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

⇑0 = 0

source

theorem LieHom.zero_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (x : L₁) :

0 x = 0

source

instance LieHom.instOne {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :

One (L₁ →ₗ⁅R⁆ L₁)

The identity map is a Lie algebra morphism.

Equations

LieHom.instOne = { one := LieHom.id }

source

@[simp]

theorem LieHom.coe_one {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :

⇑1 = _root_.id

source

theorem LieHom.one_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) :

1 x = x

source

instance LieHom.instInhabited {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

Inhabited (L₁ →ₗ⁅R⁆ L₂)

Equations

LieHom.instInhabited = { default := 0 }

source

theorem LieHom.coe_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

Function.Injective DFunLike.coe

source

theorem LieHom.ext {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] {f g : L₁ →ₗ⁅R⁆ L₂} (h : ∀ (x : L₁), f x = g x) :

f = g

source

theorem LieHom.congr_fun {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] {f g : L₁ →ₗ⁅R⁆ L₂} (h : f = g) (x : L₁) :

f x = g x

source

@[simp]

theorem LieHom.mk_coe {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h₁ : ∀ (x y : L₁), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : L₁), { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x) (h₃ : ∀ {x y : L₁}, { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ = ⁅{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun x, { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆) :

{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } = f

source

@[simp]

theorem LieHom.coe_mk {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ → L₂) (h₁ : ∀ (x y : L₁), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : L₁), { toFun := f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h₁ }.toFun x) (h₃ : ∀ {x y : L₁}, { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ = ⁅{ toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun x, { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆) :

⇑{ toFun := f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } = f

source

def LieHom.comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) :

L₁ →ₗ⁅R⁆ L₃

The composition of morphisms is a morphism.

Equations

f.comp g = { toLinearMap := ↑f ∘ₗ ↑g, map_lie' := ⋯ }

Instances For

source

theorem LieHom.comp_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) (x : L₁) :

(f.comp g) x = f (g x)

source

@[simp]

theorem LieHom.coe_comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) :

⇑(f.comp g) = ⇑f ∘ ⇑g

source

@[simp]

theorem LieHom.toLinearMap_comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) :

↑(f.comp g) = ↑f ∘ₗ ↑g

source

@[deprecated LieHom.toLinearMap_comp (since := "2024-12-30")]

theorem LieHom.coe_linearMap_comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) :

↑(f.comp g) = ↑f ∘ₗ ↑g

Alias of LieHom.toLinearMap_comp.

source

@[simp]

theorem LieHom.comp_id {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) :

f.comp id = f

source

@[simp]

theorem LieHom.id_comp {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) :

id.comp f = f

source

def LieHom.inverse {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :

L₂ →ₗ⁅R⁆ L₁

The inverse of a bijective morphism is a morphism.

Equations

f.inverse g h₁ h₂ = { toLinearMap := (↑f).inverse g h₁ h₂, map_lie' := ⋯ }

Instances For

source

def LieRingModule.compLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M] [LieRingModule L₂ M] (f : L₁ →ₗ⁅R⁆ L₂) :

LieRingModule L₁ M

A Lie ring module may be pulled back along a morphism of Lie algebras.

See note [reducible non-instances].

Equations

LieRingModule.compLieHom M f = LieRingModule.mk ⋯ ⋯ ⋯

Instances For

source

theorem LieRingModule.compLieHom_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M] [LieRingModule L₂ M] (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) (m : M) :

⁅x, m⁆ = ⁅f x, m⁆

source

theorem LieModule.compLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M] [LieRingModule L₂ M] (f : L₁ →ₗ⁅R⁆ L₂) [Module R M] [LieModule R L₂ M] :

LieModule R L₁ M

A Lie module may be pulled back along a morphism of Lie algebras.

source

structure LieEquiv (R : Type u) (L : Type v) (L' : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] extends L →ₗ⁅R⁆ L' :

Type (max v w)

An equivalence of Lie algebras (denoted as L₁ ≃ₗ⁅R⁆ L₂) is a morphism which is also a linear equivalence. We could instead define an equivalence to be a morphism which is also a (plain) equivalence. However, it is more convenient to define via linear equivalence to get .toLinearEquiv for free.

toFun : L → L'
map_add' (x y : L) : (↑self.toLieHom).toFun (x + y) = (↑self.toLieHom).toFun x + (↑self.toLieHom).toFun y
map_smul' (m : R) (x : L) : (↑self.toLieHom).toFun (m • x) = (RingHom.id R) m • (↑self.toLieHom).toFun x
map_lie' {x y : L} : (↑self.toLieHom).toFun ⁅x, y⁆ = ⁅(↑self.toLieHom).toFun x, (↑self.toLieHom).toFun y⁆
invFun : L' → L
The inverse function of an equivalence of Lie algebras
left_inv : Function.LeftInverse self.invFun (↑self.toLieHom).toFun
The inverse function of an equivalence of Lie algebras is a left inverse of the underlying function.
right_inv : Function.RightInverse self.invFun (↑self.toLieHom).toFun
The inverse function of an equivalence of Lie algebras is a right inverse of the underlying function.

Instances For

source

def «term_≃ₗ⁅_⁆_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

def LieEquiv.toLinearEquiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ ≃ₗ⁅R⁆ L₂) :

L₁ ≃ₗ[R] L₂

Consider an equivalence of Lie algebras as a linear equivalence.

Equations

f.toLinearEquiv = { toLinearMap := ↑f.toLieHom, invFun := f.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

instance LieEquiv.hasCoeToLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :

Coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ →ₗ⁅R⁆ L₂)

Equations

LieEquiv.hasCoeToLieHom = { coe := LieEquiv.toLieHom }

source

instance LieEquiv.hasCoeToLinearEquiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :

Coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ ≃ₗ[R] L₂)

Equations

LieEquiv.hasCoeToLinearEquiv = { coe := LieEquiv.toLinearEquiv }

source

instance LieEquiv.instEquivLike {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :

EquivLike (L₁ ≃ₗ⁅R⁆ L₂) L₁ L₂

Equations

LieEquiv.instEquivLike = { coe := fun (f : L₁ ≃ₗ⁅R⁆ L₂) => (↑f.toLieHom).toFun, inv := fun (f : L₁ ≃ₗ⁅R⁆ L₂) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

source

theorem LieEquiv.coe_toLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

⇑e.toLieHom = ⇑e

source

@[deprecated LieEquiv.coe_toLieHom (since := "2024-12-30")]

theorem LieEquiv.coe_to_lieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

⇑e.toLieHom = ⇑e

Alias of LieEquiv.coe_toLieHom.

source

@[simp]

theorem LieEquiv.coe_toLinearEquiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

⇑e.toLinearEquiv = ⇑e

source

@[deprecated LieEquiv.coe_toLinearEquiv (since := "2024-12-30")]

theorem LieEquiv.coe_to_linearEquiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

⇑e.toLinearEquiv = ⇑e

Alias of LieEquiv.coe_toLinearEquiv.

source

@[simp]

theorem LieEquiv.toLinearEquiv_mk {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁) (h₁ : Function.LeftInverse g (↑f).toFun) (h₂ : Function.RightInverse g (↑f).toFun) :

{ toLieHom := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toLinearEquiv = { toLinearMap := ↑f, invFun := g, left_inv := h₁, right_inv := h₂ }

source

@[deprecated LieEquiv.toLinearEquiv_mk (since := "2024-12-30")]

theorem LieEquiv.to_linearEquiv_mk {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁) (h₁ : Function.LeftInverse g (↑f).toFun) (h₂ : Function.RightInverse g (↑f).toFun) :

{ toLieHom := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toLinearEquiv = { toLinearMap := ↑f, invFun := g, left_inv := h₁, right_inv := h₂ }

Alias of LieEquiv.toLinearEquiv_mk.

source

theorem LieEquiv.toLinearEquiv_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :

Function.Injective toLinearEquiv

source

@[deprecated LieEquiv.toLinearEquiv_injective (since := "2024-12-30")]

theorem LieEquiv.coe_linearEquiv_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :

Function.Injective toLinearEquiv

Alias of LieEquiv.toLinearEquiv_injective.

source

theorem LieEquiv.coe_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :

Function.Injective DFunLike.coe

source

theorem LieEquiv.ext {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] {f g : L₁ ≃ₗ⁅R⁆ L₂} (h : ∀ (x : L₁), f x = g x) :

f = g

source

instance LieEquiv.instOne {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :

One (L₁ ≃ₗ⁅R⁆ L₁)

Equations

LieEquiv.instOne = { one := let __src := 1; { toLinearMap := ↑__src, map_lie' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ } }

source

@[simp]

theorem LieEquiv.one_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) :

1 x = x

source

instance LieEquiv.instInhabited {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :

Inhabited (L₁ ≃ₗ⁅R⁆ L₁)

Equations

LieEquiv.instInhabited = { default := 1 }

source

theorem LieEquiv.map_lie {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) (x y : L₁) :

e ⁅x, y⁆ = ⁅e x, e y⁆

source

def LieEquiv.refl {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :

L₁ ≃ₗ⁅R⁆ L₁

Lie algebra equivalences are reflexive.

Equations

LieEquiv.refl = 1

Instances For

source

@[simp]

theorem LieEquiv.refl_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) :

refl x = x

source

def LieEquiv.symm {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

L₂ ≃ₗ⁅R⁆ L₁

Lie algebra equivalences are symmetric.

Equations

e.symm = { toLieHom := e.inverse e.invFun ⋯ ⋯, invFun := e.toLinearEquiv.symm.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LieEquiv.symm_symm {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

e.symm.symm = e

source

theorem LieEquiv.symm_bijective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :

Function.Bijective symm

source

@[simp]

theorem LieEquiv.apply_symm_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) (x : L₂) :

e (e.symm x) = x

source

@[simp]

theorem LieEquiv.symm_apply_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) (x : L₁) :

e.symm (e x) = x

source

@[simp]

theorem LieEquiv.refl_symm {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :

refl.symm = refl

source

def LieEquiv.trans {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieRing L₂] [LieRing L₃] [LieAlgebra R L₁] [LieAlgebra R L₂] [LieAlgebra R L₃] (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) :

L₁ ≃ₗ⁅R⁆ L₃

Lie algebra equivalences are transitive.

Equations

e₁.trans e₂ = { toLieHom := e₂.comp e₁.toLieHom, invFun := (e₁.toLinearEquiv.trans e₂.toLinearEquiv).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LieEquiv.self_trans_symm {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

e.trans e.symm = refl

source

@[simp]

theorem LieEquiv.symm_trans_self {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

e.symm.trans e = refl

source

@[simp]

theorem LieEquiv.trans_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieRing L₂] [LieRing L₃] [LieAlgebra R L₁] [LieAlgebra R L₂] [LieAlgebra R L₃] (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) (x : L₁) :

(e₁.trans e₂) x = e₂ (e₁ x)

source

@[simp]

theorem LieEquiv.symm_trans {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieRing L₂] [LieRing L₃] [LieAlgebra R L₁] [LieAlgebra R L₂] [LieAlgebra R L₃] (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) :

(e₁.trans e₂).symm = e₂.symm.trans e₁.symm

source

theorem LieEquiv.bijective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

Function.Bijective ⇑e.toLieHom

source

theorem LieEquiv.injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

Function.Injective ⇑e.toLieHom

source

theorem LieEquiv.surjective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) :

Function.Surjective ⇑e.toLieHom

source

noncomputable def LieEquiv.ofBijective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Bijective ⇑f) :

L₁ ≃ₗ⁅R⁆ L₂

A bijective morphism of Lie algebras yields an equivalence of Lie algebras.

Equations

LieEquiv.ofBijective f h = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯, invFun := (LinearEquiv.ofBijective (↑f) h).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LieEquiv.ofBijective_invFun {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Bijective ⇑f) (a✝ : L₂) :

(ofBijective f h).invFun a✝ = (LinearEquiv.ofBijective (↑f) h).symm a✝

source

@[simp]

theorem LieEquiv.ofBijective_toFun {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Bijective ⇑f) (a : L₁) :

(ofBijective f h) a = f a

source

structure LieModuleHom (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] extends M →ₗ[R] N :

Type (max w w₁)

A morphism of Lie algebra modules (denoted as M →ₗ⁅R,L⁆ N) is a linear map which commutes with the action of the Lie algebra.

toFun : M → N
map_add' (x y : M) : (↑self).toFun (x + y) = (↑self).toFun x + (↑self).toFun y
map_smul' (m : R) (x : M) : (↑self).toFun (m • x) = (RingHom.id R) m • (↑self).toFun x
map_lie' {x : L} {m : M} : (↑self).toFun ⁅x, m⁆ = ⁅x, (↑self).toFun m⁆
A module of Lie algebra modules is compatible with the action of the Lie algebra on the modules.

Instances For

source

def «term_→ₗ⁅_,_⁆_» :

Lean.TrailingParserDescr

A morphism of Lie algebra modules (denoted as M →ₗ⁅R,L⁆ N) is a linear map which commutes with the action of the Lie algebra.

Equations

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

Instances For

source

instance LieModuleHom.instCoeOutLinearMapId {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

CoeOut (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N)

Equations

LieModuleHom.instCoeOutLinearMapId = { coe := LieModuleHom.toLinearMap }

source

instance LieModuleHom.instFunLike {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

FunLike (M →ₗ⁅R,L⁆ N) M N

Equations

LieModuleHom.instFunLike = { coe := fun (f : M →ₗ⁅R,L⁆ N) => (↑f).toFun, coe_injective' := ⋯ }

source

@[simp]

theorem LieModuleHom.coe_toLinearMap {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) :

⇑↑f = ⇑f

source

@[simp]

theorem LieModuleHom.map_smul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (c : R) (x : M) :

f (c • x) = c • f x

source

@[simp]

theorem LieModuleHom.map_add {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (x y : M) :

f (x + y) = f x + f y

source

@[simp]

theorem LieModuleHom.map_sub {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (x y : M) :

f (x - y) = f x - f y

source

@[simp]

theorem LieModuleHom.map_neg {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (x : M) :

f (-x) = -f x

source

@[simp]

theorem LieModuleHom.map_lie {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (x : L) (m : M) :

f ⁅x, m⁆ = ⁅x, f m⁆

source

theorem LieModuleHom.map_lie₂ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] [LieAlgebra R L] [LieModule R L N] [LieModule R L P] (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (x : L) (m : M) (n : N) :

⁅x, (f m) n⁆ = (f ⁅x, m⁆) n + (f m) ⁅x, n⁆

source

@[simp]

theorem LieModuleHom.map_zero {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) :

f 0 = 0

source

def LieModuleHom.id {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

M →ₗ⁅R,L⁆ M

The identity map is a morphism of Lie modules.

Equations

LieModuleHom.id = { toLinearMap := LinearMap.id, map_lie' := ⋯ }

Instances For

source

@[simp]

theorem LieModuleHom.coe_id {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

⇑id = _root_.id

source

theorem LieModuleHom.id_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (x : M) :

id x = x

source

instance LieModuleHom.instZero {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

Zero (M →ₗ⁅R,L⁆ N)

The constant 0 map is a Lie module morphism.

Equations

LieModuleHom.instZero = { zero := let __src := 0; { toLinearMap := __src, map_lie' := ⋯ } }

source

@[simp]

theorem LieModuleHom.coe_zero {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

⇑0 = 0

source

theorem LieModuleHom.zero_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (m : M) :

0 m = 0

source

instance LieModuleHom.instOne {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

One (M →ₗ⁅R,L⁆ M)

The identity map is a Lie module morphism.

Equations

LieModuleHom.instOne = { one := LieModuleHom.id }

source

instance LieModuleHom.instInhabited {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

Inhabited (M →ₗ⁅R,L⁆ N)

Equations

LieModuleHom.instInhabited = { default := 0 }

source

theorem LieModuleHom.coe_injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

Function.Injective DFunLike.coe

source

theorem LieModuleHom.ext {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] {f g : M →ₗ⁅R,L⁆ N} (h : ∀ (m : M), f m = g m) :

f = g

source

theorem LieModuleHom.congr_fun {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] {f g : M →ₗ⁅R,L⁆ N} (h : f = g) (x : M) :

f x = g x

source

@[simp]

theorem LieModuleHom.mk_coe {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (h : ∀ {x : L} {m : M}, (↑f).toFun ⁅x, m⁆ = ⁅x, (↑f).toFun m⁆) :

{ toLinearMap := ↑f, map_lie' := h } = f

source

@[simp]

theorem LieModuleHom.coe_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ[R] N) (h : ∀ {x : L} {m : M}, f.toFun ⁅x, m⁆ = ⁅x, f.toFun m⁆) :

⇑{ toLinearMap := f, map_lie' := h } = ⇑f

source

theorem LieModuleHom.coe_linear_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ[R] N) (h : ∀ {x : L} {m : M}, f.toFun ⁅x, m⁆ = ⁅x, f.toFun m⁆) :

↑{ toLinearMap := f, map_lie' := h } = f

source

def LieModuleHom.comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) :

M →ₗ⁅R,L⁆ P

The composition of Lie module morphisms is a morphism.

Equations

f.comp g = { toLinearMap := ↑f ∘ₗ ↑g, map_lie' := ⋯ }

Instances For

source

theorem LieModuleHom.comp_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) (m : M) :

(f.comp g) m = f (g m)

source

@[simp]

theorem LieModuleHom.coe_comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) :

⇑(f.comp g) = ⇑f ∘ ⇑g

source

@[simp]

theorem LieModuleHom.toLinearMap_comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) :

↑(f.comp g) = ↑f ∘ₗ ↑g

source

@[deprecated LieModuleHom.toLinearMap_comp (since := "2024-12-30")]

theorem LieModuleHom.coe_linearMap_comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) :

↑(f.comp g) = ↑f ∘ₗ ↑g

Alias of LieModuleHom.toLinearMap_comp.

source

def LieModuleHom.inverse {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (g : N → M) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :

N →ₗ⁅R,L⁆ M

The inverse of a bijective morphism of Lie modules is a morphism of Lie modules.

Equations

f.inverse g h₁ h₂ = { toLinearMap := (↑f).inverse g h₁ h₂, map_lie' := ⋯ }

Instances For

source

instance LieModuleHom.instAdd {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

Add (M →ₗ⁅R,L⁆ N)

Equations

LieModuleHom.instAdd = { add := fun (f g : M →ₗ⁅R,L⁆ N) => let __src := ↑f + ↑g; { toLinearMap := __src, map_lie' := ⋯ } }

source

instance LieModuleHom.instSub {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

Sub (M →ₗ⁅R,L⁆ N)

Equations

LieModuleHom.instSub = { sub := fun (f g : M →ₗ⁅R,L⁆ N) => let __src := ↑f - ↑g; { toLinearMap := __src, map_lie' := ⋯ } }

source

instance LieModuleHom.instNeg {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

Neg (M →ₗ⁅R,L⁆ N)

Equations

LieModuleHom.instNeg = { neg := fun (f : M →ₗ⁅R,L⁆ N) => let __src := -↑f; { toLinearMap := __src, map_lie' := ⋯ } }

source

@[simp]

theorem LieModuleHom.coe_add {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f g : M →ₗ⁅R,L⁆ N) :

⇑(f + g) = ⇑f + ⇑g

source

theorem LieModuleHom.add_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f g : M →ₗ⁅R,L⁆ N) (m : M) :

(f + g) m = f m + g m

source

@[simp]

theorem LieModuleHom.coe_sub {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f g : M →ₗ⁅R,L⁆ N) :

⇑(f - g) = ⇑f - ⇑g

source

theorem LieModuleHom.sub_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f g : M →ₗ⁅R,L⁆ N) (m : M) :

(f - g) m = f m - g m

source

@[simp]

theorem LieModuleHom.coe_neg {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) :

⇑(-f) = -⇑f

source

theorem LieModuleHom.neg_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (m : M) :

(-f) m = -f m

source

instance LieModuleHom.hasNSMul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

SMul ℕ (M →ₗ⁅R,L⁆ N)

Equations

LieModuleHom.hasNSMul = { smul := fun (n : ℕ) (f : M →ₗ⁅R,L⁆ N) => let __src := n • ↑f; { toLinearMap := __src, map_lie' := ⋯ } }

source

@[simp]

theorem LieModuleHom.coe_nsmul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (n : ℕ) (f : M →ₗ⁅R,L⁆ N) :

⇑(n • f) = n • ⇑f

source

theorem LieModuleHom.nsmul_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (n : ℕ) (f : M →ₗ⁅R,L⁆ N) (m : M) :

(n • f) m = n • f m

source

instance LieModuleHom.hasZSMul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

SMul ℤ (M →ₗ⁅R,L⁆ N)

Equations

LieModuleHom.hasZSMul = { smul := fun (z : ℤ) (f : M →ₗ⁅R,L⁆ N) => let __src := z • ↑f; { toLinearMap := __src, map_lie' := ⋯ } }

source

@[simp]

theorem LieModuleHom.coe_zsmul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (z : ℤ) (f : M →ₗ⁅R,L⁆ N) :

⇑(z • f) = z • ⇑f

source

theorem LieModuleHom.zsmul_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (z : ℤ) (f : M →ₗ⁅R,L⁆ N) (m : M) :

(z • f) m = z • f m

source

instance LieModuleHom.instAddCommGroup {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

AddCommGroup (M →ₗ⁅R,L⁆ N)

Equations

LieModuleHom.instAddCommGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

instance LieModuleHom.instSMul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieAlgebra R L] [LieModule R L N] :

SMul R (M →ₗ⁅R,L⁆ N)

Equations

LieModuleHom.instSMul = { smul := fun (t : R) (f : M →ₗ⁅R,L⁆ N) => let __src := t • ↑f; { toLinearMap := __src, map_lie' := ⋯ } }

source

@[simp]

theorem LieModuleHom.coe_smul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieAlgebra R L] [LieModule R L N] (t : R) (f : M →ₗ⁅R,L⁆ N) :

⇑(t • f) = t • ⇑f

source

theorem LieModuleHom.smul_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieAlgebra R L] [LieModule R L N] (t : R) (f : M →ₗ⁅R,L⁆ N) (m : M) :

(t • f) m = t • f m

source

instance LieModuleHom.instModule {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieAlgebra R L] [LieModule R L N] :

Module R (M →ₗ⁅R,L⁆ N)

Equations

LieModuleHom.instModule = Function.Injective.module R { toFun := fun (f : M →ₗ⁅R,L⁆ N) => (↑f).toFun, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

source

structure LieModuleEquiv (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] extends M →ₗ⁅R,L⁆ N :

Type (max w w₁)

An equivalence of Lie algebra modules (denoted as M ≃ₗ⁅R,L⁆ N) is a linear equivalence which is also a morphism of Lie algebra modules.

toFun : M → N
map_add' (x y : M) : (↑self.toLieModuleHom).toFun (x + y) = (↑self.toLieModuleHom).toFun x + (↑self.toLieModuleHom).toFun y
map_smul' (m : R) (x : M) : (↑self.toLieModuleHom).toFun (m • x) = (RingHom.id R) m • (↑self.toLieModuleHom).toFun x
map_lie' {x : L} {m : M} : (↑self.toLieModuleHom).toFun ⁅x, m⁆ = ⁅x, (↑self.toLieModuleHom).toFun m⁆
invFun : N → M
The inverse function of an equivalence of Lie modules
left_inv : Function.LeftInverse self.invFun (↑self.toLieModuleHom).toFun
The inverse function of an equivalence of Lie modules is a left inverse of the underlying function.
right_inv : Function.RightInverse self.invFun (↑self.toLieModuleHom).toFun
The inverse function of an equivalence of Lie modules is a right inverse of the underlying function.

Instances For

source

def «term_≃ₗ⁅_,_⁆_» :

Lean.TrailingParserDescr

An equivalence of Lie algebra modules (denoted as M ≃ₗ⁅R,L⁆ N) is a linear equivalence which is also a morphism of Lie algebra modules.

Equations

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

Instances For

source

def LieModuleEquiv.toLinearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

M ≃ₗ[R] N

View an equivalence of Lie modules as a linear equivalence.

Equations

e.toLinearEquiv = { toLinearMap := ↑e.toLieModuleHom, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

def LieModuleEquiv.toEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

M ≃ N

View an equivalence of Lie modules as a type level equivalence.

Equations

e.toEquiv = { toFun := (↑e.toLieModuleHom).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

instance LieModuleEquiv.hasCoeToEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

CoeOut (M ≃ₗ⁅R,L⁆ N) (M ≃ N)

Equations

LieModuleEquiv.hasCoeToEquiv = { coe := LieModuleEquiv.toEquiv }

source

instance LieModuleEquiv.hasCoeToLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

Coe (M ≃ₗ⁅R,L⁆ N) (M →ₗ⁅R,L⁆ N)

Equations

LieModuleEquiv.hasCoeToLieModuleHom = { coe := LieModuleEquiv.toLieModuleHom }

source

instance LieModuleEquiv.hasCoeToLinearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

CoeOut (M ≃ₗ⁅R,L⁆ N) (M ≃ₗ[R] N)

Equations

LieModuleEquiv.hasCoeToLinearEquiv = { coe := LieModuleEquiv.toLinearEquiv }

source

instance LieModuleEquiv.instEquivLike {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

EquivLike (M ≃ₗ⁅R,L⁆ N) M N

Equations

LieModuleEquiv.instEquivLike = { coe := fun (f : M ≃ₗ⁅R,L⁆ N) => (↑f.toLieModuleHom).toFun, inv := fun (f : M ≃ₗ⁅R,L⁆ N) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

source

@[simp]

theorem LieModuleEquiv.coe_coe {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

⇑e.toLieModuleHom = ⇑e

source

theorem LieModuleEquiv.injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

Function.Injective ⇑e

source

theorem LieModuleEquiv.surjective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

Function.Surjective ⇑e

source

@[simp]

theorem LieModuleEquiv.toEquiv_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (g : N → M) (h₁ : Function.LeftInverse g (↑f).toFun) (h₂ : Function.RightInverse g (↑f).toFun) :

{ toLieModuleHom := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toEquiv = { toFun := ⇑f, invFun := g, left_inv := h₁, right_inv := h₂ }

source

@[simp]

theorem LieModuleEquiv.coe_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (invFun : N → M) (h₁ : Function.LeftInverse invFun (↑f).toFun) (h₂ : Function.RightInverse invFun (↑f).toFun) :

⇑{ toLieModuleHom := f, invFun := invFun, left_inv := h₁, right_inv := h₂ } = ⇑f

source

theorem LieModuleEquiv.coe_toLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

⇑e.toLieModuleHom = ⇑e

source

@[deprecated LieModuleEquiv.coe_toLieModuleHom (since := "2024-12-30")]

theorem LieModuleEquiv.coe_to_lieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

⇑e.toLieModuleHom = ⇑e

Alias of LieModuleEquiv.coe_toLieModuleHom.

source

@[simp]

theorem LieModuleEquiv.coe_toLinearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

⇑e.toLinearEquiv = ⇑e

source

@[deprecated LieModuleEquiv.coe_toLinearEquiv (since := "2024-12-30")]

theorem LieModuleEquiv.coe_to_linearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

⇑e.toLinearEquiv = ⇑e

Alias of LieModuleEquiv.coe_toLinearEquiv.

source

theorem LieModuleEquiv.toEquiv_injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

Function.Injective toEquiv

source

theorem LieModuleEquiv.ext {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e₁ e₂ : M ≃ₗ⁅R,L⁆ N) (h : ∀ (m : M), e₁ m = e₂ m) :

e₁ = e₂

source

instance LieModuleEquiv.instOne {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

One (M ≃ₗ⁅R,L⁆ M)

Equations

LieModuleEquiv.instOne = { one := let __src := 1; { toLinearMap := ↑__src, map_lie' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ } }

source

@[simp]

theorem LieModuleEquiv.one_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (m : M) :

1 m = m

source

instance LieModuleEquiv.instInhabited {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Inhabited (M ≃ₗ⁅R,L⁆ M)

Equations

LieModuleEquiv.instInhabited = { default := 1 }

source

def LieModuleEquiv.refl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

M ≃ₗ⁅R,L⁆ M

Lie module equivalences are reflexive.

Equations

LieModuleEquiv.refl = 1

Instances For

source

@[simp]

theorem LieModuleEquiv.refl_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (m : M) :

refl m = m

source

def LieModuleEquiv.symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

N ≃ₗ⁅R,L⁆ M

Lie module equivalences are symmetric.

Equations

e.symm = { toLieModuleHom := e.inverse e.invFun ⋯ ⋯, invFun := e.toLinearEquiv.symm.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LieModuleEquiv.apply_symm_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) (x : N) :

e (e.symm x) = x

source

@[simp]

theorem LieModuleEquiv.symm_apply_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) (x : M) :

e.symm (e x) = x

source

theorem LieModuleEquiv.apply_eq_iff_eq_symm_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] {m : M} {n : N} (e : M ≃ₗ⁅R,L⁆ N) :

e m = n ↔ m = e.symm n

source

@[simp]

theorem LieModuleEquiv.symm_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

e.symm.symm = e

source

theorem LieModuleEquiv.symm_bijective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

Function.Bijective symm

source

def LieModuleEquiv.trans {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) :

M ≃ₗ⁅R,L⁆ P

Lie module equivalences are transitive.

Equations

e₁.trans e₂ = { toLieModuleHom := e₂.comp e₁.toLieModuleHom, invFun := (e₁.toLinearEquiv.trans e₂.toLinearEquiv).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LieModuleEquiv.trans_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) (m : M) :

(e₁.trans e₂) m = e₂ (e₁ m)

source

@[simp]

theorem LieModuleEquiv.symm_trans {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) :

(e₁.trans e₂).symm = e₂.symm.trans e₁.symm

source

@[simp]

theorem LieModuleEquiv.self_trans_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

e.trans e.symm = refl

source

@[simp]

theorem LieModuleEquiv.symm_trans_self {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) :

e.symm.trans e = refl

Documentation

Mathlib.Algebra.Lie.Basic

Lie algebras #

Main definitions #

Notation #

Implementation notes #

References #

Tags #