inclusion — Mathlib

English

Given I1 ⊆ I2, the natural inclusion map I1 → I2 is a Lie algebra homomorphism.

Русский

Если I1 ⊆ I2, естественное включение I1 → I2 является гомоморфизмом Ли-алгебр.

LaTeX

$$$I_1 \le I_2 \Rightarrow \text{incl}: I_1 \to I_2 \text{ is a LieHom}$$$

Lean4

/-- Given two nested Lie ideals `I₁ ⊆ I₂`, the inclusion `I₁ ↪ I₂` is a morphism of Lie algebras. -/
def inclusion {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) : I₁ →ₗ⁅R⁆ I₂
    where
  __ := Submodule.inclusion (show I₁.toSubmodule ≤ I₂.toSubmodule from h)
  map_lie' := rfl

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