Cyclic triple sums

Cyclic triple sums are meant as auxiliary tools for proving properties like Jacobi identities and Lie algebra 2-cocycle conditions.

Main definitions

• cyclicTripleSum: An auxiliary function given by ⟨x,y,z⟩ ↦ φ(x,β(y,z)) + φ(y,β(z,x)) + φ(z,β(x,y)) where φ and β are two-variable functions on a set V with values in sets W and V, respectively.
• cyclicTripleSumHom: A trilinear function given by ⟨x,y,z⟩ ↦ φ(x,β(y,z)) + φ(y,β(z,x)) + φ(z,β(x,y)) where φ and β are bilinear functions on V with values in sets W and V, respectively. This function can be used in calculations towards the Jacobi identity in Lie algebras and the Lie algebra 2-cocycle condition.

Main statements

A number of easy but convenient auxiliary properties towards trilinearity of cyclicTripleSumHom β φ (which is mathematically trivial but should not be repeated too often in Lean) are proven for the cyclic triple sums:

• cyclicTripleSum_map_add_of_bilin: If the functions φ and β are bilinear, then the cyclic triple sum is additive in its last variable. Additivity in the first and second variable are similarly obtained (the results immediately after).
• cyclicTripleSum_map_smul_of_bilin: If the functions φ and β are bilinear, then the cyclic triple sum respects scalar multiplication in its last variable. Scalar multiplication in the first and second variable are similarly obtained (the results immediately after).

Tags

Jacobi identity, Lie algebra 2-cocycle condition

Cyclic triple sums as tools for Jacobi identities and 2-cocycle conditions

def VirasoroProject.cyclicTripleSum {V : Type u_1} {W : Type u_2} [Add W] (β : V → V → V) (φ : V → V → W) (x y z : V) : W

An auxiliary function for proofs of Jacobi identities etc.

Given functions β : V × V → V and φ : V × V → W where W has additive structure, cyclicTripleSum β φ is the function of three variables on V defined by: ⟨x,y,z⟩ ↦ φ(x,β(y,z)) + φ(y,β(z,x)) + φ(z,β(x,y)).

Equations

• VirasoroProject.cyclicTripleSum β φ x y z = φ x (β y z) + φ y (β z x) + φ z (β x y)

theorem VirasoroProject.cyclicTripleSum_apply {V : Type u_1} {W : Type u_2} [Add W] (β : V → V → V) (φ : V → V → W) (x y z : V) : cyclicTripleSum β φ x y z = φ x (β y z) + φ y (β z x) + φ z (β x y)

theorem VirasoroProject.cyclicTripleSum_cyclic {V : Type u_1} {W : Type u_2} [AddCommMonoid W] (β : V → V → V) (φ : V → V → W) (x y z : V) : cyclicTripleSum β φ x y z = cyclicTripleSum β φ y z x

theorem VirasoroProject.cyclicTripleSum_cyclic' {V : Type u_1} {W : Type u_2} [AddCommMonoid W] (β : V → V → V) (φ : V → V → W) (x y z : V) : cyclicTripleSum β φ x y z = cyclicTripleSum β φ z x y

theorem VirasoroProject.cyclicTripleSum_map_add_fst_of_map_add {V : Type u_1} {W : Type u_2} [AddCommMonoid W] [Add V] (β : V → V → V) (φ : V → V → W) (h : ∀ (x y z₁ z₂ : V), cyclicTripleSum β φ x y (z₁ + z₂) = cyclicTripleSum β φ x y z₁ + cyclicTripleSum β φ x y z₂) (x₁ x₂ y z : V) : cyclicTripleSum β φ (x₁ + x₂) y z = cyclicTripleSum β φ x₁ y z + cyclicTripleSum β φ x₂ y z

theorem VirasoroProject.cyclicTripleSum_map_add_snd_of_map_add {V : Type u_1} {W : Type u_2} [AddCommMonoid W] [Add V] (β : V → V → V) (φ : V → V → W) (h : ∀ (x y z₁ z₂ : V), cyclicTripleSum β φ x y (z₁ + z₂) = cyclicTripleSum β φ x y z₁ + cyclicTripleSum β φ x y z₂) (x y₁ y₂ z : V) : cyclicTripleSum β φ x (y₁ + y₂) z = cyclicTripleSum β φ x y₁ z + cyclicTripleSum β φ x y₂ z

theorem VirasoroProject.cyclicTripleSum_map_smul_fst_of_map_smul {V : Type u_1} {W : Type u_2} [AddCommMonoid W] {R : Type u_3} [SMul R V] [SMul R W] (β : V → V → V) (φ : V → V → W) (h : ∀ (c : R) (x y z : V), cyclicTripleSum β φ x y (c • z) = c • cyclicTripleSum β φ x y z) (c : R) (x y z : V) : cyclicTripleSum β φ (c • x) y z = c • cyclicTripleSum β φ x y z

theorem VirasoroProject.cyclicTripleSum_map_smul_snd_of_map_smul {V : Type u_1} {W : Type u_2} [AddCommMonoid W] {R : Type u_3} [SMul R V] [SMul R W] (β : V → V → V) (φ : V → V → W) (h : ∀ (c : R) (x y z : V), cyclicTripleSum β φ x y (c • z) = c • cyclicTripleSum β φ x y z) (c : R) (x y z : V) : cyclicTripleSum β φ x (c • y) z = c • cyclicTripleSum β φ x y z

theorem VirasoroProject.cyclicTripleSum_map_add_of_bilin {V : Type u_1} {W : Type u_2} [AddCommMonoid V] [AddCommMonoid W] (β : V →+ V →+ V) (φ : V →+ V →+ W) (x y z₁ z₂ : V) : cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x y (z₁ + z₂) = cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x y z₁ + cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x y z₂

theorem VirasoroProject.cyclicTripleSum_map_add_snd_of_bilin {V : Type u_1} {W : Type u_2} [AddCommMonoid V] [AddCommMonoid W] (β : V →+ V →+ V) (φ : V →+ V →+ W) (x y₁ y₂ z : V) : cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x (y₁ + y₂) z = cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x y₁ z + cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x y₂ z

theorem VirasoroProject.cyclicTripleSum_map_add_fst_of_bilin {V : Type u_1} {W : Type u_2} [AddCommMonoid V] [AddCommMonoid W] (β : V →+ V →+ V) (φ : V →+ V →+ W) (x₁ x₂ y z : V) : cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) (x₁ + x₂) y z = cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x₁ y z + cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x₂ y z

theorem VirasoroProject.cyclicTripleSum_map_smul_of_bilin {V : Type u_1} {W : Type u_2} [AddCommMonoid V] [AddCommMonoid W] {𝕜 : Type u_3} [CommSemiring 𝕜] [Module 𝕜 V] [Module 𝕜 W] (β : V →ₗ[𝕜] V →ₗ[𝕜] V) (φ : V →ₗ[𝕜] V →ₗ[𝕜] W) (c : 𝕜) (x y z : V) : cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x y (c • z) = c • cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x y z

theorem VirasoroProject.cyclicTripleSum_map_smul_fst_of_bilin {V : Type u_1} {W : Type u_2} [AddCommMonoid V] [AddCommMonoid W] {𝕜 : Type u_3} [CommSemiring 𝕜] [Module 𝕜 V] [Module 𝕜 W] (β : V →ₗ[𝕜] V →ₗ[𝕜] V) (φ : V →ₗ[𝕜] V →ₗ[𝕜] W) (c : 𝕜) (x y z : V) : cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) (c • x) y z = c • cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x y z

theorem VirasoroProject.cyclicTripleSum_map_smul_snd_of_bilin {V : Type u_1} {W : Type u_2} [AddCommMonoid V] [AddCommMonoid W] {𝕜 : Type u_3} [CommSemiring 𝕜] [Module 𝕜 V] [Module 𝕜 W] (β : V →ₗ[𝕜] V →ₗ[𝕜] V) (φ : V →ₗ[𝕜] V →ₗ[𝕜] W) (c : 𝕜) (x y z : V) : cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x (c • y) z = c • cyclicTripleSum (fun (a : V) => ⇑(β a)) (fun (a : V) => ⇑(φ a)) x y z

def LinearMap.toBiadditive {V₁ : Type u_1} {V₂ : Type u_2} {V₃ : Type u_3} [AddCommMonoid V₁] [AddCommMonoid V₂] [AddCommMonoid V₃] {R₁ : Type u_4} {R₂ : Type u_5} {R₃ : Type u_6} [CommSemiring R₁] [CommSemiring R₂] [CommSemiring R₃] {σ : R₁ →+* R₃} {τ : R₂ →+* R₃} [Module R₁ V₁] [Module R₂ V₂] [Module R₃ V₃] (f : V₁ →ₛₗ[σ] V₂ →ₛₗ[τ] V₃) : V₁ →+ V₂ →+ V₃

"Coerce" a bilinear map into a biadditive map.

Equations

• f.toBiadditive = { toFun := fun (x : V₁) => { toFun := fun (y : V₂) => (f x) y, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def VirasoroProject.cyclicTripleSumHom {V : Type u_1} {W : Type u_2} [AddCommMonoid V] [AddCommMonoid W] {𝕜 : Type u_3} [CommSemiring 𝕜] [Module 𝕜 V] [Module 𝕜 W] (β : V →ₗ[𝕜] V →ₗ[𝕜] V) (φ : V →ₗ[𝕜] V →ₗ[𝕜] W) : V →ₗ[𝕜] V →ₗ[𝕜] V →ₗ[𝕜] W

An auxiliary trilinear map for proofs of Jacobi identities.

Given bilinear functions β : V × V → V and φ : V × V → W, cyclicTripleSumHom β φ is the trilinear function on V defined by: ⟨x,y,z⟩ ↦ φ(x,β(y,z)) + φ(y,β(z,x)) + φ(z,β(x,y)).

Equations

• One or more equations did not get rendered due to their size.

theorem VirasoroProject.cyclicTripleSumHom_apply {V : Type u_1} {W : Type u_2} [AddCommMonoid V] [AddCommMonoid W] {𝕜 : Type u_3} [CommSemiring 𝕜] [Module 𝕜 V] [Module 𝕜 W] (β : V →ₗ[𝕜] V →ₗ[𝕜] V) (φ : V →ₗ[𝕜] V →ₗ[𝕜] W) (x y z : V) : (((cyclicTripleSumHom β φ) x) y) z = (φ x) ((β y) z) + (φ y) ((β z) x) + (φ z) ((β x) y)