lie_abelian_iff_equiv_lie_abelian

English

LieAbelian is preserved under Lie algebra isomorphisms: if e: L1 ≃_R L2 is a Lie equivalence, then L1 is LieAbelian iff L2 is LieAbelian.

Русский

Абелевность Ли сохраняется при изоморфизме Ли: если e: L1 ≃_R L2 — изоморфизм Ли, то L1 абелев по Ли тогда и только тогда, когда L2 абелев по Ли.

LaTeX

$$IsLieAbelian L1 ↔ IsLieAbelian L2$$

Lean4

theorem lie_abelian_iff_equiv_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁]
    [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) : IsLieAbelian L₁ ↔ IsLieAbelian L₂ :=
  ⟨e.symm.injective.isLieAbelian, e.injective.isLieAbelian⟩

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