Theorems · Definition · nonassociative algebras

LieModule.Cohomology.twoCochain

(R : Type u_1) →
  [inst : CommRing R] →
    (L : Type u_2) →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (M : Type u_3) → [inst_3 : AddCommGroup M] → [inst_4 : Module R M] → Submodule R (L →ₗ[R] L →ₗ[R] M)

Lie algebra 2-cochains over L with coefficients in the module M.

Defined in

Mathlib.Algebra.Lie.Cochain

Cited by

38 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Quot.sound

Assumes

CommRingLieRingLieAlgebraAddCommGroupModule