isLieAbelian — Mathlib

English

If f: L1 → L2 is an injective Lie map and L2 is LieAbelian, then L1 is LieAbelian.

Русский

Если f: L1 → L2 строго инъективно как отображение Ли, и L2 является абелевым по Ли, то L1 тоже абелев.

LaTeX

$$IsLieAbelian(L1)$$

Lean4

theorem isLieAbelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁]
    [LieAlgebra R L₂] {f : L₁ →ₗ⁅R⁆ L₂} (h₁ : Function.Injective f) (_ : IsLieAbelian L₂) : IsLieAbelian L₁ :=
  {
    trivial := fun x y =>
      h₁ <|
        calc
          f ⁅x, y⁆ = ⁅f x, f y⁆ := LieHom.map_lie f x y
          _ = 0 := (trivial_lie_zero _ _ _ _)
          _ = f 0 := f.map_zero.symm }

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