Roots of Lie algebras with non-degenerate Killing forms

The file contains definitions and results about roots of Lie algebras with non-degenerate Killing forms.

Main definitions

• LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra: if the Killing form of a Lie algebra is non-singular, it remains non-singular when restricted to a Cartan subalgebra.
• LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra: if the Killing form of a Lie algebra is non-singular, then its Cartan subalgebras are Abelian.
• LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra: over a perfect field, if a Lie algebra has non-degenerate Killing form, Cartan subalgebras contain only semisimple elements.
• LieAlgebra.IsKilling.span_weight_eq_top: given a splitting Cartan subalgebra H of a finite-dimensional Lie algebra with non-singular Killing form, the corresponding roots span the dual space of H.
• LieAlgebra.IsKilling.coroot: the coroot corresponding to a root.
• LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot: given a root α with respect to a Cartan subalgebra H, we have a natural decomposition of H as the kernel of α and the span of the coroot corresponding to α.
• LieAlgebra.IsKilling.finrank_rootSpace_eq_one: root spaces are one-dimensional.

theorem LieAlgebra.restrict_killingForm (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) : (killingForm R L).restrict H.toSubmodule = LieModule.traceForm R { x : L // x ∈ H } L

theorem LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] : LinearMap.ker ((killingForm R L).restrict H.toSubmodule) = ⊥

If the Killing form of a Lie algebra is non-singular, it remains non-singular when restricted to a Cartan subalgebra.

@[simp]

theorem LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] : LinearMap.ker (LieModule.traceForm R { x : L // x ∈ H } L) = ⊥

theorem LieAlgebra.IsKilling.traceForm_cartan_nondegenerate (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] : (LieModule.traceForm R { x : L // x ∈ H } L).Nondegenerate

instance LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsKilling R L] [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] : IsLieAbelian { x : L // x ∈ H }

Equations

• ⋯ = ⋯

theorem LieAlgebra.killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero (K : Type u_2) (L : Type u_3) [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] {α : { x : L // x ∈ H } → K} {β : { x : L // x ∈ H } → K} {x : L} {y : L} (hx : x ∈ LieAlgebra.rootSpace H α) (hy : y ∈ LieAlgebra.rootSpace H β) (hαβ : α + β ≠ 0) : ((killingForm K L) x) y = 0

For any α and β, the corresponding root spaces are orthogonal with respect to the Killing form, provided α + β ≠ 0.

theorem LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg (K : Type u_2) (L : Type u_3) [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] {α : { x : L // x ∈ H } → K} {x : L} (hx : x ∈ LieAlgebra.rootSpace H α) (hx' : ∀ y ∈ LieAlgebra.rootSpace H (-α), ((killingForm K L) x) y = 0) : x ∈ LinearMap.ker (killingForm K L)

Elements of the α root space which are Killing-orthogonal to the -α root space are Killing-orthogonal to all of L.

theorem LieAlgebra.IsKilling.eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra (K : Type u_2) (L : Type u_3) [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] {x : L} (hx : x ∈ H) (hx' : IsNilpotent ((LieAlgebra.ad K L) x)) : x = 0

If a Lie algebra L has non-degenerate Killing form, the only element of a Cartan subalgebra whose adjoint action on L is nilpotent, is the zero element.

Over a perfect field a much stronger result is true, see LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra.

@[simp]

theorem LieAlgebra.IsKilling.corootSpace_zero_eq_bot (K : Type u_2) (L : Type u_3) [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] : LieAlgebra.corootSpace 0 = ⊥

@[simp]

theorem LieAlgebra.IsKilling.cartanEquivDual_apply_apply {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] : ∀ (a m : { x : L // x ∈ H }), ((LieAlgebra.IsKilling.cartanEquivDual H) a) m = (LinearMap.trace K L) ((LieModule.toEnd K { x : L // x ∈ H } L) a * (LieModule.toEnd K { x : L // x ∈ H } L) m)

noncomputable def LieAlgebra.IsKilling.cartanEquivDual {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] : { x : L // x ∈ H } ≃ₗ[K] Module.Dual K { x : L // x ∈ H }

The restriction of the Killing form to a Cartan subalgebra, as a linear equivalence to the dual.

Equations

• LieAlgebra.IsKilling.cartanEquivDual H = (LieModule.traceForm K { x : L // x ∈ H } L).toDual ⋯

noncomputable def LieAlgebra.IsKilling.coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] (α : LieModule.Weight K { x : L // x ∈ H } L) : { x : L // x ∈ H }

The coroot corresponding to a root.

Equations

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

theorem LieAlgebra.IsKilling.traceForm_coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] (α : LieModule.Weight K { x : L // x ∈ H } L) (x : { x : L // x ∈ H }) : ((LieModule.traceForm K { x : L // x ∈ H } L) (LieAlgebra.IsKilling.coroot α)) x = 2 • (α ((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K { x : L // x ∈ H } L α)))⁻¹ • α x

theorem LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] {α : LieModule.Weight K { x : L // x ∈ H } L} {e : L} {f : L} (heα : e ∈ LieAlgebra.rootSpace H ⇑α) (hfα : f ∈ LieAlgebra.rootSpace H (-⇑α)) (aux : ∀ (h : { x : L // x ∈ H }), ⁅h, e⁆ = α h • e) : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K { x : L // x ∈ H } L α))

theorem LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] (α : LieModule.Weight K { x : L // x ∈ H } L) : (LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K { x : L // x ∈ H } L α) ∈ LieAlgebra.corootSpace ⇑α

This is Proposition 4.18 from [carter2005] except that we use LieModule.exists_forall_lie_eq_smul instead of Lie's theorem (and so avoid assuming K has characteristic zero).

@[simp]

theorem LieAlgebra.IsKilling.span_weight_eq_top {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] : Submodule.span K (Set.range (LieModule.Weight.toLinear K { x : L // x ∈ H } L)) = ⊤

Given a splitting Cartan subalgebra H of a finite-dimensional Lie algebra with non-singular Killing form, the corresponding roots span the dual space of H.

@[simp]

theorem LieAlgebra.IsKilling.span_weight_isNonZero_eq_top (K : Type u_2) (L : Type u_3) [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] : Submodule.span K (LieModule.Weight.toLinear K { x : L // x ∈ H } L '' {α : LieModule.Weight K { x : L // x ∈ H } L | α.IsNonZero}) = ⊤

@[simp]

theorem LieAlgebra.IsKilling.iInf_ker_weight_eq_bot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] : ⨅ (α : LieModule.Weight K { x : L // x ∈ H } L), LieModule.Weight.ker = ⊥

theorem LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [PerfectField K] {x : L} (hx : x ∈ H) : ((LieAlgebra.ad K L) x).IsSemisimple

theorem LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [PerfectField K] {α : { x : L // x ∈ H } → K} {x : L} (hx : x ∈ LieAlgebra.rootSpace H α) (h : { x : L // x ∈ H }) : ⁅h, x⁆ = α h • x

theorem LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [PerfectField K] {α : LieModule.Weight K { x : L // x ∈ H } L} {e : L} {f : L} (heα : e ∈ LieAlgebra.rootSpace H ⇑α) (hfα : f ∈ LieAlgebra.rootSpace H (-⇑α)) : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K { x : L // x ∈ H } L α))

theorem LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton' {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [PerfectField K] (α : LieModule.Weight K { x : L // x ∈ H } L) : ↑(LieAlgebra.corootSpace ⇑α) = Submodule.span K {(LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K { x : L // x ∈ H } L α)}

theorem LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_corootSpace {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] (x : { x : L // x ∈ H }) (α : { x : L // x ∈ H } → K) (hαx : α x = 0) (hx : x ∈ LieAlgebra.corootSpace α) : x = 0

The contrapositive of this result is very useful, taking x to be the element of H corresponding to a root α under the identification between H and H^* provided by the Killing form.

theorem LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] (α : LieModule.Weight K { x : L // x ∈ H } L) : Disjoint LieModule.Weight.ker (lieIdealSubalgebra K { x : L // x ∈ H } (LieAlgebra.corootSpace ⇑α)).toSubmodule

theorem LieAlgebra.IsKilling.root_apply_cartanEquivDual_symm_ne_zero {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] {α : LieModule.Weight K { x : L // x ∈ H } L} (hα : α.IsNonZero) : α ((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K { x : L // x ∈ H } L α)) ≠ 0

theorem LieAlgebra.IsKilling.root_apply_coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] {α : LieModule.Weight K { x : L // x ∈ H } L} (hα : α.IsNonZero) : α (LieAlgebra.IsKilling.coroot α) = 2

@[simp]

theorem LieAlgebra.IsKilling.coroot_eq_zero_iff {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] {α : LieModule.Weight K { x : L // x ∈ H } L} : LieAlgebra.IsKilling.coroot α = 0 ↔ α.IsZero

@[simp]

theorem LieAlgebra.IsKilling.coroot_zero {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] [Nontrivial L] : LieAlgebra.IsKilling.coroot 0 = 0

theorem LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] (α : LieModule.Weight K { x : L // x ∈ H } L) : ↑(LieAlgebra.corootSpace ⇑α) = Submodule.span K {LieAlgebra.IsKilling.coroot α}

@[simp]

theorem LieAlgebra.IsKilling.corootSpace_eq_bot_iff {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] {α : LieModule.Weight K { x : L // x ∈ H } L} : LieAlgebra.corootSpace ⇑α = ⊥ ↔ α.IsZero

theorem LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] (α : LieModule.Weight K { x : L // x ∈ H } L) : IsCompl LieModule.Weight.ker (Submodule.span K {LieAlgebra.IsKilling.coroot α})

theorem LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] {α : LieModule.Weight K { x : L // x ∈ H } L} {x : { x : L // x ∈ H }} {y : { x : L // x ∈ H }} (hx : x ∈ LieModule.Weight.ker) (hy : y ∈ Submodule.span K {LieAlgebra.IsKilling.coroot α}) : ((LieModule.traceForm K { x : L // x ∈ H } L) x) y = 0

@[simp]

theorem LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] (α : LieModule.Weight K { x : L // x ∈ H } L) : (LieModule.traceForm K { x : L // x ∈ H } L).orthogonal (Submodule.span K {LieAlgebra.IsKilling.coroot α}) = LieModule.Weight.ker

@[simp]

theorem LieAlgebra.IsKilling.coroot_eq_iff {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] (α : LieModule.Weight K { x : L // x ∈ H } L) (β : LieModule.Weight K { x : L // x ∈ H } L) : LieAlgebra.IsKilling.coroot α = LieAlgebra.IsKilling.coroot β ↔ α = β

theorem LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] {α : LieModule.Weight K { x : L // x ∈ H } L} (hα : α.IsNonZero) : ∃ (h : L) (e : L) (f : L), IsSl2Triple h e f ∧ e ∈ LieAlgebra.rootSpace H ⇑α ∧ f ∈ LieAlgebra.rootSpace H (-⇑α)

theorem IsSl2Triple.h_eq_coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] {α : LieModule.Weight K { x : L // x ∈ H } L} (hα : α.IsNonZero) {h : L} {e : L} {f : L} (ht : IsSl2Triple h e f) (heα : e ∈ LieAlgebra.rootSpace H ⇑α) (hfα : f ∈ LieAlgebra.rootSpace H (-⇑α)) : h = ↑(LieAlgebra.IsKilling.coroot α)

theorem LieAlgebra.IsKilling.finrank_rootSpace_eq_one {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] (α : LieModule.Weight K { x : L // x ∈ H } L) (hα : α.IsNonZero) : FiniteDimensional.finrank K { x : L // x ∈ ↑(LieAlgebra.rootSpace H ⇑α) } = 1

instance LieModule.Weight.instInvolutiveNegSubtypeMemLieSubalgebra {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] : InvolutiveNeg (LieModule.Weight K { x : L // x ∈ H } L)

Equations

• LieModule.Weight.instInvolutiveNegSubtypeMemLieSubalgebra = InvolutiveNeg.mk ⋯

@[simp]

theorem LieModule.Weight.coe_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] {α : LieModule.Weight K { x : L // x ∈ H } L} : ⇑(-α) = -⇑α

theorem LieModule.Weight.IsZero.neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] {α : LieModule.Weight K { x : L // x ∈ H } L} (h : α.IsZero) : (-α).IsZero

@[simp]

theorem LieModule.Weight.isZero_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] {α : LieModule.Weight K { x : L // x ∈ H } L} : (-α).IsZero ↔ α.IsZero

theorem LieModule.Weight.IsNonZero.neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] {α : LieModule.Weight K { x : L // x ∈ H } L} (h : α.IsNonZero) : (-α).IsNonZero

@[simp]

theorem LieModule.Weight.isNonZero_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] {α : LieModule.Weight K { x : L // x ∈ H } L} : (-α).IsNonZero ↔ α.IsNonZero

@[simp]

theorem LieModule.Weight.toLinear_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] {α : LieModule.Weight K { x : L // x ∈ H } L} : LieModule.Weight.toLinear K { x : L // x ∈ H } L (-α) = -LieModule.Weight.toLinear K { x : L // x ∈ H } L α

@[simp]

theorem LieAlgebra.IsKilling.coroot_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K { x : L // x ∈ H } L] [CharZero K] (α : LieModule.Weight K { x : L // x ∈ H } L) : LieAlgebra.IsKilling.coroot (-α) = -LieAlgebra.IsKilling.coroot α