ad_comp_incl_eq — Mathlib

English

For a Lie subalgebra K ⊆ L and x ∈ K, the adjoint action of x composed with the inclusion K ↪ L equals the inclusion composed with ad on K.

Русский

Для подалгебры K ⊆ L и x ∈ K, действие ad x после включения равно включению после ad на K.

LaTeX

$$$\mathrm{ad}_{R,L} \uparrow x \circ (\mathrm{incl}_{K}) = (\mathrm{incl}_{K}) \circ \mathrm{ad}_{R,K} x$$$

Lean4

theorem ad_comp_incl_eq (K : LieSubalgebra R L) (x : K) :
    (ad R L ↑x).comp (K.incl : K →ₗ[R] L) = (K.incl : K →ₗ[R] L).comp (ad R K x) :=
  by
  ext y
  simp only [ad_apply, LieHom.coe_toLinearMap, LieSubalgebra.coe_incl, LinearMap.coe_comp, LieSubalgebra.coe_bracket,
    Function.comp_apply]

Похожие утверждения