def UnivEnvelopingAction.extendToUEA {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {V : Type u_3} [AddCommGroup V] [Module R V] (f : L →ₗ⁅R⁆ Module.End R V) : UniversalEnvelopingAlgebra R L →ₐ[R] Module.End R V

@[reducible, inline]

abbrev UnivEnvelopingAction.CenterUEA (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] : Subalgebra R (UniversalEnvelopingAlgebra R L)

theorem UnivEnvelopingAction.centerUEA_comm (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (a b : ↥(CenterUEA R L)) : a * b = b * a

def UnivEnvelopingAction.ActsByScalar (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] {V : Type u_3} [AddCommGroup V] [Module R V] (φ : UniversalEnvelopingAlgebra R L →ₐ[R] Module.End R V) (z : UniversalEnvelopingAlgebra R L) (c : R) : Prop

structure UnivEnvelopingAction.InfinitesimalCharacter (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] : Type (max u_1 u_2)

• toAlgHom : ↥(CenterUEA R L) →ₐ[R] R

def UnivEnvelopingAction.InfinitesimalCharacter.apply (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (χ : InfinitesimalCharacter R L) (z : ↥(CenterUEA R L)) : R

theorem UnivEnvelopingAction.center_acts_by_scalar (R : Type u_1) [Field R] [IsAlgClosed R] (L : Type u_2) [LieRing L] [LieAlgebra R L] {V : Type u_3} [AddCommGroup V] [Module R V] [Module (UniversalEnvelopingAlgebra R L) V] [IsScalarTower R (UniversalEnvelopingAlgebra R L) V] [IsSimpleModule (UniversalEnvelopingAlgebra R L) V] [Nontrivial V] [FiniteDimensional R V] (z : ↥(CenterUEA R L)) : ∃ (c : R), ∀ (v : V), ↑z • v = c • v

structure UnivEnvelopingAction.IsKillingDualBasis (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b d : ι → L) : Prop

• orthonormal (i j : ι) : ((killingForm R L) (b i)) (d j) = if i = j then 1 else 0
• expand_b (y : L) : y = ∑ i : ι, ((killingForm R L) y) (d i) • b i
• expand_d (y : L) : y = ∑ i : ι, ((killingForm R L) (b i)) y • d i

def UnivEnvelopingAction.casimirElement (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] {ι : Type u_3} [Fintype ι] (b d : ι → L) : UniversalEnvelopingAlgebra R L

theorem UnivEnvelopingAction.casimirElement_central (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b d : ι → L) (hbd : IsKillingDualBasis R L b d) : casimirElement R L b d ∈ Subalgebra.center R (UniversalEnvelopingAlgebra R L)