LeanPool.LowDimSolvClassification.LemmasDim3

theorem LieAlgebra.Dim3.case1a {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (dim3 : Module.finrank K L = 3) (h₁ : Module.finrank K ↥(commutator K L) = 1) (h : IsTwoStepNilpotent K L) : ∃ (B : Module.Basis (Fin 3) K L), ⁅B 1, B 2⁆ = B 0 ∧ ⁅B 0, B 1⁆ = 0 ∧ ⁅B 0, B 2⁆ = 0

theorem LieAlgebra.Dim3.case1a' {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] : Module.finrank K L = 3 ∧ Module.finrank K ↥(commutator K L) = 1 ∧ IsTwoStepNilpotent K L ↔ ∃ (B : Module.Basis (Fin 3) K L), ⁅B 1, B 2⁆ = B 0 ∧ ⁅B 0, B 1⁆ = 0 ∧ ⁅B 0, B 2⁆ = 0

theorem LieAlgebra.Dim3.case1b {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (dim3 : Module.finrank K L = 3) (h₁ : Module.finrank K ↥(commutator K L) = 1) (h : ¬IsTwoStepNilpotent K L) : ∃ (B : Module.Basis (Fin 3) K L), ⁅B 0, B 1⁆ = 0 ∧ ⁅B 0, B 2⁆ = 0 ∧ ⁅B 1, B 2⁆ = B 1

theorem LieAlgebra.Dim3.case1b' {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] : Module.finrank K L = 3 ∧ Module.finrank K ↥(commutator K L) = 1 ∧ ¬IsTwoStepNilpotent K L ↔ ∃ (B : Module.Basis (Fin 3) K L), ⁅B 0, B 1⁆ = 0 ∧ ⁅B 0, B 2⁆ = 0 ∧ ⁅B 1, B 2⁆ = B 1

theorem LieAlgebra.Dim3.commutator_abelian_of_dim_two {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (dim3 : Module.finrank K L = 3) (h₂ : Module.finrank K ↥(commutator K L) = 2) : IsLieAbelian ↥(commutator K L)

theorem LieAlgebra.Dim3.case2_coarse {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (dim3 : Module.finrank K L = 3) (h₂ : Module.finrank K ↥(commutator K L) = 2) : (∃ (B : Module.Basis (Fin 3) K L), ⁅B 0, B 1⁆ = B 1 ∧ ⁅B 0, B 2⁆ = B 2 ∧ ⁅B 1, B 2⁆ = 0) ∨ ∃ (B : Module.Basis (Fin 3) K L), ⁅B 0, B 1⁆ = B 2 ∧ ⁅B 1, B 2⁆ = 0 ∧ ∃ (α : K) (β : K), α ≠ 0 ∧ ⁅B 0, B 2⁆ = α • B 1 + β • B 2

theorem LieAlgebra.Dim3.finrank_com_eq2_from_basis_bracket {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (hb : ∃ (B : Module.Basis (Fin 3) K L), ⁅B 0, B 1⁆ = B 2 ∧ ⁅B 1, B 2⁆ = 0 ∧ ∃ (α : K) (β : K), α ≠ 0 ∧ ⁅B 0, B 2⁆ = α • B 1 + β • B 2) : Module.finrank K ↥(commutator K L) = 2

theorem LieAlgebra.Dim3.case2 {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] : Module.finrank K L = 3 ∧ Module.finrank K ↥(commutator K L) = 2 ↔ (∃ (B : Module.Basis (Fin 3) K L), ⁅B 0, B 1⁆ = B 1 ∧ ⁅B 0, B 2⁆ = B 2 ∧ ⁅B 1, B 2⁆ = 0) ∨ (∃ (B : Module.Basis (Fin 3) K L), ⁅B 0, B 1⁆ = B 2 ∧ ⁅B 1, B 2⁆ = 0 ∧ ∃ (α : K), α ≠ 0 ∧ ⁅B 0, B 2⁆ = α • B 1) ∨ ∃ (B : Module.Basis (Fin 3) K L), ⁅B 0, B 1⁆ = B 2 ∧ ⁅B 1, B 2⁆ = 0 ∧ ∃ (α : K), α ≠ 0 ∧ ⁅B 0, B 2⁆ = α • B 1 + B 2