isLieAbelian — Mathlib

English

If f: L1 → L2 is surjective and L1 is LieAbelian, then L2 is LieAbelian.

Русский

Если f: L1 → L2 сюръективно и L1 абелев по Ли, то L2 абелев по Ли.

LaTeX

$$IsLieAbelian L2$$

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.Surjective f) (h₂ : IsLieAbelian L₁) : IsLieAbelian L₂ :=
  {
    trivial := fun x y => by
      obtain ⟨u, rfl⟩ := h₁ x
      obtain ⟨v, rfl⟩ := h₁ y
      rw [← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero] }

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