LeanPool.LowDimSolvClassification.Semidirect #

source

def LieSemidirectProduct {K : Type u_1} (L : Type u_2) (J : Type u_3) [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] (φ : L →ₗ⁅K⁆ LieDerivation K J J) :

Type (max u_2 u_3)

The semidirect product of two Lie algebras L and J, defined by specifying a homomorphism from L to the Lie algebra of derivations of J. The homomorphism φ indexes the type, but does not appear in the underlying carrier; consuming it via id keeps the linter happy.

Equations

(L ⋉[φ] J) = (fun (x : L →ₗ⁅K⁆ LieDerivation K J J) => L × J) (id φ)

Instances For

source

def «term_⋉[_]_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

theorem LieSemidirectProduct.ext {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} {a b : L ⋉[φ] J} (h1 : a.1 = b.1) (h2 : a.2 = b.2) :

a = b

source

theorem LieSemidirectProduct.ext_iff {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} {a b : L ⋉[φ] J} :

a = b ↔ a.1 = b.1 ∧ a.2 = b.2

source

@[implicit_reducible]

instance LieSemidirectProduct.instAddCommGroup {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} :

AddCommGroup (L ⋉[φ] J)

Equations

LieSemidirectProduct.instAddCommGroup = inferInstance

source

@[implicit_reducible]

instance LieSemidirectProduct.instModule {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} :

Module K (L ⋉[φ] J)

Equations

LieSemidirectProduct.instModule = inferInstance

source

@[simp]

theorem LieSemidirectProduct.add_left {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (a b : L ⋉[φ] J) :

(a + b).1 = a.1 + b.1

source

@[simp]

theorem LieSemidirectProduct.add_right {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (a b : L ⋉[φ] J) :

(a + b).2 = a.2 + b.2

source

@[simp]

theorem LieSemidirectProduct.zero_left {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} :

0.1 = 0

source

@[simp]

theorem LieSemidirectProduct.zero_right {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} :

0.2 = 0

source

@[simp]

theorem LieSemidirectProduct.neg_left {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (a : L ⋉[φ] J) :

(-a).1 = -a.1

source

@[simp]

theorem LieSemidirectProduct.neg_right {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (a : L ⋉[φ] J) :

(-a).2 = -a.2

source

@[simp]

theorem LieSemidirectProduct.smul_left {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (k : K) (a : L ⋉[φ] J) :

(k • a).1 = k • a.1

source

@[simp]

theorem LieSemidirectProduct.smul_right {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (k : K) (a : L ⋉[φ] J) :

(k • a).2 = k • a.2

source

@[implicit_reducible]

instance LieSemidirectProduct.instBracket {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} :

Bracket (L ⋉[φ] J) (L ⋉[φ] J)

Equations

LieSemidirectProduct.instBracket = { bracket := fun (a b : L ⋉[φ] J) => (⁅a.1, b.1⁆, (φ a.1) b.2 - (φ b.1) a.2 + ⁅a.2, b.2⁆) }

source

theorem LieSemidirectProduct.bracket_def {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (a b : L ⋉[φ] J) :

⁅a, b⁆ = (⁅a.1, b.1⁆, (φ a.1) b.2 - (φ b.1) a.2 + ⁅a.2, b.2⁆)

source

@[implicit_reducible]

instance LieSemidirectProduct.instLieRing {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} :

LieRing (L ⋉[φ] J)

Equations

LieSemidirectProduct.instLieRing = { toAddCommGroup := inferInstance, toBracket := LieSemidirectProduct.instBracket, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

source

@[implicit_reducible]

instance LieSemidirectProduct.instLieAlgebra {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} :

LieAlgebra K (L ⋉[φ] J)

Equations

LieSemidirectProduct.instLieAlgebra = { toModule := LieSemidirectProduct.instModule, lie_smul := ⋯ }

source

def LieSemidirectProduct.inl {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} :

L →ₗ⁅K⁆ L ⋉[φ] J

TODO.

Equations

LieSemidirectProduct.inl = { toFun := fun (x : L) => (x, 0), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

Instances For

source

def LieSemidirectProduct.inr {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} :

J →ₗ⁅K⁆ L ⋉[φ] J

TODO.

Equations

LieSemidirectProduct.inr = { toFun := fun (x : J) => (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

Instances For

source

def LieSemidirectProduct.fst {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} :

L ⋉[φ] J →ₗ⁅K⁆ L

TODO.

Equations

LieSemidirectProduct.fst = { toFun := fun (x : L ⋉[φ] J) => x.1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

Instances For

source

@[simp]

theorem LieSemidirectProduct.fst_inl {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (x : L) :

fst (inl x) = x

source

@[simp]

theorem LieSemidirectProduct.fst_inr {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (x : J) :

fst (inr x) = 0

source

@[simp]

theorem LieSemidirectProduct.fst_inl' {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (x : L) :

(inl x).1 = x

source

@[simp]

theorem LieSemidirectProduct.fst_inr' {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (x : J) :

(inr x).1 = 0

source

@[simp]

theorem LieSemidirectProduct.snd_inl' {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (x : L) :

(inl x).2 = 0

source

@[simp]

theorem LieSemidirectProduct.snd_inr' {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (x : J) :

(inr x).2 = x

source

@[simp]

theorem LieSemidirectProduct.inl_left_add_inr_right {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] {φ : L →ₗ⁅K⁆ LieDerivation K J J} (x : L ⋉[φ] J) :

inl x.1 + inr x.2 = x

source

def LieSemidirectProduct.leftSubalgebra {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] (φ : L →ₗ⁅K⁆ LieDerivation K J J) :

LieSubalgebra K (L ⋉[φ] J)

TODO.

Equations

LieSemidirectProduct.leftSubalgebra φ = LieSemidirectProduct.inl.range

Instances For

source

def LieSemidirectProduct.rightIdeal {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] (φ : L →ₗ⁅K⁆ LieDerivation K J J) :

LieIdeal K (L ⋉[φ] J)

TODO.

Equations

LieSemidirectProduct.rightIdeal φ = LieSemidirectProduct.fst.ker

Instances For

source

def LieSemidirectProduct.rightIdealEquivRight {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] (φ : L →ₗ⁅K⁆ LieDerivation K J J) :

↥(rightIdeal φ) ≃ₗ⁅K⁆ J

TODO.

Equations

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

Instances For

source

theorem LieSemidirectProduct.range_inr_eq_ker_fst {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] (φ : L →ₗ⁅K⁆ LieDerivation K J J) :

inr.range = LieIdeal.toLieSubalgebra K (L ⋉[φ] J) (rightIdeal φ)

source

theorem LieSemidirectProduct.finrank_eq {K : Type u_4} {L : Type u_5} {J : Type u_6} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] (φ : L →ₗ⁅K⁆ LieDerivation K J J) [StrongRankCondition K] [Module.Free K L] [Module.Free K J] [Module.Finite K L] [Module.Finite K J] :

Module.finrank K (L ⋉[φ] J) = Module.finrank K L + Module.finrank K J

source

theorem LieSemidirectProduct.isAlmostAbelian {K : Type u_4} {L : Type u_5} [CommRing K] [LieRing L] [LieAlgebra K L] {φ : K →ₗ⁅K⁆ LieDerivation K L L} [IsLieAbelian L] [StrongRankCondition K] [Module.Free K L] [Module.Finite K L] :

LieAlgebra.IsAlmostAbelian K (K ⋉[φ] L)

Any semidirect product of the base field with an abelian Lie algebra is almost abelian.

source

@[implicit_reducible]

instance instBracketProdLeanPool {L : Type u_2} {J : Type u_3} [LieRing L] [LieRing J] :

Bracket (L × J) (L × J)

Equations

instBracketProdLeanPool = { bracket := fun (a b : L × J) => (⁅a.1, b.1⁆, ⁅a.2, b.2⁆) }

source

theorem Prod.bracket_def {L : Type u_2} {J : Type u_3} [LieRing L] [LieRing J] (a b : L × J) :

⁅a, b⁆ = (⁅a.1, b.1⁆, ⁅a.2, b.2⁆)

source

@[implicit_reducible]

instance instLieRingProdLeanPool {L : Type u_2} {J : Type u_3} [LieRing L] [LieRing J] :

LieRing (L × J)

Equations

instLieRingProdLeanPool = { toAddCommGroup := inferInstance, toBracket := instBracketProdLeanPool, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

source

@[implicit_reducible]

instance instLieAlgebraProdLeanPool {K : Type u_1} {L : Type u_2} {J : Type u_3} [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] :

LieAlgebra K (L × J)

Equations

instLieAlgebraProdLeanPool = { toModule := Prod.instModule, lie_smul := ⋯ }

source

def LieHom.inl (K : Type u_4) (L : Type u_5) (J : Type u_6) [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] :

L →ₗ⁅K⁆ L × J

TODO.

Equations

LieHom.inl K L J = { toFun := fun (x : L) => (x, 0), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

Instances For

source

def LieHom.inr (K : Type u_4) (L : Type u_5) (J : Type u_6) [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] :

J →ₗ⁅K⁆ L × J

TODO.

Equations

LieHom.inr K L J = { toFun := fun (x : J) => (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

Instances For

source

def LieHom.fst (K : Type u_4) (L : Type u_5) (J : Type u_6) [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] :

L × J →ₗ⁅K⁆ L

TODO.

Equations

LieHom.fst K L J = { toFun := fun (x : L × J) => x.1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

Instances For

source

def LieHom.snd (K : Type u_4) (L : Type u_5) (J : Type u_6) [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] :

L × J →ₗ⁅K⁆ J

TODO.

Equations

LieHom.snd K L J = { toFun := fun (x : L × J) => x.2, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

Instances For

source

def leftIdeal (K : Type u_4) (L : Type u_5) (J : Type u_6) [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] :

LieIdeal K (L × J)

TODO.

Equations

leftIdeal K L J = (LieHom.snd K L J).ker

Instances For

source

def leftIdealEquivLeft (K : Type u_4) (L : Type u_5) (J : Type u_6) [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] :

↥(leftIdeal K L J) ≃ₗ⁅K⁆ L

TODO.

Equations

leftIdealEquivLeft K L J = { toFun := fun (x : ↥(leftIdeal K L J)) => (↑x).1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯, invFun := fun (x : L) => ⟨(x, 0), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

def rightIdeal (K : Type u_4) (L : Type u_5) (J : Type u_6) [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] :

LieIdeal K (L × J)

TODO.

Equations

rightIdeal K L J = (LieHom.fst K L J).ker

Instances For

source

def rightIdealEquivRight (K : Type u_4) (L : Type u_5) (J : Type u_6) [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] :

↥(rightIdeal K L J) ≃ₗ⁅K⁆ J

TODO.

Equations

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

Instances For

source

def Prod.toLieSemidirectProduct (K : Type u_4) (L : Type u_5) (J : Type u_6) [CommRing K] [LieRing L] [LieRing J] [LieAlgebra K L] [LieAlgebra K J] :

(L × J) ≃ₗ⁅K⁆ L ⋉[0] J

TODO.

Equations

Prod.toLieSemidirectProduct K L J = { toLinearMap := ↑(LinearEquiv.refl K (L × J)), map_lie' := ⋯, invFun := (LinearEquiv.refl K (L × J)).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For