mathlib3 documentation

algebra.lie.direct_sum

Direct sums of Lie algebras and Lie modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Direct sums of Lie algebras and Lie modules carry natural algebra and module structures.

Tags #

lie algebra, lie module, direct sum

The direct sum of Lie modules over a fixed Lie algebra carries a natural Lie module structure.

@[protected, instance]
def direct_sum.lie_ring_module {ι : Type v} {L : Type w₁} {M : ι Type w} [lie_ring L] [Π (i : ι), add_comm_group (M i)] [Π (i : ι), lie_ring_module L (M i)] :
lie_ring_module L (direct_sum ι (λ (i : ι), M i))
Equations
@[simp]
theorem direct_sum.lie_module_bracket_apply {ι : Type v} {L : Type w₁} {M : ι Type w} [lie_ring L] [Π (i : ι), add_comm_group (M i)] [Π (i : ι), lie_ring_module L (M i)] (x : L) (m : direct_sum ι (λ (i : ι), M i)) (i : ι) :
@[protected, instance]
def direct_sum.lie_module {R : Type u} {ι : Type v} [comm_ring R] {L : Type w₁} {M : ι Type w} [lie_ring L] [lie_algebra R L] [Π (i : ι), add_comm_group (M i)] [Π (i : ι), module R (M i)] [Π (i : ι), lie_ring_module L (M i)] [Π (i : ι), lie_module R L (M i)] :
lie_module R L (direct_sum ι (λ (i : ι), M i))
Equations
def direct_sum.lie_module_of (R : Type u) (ι : Type v) [comm_ring R] (L : Type w₁) (M : ι Type w) [lie_ring L] [lie_algebra R L] [Π (i : ι), add_comm_group (M i)] [Π (i : ι), module R (M i)] [Π (i : ι), lie_ring_module L (M i)] [Π (i : ι), lie_module R L (M i)] [decidable_eq ι] (j : ι) :
M j →ₗ⁅R,L direct_sum ι (λ (i : ι), M i)

The inclusion of each component into a direct sum as a morphism of Lie modules.

Equations
def direct_sum.lie_module_component (R : Type u) (ι : Type v) [comm_ring R] (L : Type w₁) (M : ι Type w) [lie_ring L] [lie_algebra R L] [Π (i : ι), add_comm_group (M i)] [Π (i : ι), module R (M i)] [Π (i : ι), lie_ring_module L (M i)] [Π (i : ι), lie_module R L (M i)] (j : ι) :
direct_sum ι (λ (i : ι), M i) →ₗ⁅R,L M j

The projection map onto one component, as a morphism of Lie modules.

Equations

The direct sum of Lie algebras carries a natural Lie algebra structure.

@[simp]
theorem direct_sum.bracket_apply {ι : Type v} (L : ι Type w) [Π (i : ι), lie_ring (L i)] (x y : direct_sum ι (λ (i : ι), L i)) (i : ι) :
@[protected, instance]
def direct_sum.lie_algebra {R : Type u} {ι : Type v} [comm_ring R] (L : ι Type w) [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] :
lie_algebra R (direct_sum ι (λ (i : ι), L i))
Equations
@[simp]
theorem direct_sum.lie_algebra_of_apply (R : Type u) (ι : Type v) [comm_ring R] (L : ι Type w) [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] [decidable_eq ι] (j : ι) (ᾰ : L j) :
@[simp]
theorem direct_sum.lie_algebra_of_to_linear_map_apply (R : Type u) (ι : Type v) [comm_ring R] (L : ι Type w) [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] [decidable_eq ι] (j : ι) (ᾰ : L j) :
def direct_sum.lie_algebra_of (R : Type u) (ι : Type v) [comm_ring R] (L : ι Type w) [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] [decidable_eq ι] (j : ι) :
L j →ₗ⁅R direct_sum ι (λ (i : ι), L i)

The inclusion of each component into the direct sum as morphism of Lie algebras.

Equations
def direct_sum.lie_algebra_component (R : Type u) (ι : Type v) [comm_ring R] (L : ι Type w) [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] (j : ι) :
direct_sum ι (λ (i : ι), L i) →ₗ⁅R L j

The projection map onto one component, as a morphism of Lie algebras.

Equations
@[simp]
theorem direct_sum.lie_algebra_component_to_linear_map_apply (R : Type u) (ι : Type v) [comm_ring R] (L : ι Type w) [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] (j : ι) (ᾰ : direct_sum ι (λ (i : ι), L i)) :
@[simp]
theorem direct_sum.lie_algebra_component_apply (R : Type u) (ι : Type v) [comm_ring R] (L : ι Type w) [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] (j : ι) (ᾰ : direct_sum ι (λ (i : ι), L i)) :
@[ext]
theorem direct_sum.lie_algebra_ext (R : Type u) (ι : Type v) [comm_ring R] (L : ι Type w) [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] {x y : direct_sum ι (λ (i : ι), L i)} (h : (i : ι), (direct_sum.lie_algebra_component R ι L i) x = (direct_sum.lie_algebra_component R ι L i) y) :
x = y
theorem direct_sum.lie_of_of_ne (R : Type u) (ι : Type v) [comm_ring R] (L : ι Type w) [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] [decidable_eq ι] {i j : ι} (hij : j i) (x : L i) (y : L j) :
theorem direct_sum.lie_of_of_eq (R : Type u) (ι : Type v) [comm_ring R] (L : ι Type w) [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] [decidable_eq ι] {i j : ι} (hij : j = i) (x : L i) (y : L j) :
@[simp]
theorem direct_sum.lie_of (R : Type u) (ι : Type v) [comm_ring R] (L : ι Type w) [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] [decidable_eq ι] {i j : ι} (x : L i) (y : L j) :
(direct_sum.of L i) x, (direct_sum.of L j) y = dite (j = i) (λ (hij : j = i), (direct_sum.lie_algebra_of R ι L i) x, hij.rec_on y) (λ (hij : ¬j = i), 0)
@[simp]
theorem direct_sum.to_lie_algebra_to_linear_map_apply {R : Type u} {ι : Type v} [comm_ring R] {L : ι Type w} [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] [decidable_eq ι] (L' : Type w₁) [lie_ring L'] [lie_algebra R L'] (f : Π (i : ι), L i →ₗ⁅R L') (hf : (i j : ι), i j (x : L i) (y : L j), (f i) x, (f j) y = 0) (ᾰ : direct_sum ι (λ (i : ι), (λ (i : ι), L i) i)) :
((direct_sum.to_lie_algebra L' f hf).to_linear_map) = (direct_sum.to_module R ι L' (λ (i : ι), (f i)))
def direct_sum.to_lie_algebra {R : Type u} {ι : Type v} [comm_ring R] {L : ι Type w} [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] [decidable_eq ι] (L' : Type w₁) [lie_ring L'] [lie_algebra R L'] (f : Π (i : ι), L i →ₗ⁅R L') (hf : (i j : ι), i j (x : L i) (y : L j), (f i) x, (f j) y = 0) :
direct_sum ι (λ (i : ι), L i) →ₗ⁅R L'

Given a family of Lie algebras L i, together with a family of morphisms of Lie algebras f i : L i →ₗ⁅R⁆ L' into a fixed Lie algebra L', we have a natural linear map: (⨁ i, L i) →ₗ[R] L'. If in addition ⁅f i x, f j y⁆ = 0 for any x ∈ L i and y ∈ L j (i ≠ j) then this map is a morphism of Lie algebras.

Equations
@[simp]
theorem direct_sum.to_lie_algebra_apply {R : Type u} {ι : Type v} [comm_ring R] {L : ι Type w} [Π (i : ι), lie_ring (L i)] [Π (i : ι), lie_algebra R (L i)] [decidable_eq ι] (L' : Type w₁) [lie_ring L'] [lie_algebra R L'] (f : Π (i : ι), L i →ₗ⁅R L') (hf : (i j : ι), i j (x : L i) (y : L j), (f i) x, (f j) y = 0) (ᾰ : direct_sum ι (λ (i : ι), (λ (i : ι), L i) i)) :
(direct_sum.to_lie_algebra L' f hf) = (direct_sum.to_module R ι L' (λ (i : ι), (f i)))
@[protected, instance]
def direct_sum.lie_ring_of_ideals {R : Type u} {ι : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] (I : ι lie_ideal R L) :
lie_ring (direct_sum ι (λ (i : ι), (I i)))

The fact that this instance is necessary seems to be a bug in typeclass inference. See [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ Typeclass.20resolution.20under.20binders/near/245151099).

Equations
@[protected, instance]
def direct_sum.lie_algebra_of_ideals {R : Type u} {ι : Type v} [comm_ring R] {L : Type w} [lie_ring L] [lie_algebra R L] (I : ι lie_ideal R L) :
lie_algebra R (direct_sum ι (λ (i : ι), (I i)))

See direct_sum.lie_ring_of_ideals comment.

Equations