@[simp]

theorem LieAlgebra.SemiDirectSum.isIdealMorphism_inl {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : (inl ψ).IsIdealMorphism

instance LieAlgebra.SemiDirectSum.instFinite_ado {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) [Module.Finite R K] [Module.Finite R L] : Module.Finite R (K ⋊⁅ψ⁆ L)

def LieAlgebra.SemiDirectSum.equivIdealRangeInl {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : K ≃ₗ⁅R⁆ ↥(inl ψ).idealRange

Equations

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

@[simp]

theorem LieAlgebra.SemiDirectSum.equivIdealRangeInl_apply_coe {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K) : ↑((equivIdealRangeInl ψ) x) = (inl ψ) x

@[simp]

theorem LieAlgebra.SemiDirectSum.incl_idealRange_inl_equivIdealRangeInl {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : (inl ψ).idealRange.incl.comp (equivIdealRangeInl ψ).toLieHom = inl ψ

@[simp]

theorem LieAlgebra.SemiDirectSum.equivIdealRangeInl_symm_apply {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : ↥(inl ψ).idealRange) : (equivIdealRangeInl ψ).symm x = (↑x).left

def LieAlgebra.SemiDirectSum.equivRangeInr {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : L ≃ₗ⁅R⁆ ↥(inr ψ).range

Equations

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

@[simp]

theorem LieAlgebra.SemiDirectSum.equivRangeInr_apply_coe {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : L) : ↑((equivRangeInr ψ) x) = (inr ψ) x

@[simp]

theorem LieAlgebra.SemiDirectSum.equivRangeInr_symm_apply {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : ↥(inr ψ).range) : (equivRangeInr ψ).symm x = (↑x).right

theorem LieAlgebra.SemiDirectSum.inr_lie_inl {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : L) (y : K) : ⁅(inr ψ) x, (inl ψ) y⁆ = (inl ψ) ((ψ x) y)

theorem LieAlgebra.SemiDirectSum.inl_lie_inr {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K) (y : L) : ⁅(inl ψ) x, (inr ψ) y⁆ = -(inl ψ) ((ψ y) x)

def LieAlgebra.SemiDirectSum.lift {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] {L₂ : Type u_4} [LieRing L₂] [LieAlgebra R L₂] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (f : K →ₗ⁅R⁆ L₂) (g : L →ₗ⁅R⁆ L₂) (h : ∀ (x : L), ↑f ∘ₗ ↑(ψ x) = (ad R L₂) (g x) ∘ₗ ↑f) : K ⋊⁅ψ⁆ L →ₗ⁅R⁆ L₂

Equations

• LieAlgebra.SemiDirectSum.lift ψ f g h = { toLinearMap := (↑f).coprod ↑g ∘ₗ ↑(LieAlgebra.SemiDirectSum.toProdl ψ), map_lie' := ⋯ }

@[simp]

theorem LieAlgebra.SemiDirectSum.lift_apply {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] {L₂ : Type u_4} [LieRing L₂] [LieAlgebra R L₂] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (f : K →ₗ⁅R⁆ L₂) (g : L →ₗ⁅R⁆ L₂) (h : ∀ (x : L), ↑f ∘ₗ ↑(ψ x) = (ad R L₂) (g x) ∘ₗ ↑f) (x : K ⋊⁅ψ⁆ L) : (lift ψ f g h) x = f x.left + g x.right

def LieAlgebra.IsInnerSemiDirectSum {R : Type u_1} [CommRing R] {L : Type u_3} [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (L' : LieSubalgebra R L) : Prop

Equations

• LieAlgebra.IsInnerSemiDirectSum I L' = IsCompl (↑I) L'.toSubmodule

theorem LieAlgebra.isInnerSemiDirectSum_iff {R : Type u_1} [CommRing R] {L : Type u_3} [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} {L' : LieSubalgebra R L} : IsInnerSemiDirectSum I L' ↔ IsCompl (↑I) L'.toSubmodule

theorem LieAlgebra.IsInnerSemiDirectSum.isCompl {R : Type u_1} [CommRing R] {L : Type u_3} [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} {L' : LieSubalgebra R L} : IsInnerSemiDirectSum I L' → IsCompl (↑I) L'.toSubmodule

Alias of the forward direction of LieAlgebra.isInnerSemiDirectSum_iff.

theorem IsCompl.isInnerSemidirectSum {R : Type u_1} [CommRing R] {L : Type u_3} [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} {L' : LieSubalgebra R L} : IsCompl (↑I) L'.toSubmodule → LieAlgebra.IsInnerSemiDirectSum I L'

Alias of the reverse direction of LieAlgebra.isInnerSemiDirectSum_iff.

noncomputable def LieAlgebra.SemiDirectSum.lieEquivLieSubalgebra {R : Type u_1} [CommRing R] {L : Type u_3} [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} {L' : LieSubalgebra R L} (h : IsInnerSemiDirectSum I L') : (↥I ⋊⁅(LieDerivation.adIdeal I).comp L'.incl⁆ ↥L') ≃ₗ⁅R⁆ L

Equations

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

@[simp]

theorem LieAlgebra.SemiDirectSum.lieEquivLieSubalgebra_apply {R : Type u_1} [CommRing R] {L : Type u_3} [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} {L' : LieSubalgebra R L} (h : IsInnerSemiDirectSum I L') (x : ↥I ⋊⁅(LieDerivation.adIdeal I).comp L'.incl⁆ ↥L') : (lieEquivLieSubalgebra h) x = ↑x.left + ↑x.right

theorem LieAlgebra.SemiDirectSum.isInnerSemiDirectSum_self {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : IsInnerSemiDirectSum (inl ψ).idealRange (inr ψ).range