半直和から普遍被覆代数への作用

def LieAlgebra.SemiDirectSum.leftLieUEAux {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) : 𝔥 →ₗ[K] Module.End K (TensorAlgebra K 𝔞)

Equations

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

@[simp]

theorem LieAlgebra.SemiDirectSum.leftLieUEAux_ι {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔥) (y : 𝔞) : ((leftLieUEAux ψ) x) ((TensorAlgebra.ι K) y) = (TensorAlgebra.ι K) ((ψ x) y)

@[simp]

theorem LieAlgebra.SemiDirectSum.leftLieUEAux_tprod {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔥) {n : ℕ} (f : Fin n → 𝔞) : ((leftLieUEAux ψ) x) ((TensorAlgebra.tprod K 𝔞 n) f) = ∑ i : Fin n, (TensorAlgebra.tprod K 𝔞 n) (Function.update f i ((ψ x) (f i)))

theorem LieAlgebra.SemiDirectSum.leftLieUEAux_leftLieUEAux_tprod {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x y : 𝔥) {n : ℕ} (f : Fin n → 𝔞) : ((leftLieUEAux ψ) x) (((leftLieUEAux ψ) y) ((TensorAlgebra.tprod K 𝔞 n) f)) = ∑ i : Fin n, (TensorAlgebra.tprod K 𝔞 n) (Function.update f i ((ψ x) ((ψ y) (f i)))) + ∑ p ∈ Finset.univ.offDiag, (TensorAlgebra.tprod K 𝔞 n) (Function.update (Function.update f p.1 ((ψ y) (f p.1))) p.2 ((ψ x) (f p.2)))

theorem LieAlgebra.SemiDirectSum.leftLieUEAux_lie_left {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x y : 𝔥) (a : TensorAlgebra K 𝔞) : ((leftLieUEAux ψ) ⁅x, y⁆) a = ((leftLieUEAux ψ) x) (((leftLieUEAux ψ) y) a) - ((leftLieUEAux ψ) y) (((leftLieUEAux ψ) x) a)

theorem LieAlgebra.SemiDirectSum.leftLieUEAux_mul {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔥) (a b : TensorAlgebra K 𝔞) : ((leftLieUEAux ψ) x) (a * b) = a * ((leftLieUEAux ψ) x) b + ((leftLieUEAux ψ) x) a * b

theorem LieAlgebra.SemiDirectSum.mkAlgHom_leftLieUEAux_eq_of_ringCon {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔥) (a b : TensorAlgebra K 𝔞) (h : (UniversalEnvelopingAlgebra.ringCon K 𝔞) a b) : (UniversalEnvelopingAlgebra.mkAlgHom K 𝔞) (((leftLieUEAux ψ) x) a) = (UniversalEnvelopingAlgebra.mkAlgHom K 𝔞) (((leftLieUEAux ψ) x) b)

theorem LieAlgebra.SemiDirectSum.ringCon_leftLieUEAux_of_ringCon {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔥) (a b : TensorAlgebra K 𝔞) (h : (UniversalEnvelopingAlgebra.ringCon K 𝔞) a b) : (UniversalEnvelopingAlgebra.ringCon K 𝔞) (((leftLieUEAux ψ) x) a) (((leftLieUEAux ψ) x) b)

def LieAlgebra.SemiDirectSum.leftLieUE {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) : 𝔥 →ₗ[K] Module.End K (UniversalEnvelopingAlgebra K 𝔞)

Equations

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

theorem LieAlgebra.SemiDirectSum.leftLieUE_def {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔥) (a : UniversalEnvelopingAlgebra K 𝔞) : ((leftLieUE ψ) x) a = UniversalEnvelopingAlgebra.tensorLift (⇑(UniversalEnvelopingAlgebra.mkAlgHom K 𝔞) ∘ ⇑((leftLieUEAux ψ) x)) ⋯ a

theorem LieAlgebra.SemiDirectSum.leftLieUE_mkAlgHom {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔥) (a : TensorAlgebra K 𝔞) : ((leftLieUE ψ) x) ((UniversalEnvelopingAlgebra.mkAlgHom K 𝔞) a) = (UniversalEnvelopingAlgebra.mkAlgHom K 𝔞) (((leftLieUEAux ψ) x) a)

theorem LieAlgebra.SemiDirectSum.leftLieUE_lie_left {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x y : 𝔥) (a : UniversalEnvelopingAlgebra K 𝔞) : ((leftLieUE ψ) ⁅x, y⁆) a = ((leftLieUE ψ) x) (((leftLieUE ψ) y) a) - ((leftLieUE ψ) y) (((leftLieUE ψ) x) a)

@[simp]

theorem LieAlgebra.SemiDirectSum.leftLieUE_mul {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔥) (a b : UniversalEnvelopingAlgebra K 𝔞) : ((leftLieUE ψ) x) (a * b) = a * ((leftLieUE ψ) x) b + ((leftLieUE ψ) x) a * b

@[simp]

theorem LieAlgebra.SemiDirectSum.leftLieUE_ι {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔥) (y : 𝔞) : ((leftLieUE ψ) x) ((UniversalEnvelopingAlgebra.ι K) y) = (UniversalEnvelopingAlgebra.ι K) ((ψ x) y)

@[instance_reducible]

instance LieAlgebra.SemiDirectSum.instBracketUniversalEnvelopingAlgebra_ado {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) : Bracket (𝔞 ⋊⁅ψ⁆ 𝔥) (UniversalEnvelopingAlgebra K 𝔞)

Equations

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

theorem LieAlgebra.SemiDirectSum.lieUE_def {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] {ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞} (x : 𝔞 ⋊⁅ψ⁆ 𝔥) (a : UniversalEnvelopingAlgebra K 𝔞) : ⁅x, a⁆ = ⁅x.left, a⁆ + ((leftLieUE ψ) x.right) a

@[simp]

theorem LieAlgebra.SemiDirectSum.inl_lieUE {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔞) (a : UniversalEnvelopingAlgebra K 𝔞) : ⁅(inl ψ) x, a⁆ = ⁅x, a⁆

@[simp]

theorem LieAlgebra.SemiDirectSum.inr_lieUE {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔥) (a : UniversalEnvelopingAlgebra K 𝔞) : ⁅(inr ψ) x, a⁆ = ((leftLieUE ψ) x) a

theorem LieAlgebra.SemiDirectSum.add_lieUE {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] {ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞} (x y : 𝔞 ⋊⁅ψ⁆ 𝔥) (a : UniversalEnvelopingAlgebra K 𝔞) : ⁅x + y, a⁆ = ⁅x, a⁆ + ⁅y, a⁆

theorem LieAlgebra.SemiDirectSum.smul_lieUE {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] {ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞} (t : K) (x : 𝔞 ⋊⁅ψ⁆ 𝔥) (a : UniversalEnvelopingAlgebra K 𝔞) : ⁅t • x, a⁆ = t • ⁅x, a⁆

theorem LieAlgebra.SemiDirectSum.neg_lieUE {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] {ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞} (x : 𝔞 ⋊⁅ψ⁆ 𝔥) (a : UniversalEnvelopingAlgebra K 𝔞) : ⁅-x, a⁆ = -⁅x, a⁆

@[instance_reducible]

instance LieAlgebra.SemiDirectSum.instLieRingModuleUniversalEnvelopingAlgebra_ado {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) : LieRingModule (𝔞 ⋊⁅ψ⁆ 𝔥) (UniversalEnvelopingAlgebra K 𝔞)

Equations

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

instance LieAlgebra.SemiDirectSum.instLieModuleUniversalEnvelopingAlgebra_ado {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) : LieModule K (𝔞 ⋊⁅ψ⁆ 𝔥) (UniversalEnvelopingAlgebra K 𝔞)

@[simp]

theorem LieAlgebra.SemiDirectSum.toEndUE_inl {K : Type u_1} [Field K] {𝔞 : Type u_2} {𝔥 : Type u_3} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) (x : 𝔞) : (LieModule.toEnd K (𝔞 ⋊⁅ψ⁆ 𝔥) (UniversalEnvelopingAlgebra K 𝔞)) ((inl ψ) x) = (LieModule.toEnd K 𝔞 (UniversalEnvelopingAlgebra K 𝔞)) x