LeanPool.LowDimSolvClassification.GeneralResults

theorem Basis.repr_fin_one {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (B : Module.Basis (Fin 1) K L) (x : L) : x = (B.repr x) 0 • B 0

In a basis of size 1, we represent any element as an explicit sum.

theorem Basis.repr_fin_two {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (B : Module.Basis (Fin 2) K L) (x : L) : x = (B.repr x) 0 • B 0 + (B.repr x) 1 • B 1

In a basis of size 2, we represent any element as an explicit sum.

theorem Basis.repr_fin_three {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (B : Module.Basis (Fin 3) K L) (x : L) : x = (B.repr x) 0 • B 0 + (B.repr x) 1 • B 1 + (B.repr x) 2 • B 2

In a basis of size 3, we represent any element as an explicit sum.

theorem not_linearIndependent_pair_iff {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (x y : L) (hy : y ≠ 0) : ¬LinearIndependent K ![x, y] ↔ ∃ (c : K), x = c • y

theorem LinearIndependent.iff_in_submodule {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {S : Type u_3} (N : Submodule K L) {f : S → ↥N} : LinearIndependent K f ↔ LinearIndependent K (Subtype.val ∘ f)

A linearly independent set in a submodule is linearly independent in the ambient space.

def Submodule.mapIntoSubtype {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {S : Type u_3} (N : Submodule K L) (f : S → L) (hr : Set.range f ⊆ ↑N) : S → ↥N

A function into a submodule N defined by specifying a function into the ambient space with range in N.

Equations

• N.mapIntoSubtype f hr x = ⟨f x, ⋯⟩

def Set.mapIntoSubtype {α : Type u_3} {β : Type u_4} (s : Set β) (f : α → β) (hr : range f ⊆ s) : α → ↑s

A function with range in a given subset gives rise to a function to the corresponding subtype.

Equations

• s.mapIntoSubtype f hr = Subtype.coind f ⋯

theorem Set.map_into_subtype_apply {α : Type u_3} {β : Type u_4} (s : Set β) (f : α → β) (hr : range f ⊆ s) (a : α) : ↑(s.mapIntoSubtype f hr a) = f a

theorem Submodule.linearIndependent_from_ambient {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {S : Type u_3} (N : Submodule K L) (f : S → L) (hs : LinearIndependent K f) (hr : Set.range f ⊆ ↑N) : LinearIndependent K ((↑N).mapIntoSubtype f hr)

A linear independent set which is a subset of a submodule N gives a linear independent set in the module N.

noncomputable def LinearIndependent.extendFinSuccFun {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {n : ℕ} {l : Fin n → L} (hs : LinearIndependent K l) (ht : n + 1 ≤ Module.finrank K L) : Fin (n + 1) → L

extends linear independent set

Equations

• hs.extendFinSuccFun ht = Fin.cons (Classical.choose ⋯) l

theorem LinearIndependent.extendFinSucc {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {n : ℕ} {l : Fin n → L} (hs : LinearIndependent K l) (ht : n + 1 ≤ Module.finrank K L) : LinearIndependent K (hs.extendFinSuccFun ht) ∧ ∀ (i : Fin n), hs.extendFinSuccFun ht i.succ = l i

the previous extension gives a linearly independent set adding the new element as 0th element of the new set

theorem LinearIndependent.extend_fin {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {n k : ℕ} {l : Fin n → L} (hs : LinearIndependent K l) (ht : n + k ≤ Module.finrank K L) : ∃ (b : Fin (n + k) → L), LinearIndependent K b ∧ ∀ (i : Fin n), b (i.addNat k) = l i

extends a l.i. set of n elements to a n+k set, adding the new elements at the beggining

noncomputable def Basis.extendFinSucc {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {n : ℕ} {l : Fin n → L} (hs : LinearIndependent K l) (ht : Module.finrank K L = n + 1) : Module.Basis (Fin (n + 1)) K L

extends a li set of n elements to a basis of n+1 elements (dim space = n+1)

Equations

• Basis.extendFinSucc hs ht = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

theorem Basis.coe_extend_fin_succ {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {n : ℕ} {l : Fin n → L} (hs : LinearIndependent K l) (ht : Module.finrank K L = n + 1) : ⇑(extendFinSucc hs ht) = hs.extendFinSuccFun ⋯

The underlying function of Basis.extendFinSucc is the extended family.

theorem Basis.extend_fin_succ_tail_eq {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {n : ℕ} {l : Fin n → L} (hs : LinearIndependent K l) (ht : Module.finrank K L = n + 1) : Fin.tail ⇑(extendFinSucc hs ht) = l

states that Basis.extendFinSucc adds an element at the 0th place

theorem Basis.extend_fin_succ_head_not_in_span {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {n : ℕ} {l : Fin n → L} (hs : LinearIndependent K l) (ht : Module.finrank K L = n + 1) : (extendFinSucc hs ht) 0 ∉ Submodule.span K (Set.range l)

the new zeroth element is not contained in the span of l

theorem Basis.exists_unitsSMul {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (B : Module.Basis (Fin 3) K L) (α β γ : Kˣ) : ∃ (B' : Module.Basis (Fin 3) K L), B' 0 = α • B 0 ∧ B' 1 = β • B 1 ∧ B' 2 = γ • B 2

theorem LinearEquiv.conj_symm {K : Type u_3} {L₁ : Type u_4} {L₂ : Type u_5} [CommRing K] [AddCommGroup L₁] [AddCommGroup L₂] [Module K L₁] [Module K L₂] (e : L₁ ≃ₗ[K] L₂) : e.conj.symm = e.symm.conj

theorem Submodule.compl_span_singleton_of_codim_one {K : Type u_6} {L : Type u_7} [Field K] [AddCommGroup L] [Module K L] (p : Submodule K L) (h : Module.finrank K L = Module.finrank K ↥p + 1) : ∃ (x : L), IsCompl p (K ∙ x)

def LinearMap.ofProd {K : Type u_8} {L : Type u_9} [CommRing K] [AddCommGroup L] [Module K L] {M₁ : Type u_10} {M₂ : Type u_11} [AddCommGroup M₁] [AddCommGroup M₂] [Module K M₁] [Module K M₂] (f : M₁ →ₗ[K] L) (g : M₂ →ₗ[K] L) : M₁ × M₂ →ₗ[K] L

The linear map from M₁ × M₂ to L defined by specifying maps from M₁ and M₂ to L.

Equations

• f.ofProd g = f ∘ₗ LinearMap.fst K M₁ M₂ + g ∘ₗ LinearMap.snd K M₁ M₂

@[simp]

theorem LinearMap.ofProd_apply {K : Type u_8} {L : Type u_9} [CommRing K] [AddCommGroup L] [Module K L] {M₁ : Type u_10} {M₂ : Type u_11} [AddCommGroup M₁] [AddCommGroup M₂] [Module K M₁] [Module K M₂] (f : M₁ →ₗ[K] L) (g : M₂ →ₗ[K] L) (x : M₁ × M₂) : (f.ofProd g) x = f x.1 + g x.2

theorem Submodule.prod_injective_of_disjoint {K : Type u_10} {L : Type u_11} [CommRing K] [AddCommGroup L] [Module K L] {p q : Submodule K L} (h : Disjoint p q) : Function.Injective ⇑(p.subtype.ofProd q.subtype)

If two submodules are disjoint, then the canonical map from the product is injective.

theorem Submodule.prod_surjective_of_codisjoint {K : Type u_10} {L : Type u_11} [CommRing K] [AddCommGroup L] [Module K L] {p q : Submodule K L} (h : Codisjoint p q) : Function.Surjective ⇑(p.subtype.ofProd q.subtype)

If two submodules are codisjoint, then the canonical map from the product is surjectve.

noncomputable def LinearEquiv.ofComplSubmodules {K : Type u_10} {L : Type u_11} [CommRing K] [AddCommGroup L] [Module K L] {p q : Submodule K L} (h : IsCompl p q) : (↥p × ↥q) ≃ₗ[K] L

If two submodules are complementary, then their product is isomorphic to the ambient space.

Equations

• LinearEquiv.ofComplSubmodules h = LinearEquiv.ofBijective (p.subtype.ofProd q.subtype) ⋯

@[simp]

theorem LinearEquiv.ofComplSubmodules_apply {K : Type u_10} {L : Type u_11} [CommRing K] [AddCommGroup L] [Module K L] {p q : Submodule K L} (h : IsCompl p q) (x : ↥p × ↥q) : (ofComplSubmodules h) x = ↑x.1 + ↑x.2

theorem LinearEquiv.ofComplSubmodules_symm_apply {K : Type u_10} {L : Type u_11} [CommRing K] [AddCommGroup L] [Module K L] {p q : Submodule K L} (h : IsCompl p q) (x y z : L) (hy : y ∈ p) (hz : z ∈ q) (hx : x = y + z) : (ofComplSubmodules h).symm x = (⟨y, hy⟩, ⟨z, hz⟩)

theorem LinearEquiv.ofComplSubmodules_symm_apply_left {K : Type u_10} {L : Type u_11} [CommRing K] [AddCommGroup L] [Module K L] {p q : Submodule K L} (h : IsCompl p q) (x : L) (hx : x ∈ p) : (ofComplSubmodules h).symm x = (⟨x, hx⟩, 0)

theorem LinearEquiv.ofComplSubmodules_symm_apply_right {K : Type u_10} {L : Type u_11} [CommRing K] [AddCommGroup L] [Module K L] {p q : Submodule K L} (h : IsCompl p q) (x : L) (hx : x ∈ q) : (ofComplSubmodules h).symm x = (0, ⟨x, hx⟩)

theorem LinearEquiv.ofComplSubmodules_symm_add {K : Type u_10} {L : Type u_11} [CommRing K] [AddCommGroup L] [Module K L] {p q : Submodule K L} (h : IsCompl p q) (x : L) : x = ↑((ofComplSubmodules h).symm x).1 + ↑((ofComplSubmodules h).symm x).2

noncomputable def LinearEquiv.toSpanSingleton (K : Type u_12) (L : Type u_13) [Field K] [AddCommGroup L] [Module K L] {x : L} (h : x ≠ 0) : K ≃ₗ[K] ↥(K ∙ x)

The natural map from the base field to scalar multiples of x is an isomorphism if x ≠ 0.

Equations

• LinearEquiv.toSpanSingleton K L h = ⋯.mp (LinearEquiv.ofInjective (LinearMap.toSpanSingleton K L x) ⋯)

@[simp]

theorem LinearEquiv.toSpanSingleton_apply (K : Type u_12) (L : Type u_13) [Field K] [AddCommGroup L] [Module K L] {x : L} (h : x ≠ 0) (a : K) : (toSpanSingleton K L h) a = ⟨a • x, ⋯⟩

@[simp]

theorem LinearEquiv.toSpanSingleton_symm_apply (K : Type u_12) (L : Type u_13) [Field K] [AddCommGroup L] [Module K L] {x : L} (h : x ≠ 0) (a : K) : (toSpanSingleton K L h).symm ⟨a • x, ⋯⟩ = a

theorem LinearEquiv.toSpanSingleton_symm_apply' (K : Type u_12) (L : Type u_13) [Field K] [AddCommGroup L] [Module K L] {x : L} (h : x ≠ 0) (y : ↥(K ∙ x)) : (toSpanSingleton K L h).symm y • x = ↑y

theorem LieAlgebra.coeff_zero_of_lin_dep {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] {X Y : L} {α β : K} (hXY : ⁅X, Y⁆ ≠ 0) (Hzero : α • X + β • Y = 0) : α = 0

theorem LieAlgebra.linearIndependent_of_bracket_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (X Y : L) (hXY : ⁅X, Y⁆ ≠ 0) : LinearIndependent K ![X, Y]

If ⁅X, Y⁆ ≠ 0, then X and Y are linearly independent.

theorem LieAlgebra.basis_of_bracket_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (h : Module.finrank K L = 2) (X Y : L) (hXY : ⁅X, Y⁆ ≠ 0) : ∃ (B : Module.Basis (Fin 2) K L), B 0 = X ∧ B 1 = Y

If ⁅X, Y⁆ ≠ 0 in a two-dimensional Lie algebra, then X and Y form a basis.

theorem LieAlgebra.derivedSeries_succ_is_span {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] {k : ℕ} : ↑(derivedSeries K L (k + 1)) = Submodule.span K {x : L | ∃ (y : ↥(derivedSeries K L k)) (z : ↥(derivedSeries K L k)), ↑⁅y, z⁆ = x}

The k+1-th term of the derived series is spanned as submodule by Lie brackets of elements in the k-th term.

@[reducible, inline]

abbrev LieAlgebra.commutator (K : Type u_5) (L : Type u_6) [CommRing K] [LieRing L] [LieAlgebra K L] : LieIdeal K L

The commutator ideal of a Lie algebra.

Equations

• LieAlgebra.commutator K L = LieAlgebra.derivedSeries K L 1

theorem LieAlgebra.commutator_eq_span {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] : ↑(commutator K L) = Submodule.span K {x : L | ∃ (y : L) (z : L), ⁅y, z⁆ = x}

The commutator ideal is linearly spanned by Lie brackets.

theorem LieAlgebra.lie_mem_commutator {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] (x y : L) : ⁅x, y⁆ ∈ commutator K L

Lie brackets are contained in the commutator ideal.

theorem LieAlgebra.solvable_of_commutator_solvable {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] (comm : IsSolvable ↥(commutator K L)) : IsSolvable L

If the commutator of a Lie algebra is solvable, then the Lie algebra is solvable.

theorem LieSubalgebra.mem_lieSpan_singleton {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] {y x : L} : x ∈ lieSpan K L {y} ↔ ∃ (a : K), a • y = x

theorem LieSubalgebra.lieSpan_singleton {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] {x : L} : (lieSpan K L {x}).toSubmodule = K ∙ x

The Lie subalgebra generated by a single element equals the linear subspace spanned by it.

theorem LieSubmodule.mem_lieSpan_singleton {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] {y x : L} (H : ∀ (z : L), ∃ (a : K), ⁅z, y⁆ = a • y) : x ∈ lieSpan K L {y} ↔ ∃ (a : K), a • y = x

theorem LieSubmodule.lieSpan_singleton {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] {x : L} (H : ∀ (z : L), ∃ (a : K), ⁅z, x⁆ = a • x) : ↑(lieSpan K L {x}) = K ∙ x

The Lie submodule generated by a single element x equals the linear subspace spanned by it if ⁅z, x⁆ is a multiple of x for all z.

theorem LieIdeal.finrank_toSubmodule {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] {I : LieIdeal K L} : Module.finrank K ↥I = Module.finrank K ↥↑I

theorem binary_predicate_3_choose_2 {P : Fin 3 → Fin 3 → Prop} (h₀₁ : P 0 1) (h₀₂ : P 0 2) (h₁₂ : P 1 2) (i j : Fin 3) : i < j → P i j

def LieHom.smulRight {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] (f : Module.End K L) : K →ₗ⁅K⁆ Module.End K L

LinearMap.smulRight as a Lie algebra homomorphism.

Equations

• LieHom.smulRight f = { toLinearMap := LinearMap.id.smulRight f, map_lie' := ⋯ }

@[simp]

theorem LieHom.coe_smulRight {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] (f : Module.End K L) : ⇑(smulRight f) = fun (a : K) => a • f

theorem LieHom.smulRight_apply {K : Type u_3} {L : Type u_4} [CommRing K] [LieRing L] [LieAlgebra K L] (f : Module.End K L) (a : K) : (smulRight f) a = a • f

theorem LieAlgebra.codim_commutator_ge_one_of_solvable {K : Type u_5} {L : Type u_6} [Field K] [LieRing L] [LieAlgebra K L] {n : ℕ} (dimn : Module.finrank K L = n + 1) (issolvable : IsSolvable L) : Module.finrank K ↥(commutator K L) ≤ n

If the Lie algebra L of dimension n + 1 is solvable, then its commutator ideal has dimension at most n.

theorem LieAlgebra.finrank_commutator_le_one_of_lie_basis {K : Type u_5} {L : Type u_6} [Field K] [LieRing L] [LieAlgebra K L] {n : ℕ} (B : Module.Basis (Fin n) K L) (X : L) (h : ∀ (i j : Fin n), i < j → ∃ (α : K), ⁅B i, B j⁆ = α • X) : Module.finrank K ↥(commutator K L) ≤ 1

A finite-dimensional Lie algebra has commutator dimension at most one if for a basis, all Lie brackets are multiples of the same element.

def LieAlgebra.IsTwoStepNilpotent (K : Type u_7) (L : Type u_8) [CommRing K] [LieRing L] [LieAlgebra K L] : Prop

We define a Lie algebra to be two-step nilpotent if its commutator ideal is contained in the center.

Equations

• LieAlgebra.IsTwoStepNilpotent K L = (LieAlgebra.commutator K L ≤ LieAlgebra.center K L)

theorem LieAlgebra.isTwoStepNilpotent_iff (K : Type u_7) (L : Type u_8) [CommRing K] [LieRing L] [LieAlgebra K L] : IsTwoStepNilpotent K L ↔ commutator K L ≤ center K L

theorem LieAlgebra.isTwoStepNilpotent_iff_lowerCentral (K : Type u_7) (L : Type u_8) [CommRing K] [LieRing L] [LieAlgebra K L] : IsTwoStepNilpotent K L ↔ LieModule.lowerCentralSeries K L L 2 = ⊥

A Lie algebra is two-step nilpotent iff its lower central series terminates after two steps.

theorem LieAlgebra.isTwoStepNilpotent_iff_lowerCentral' (K : Type u_7) (L : Type u_8) [CommRing K] [LieRing L] [LieAlgebra K L] : IsTwoStepNilpotent K L ↔ LieModule.lowerCentralSeries ℤ L L 2 = ⊥

A Lie algebra is two-step nilpotent iff its lower central series terminates after two steps.

def LieAlgebra.IsAlmostAbelian (K : Type u_7) (L : Type u_8) [CommRing K] [LieRing L] [LieAlgebra K L] : Prop

A Lie algebra is almost abelian if it has a codimension one abelian ideal.

Equations

• LieAlgebra.IsAlmostAbelian K L = ∃ (I : LieIdeal K L), IsLieAbelian ↥I ∧ Module.finrank K L = Module.finrank K ↥I + 1

theorem LieAlgebra.isAlmostAbelian_iff (K : Type u_7) (L : Type u_8) [CommRing K] [LieRing L] [LieAlgebra K L] : IsAlmostAbelian K L ↔ ∃ (I : LieIdeal K L), IsLieAbelian ↥I ∧ Module.finrank K L = Module.finrank K ↥I + 1

@[simp]

theorem LieIdeal.rank_top (K : Type u_5) (L : Type u_6) [CommRing K] [LieRing L] [LieAlgebra K L] : Module.rank K ↥⊤ = Module.rank K L

@[simp]

theorem LieIdeal.finrank_top (K : Type u_5) (L : Type u_6) [CommRing K] [LieRing L] [LieAlgebra K L] : Module.finrank K ↥⊤ = Module.finrank K L

theorem LieDerivation.map_commutator {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] (D : LieDerivation K L L) : Submodule.map ↑D ↑(LieAlgebra.commutator K L) ≤ ↑(LieAlgebra.commutator K L)

A derivation of a Lie algebra maps the commutator into the commutator.

theorem LieAlgebra.ad_into_commutator' {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] (x : L) : Submodule.map ↑((LieDerivation.ad K L) x) ⊤ ≤ ↑(commutator K L)

The adjoint action of a Lie algebra on itself maps everything into the commutator.

theorem LieAlgebra.ad_into_commutator {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] (x : L) : Submodule.map ((ad K L) x) ⊤ ≤ ↑(commutator K L)

The adjoint action of a Lie algebra on itself maps everything into the commutator.

theorem LieAlgebra.abelian_iff_dim_comm_zero {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] : Module.finrank K ↥(commutator K L) = 0 ↔ IsLieAbelian L

A finite-dimensional Lie algebra is abelian if and only if its commutator ideal has dimension zero.

theorem LieAlgebra.abelian_iff_lie_basis_eq_zero {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] {n : ℕ} (B : Module.Basis (Fin n) K L) : IsLieAbelian L ↔ ∀ (i j : Fin n), i < j → ⁅B i, B j⁆ = 0

A finite-dimensional Lie algebra is abelian if and only if for any basis, all Lie brackets vanish.

theorem LieEquiv.symm_toLinearEquiv {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') : e.symm.toLinearEquiv = e.toLinearEquiv.symm

theorem LieIdeal.map_eq_image_of_surj {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] {f : L →ₗ⁅K⁆ L'} (h : Function.Surjective ⇑f) (I : LieIdeal K L) : ↑(map f I) = Submodule.map (↑f) (toLieSubalgebra K L I).toSubmodule

If f is a surjective homomorphism of Lie algebras, then LieIdeal.map f I is the image of I under f (equality of submodules).

theorem LieIdeal.map_eq_image_of_surj' {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] {f : L →ₗ⁅K⁆ L'} (h : Function.Surjective ⇑f) (I : LieIdeal K L) : toLieSubalgebra K L' (map f I) = LieSubalgebra.map f (toLieSubalgebra K L I)

If f is a surjective homomorphism of Lie algebras, then LieIdeal.map f I is the image of I under f (equality of Lie subalgebras).

theorem LieIdeal.map_eq_image_of_surj'' {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] {f : L →ₗ⁅K⁆ L'} (h : Function.Surjective ⇑f) (I : LieIdeal K L) : ↑(map f I) = ⇑f '' ↑I

If f is a surjective homomorphism of Lie algebras, then LieIdeal.map f I is the image of I under f (equality of sets).

theorem LieIdeal.map_comap_eq_of_surjective {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] {f : L →ₗ⁅K⁆ L'} (h : Function.Surjective ⇑f) (I : LieIdeal K L') : map f (comap f I) = I

def LieEquiv.ofIdeals {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') (I : LieIdeal K L) (I' : LieIdeal K L') (h : LieIdeal.map e.toLieHom I = I') : ↥I ≃ₗ⁅K⁆ ↥I'

An equivalence of Lie algebras restricts to an equivalence from any ideal onto its image.

Equations

• e.ofIdeals I I' h = LieEquiv.ofSubalgebras (LieIdeal.toLieSubalgebra K L I) (LieIdeal.toLieSubalgebra K L' I') e ⋯

theorem LieEquiv.commutator_map {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') : LieIdeal.map e.toLieHom (LieAlgebra.commutator K L) = LieAlgebra.commutator K L'

Under an equivalence of Lie algebras, the commutator is mapped to the commutator.

def LieEquiv.commutatorEquiv {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') : ↥(LieAlgebra.commutator K L) ≃ₗ⁅K⁆ ↥(LieAlgebra.commutator K L')

An equivalence of Lie algebras induces an equivalence of commutator subalgebras.

Equations

• e.commutatorEquiv = e.ofIdeals (LieAlgebra.commutator K L) (LieAlgebra.commutator K L') ⋯

theorem LieEquiv.commutator_equiv_apply {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') (x : L) (hx : x ∈ LieAlgebra.commutator K L) : e.commutatorEquiv ⟨x, hx⟩ = ⟨e x, ⋯⟩

theorem LieEquiv.commutator_equiv_symm {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') : e.commutatorEquiv.symm = e.symm.commutatorEquiv

theorem LieAlgebra.dim_commutator_eq_of_lieEquiv {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') : Module.finrank K ↥(commutator K L) = Module.finrank K ↥(commutator K L')

theorem LieEquiv.center_map {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') : LieIdeal.map e.toLieHom (LieAlgebra.center K L) = LieAlgebra.center K L'

Under an equivalence of Lie algebras, the center is mapped to the center.

theorem LieIdeal.comap_map_eq_of_equiv {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') (I : LieIdeal K L) : comap e.toLieHom (map e.toLieHom I) = I

theorem LieEquiv.preserves_isTwoStepNilpotent {K : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing K] [LieRing L] [LieRing L'] [LieAlgebra K L] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') : LieAlgebra.IsTwoStepNilpotent K L ↔ LieAlgebra.IsTwoStepNilpotent K L'

Under an equivalence of Lie algebras, two-step nilpotency is preserved.

def LinearEquiv.smulId {K : Type u_1} [CommRing K] : K ≃ₗ[K] K →ₗ[K] K

The canonical isomorphism from K to K →ₗ[K] K.

Equations

• LinearEquiv.smulId = { toFun := fun (x : K) => x • LinearMap.id, map_add' := ⋯, map_smul' := ⋯, invFun := fun (f : K →ₗ[K] K) => f 1, left_inv := ⋯, right_inv := ⋯ }

noncomputable def Basis.ofEndSelf {K : Type u_1} [CommRing K] : Module.Basis (Fin 1) K (K →ₗ[K] K)

The basis of K →ₗ[K] K consisting of LinearMap.id.

Equations

• Basis.ofEndSelf = (Module.Basis.singleton (Fin 1) K).map LinearEquiv.smulId