@[simp]

theorem LieModule.Cohomology.twoCochain_mk_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] (f : L →ₗ[R] L →ₗ[R] M) (hf : f ∈ twoCochain R L M) (x : L) : ⟨f, hf⟩ x = f x

theorem LieModule.Cohomology.twoCocycle_lie_jacobi_eq_lie_apply {R : Type u_3} {L : Type u_1} {M : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (f : ↥(twoCochain R L M)) (hf : f ∈ twoCocycle R L M) (x y z : L) : (f ⁅x, y⁆) z + (f ⁅y, z⁆) x + (f ⁅z, x⁆) y = ⁅x, (f y) z⁆ + ⁅y, (f z) x⁆ + ⁅z, (f x) y⁆

def LieModule.Cohomology.twoCochain.compCodomain {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] (f : ↥(twoCochain R L M)) (g : M →ₗ⁅R,L⁆ M₂) : ↥(twoCochain R L M₂)

Equations

• LieModule.Cohomology.twoCochain.compCodomain f g = ⟨(↑f).compr₂ ↑g, ⋯⟩

@[simp]

theorem LieModule.Cohomology.twoCochain.compCodomain_apply_apply {R : Type u_3} {L : Type u_1} {M : Type u_2} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] (f : ↥(twoCochain R L M)) (g : M →ₗ⁅R,L⁆ M₂) (x y : L) : ((compCodomain f g) x) y = g ((f x) y)

@[simp]

theorem LieModule.Cohomology.twoCochain.compCodomain_mem_twoCocycle {R : Type u_3} {L : Type u_1} {M : Type u_2} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (f : ↥(twoCochain R L M)) (g : M →ₗ⁅R,L⁆ M₂) (hf : f ∈ twoCocycle R L M) : compCodomain f g ∈ twoCocycle R L M₂