mathlib3 documentation

algebra.lie.base_change

Extension and restriction of scalars for Lie algebras #

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

Lie algebras have a well-behaved theory of extension and restriction of scalars.

Main definitions #

Tags #

lie ring, lie algebra, extension of scalars, restriction of scalars, base change

@[protected, instance]

def lie_algebra.extend_scalars.tensor_product.has_bracket (R : Type u) (A : Type w) (L : Type v) [comm_ring R] [comm_ring A] [algebra R A] [lie_ring L] [lie_algebra R L] :

has_bracket (tensor_product R A L) (tensor_product R A L)

Equations

lie_algebra.extend_scalars.tensor_product.has_bracket R A L = {bracket := λ (x y : tensor_product R A L), ⇑(⇑(bracket' R A L) x) y}

@[simp]

theorem lie_algebra.extend_scalars.bracket_tmul (R : Type u) (A : Type w) (L : Type v) [comm_ring R] [comm_ring A] [algebra R A] [lie_ring L] [lie_algebra R L] (s t : A) (x y : L) :

⁅s ⊗ₜ[R] x, t ⊗ₜ[R] y⁆ = (s * t) ⊗ₜ[R] ⁅x, y⁆

@[protected, instance]

def lie_algebra.extend_scalars.tensor_product.lie_ring (R : Type u) (A : Type w) (L : Type v) [comm_ring R] [comm_ring A] [algebra R A] [lie_ring L] [lie_algebra R L] :

lie_ring (tensor_product R A L)

Equations

lie_algebra.extend_scalars.tensor_product.lie_ring R A L = {to_add_comm_group := tensor_product.add_comm_group lie_algebra.to_module, to_has_bracket := lie_algebra.extend_scalars.tensor_product.has_bracket R A L _inst_5, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}

@[protected, instance]

def lie_algebra.extend_scalars.lie_algebra (R : Type u) (A : Type w) (L : Type v) [comm_ring R] [comm_ring A] [algebra R A] [lie_ring L] [lie_algebra R L] :

lie_algebra A (tensor_product R A L)

Equations

lie_algebra.extend_scalars.lie_algebra R A L = {to_module := tensor_product.left_module _, lie_smul := _}

@[protected, instance]

def lie_algebra.restrict_scalars.restrict_scalars.lie_ring (R : Type u) (A : Type w) (L : Type v) [h : lie_ring L] :

lie_ring (restrict_scalars R A L)

Equations

lie_algebra.restrict_scalars.restrict_scalars.lie_ring R A L = h

@[protected, instance]

def lie_algebra.restrict_scalars.lie_algebra (R : Type u) (A : Type w) (L : Type v) [h : lie_ring L] [comm_ring A] [lie_algebra A L] [comm_ring R] [algebra R A] :

lie_algebra R (restrict_scalars R A L)

Equations

lie_algebra.restrict_scalars.lie_algebra R A L = {to_module := restrict_scalars.module R A L lie_algebra.to_module, lie_smul := _}