LeanPool.LowDimSolvClassification.InstancesLowDim

@[reducible, inline]

abbrev LieAlgebra.Dim2.Abelian (K : Type u_1) [CommRing K] : Type u_1

TODO.

Equations

• LieAlgebra.Dim2.Abelian K = LieAlgebra.mkAbelian K (Fin 2 → K)

def LieAlgebra.Dim2.Affine (K : Type u_1) : Type u_1

TODO.

Equations

• LieAlgebra.Dim2.Affine K = (Fin 2 → K)

@[implicit_reducible]

instance LieAlgebra.Dim2.instLieRingAffine (K : Type u_1) [CommRing K] : LieRing (Affine K)

Equations

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

theorem LieAlgebra.Dim2.Affine.bracket (K : Type u_1) [CommRing K] {l r : Affine K} : ⁅l, r⁆ = ![0, l 0 * r 1 - r 0 * l 1]

@[implicit_reducible]

instance LieAlgebra.Dim2.instAffine (K : Type u_1) [CommRing K] : LieAlgebra K (Affine K)

Equations

• LieAlgebra.Dim2.instAffine K = { toModule := inferInstance, lie_smul := ⋯ }

def LieAlgebra.Dim2.Affine.equivToLieAlgOfAffineEquiv {K : Type u_1} [Field K] : 𝔞𝔣𝔣 K K ≃ₗ⁅K⁆ Affine K

In this section we prove that Dim2.Affine is isomorphic to the semidirect product gl(K) ⋉ K, where K is the 1-dimensional vector space over K

Equations

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

def LieAlgebra.Dim2.Affine.equivToRealHyperbolic {K : Type u_1} [Field K] : Affine K ≃ₗ⁅K⁆ 𝔥𝔶𝔭 2 K

TODO.

Equations

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

@[reducible, inline]

abbrev LieAlgebra.Dim3.Abelian (K : Type u_1) [CommRing K] : Type u_1

The three-dimensional abelian Lie algebra.

Equations

• LieAlgebra.Dim3.Abelian K = LieAlgebra.mkAbelian K (Fin 3 → K)

def LieAlgebra.Dim3.Heisenberg (K : Type u_1) : Type u_1

The three-dimensional Heisenberg Lie algebra.

Equations

• LieAlgebra.Dim3.Heisenberg K = (Fin 3 → K)

@[implicit_reducible]

instance LieAlgebra.Dim3.instLieRingHeisenberg (K : Type u_1) [CommRing K] : LieRing (Heisenberg K)

Equations

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

theorem LieAlgebra.Dim3.Heisenberg.bracket (K : Type u_1) [CommRing K] {l r : Heisenberg K} : ⁅l, r⁆ = ![l 1 * r 2 - r 1 * l 2, 0, 0]

@[implicit_reducible]

instance LieAlgebra.Dim3.instHeisenberg (K : Type u_1) [CommRing K] : LieAlgebra K (Heisenberg K)

Equations

• LieAlgebra.Dim3.instHeisenberg K = { toModule := inferInstance, lie_smul := ⋯ }

def LieAlgebra.Dim3.AffinePlusAbelian (K : Type u_1) : Type u_1

The three-dimensional Lie algebra which has one-dimensional commutator and is not nilpotent.

Equations

• LieAlgebra.Dim3.AffinePlusAbelian K = (Fin 3 → K)

@[implicit_reducible]

instance LieAlgebra.Dim3.instLieRingAffinePlusAbelian (K : Type u_1) [CommRing K] : LieRing (AffinePlusAbelian K)

Equations

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

theorem LieAlgebra.Dim3.AffinePlusAbelian.bracket (K : Type u_1) [CommRing K] {l r : AffinePlusAbelian K} : ⁅l, r⁆ = ![0, l 1 * r 2 - r 1 * l 2, 0]

@[implicit_reducible]

instance LieAlgebra.Dim3.instAffinePlusAbelian (K : Type u_1) [CommRing K] : LieAlgebra K (AffinePlusAbelian K)

Equations

• LieAlgebra.Dim3.instAffinePlusAbelian K = { toModule := inferInstance, lie_smul := ⋯ }

def LieAlgebra.Dim3.Hyperbolic (K : Type u_1) : Type u_1

The three-dimensional solvable Lie algebra associated to real hyperbolic space.

Equations

• LieAlgebra.Dim3.Hyperbolic K = (Fin 3 → K)

@[implicit_reducible]

instance LieAlgebra.Dim3.instLieRingHyperbolic (K : Type u_1) [CommRing K] : LieRing (Hyperbolic K)

Equations

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

@[implicit_reducible]

instance LieAlgebra.Dim3.instHyperbolic (K : Type u_1) [CommRing K] : LieAlgebra K (Hyperbolic K)

Equations

• LieAlgebra.Dim3.instHyperbolic K = { toModule := inferInstance, lie_smul := ⋯ }

theorem LieAlgebra.Dim3.Hyperbolic.bracket (K : Type u_1) [CommRing K] (l r : Hyperbolic K) : ⁅l, r⁆ = ![0, l 0 * r 1 - r 0 * l 1, l 0 * r 2 - r 0 * l 2]

def LieAlgebra.Dim3.Family (K : Type u_1) (α β : K) : Type u_1

The two-parameter family of solvable Lie algebras appearing in the classification of 3-dimensional Lie algebras. The two K parameters are phantom: they index the bracket structure but do not appear in the underlying type; consuming them via id keeps the linter happy.

Equations

• LieAlgebra.Dim3.Family K α β = (fun (x : K × K) => Fin 3 → K) (id (α, β))

@[implicit_reducible]

instance LieAlgebra.Dim3.instLieRingFamily (K : Type u_1) [CommRing K] (α β : K) : LieRing (Family K α β)

Equations

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

@[implicit_reducible]

instance LieAlgebra.Dim3.instFamily (K : Type u_1) [CommRing K] (α β : K) : LieAlgebra K (Family K α β)

Equations

• LieAlgebra.Dim3.instFamily K α β = { toModule := inferInstance, lie_smul := ⋯ }

theorem LieAlgebra.Dim3.Family.bracket (K : Type u_1) [CommRing K] (α β : K) (l r : Family K α β) : ⁅l, r⁆ = ![0, (l 0 * r 2 - l 2 * r 0) * α, (l 0 * r 2 - l 2 * r 0) * β + l 0 * r 1 - l 1 * r 0]

def LieAlgebra.Dim3.Heisenberg.semidirectAux' {K : Type u_1} [CommRing K] : Module.End K (Dim2.Abelian K)

TODO.

Equations

• LieAlgebra.Dim3.Heisenberg.semidirectAux' = { toFun := fun (v : LieAlgebra.Dim2.Abelian K) => ![v 1, 0], map_add' := ⋯, map_smul' := ⋯ }

def LieAlgebra.Dim3.Heisenberg.semidirectAux {K : Type u_1} [CommRing K] : K →ₗ⁅K⁆ LieDerivation K (Dim2.Abelian K) (Dim2.Abelian K)

TODO.

Equations

• LieAlgebra.Dim3.Heisenberg.semidirectAux = (LieAlgebra.Abelian.DerivationOfLinearMap K (LieAlgebra.Dim2.Abelian K)).comp (LieHom.smulRight LieAlgebra.Dim3.Heisenberg.semidirectAux')

def LieAlgebra.Dim3.Heisenberg.equivToSemidirect {K : Type u_1} [CommRing K] : Heisenberg K ≃ₗ⁅K⁆ K ⋉[semidirectAux] Dim2.Abelian K

The three-dimensional Heisenberg Lie algebra over K is isomorphic to a semidirect product of K with the two-dimensional abelian Lie algebra.

Equations

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

def LieAlgebra.Dim3.AffinePlusAbelian.equivToDirectSum {K : Type u_1} [CommRing K] : AffinePlusAbelian K ≃ₗ⁅K⁆ K × Dim2.Affine K

The three-dimensional Lie algebra AffinePlusAbelian K is indeed isomorphic to the direct sum/product of K with LieAlgebra.Dim2.Affine K.

Equations

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

def LieAlgebra.Dim3.AffinePlusAbelian.semidirectAux' {K : Type u_1} [CommRing K] : Module.End K (Dim2.Abelian K)

TODO.

Equations

• LieAlgebra.Dim3.AffinePlusAbelian.semidirectAux' = { toFun := fun (v : LieAlgebra.Dim2.Abelian K) => ![0, -v 1], map_add' := ⋯, map_smul' := ⋯ }

def LieAlgebra.Dim3.AffinePlusAbelian.semidirectAux {K : Type u_1} [CommRing K] : K →ₗ⁅K⁆ LieDerivation K (Dim2.Abelian K) (Dim2.Abelian K)

TODO.

Equations

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

def LieAlgebra.Dim3.AffinePlusAbelian.equivToSemidirect {K : Type u_1} [CommRing K] : AffinePlusAbelian K ≃ₗ⁅K⁆ K ⋉[semidirectAux] Dim2.Abelian K

The three-dimensional Lie algebra AffinePlusAbelian K is isomorphic to a semidirect product of K with the two-dimensional abelian Lie algebra.

Equations

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

def LieAlgebra.Dim3.Hyperbolic.equivToRealHyperbolic {K : Type u_1} [CommRing K] : Hyperbolic K ≃ₗ⁅K⁆ 𝔥𝔶𝔭 3 K

TODO.

Equations

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

def LieAlgebra.Dim3.Hyperbolic.e₁ {K : Type u_1} [CommRing K] : Hyperbolic K

TODO.

Equations

• LieAlgebra.Dim3.Hyperbolic.e₁ = ![1, 0, 0]

theorem LieAlgebra.Dim3.Hyperbolic.e₁_def {K : Type u_1} [CommRing K] : e₁ = ![1, 0, 0]

def LieAlgebra.Dim3.Hyperbolic.e₂ {K : Type u_1} [CommRing K] : Hyperbolic K

TODO.

Equations

• LieAlgebra.Dim3.Hyperbolic.e₂ = ![0, 1, 0]

theorem LieAlgebra.Dim3.Hyperbolic.e₂_def {K : Type u_1} [CommRing K] : e₂ = ![0, 1, 0]

def LieAlgebra.Dim3.Hyperbolic.e₃ {K : Type u_1} [CommRing K] : Hyperbolic K

TODO.

Equations

• LieAlgebra.Dim3.Hyperbolic.e₃ = ![0, 0, 1]

theorem LieAlgebra.Dim3.Hyperbolic.e₃_def {K : Type u_1} [CommRing K] : e₃ = ![0, 0, 1]

theorem LieAlgebra.Dim3.Hyperbolic.commutator_is_span_e₂e₃ {K : Type u_1} [CommRing K] : ↑(commutator K (Hyperbolic K)) = Submodule.span K {e₂, e₃}

theorem LieAlgebra.Dim3.Hyperbolic.commutator_repr {K : Type u_1} [CommRing K] {x : Hyperbolic K} : x ∈ commutator K (Hyperbolic K) ↔ ∃ (a : K) (b : K), a • e₂ + b • e₃ = x

noncomputable def LieAlgebra.Dim3.Hyperbolic.stdBasis {K : Type u_1} [CommRing K] : Module.Basis (Fin 3) K (Hyperbolic K)

TODO.

Equations

• LieAlgebra.Dim3.Hyperbolic.stdBasis = Module.Basis.ofEquivFun (LinearEquiv.refl K (Fin 3 → K))

theorem LieAlgebra.Dim3.Hyperbolic.stdBasis₁ {K : Type u_1} [CommRing K] : stdBasis 0 = e₁

theorem LieAlgebra.Dim3.Hyperbolic.stdBasis₂ {K : Type u_1} [CommRing K] : stdBasis 1 = e₂

theorem LieAlgebra.Dim3.Hyperbolic.stdBasis₃ {K : Type u_1} [CommRing K] : stdBasis 2 = e₃

noncomputable def LieAlgebra.Dim3.Hyperbolic.commutatorBasis {K : Type u_1} [CommRing K] : Module.Basis (Fin 2) K ↥(commutator K (Hyperbolic K))

TODO.

Equations

• LieAlgebra.Dim3.Hyperbolic.commutatorBasis = ⋯.mp (⋯.mp (Module.Basis.span ⋯))

theorem LieAlgebra.Dim3.Hyperbolic.dim_commutator {K : Type u_2} [Field K] : Module.finrank K ↥(commutator K (Hyperbolic K)) = 2

def LieAlgebra.Dim3.Hyperbolic.adjoint {K : Type u_1} [CommRing K] (x : Hyperbolic K) : Module.End K (Hyperbolic K)

TODO.

Equations

• x.adjoint = (LieAlgebra.ad K (LieAlgebra.Dim3.Hyperbolic K)) x

def LieAlgebra.Dim3.Hyperbolic.ade₁ {K : Type u_1} [CommRing K] : Module.End K (Hyperbolic K)

TODO.

Equations

• LieAlgebra.Dim3.Hyperbolic.ade₁ = LieAlgebra.Dim3.Hyperbolic.e₁.adjoint

theorem LieAlgebra.Dim3.Hyperbolic.ad_preserves_commutator {K : Type u_1} [CommRing K] (x y : Hyperbolic K) : y ∈ commutator K (Hyperbolic K) → x.adjoint y ∈ commutator K (Hyperbolic K)

def LieAlgebra.Dim3.Hyperbolic.adRestr {K : Type u_1} [CommRing K] (x : Hyperbolic K) : ↥(commutator K (Hyperbolic K)) →ₗ[K] ↥(commutator K (Hyperbolic K))

TODO.

Equations

• x.adRestr = LinearMap.restrict x.adjoint ⋯

theorem LieAlgebra.Dim3.Hyperbolic.ad_restr_apply {K : Type u_1} [CommRing K] (x y : Hyperbolic K) (hy : y ∈ commutator K (Hyperbolic K)) : x.adRestr ⟨y, hy⟩ = ⟨x.adjoint y, ⋯⟩

theorem LieAlgebra.Dim3.Hyperbolic.ad_restr_add {K : Type u_1} [CommRing K] (x y : Hyperbolic K) : (x + y).adRestr = x.adRestr + y.adRestr

theorem LieAlgebra.Dim3.Hyperbolic.ad_restr_smul {K : Type u_1} [CommRing K] (a : K) (x : Hyperbolic K) : (a • x).adRestr = a • x.adRestr

theorem LieAlgebra.Dim3.Hyperbolic.lie_e₁e₂ {K : Type u_1} [CommRing K] : ⁅e₁, e₂⁆ = e₂

theorem LieAlgebra.Dim3.Hyperbolic.lie_e₁e₃ {K : Type u_1} [CommRing K] : ⁅e₁, e₃⁆ = e₃

theorem LieAlgebra.Dim3.Hyperbolic.lie_e₂e₃ {K : Type u_1} [CommRing K] : ⁅e₂, e₃⁆ = 0

theorem LieAlgebra.Dim3.Hyperbolic.ade₁_restr_id {K : Type u_1} [CommRing K] : e₁.adRestr = LinearMap.id

theorem LieAlgebra.Dim3.Hyperbolic.ad_comm_restr {K : Type u_1} [CommRing K] {x : Hyperbolic K} (hx : x ∈ commutator K (Hyperbolic K)) : x.adRestr = 0

def LieAlgebra.Dim3.Family.semidirectAux' {K : Type u_1} [CommRing K] (α β : K) : Module.End K (Dim2.Abelian K)

TODO.

Equations

• LieAlgebra.Dim3.Family.semidirectAux' α β = { toFun := fun (v : LieAlgebra.Dim2.Abelian K) => ![α • v 1, v 0 + β • v 1], map_add' := ⋯, map_smul' := ⋯ }

def LieAlgebra.Dim3.Family.semidirectAux {K : Type u_1} [CommRing K] (α β : K) : K →ₗ⁅K⁆ LieDerivation K (Dim2.Abelian K) (Dim2.Abelian K)

TODO.

Equations

• LieAlgebra.Dim3.Family.semidirectAux α β = (LieAlgebra.Abelian.DerivationOfLinearMap K (LieAlgebra.Dim2.Abelian K)).comp (LieHom.smulRight (LieAlgebra.Dim3.Family.semidirectAux' α β))

def LieAlgebra.Dim3.Family.equivToSemidirect {K : Type u_1} [CommRing K] (α β : K) : Family K α β ≃ₗ⁅K⁆ K ⋉[semidirectAux α β] Dim2.Abelian K

TODO.

Equations

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

def LieAlgebra.Dim3.Family.M {K : Type u_1} [CommRing K] (α β : K) : Matrix (Fin 2) (Fin 2) K

TODO.

Equations

• LieAlgebra.Dim3.Family.M α β = ![![0, α], ![1, β]]

theorem LieAlgebra.Dim3.Family.M_det {K : Type u_1} [CommRing K] {α β : K} : (M α β).det = -α

theorem LieAlgebra.Dim3.Family.M_trace {K : Type u_1} [CommRing K] {α β : K} : (M α β).trace = β

def LieAlgebra.Dim3.Family.e₁ {K : Type u_1} [CommRing K] {α β : K} : Family K α β

TODO.

Equations

• LieAlgebra.Dim3.Family.e₁ = ![1, 0, 0]

theorem LieAlgebra.Dim3.Family.e₁_def {K : Type u_1} [CommRing K] {α β : K} : e₁ = ![1, 0, 0]

def LieAlgebra.Dim3.Family.e₂ {K : Type u_1} [CommRing K] {α β : K} : Family K α β

TODO.

Equations

• LieAlgebra.Dim3.Family.e₂ = ![0, 1, 0]

theorem LieAlgebra.Dim3.Family.e₂_def {K : Type u_1} [CommRing K] {α β : K} : e₂ = ![0, 1, 0]

def LieAlgebra.Dim3.Family.e₃ {K : Type u_1} [CommRing K] {α β : K} : Family K α β

TODO.

Equations

• LieAlgebra.Dim3.Family.e₃ = ![0, 0, 1]

theorem LieAlgebra.Dim3.Family.e₃_def {K : Type u_1} [CommRing K] {α β : K} : e₃ = ![0, 0, 1]

theorem LieAlgebra.Dim3.Family.commutator_is_span_e₂e₃ {K : Type u_2} [Field K] {α β : K} (hα : α ≠ 0) : ↑(commutator K (Family K α β)) = Submodule.span K {e₂, e₃}

def LieAlgebra.Dim3.Family.B {K : Type u_2} [Field K] (α β : K) : Fin 2 → Family K α β

TODO.

Equations

• LieAlgebra.Dim3.Family.B α β = ![LieAlgebra.Dim3.Family.e₂, LieAlgebra.Dim3.Family.e₃]

theorem LieAlgebra.Dim3.Family.B_is_li_ambient {K : Type u_2} [Field K] {α β : K} : LinearIndependent K (B α β)

def LieAlgebra.Dim3.Family.e₁α {K : Type u_2} [Field K] {α β : K} : Family K α β

TODO.

Equations

• LieAlgebra.Dim3.Family.e₁α = ![α⁻¹, 0, 0]

def LieAlgebra.Dim3.Family.e₂β {K : Type u_2} [Field K] {α β : K} : Family K α β

TODO.

Equations

• LieAlgebra.Dim3.Family.e₂β = ![0, -β, 1]

theorem LieAlgebra.Dim3.Family.e₂_bracket {K : Type u_2} [Field K] {α β : K} {hα : α ≠ 0} : ⁅e₁α, e₂β⁆ = e₂

theorem LieAlgebra.Dim3.Family.e₃_bracket {K : Type u_2} [Field K] {α β : K} : ⁅e₁, e₂⁆ = e₃

theorem LieAlgebra.Dim3.Family.e₂_in_comm {K : Type u_2} [Field K] {α β : K} {hα : α ≠ 0} : e₂ ∈ commutator K (Family K α β)

theorem LieAlgebra.Dim3.Family.e₃_in_comm {K : Type u_2} [Field K] {α β : K} : e₃ ∈ commutator K (Family K α β)

noncomputable def LieAlgebra.Dim3.Family.commutatorBasis {K : Type u_2} [Field K] (α β : K) (hα : α ≠ 0) : Module.Basis (Fin 2) K ↥(commutator K (Family K α β))

TODO.

Equations

• LieAlgebra.Dim3.Family.commutatorBasis α β hα = Module.Basis.mk ⋯ ⋯

theorem LieAlgebra.Dim3.Family.dim_commutator {K : Type u_2} [Field K] {α β : K} {hα : α ≠ 0} : Module.finrank K ↥(commutator K (Family K α β)) = 2

theorem LieAlgebra.Dim3.Family.B_basis_0 {K : Type u_2} [Field K] {α β : K} {hα : α ≠ 0} : ↑((commutatorBasis α β hα) 0) = e₂

theorem LieAlgebra.Dim3.Family.B_basis_1 {K : Type u_2} [Field K] {α β : K} {hα : α ≠ 0} : ↑((commutatorBasis α β hα) 1) = e₃

theorem LieAlgebra.Dim3.Family.B_basis_repr {K : Type u_2} [Field K] {α β : K} {hα : α ≠ 0} {x : ↥(commutator K (Family K α β))} : ⇑((commutatorBasis α β hα).repr x) = ![↑x 1, ↑x 2]

def LieAlgebra.Dim3.Family.ade₁ {K : Type u_2} [Field K] {α β : K} : Module.End K (Family K α β)

TODO.

Equations

• LieAlgebra.Dim3.Family.ade₁ = (LieAlgebra.ad K (LieAlgebra.Dim3.Family K α β)) LieAlgebra.Dim3.Family.e₁

def LieAlgebra.Dim3.Family.adjoint {K : Type u_2} [Field K] {α β : K} (x : Family K α β) : Module.End K (Family K α β)

TODO.

Equations

• x.adjoint = (LieAlgebra.ad K (LieAlgebra.Dim3.Family K α β)) x

theorem LieAlgebra.Dim3.Family.ade₁_pc {K : Type u_2} [Field K] {α β : K} (x : Family K α β) : x ∈ commutator K (Family K α β) → ade₁ x ∈ commutator K (Family K α β)

theorem LieAlgebra.Dim3.Family.ad_pc {K : Type u_2} [Field K] {α β : K} (x y : Family K α β) : y ∈ commutator K (Family K α β) → x.adjoint y ∈ commutator K (Family K α β)

def LieAlgebra.Dim3.Family.adRestr {K : Type u_2} [Field K] {α β : K} (x : Family K α β) : ↥(commutator K (Family K α β)) →ₗ[K] ↥(commutator K (Family K α β))

TODO.

Equations

• x.adRestr = LinearMap.restrict x.adjoint ⋯

def LieAlgebra.Dim3.Family.ade₁Restr {K : Type u_2} [Field K] (α β : K) : ↥(commutator K (Family K α β)) →ₗ[K] ↥(commutator K (Family K α β))

TODO.

Equations

• LieAlgebra.Dim3.Family.ade₁Restr α β = LieAlgebra.Dim3.Family.e₁.adRestr

theorem LieAlgebra.Dim3.Family.ad_restr_apply {K : Type u_2} [Field K] {α β : K} (x y : Family K α β) (hy : y ∈ commutator K (Family K α β)) : x.adRestr ⟨y, hy⟩ = ⟨x.adjoint y, ⋯⟩

theorem LieAlgebra.Dim3.Family.M_is_ade₁_restr {K : Type u_2} [Field K] {α β : K} {hα : α ≠ 0} : (LinearMap.toMatrix (commutatorBasis α β hα) (commutatorBasis α β hα)) (ade₁Restr α β) = M α β

theorem LieAlgebra.Dim3.Family.tr_ade₁ {K : Type u_2} [Field K] {α β : K} (hα : α ≠ 0) : (LinearMap.trace K ↥(commutator K (Family K α β))) (ade₁Restr α β) = β

theorem LieAlgebra.Dim3.Family.det_ade₁ {K : Type u_2} [Field K] {α β : K} (hα : α ≠ 0) : LinearMap.det (ade₁Restr α β) = -α

theorem LieAlgebra.Dim3.Family.e₁_not_in_comm {K : Type u_2} [Field K] {α β : K} (hα : α ≠ 0) : e₁ ∉ commutator K (Family K α β)