twoCochain — Mathlib

English

TwoCochain R L M is the submodule of linear maps c ∈ L →ₗ[R] (L →ₗ[R] M) such that ∀ x ∈ L, c x x = 0.

Русский

TwoCochain — подмодуль линейных отображений c ∈ L →ₗ[R] (L →ₗ[R] M) с условием ∀ x, c x x = 0.

LaTeX

$$$ twoCochain: = \{ c \in L →ₗ[R] (L →ₗ[R] M) \mid ∀ x, c(x)(x) = 0 \} $$$

Lean4

/-- Lie algebra 2-cochains over `L` with coefficients in the module `M`. -/
def twoCochain : Submodule R (L →ₗ[R] L →ₗ[R] M)
    where
  carrier := {c | ∀ x, c x x = 0}
  add_mem' {a b} ha hb x := by simp [ha x, hb x]
  zero_mem' := by simp
  smul_mem' t {c} hc x := by simp [hc x]

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