Mathlib.Algebra.Lie.Prod

Products of Lie algebras #

This file defines the Lie algebra structure the Product of two Lie algebras

Main definitions #

products in the domain:
- LieHom.fst The first projection of a product is a Lie algebra map.
- LieHom.snd The second projection of a product is a Lie algebra map.
- LieHom.prod_ext Split equality of Lie algebra homomorphisms from a product into Lie algebra homomorphism over each component,
products in the codomain:
- LieHom.inl The left injection into a product is a Lie algebra map.
- LieHom.inr The right injection into a product is a Lie algebra map.
- LieHom.prod The prod of two Lie algebra homomorphisms is a Lie algebra homomorphism.
products in both domain and codomain:
- LieHom.prodMap the Prod.map of two Lie algebra homomorphisms is a Lie algebra homomorphism.

Todo: Extend to further functionality from LinearMap.prod e.g. #

Lie Equivalences related to products
Lie Submodule statements

source

🔸 coverage

@[implicit_reducible]

instance LieAlgebra.Prod.instLieRing {L₁ : Type u_2} {L₂ : Type u_3} [LieRing L₁] [LieRing L₂] :

LieRing (L₁ × L₂)

source

📐 coverage

@[simp]

theorem LieAlgebra.Prod.bracket_apply {L₁ : Type u_2} {L₂ : Type u_3} [LieRing L₁] [LieRing L₂] (x y : L₁ × L₂) :

⁅x, y⁆ = (⁅x.1, y.1⁆, ⁅x.2, y.2⁆)

source

🔸 coverage

@[implicit_reducible]

instance LieAlgebra.Prod.instLieAlgebra {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

LieAlgebra R (L₁ × L₂)

source

🔸 coverage

def LieHom.fst (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

L₁ × L₂ →ₗ⁅R⁆ L₁

The first projection of a product is a Lie algebra map.

Instances For

source

🔸 coverage

def LieHom.snd (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

L₁ × L₂ →ₗ⁅R⁆ L₂

The second projection of a product is a Lie algebra map.

Instances For

source

🔸 coverage

def LieHom.inl (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

L₁ →ₗ⁅R⁆ L₁ × L₂

The left injection into a product is a Lie algebra map.

Instances For

source

🔸 coverage

def LieHom.inr (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

L₂ →ₗ⁅R⁆ L₁ × L₂

The right injection into a product is a Lie algebra map.

Instances For

source

📐 coverage

@[simp]

theorem LieHom.fst_apply {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (x : L₁ × L₂) :

(fst R L₁ L₂) x = x.1

source

📐 coverage

@[simp]

theorem LieHom.snd_apply {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (x : L₁ × L₂) :

(snd R L₁ L₂) x = x.2

source

📐 coverage

@[simp]

theorem LieHom.coe_fst {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

⇑(fst R L₁ L₂) = Prod.fst

source

📐 coverage

@[simp]

theorem LieHom.coe_snd {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

⇑(snd R L₁ L₂) = Prod.snd

source

📐 coverage

theorem LieHom.fst_surjective {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

Function.Surjective ⇑(fst R L₁ L₂)

source

📐 coverage

theorem LieHom.snd_surjective {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

Function.Surjective ⇑(snd R L₁ L₂)

source

🔸 coverage

def LieHom.prod {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [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₁ × L₂

The prod of two Lie algebra homomorphisms is a Lie algebra homomorphism.

Instances For

source

📐 coverage

@[simp]

theorem LieHom.prod_apply {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [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₂) (i : L) :

(f.prod g) i = (f i, g i)

source

📐 coverage

theorem LieHom.coe_prod {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [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.prod g) = Pi.prod ⇑f ⇑g

source

📐 coverage

@[simp]

theorem LieHom.fst_prod {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [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₂) :

(fst R L₁ L₂).comp (f.prod g) = f

source

📐 coverage

@[simp]

theorem LieHom.snd_prod {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [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₂) :

(snd R L₁ L₂).comp (f.prod g) = g

source

📐 coverage

@[simp]

theorem LieHom.pair_fst_snd {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

(fst R L₁ L₂).prod (snd R L₁ L₂) = id

source

📐 coverage

theorem LieHom.prod_comp {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [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) (h : L →ₗ⁅R⁆ L₁) :

(f.prod g).comp h = (f.comp h).prod (g.comp h)

source

📐 coverage

theorem LieHom.inl_apply {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (x : L₁) :

(inl R L₁ L₂) x = (x, 0)

source

📐 coverage

theorem LieHom.inr_apply {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (x : L₂) :

(inr R L₁ L₂) x = (0, x)

source

📐 coverage

@[simp]

theorem LieHom.coe_inl {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

⇑(inl R L₁ L₂) = fun (x : L₁) => (x, 0)

source

📐 coverage

@[simp]

theorem LieHom.coe_inr {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

⇑(inr R L₁ L₂) = Prod.mk 0

source

📐 coverage

theorem LieHom.inl_injective {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

Function.Injective ⇑(inl R L₁ L₂)

source

📐 coverage

theorem LieHom.inr_injective {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

Function.Injective ⇑(inr R L₁ L₂)

source

📐 coverage

theorem LieHom.range_inl (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

(inl R L₁ L₂).range = LieIdeal.toLieSubalgebra R (L₁ × L₂) (snd R L₁ L₂).ker

source

📐 coverage

theorem LieHom.ker_snd (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

LieIdeal.toLieSubalgebra R (L₁ × L₂) (snd R L₁ L₂).ker = (inl R L₁ L₂).range

source

📐 coverage

theorem LieHom.range_inr (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

(inr R L₁ L₂).range = LieIdeal.toLieSubalgebra R (L₁ × L₂) (fst R L₁ L₂).ker

source

📐 coverage

theorem LieHom.ker_fst (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

LieIdeal.toLieSubalgebra R (L₁ × L₂) (fst R L₁ L₂).ker = (inr R L₁ L₂).range

source

📐 coverage

@[simp]

theorem LieHom.fst_comp_inl (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

(fst R L₁ L₂).comp (inl R L₁ L₂) = id

source

📐 coverage

@[simp]

theorem LieHom.snd_comp_inl (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

(snd R L₁ L₂).comp (inl R L₁ L₂) = 0

source

📐 coverage

@[simp]

theorem LieHom.fst_comp_inr (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

(fst R L₁ L₂).comp (inr R L₁ L₂) = 0

source

📐 coverage

@[simp]

theorem LieHom.snd_comp_inr (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

(snd R L₁ L₂).comp (inr R L₁ L₂) = id

source

📐 coverage

theorem LieHom.inl_eq_prod (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

inl R L₁ L₂ = id.prod 0

source

📐 coverage

theorem LieHom.inr_eq_prod (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :

inr R L₁ L₂ = prod 0 id

source

📐 coverage

theorem LieHom.prod_ext_iff (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) {L : Type u_4} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L] [LieAlgebra R L] {f g : L₁ × L₂ →ₗ⁅R⁆ L} :

f = g ↔ f.comp (inl R L₁ L₂) = g.comp (inl R L₁ L₂) ∧ f.comp (inr R L₁ L₂) = g.comp (inr R L₁ L₂)

source

theorem LieHom.prod_ext (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) {L : Type u_4} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L] [LieAlgebra R L] {f g : L₁ × L₂ →ₗ⁅R⁆ L} (hl : f.comp (inl R L₁ L₂) = g.comp (inl R L₁ L₂)) (hr : f.comp (inr R L₁ L₂) = g.comp (inr R L₁ L₂)) :

f = g

Split equality of Lie algebra homomorphisms from a product into Lie algebra homomorphism over each component, to allow ext to apply lemmas specific to L₁ →ₗ L and L₂ →ₗ L.

See note [partially-applied ext lemmas].

source

🔸 coverage

def LieHom.prodMap {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L₃ : Type u_5} {L₄ : Type u_6} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] [LieRing L₄] [LieAlgebra R L₄] (f : L₁ →ₗ⁅R⁆ L₃) (g : L₂ →ₗ⁅R⁆ L₄) :

L₁ × L₂ →ₗ⁅R⁆ L₃ × L₄

Prod.map of two Lie algebra homomorphisms.

Instances For

source

📐 coverage

theorem LieHom.coe_prodMap {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L₃ : Type u_5} {L₄ : Type u_6} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] [LieRing L₄] [LieAlgebra R L₄] (f : L₁ →ₗ⁅R⁆ L₃) (g : L₂ →ₗ⁅R⁆ L₄) :

⇑(f.prodMap g) = Prod.map ⇑f ⇑g

source

📐 coverage

@[simp]

theorem LieHom.prodMap_apply {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L₃ : Type u_5} {L₄ : Type u_6} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [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₁ × L₂) :

(f.prodMap g) x = (f x.1, g x.2)

source

📐 coverage

@[simp]

theorem LieHom.prodMap_id {R : Type u_1} {L₁ : Type u_2} {L : Type u_4} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L] [LieAlgebra R L] :

id.prodMap id = id

source

📐 coverage

@[simp]

theorem LieHom.prodMap_one {R : Type u_1} {L₁ : Type u_2} {L : Type u_4} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L] [LieAlgebra R L] :

prodMap 1 1 = 1

source

📐 coverage

theorem LieHom.prodMap_comp {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L₃ : Type u_5} {L₄ : Type u_6} {L₅ : Type u_7} {L₆ : Type u_8} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] [LieRing L₄] [LieAlgebra R L₄] [LieRing L₅] [LieAlgebra R L₅] [LieRing L₆] [LieAlgebra R L₆] (f₁₂ : L₁ →ₗ⁅R⁆ L₂) (f₂₃ : L₂ →ₗ⁅R⁆ L₃) (g₁₂ : L₄ →ₗ⁅R⁆ L₅) (g₂₃ : L₅ →ₗ⁅R⁆ L₆) :

(f₂₃.prodMap g₂₃).comp (f₁₂.prodMap g₁₂) = (f₂₃.comp f₁₂).prodMap (g₂₃.comp g₁₂)

source

📐 coverage

@[simp]

theorem LieHom.prodMap_zero {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L₃ : Type u_5} {L₄ : Type u_6} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] [LieRing L₄] [LieAlgebra R L₄] :

prodMap 0 0 = 0