# mathlibdocumentation

algebra.lie.base_change

# Extension and restriction of scalars for Lie algebras #

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

## Main definitions #

• lie_algebra.extend_scalars.lie_algebra
• lie_algebra.restrict_scalars.lie_algebra

## 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] [ A] [lie_ring L] [ L] :
has_bracket (A L) (A L)
Equations
@[simp]
theorem lie_algebra.extend_scalars.bracket_tmul (R : Type u) (A : Type w) (L : Type v) [comm_ring R] [comm_ring A] [ A] [lie_ring L] [ L] (s t : A) (x y : L) :
@[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] [ A] [lie_ring L] [ L] :
Equations
@[protected, instance]
def lie_algebra.extend_scalars.lie_algebra (R : Type u) (A : Type w) (L : Type v) [comm_ring R] [comm_ring A] [ A] [lie_ring L] [ L] :
(A L)
Equations
@[protected, instance]
def lie_algebra.restrict_scalars.restrict_scalars.lie_ring (R : Type u) (A : Type w) (L : Type v) [h : lie_ring L] :
Equations
@[protected, nolint, instance]
def lie_algebra.restrict_scalars.lie_algebra (R : Type u) (A : Type w) (L : Type v) [h : lie_ring L] [comm_ring A] [ L] [comm_ring R] [ A] :
A L)
Equations