Theorems · Definition · nonassociative algebras

skewAdjointLieSubalgebraEquiv

{R : Type u} →
  {M : Type v} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (B : LinearMap.BilinForm R M) →
            {N : Type w} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (e : N ≃ₗ[R] M) →
                    ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e)) ≃ₗ⁅R⁆ ↥(skewAdjointLieSubalgebra B)

An equivalence of modules with bilinear forms gives equivalence of Lie algebras of skew-adjoint endomorphisms.

Defined in

Mathlib.Algebra.Lie.SkewAdjoint

Cited by

2 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleAddCommGroupModule