def LieDerivation.adIdeal {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : L →ₗ⁅R⁆ LieDerivation R ↥I ↥I

Equations

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

@[simp]

theorem LieDerivation.adIdeal_apply_apply {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x : L) (m : ↥I) : ((adIdeal I) x) m = ⁅x, m⁆

def LieDerivation.compCodomain {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_4} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (D : LieDerivation R L M) (f : M →ₗ⁅R,L⁆ M₂) : LieDerivation R L M₂

Equations

• D.compCodomain f = { toLinearMap := ↑f ∘ₗ ↑D, leibniz' := ⋯ }

@[simp]

theorem LieDerivation.compCodomain_apply {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_4} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (D : LieDerivation R L M) (f : M →ₗ⁅R,L⁆ M₂) (x : L) : (D.compCodomain f) x = f (D x)

def LieDerivation.codRestrict {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_4} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (D : LieDerivation R L M) (h : ∀ (x : L), D x ∈ N) : LieDerivation R L ↥N

Equations

• LieDerivation.codRestrict N D h = { toLinearMap := LinearMap.codRestrict (↑N) (↑D) h, leibniz' := ⋯ }

@[simp]

theorem LieDerivation.codRestrict_apply_coe {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_4} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (D : LieDerivation R L M) (h : ∀ (x : L), D x ∈ N) (x : L) : ↑((codRestrict N D h) x) = D x

theorem LieDerivation.injective_toLinearMap (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Function.Injective toLinearMap

instance LieDerivation.instSubsingleton_ado {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_4} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Subsingleton M] : Subsingleton (LieDerivation R L M)