LeanPool.LowDimSolvClassification.Classification3

theorem LieAlgebra.Dim3.aux_dim_comm {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (dim3 : Module.finrank K L = 3) : Module.finrank K ↥(commutator K L) = 0 ∨ Module.finrank K ↥(commutator K L) = 1 ∨ Module.finrank K ↥(commutator K L) = 2 ∨ Module.finrank K ↥(commutator K L) = 3

theorem LieAlgebra.Dim3.heisenberg_iff {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] : Nonempty (L ≃ₗ⁅K⁆ Heisenberg K) ↔ Module.finrank K L = 3 ∧ Module.finrank K ↥(commutator K L) = 1 ∧ IsTwoStepNilpotent K L

Characterization of the three-dimensional Heisenberg Lie algebra.

theorem LieAlgebra.Dim3.affinePlusAbelian_iff {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] : Nonempty (L ≃ₗ⁅K⁆ AffinePlusAbelian K) ↔ Module.finrank K L = 3 ∧ Module.finrank K ↥(commutator K L) = 1 ∧ ¬IsTwoStepNilpotent K L

Characterization of the three-dimensional Lie algebra AffinePlusAbelian.

theorem LieAlgebra.Dim3.hyperbolic_iff {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] : Nonempty (L ≃ₗ⁅K⁆ Hyperbolic K) ↔ ∃ (B : Module.Basis (Fin 3) K L), ⁅B 0, B 1⁆ = B 1 ∧ ⁅B 0, B 2⁆ = B 2 ∧ ⁅B 1, B 2⁆ = 0

Choice of basis for the three-dimensional Lie algebra Hyperbolic.

theorem LieAlgebra.Dim3.family_iff {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (α β : K) : Nonempty (L ≃ₗ⁅K⁆ Family K α β) ↔ ∃ (B : Module.Basis (Fin 3) K L), ⁅B 0, B 1⁆ = B 2 ∧ ⁅B 1, B 2⁆ = 0 ∧ ⁅B 0, B 2⁆ = α • B 1 + β • B 2

Choice of basis for the three-dimensional Lie algebra Family.

theorem LieAlgebra.Dim3.classification {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (dim3 : Module.finrank K L = 3) (hs : IsSolvable L) : Nonempty (L ≃ₗ⁅K⁆ Abelian K) ∨ Nonempty (L ≃ₗ⁅K⁆ Heisenberg K) ∨ Nonempty (L ≃ₗ⁅K⁆ AffinePlusAbelian K) ∨ Nonempty (L ≃ₗ⁅K⁆ Hyperbolic K) ∨ (∃ (α : K), α ≠ 0 ∧ Nonempty (L ≃ₗ⁅K⁆ Family K α 0)) ∨ ∃ (α : K), α ≠ 0 ∧ Nonempty (L ≃ₗ⁅K⁆ Family K α 1)

theorem LieAlgebra.Dim3.Family.iso_iff {K : Type u_1} [Field K] {α α' β β' : K} (hα : α ≠ 0) (hα' : α' ≠ 0) : Nonempty (Family K α β ≃ₗ⁅K⁆ Family K α' β') ↔ ∃ (γ : Kˣ), α = ↑γ ^ 2 * α' ∧ β = ↑γ * β'

theorem LieAlgebra.Dim3.Family.not_iso_hyperbolic {K : Type u_1} [Field K] {α β : K} (hα : α ≠ 0) : IsEmpty (Family K α β ≃ₗ⁅K⁆ Hyperbolic K)

theorem LieAlgebra.Dim3.Family.iso_1 {K : Type u_1} [Field K] {α α' : K} (hα : α ≠ 0) (hα' : α' ≠ 0) : ∀ (a : Family K α 1 ≃ₗ⁅K⁆ Family K α' 1), α = α'

theorem LieAlgebra.Dim3.Family.not_iso_0_1 {K : Type u_1} [Field K] {α α' : K} (hα : α ≠ 0) (hα' : α' ≠ 0) : IsEmpty (Family K α 0 ≃ₗ⁅K⁆ Family K α' 1)

theorem LieAlgebra.Dim3.Family.iso_0 {K : Type u_1} [Field K] {α α' : K} (hα : α ≠ 0) (hα' : α' ≠ 0) : ∀ (a : Family K α 0 ≃ₗ⁅K⁆ Family K α' 0), ∃ (γ : K), α = γ ^ 2 * α'