Casimir 元

noncomputable def UniversalEnvelopingAlgebra.casimirOfFaithful (K : Type u_1) (L : Type u_2) (V : Type u_3) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K V] [LieAlgebra.HasTrivialRadical K L] [LieModule.IsFaithful K L V] [FiniteDimensional K L] : UniversalEnvelopingAlgebra K L

TODO: {name (scope := "Ado.Casimir")}casimir が忠実ならこれと等しい事に示して統一

Equations

• UniversalEnvelopingAlgebra.casimirOfFaithful K L V = UniversalEnvelopingAlgebra.casimirOfBasis✝ V (Module.finBasis K L)

theorem UniversalEnvelopingAlgebra.casimirOfFaithful_eq {K : Type u_1} {L : Type u_2} (V : Type u_3) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K V] [LieAlgebra.HasTrivialRadical K L] [LieModule.IsFaithful K L V] {x✝ : FiniteDimensional K L} {n : Type u_4} [Fintype n] [DecidableEq n] (B : Module.Basis n K L) : casimirOfFaithful K L V = ∑ i : n, (ι K) (B i) * (ι K) (((LieModule.traceForm K L V).dualBasis ⋯ B) i)

theorem UniversalEnvelopingAlgebra.trace_lift_casimirOfFaithful (K : Type u_1) (L : Type u_2) (V : Type u_3) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K V] [LieAlgebra.HasTrivialRadical K L] [LieModule.IsFaithful K L V] [FiniteDimensional K L] : (LinearMap.trace K V) (((lift K) (LieModule.toEnd K L V)) (casimirOfFaithful K L V)) = ↑(Module.finrank K L)

theorem UniversalEnvelopingAlgebra.lift_casimirOfFaithful_comm (K : Type u_1) {L : Type u_2} {V : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K V] [LieAlgebra.HasTrivialRadical K L] [LieModule.IsFaithful K L V] [FiniteDimensional K L] (x : L) (v : V) : (((lift K) (LieModule.toEnd K L V)) (casimirOfFaithful K L V)) ⁅x, v⁆ = ⁅x, (((lift K) (LieModule.toEnd K L V)) (casimirOfFaithful K L V)) v⁆

noncomputable def UniversalEnvelopingAlgebra.casimir (K : Type u_1) (L : Type u_2) (V : Type u_3) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K V] [LieAlgebra.HasTrivialRadical K L] [FiniteDimensional K L] : UniversalEnvelopingAlgebra K L

Equations

• UniversalEnvelopingAlgebra.casimir K L V = (UniversalEnvelopingAlgebra.map K (LieModule.ker K L V)ᶜ.incl) (UniversalEnvelopingAlgebra.casimirOfFaithful K (↥(LieModule.ker K L V)ᶜ) V)

theorem UniversalEnvelopingAlgebra.lift_casimir_eq_lift_casimirOfFaithful (K : Type u_1) (L : Type u_2) (V : Type u_3) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K V] [LieAlgebra.HasTrivialRadical K L] [FiniteDimensional K L] : ((lift K) (LieModule.toEnd K L V)) (casimir K L V) = ((lift K) (LieModule.toEnd K (↥(LieModule.ker K L V)ᶜ) V)) (casimirOfFaithful K (↥(LieModule.ker K L V)ᶜ) V)

theorem UniversalEnvelopingAlgebra.trace_lift_casimir (K : Type u_1) (L : Type u_2) (V : Type u_3) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K V] [LieAlgebra.HasTrivialRadical K L] [FiniteDimensional K L] : (LinearMap.trace K V) (((lift K) (LieModule.toEnd K L V)) (casimir K L V)) = ↑(Module.finrank K L) - ↑(Module.finrank K ↥(LieModule.ker K L V))

theorem UniversalEnvelopingAlgebra.lift_casimir_comm (K : Type u_1) {L : Type u_2} {V : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K V] [LieAlgebra.HasTrivialRadical K L] [FiniteDimensional K L] (x : L) (v : V) : (((lift K) (LieModule.toEnd K L V)) (casimir K L V)) ⁅x, v⁆ = ⁅x, (((lift K) (LieModule.toEnd K L V)) (casimir K L V)) v⁆

theorem LieDerivation.exists_lift_casimir_apply_eq_lie {K : Type u_1} {L : Type u_2} {V : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K V] [LieAlgebra.HasTrivialRadical K L] [FiniteDimensional K L] (D : LieDerivation K L V) : ∃ (v : V), ∀ (x : L), (((UniversalEnvelopingAlgebra.lift K) (LieModule.toEnd K L V)) (UniversalEnvelopingAlgebra.casimir K L V)) (D x) = ⁅x, v⁆

theorem LieModule.Cohomology.exists_lift_casimir_twoCocycle_apply_eq_d₁₂ {K : Type u_1} {L : Type u_2} {V : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K V] [LieAlgebra.HasTrivialRadical K L] [FiniteDimensional K L] (f : ↥(twoCochain K L V)) (hf : f ∈ twoCocycle K L V) : ∃ (g : oneCochain K L V), ∀ (x y : L), (((UniversalEnvelopingAlgebra.lift K) (toEnd K L V)) (UniversalEnvelopingAlgebra.casimir K L V)) ((f x) y) = (((d₁₂ K L V) g) x) y