Direct sums of Lie algebras and Lie modules #
Direct sums of Lie algebras and Lie modules carry natural algbebra 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 (⨁ (i : ι), M i)
Equations
- direct_sum.lie_ring_module = {to_has_bracket := {bracket := λ (x : L) (m : ⨁ (i : ι), M i), dfinsupp.map_range (λ (i : ι) (m' : (λ (i : ι), M i) i), ⁅x,m'⁆) _ m}, add_lie := _, lie_add := _, leibniz_lie := _}
@[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 : ⨁ (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 (⨁ (i : ι), M i)
Equations
- direct_sum.lie_module = {smul_lie := _, lie_smul := _}
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 : ι) :
The inclusion of each component into a direct sum as a morphism of Lie modules.
Equations
- direct_sum.lie_module_of R ι L M j = {to_linear_map := {to_fun := (direct_sum.lof R ι M j).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}
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 : ι) :
The projection map onto one component, as a morphism of Lie modules.
Equations
- direct_sum.lie_module_component R ι L M j = {to_linear_map := {to_fun := (direct_sum.component R ι M j).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}
The direct sum of Lie algebras carries a natural Lie algebra structure.
@[protected, instance]
def
direct_sum.lie_ring
{ι : Type v}
(L : ι → Type w)
[Π (i : ι), lie_ring (L i)] :
lie_ring (⨁ (i : ι), L i)
Equations
- direct_sum.lie_ring L = {to_add_comm_group := {add := add_comm_group.add infer_instance, add_assoc := _, zero := add_comm_group.zero infer_instance, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg infer_instance, sub := add_comm_group.sub infer_instance, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul infer_instance, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}, to_has_bracket := {bracket := dfinsupp.zip_with (λ (i : ι) (x y : (λ (i : ι), L i) i), ⁅x,y⁆) _}, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}
@[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 (⨁ (i : ι), L i)
Equations
- direct_sum.lie_algebra L = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action infer_instance, add_smul := _, zero_smul := _}, lie_smul := _}
@[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) :
⇑(direct_sum.lie_algebra_of R ι L j) ᾰ = ⇑(direct_sum.of 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) :
⇑((direct_sum.lie_algebra_of R ι L j).to_linear_map) ᾰ = ⇑(direct_sum.of 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 : ι) :
The inclusion of each component into the direct sum as morphism of Lie algebras.
Equations
- direct_sum.lie_algebra_of R ι L j = {to_linear_map := {to_fun := ⇑(direct_sum.of L j), map_add' := _, map_smul' := _}, map_lie' := _}
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 : ι) :
The projection map onto one component, as a morphism of Lie algebras.
Equations
- direct_sum.lie_algebra_component R ι L j = {to_linear_map := {to_fun := ⇑(direct_sum.component R ι L j), map_add' := _, map_smul' := _}, map_lie' := _}
@[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 : ι)
(ᾰ : ⨁ (i : ι), L i) :
⇑((direct_sum.lie_algebra_component R ι L j).to_linear_map) ᾰ = ⇑(direct_sum.component R ι L j) ᾰ
@[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 : ι)
(ᾰ : ⨁ (i : ι), L i) :
⇑(direct_sum.lie_algebra_component R ι L j) ᾰ = ⇑(direct_sum.component R ι L j) ᾰ
@[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 : ⨁ (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) :
⁅⇑(direct_sum.of L i) x,⇑(direct_sum.of L j) y⁆ = 0
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) :
⁅⇑(direct_sum.of L i) x,⇑(direct_sum.of L j) y⁆ = ⇑(direct_sum.of L i) ⁅x,hij.rec_on y⁆
@[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) :
@[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)
(ᾰ : ⨁ (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) :
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
- direct_sum.to_lie_algebra L' f hf = {to_linear_map := {to_fun := ⇑(direct_sum.to_module R ι L' (λ (i : ι), ↑(f i))), map_add' := _, map_smul' := _}, map_lie' := _}
@[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)
(ᾰ : ⨁ (i : ι), (λ (i : ι), L i) i) :
⇑(direct_sum.to_lie_algebra L' f hf) ᾰ = ⇑(direct_sum.to_module R ι L' (λ (i : ι), ↑(f i))) ᾰ
def
direct_sum.lie_algebra_is_internal
{R : Type u}
{ι : Type v}
[comm_ring R]
{L : Type w}
[lie_ring L]
[lie_algebra R L]
(I : ι → lie_ideal R L)
[decidable_eq ι] :
Prop
Given a Lie algebra L and a family of ideals I i ⊆ L, informally this definition is the
statement that L = ⨁ i, I i.
More formally, the inclusions give a natural map from the (external) direct sum to the enclosing Lie
algebra: (⨁ i, I i) → L, and this definition is the proposition that this map is bijective.
Equations
- direct_sum.lie_algebra_is_internal I = function.bijective ⇑(direct_sum.to_module R ι L (λ (i : ι), ↑((I i).incl)))
@[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) :
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
- direct_sum.lie_ring_of_ideals I = direct_sum.lie_ring (λ (i : ι), ↥(I i))
@[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 (⨁ (i : ι), ↥(I i))
See direct_sum.lie_ring_of_ideals comment.
Equations
- direct_sum.lie_algebra_of_ideals I = direct_sum.lie_algebra (λ (i : ι), ↥(I i))