LeanPool.LowDimSolvClassification.InstancesConstructions

def LieAlgebra.mkAbelian (K : Type u_1) [CommRing K] (V : Type u_2) [AddCommGroup V] [Module K V] : Type u_2

The abelian Lie algebra constructed from a vector space by setting the bracket to zero. The unused Module K V instance is consumed by inferInstance so the unusedArguments linter accepts the definition; the result is still a synonym for V.

Equations

• LieAlgebra.mkAbelian K V = (fun (x : SMul K V) => V) inferInstance.toSMul

@[implicit_reducible]

instance LieAlgebra.instBracketMkAbelian (K : Type u_1) [CommRing K] (V : Type u_2) [AddCommGroup V] [Module K V] : Bracket (mkAbelian K V) (mkAbelian K V)

Equations

• LieAlgebra.instBracketMkAbelian K V = { bracket := fun (x x_1 : LieAlgebra.mkAbelian K V) => 0 }

@[implicit_reducible]

instance LieAlgebra.instLieRingMkAbelian (K : Type u_1) [CommRing K] (V : Type u_2) [AddCommGroup V] [Module K V] : LieRing (mkAbelian K V)

Equations

• LieAlgebra.instLieRingMkAbelian K V = { toAddCommGroup := inferInstance, toBracket := LieAlgebra.instBracketMkAbelian K V, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

@[implicit_reducible]

instance LieAlgebra.instMkAbelian (K : Type u_1) [CommRing K] (V : Type u_2) [AddCommGroup V] [Module K V] : LieAlgebra K (mkAbelian K V)

Equations

• LieAlgebra.instMkAbelian K V = { toModule := inferInstance, lie_smul := ⋯ }

instance LieAlgebra.instIsLieAbelianMkAbelian (K : Type u_1) [CommRing K] (V : Type u_2) [AddCommGroup V] [Module K V] : IsLieAbelian (mkAbelian K V)

def LieAlgebra.Abelian.DerivationOfLinearMap' {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] [IsLieAbelian L] (f : Module.End K L) : LieDerivation K L L

TODO.

Equations

• LieAlgebra.Abelian.DerivationOfLinearMap' f = { toLinearMap := f, leibniz' := ⋯ }

def LieAlgebra.Abelian.DerivationOfLinearMap (K : Type u_1) (L : Type u_2) [CommRing K] [LieRing L] [LieAlgebra K L] [IsLieAbelian L] : Module.End K L ≃ₗ⁅K⁆ LieDerivation K L L

If L is an abelian Lie algebra, any linear endomorphism of L is also a derivation of L.

Equations

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

@[simp]

theorem LieAlgebra.Abelian.DerivationCoeLinearMap {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] [IsLieAbelian L] (f : L →ₗ[K] L) : ↑((DerivationOfLinearMap K L) f) = f

@[simp]

theorem LieAlgebra.Abelian.DerivationCoeFun {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] [IsLieAbelian L] (f : L →ₗ[K] L) : ⇑((DerivationOfLinearMap K L) f) = ⇑f

@[simp]

theorem LieAlgebra.Abelian.DerivationCoeFun' {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] [IsLieAbelian L] (f : L →ₗ[K] L) : ⇑((DerivationOfLinearMap K L).toLieHom f) = ⇑f

def LieAlgebra.ofAffineEquivAux (K : Type u_1) [CommRing K] (V : Type u_2) [AddCommGroup V] [Module K V] : Module.End K (mkAbelian K V) →ₗ⁅K⁆ LieDerivation K (mkAbelian K V) (mkAbelian K V)

TODO.

Equations

• LieAlgebra.ofAffineEquivAux K V = (LieAlgebra.Abelian.DerivationOfLinearMap K (LieAlgebra.mkAbelian K V)).toLieHom

@[reducible, inline]

abbrev LieAlgebra.OfAffineEquiv (K : Type u_1) [CommRing K] (V : Type u_2) [AddCommGroup V] [Module K V] : Type u_2

The Lie algebra of the general affine group on a vector space V, constructed as semidirect product of V →ₗ[K] V with the abelian Lie algebra V.

Equations

• 𝔞𝔣𝔣 K V = (Module.End K (LieAlgebra.mkAbelian K V) ⋉[LieAlgebra.ofAffineEquivAux K V] LieAlgebra.mkAbelian K V)

def LieAlgebra.term𝔞𝔣𝔣 : Lean.ParserDescr

The Lie algebra of the general affine group on a vector space V, constructed as semidirect product of V →ₗ[K] V with the abelian Lie algebra V.

Equations

• LieAlgebra.term𝔞𝔣𝔣 = Lean.ParserDescr.node `LieAlgebra.term𝔞𝔣𝔣 1024 (Lean.ParserDescr.symbol "𝔞𝔣𝔣")

def LieAlgebra.RealHyperbolicAux' (K : Type u_1) [CommRing K] (L : Type u_3) [LieRing L] [LieAlgebra K L] [IsLieAbelian L] : K →ₗ⁅K⁆ LieDerivation K L L

TODO.

Equations

• LieAlgebra.RealHyperbolicAux' K L = (LieAlgebra.Abelian.DerivationOfLinearMap K L).comp (LieHom.smulRight LinearMap.id)

def LieAlgebra.RealHyperbolicAux (K : Type u_1) [CommRing K] (V : Type u_2) [AddCommGroup V] [Module K V] : K →ₗ⁅K⁆ LieDerivation K (mkAbelian K V) (mkAbelian K V)

TODO.

Equations

• LieAlgebra.RealHyperbolicAux K V = LieAlgebra.RealHyperbolicAux' K (LieAlgebra.mkAbelian K V)

@[reducible, inline]

abbrev LieAlgebra.RealHyperbolic (K : Type u_1) [CommRing K] (V : Type u_2) [AddCommGroup V] [Module K V] : Type (max u_1 u_2)

The almost abelian Lie algebra associated to real hyperbolic space, generalized to arbitrary K.

Equations

• LieAlgebra.RealHyperbolic K V = (K ⋉[LieAlgebra.RealHyperbolicAux K V] LieAlgebra.mkAbelian K V)

@[reducible, inline]

abbrev LieAlgebra.RealHyperbolic' (n : ℕ) (K : Type u_4) [CommRing K] : Type u_4

The almost abelian Lie algebra associated to real hyperbolic n-space, generalized to arbitrary K.

Equations

• 𝔥𝔶𝔭 n K = (K ⋉[LieAlgebra.RealHyperbolicAux K (Fin (n - 1) → K)] LieAlgebra.mkAbelian K (Fin (n - 1) → K))

def LieAlgebra.term𝔥𝔶𝔭 : Lean.ParserDescr

The almost abelian Lie algebra associated to real hyperbolic n-space, generalized to arbitrary K.

Equations

• LieAlgebra.term𝔥𝔶𝔭 = Lean.ParserDescr.node `LieAlgebra.term𝔥𝔶𝔭 1024 (Lean.ParserDescr.symbol "𝔥𝔶𝔭")