Lie

Results named in Tau Ceti's TauCeti.RepresentationTheory.Lie modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremAdo's theorem in characteristic zero#

Every finite-dimensional Lie algebra over a field of characteristic zero admits a faithful finite-dimensional representation.

TauCeti.adoCharZero.{u, v} (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L]
  [FiniteDimensional K L] [CharZero K] :
  ∃ V x x_1, ∃ (_ : FiniteDimensional K V), ∃ ρ, Function.Injective ⇑ρ

Lean

Formalized in Tau Ceti as TauCeti.adoCharZero.

Other forms

Ado's theorem in characteristic zero, with nilpotence on the nilradical. Formalized in Tau Ceti as TauCeti.exists_faithful_nilrepresentation_charZero.

TauCeti.exists_faithful_nilrepresentation_charZero.{u, v} (K : Type u) (L : Type v) [Field K]
  [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [CharZero K] :
  ∃ V x x_1,
    ∃ (_ : FiniteDimensional K V),
      ∃ ρ, Function.Injective ⇑ρ ∧ ∀ x_3 ∈ TauCeti.LieAlgebra.nilradical K L, IsNilpotent (ρ x_3)

Ado's theorem in prime characteristic. Formalized in Tau Ceti as TauCeti.adoCharP.

TauCeti.adoCharP.{u, v} (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L]
  [FiniteDimensional K L] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] :
  ∃ V x x_1, ∃ (_ : FiniteDimensional K V), ∃ ρ, Function.Injective ⇑ρ

Sources

• Tau Ceti documentation: TauCeti.adoCharZero
• Source of TauCeti.adoCharZero in TauCeti/RepresentationTheory/Lie/Ado/CharacteristicZero.lean

LeanTauCeti.adoCharZero · TauCeti.exists_faithful_nilrepresentation_charZero · TauCeti.adoCharP

Uses 5 · Used by 1

Proof usesThe Frobenius commutator identity · The Krull intersection theorem for an extended ideal · Levi's theorem · The linear-independence half of the Poincaré--Birkhoff--Witt theorem · The Poincaré--Birkhoff--Witt theorem

Used byHochschild's strengthening of Ado's theorem in characteristic zero

TheoremThe Ado–Iwasawa theorem#

Every finite-dimensional Lie algebra over a field admits a faithful finite-dimensional representation.

TauCeti.adoIwasawa.{u, v} (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L]
  [FiniteDimensional K L] : ∃ V x x_1, ∃ (_ : FiniteDimensional K V), ∃ ρ, Function.Injective ⇑ρ

Lean

Formalized in Tau Ceti as TauCeti.adoIwasawa.

Other forms

The Ado–Iwasawa theorem with nilpotence on the nilradical. Formalized in Tau Ceti as TauCeti.exists_faithful_nilrepresentation.

TauCeti.exists_faithful_nilrepresentation.{u, v} (K : Type u) (L : Type v) [Field K] [LieRing L]
  [LieAlgebra K L] [FiniteDimensional K L] :
  ∃ V x x_1,
    ∃ (_ : FiniteDimensional K V),
      ∃ ρ, Function.Injective ⇑ρ ∧ ∀ x_3 ∈ TauCeti.LieAlgebra.nilradical K L, IsNilpotent (ρ x_3)

Sources

• Tau Ceti documentation: TauCeti.adoIwasawa
• Source of TauCeti.adoIwasawa in TauCeti/RepresentationTheory/Lie/Ado/ArbitraryField.lean

LeanTauCeti.adoIwasawa · TauCeti.exists_faithful_nilrepresentation

Uses 1 · Used by 1

Proof usesHochschild's strengthening of the Ado–Iwasawa theorem

Used byThe matrix form of the Ado–Iwasawa theorem

TheoremBirkhoff's theorem on a weighted PBW quotient#

A finite-dimensional nilpotent Lie algebra has a faithful left-multiplication representation on a finite-dimensional weighted enveloping quotient, with one positive nilpotence bound for all acting operators. The basis, weights, and cutoff are supplied by the conclusion, in every characteristic.

TauCeti.exists_faithful_weightedPBWRepresentation.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K]
  [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieRing.IsNilpotent L] :
  ∃ N b w,
    ∃ (hbracket :
      ∀ (i j k : Fin (Module.finrank K L)), w k < w i + w j → (b.repr ⁅b i, b j⁆) k = 0),
      0 < N ∧
        (∀ (i : Fin (Module.finrank K L)), 0 < w i ∧ w i < N) ∧
          Module.Finite K (UniversalEnvelopingAlgebra K L ⧸ b.weightedPBWIdeal w hbracket N) ∧
            Function.Injective ⇑(b.weightedPBWRepresentation w hbracket N) ∧
              ∀ (x : L), (b.weightedPBWRepresentation w hbracket N) x ^ N = 0

Lean

Formalized in Tau Ceti as TauCeti.exists_faithful_weightedPBWRepresentation.

Sources

• Tau Ceti documentation: TauCeti.exists_faithful_weightedPBWRepresentation
• Source of TauCeti.exists_faithful_weightedPBWRepresentation in TauCeti/RepresentationTheory/Lie/NilpotentFaithful.lean

LeanTauCeti.exists_faithful_weightedPBWRepresentation

TheoremHochschild's nilpotence theorem in characteristic zero#

if the nilradical of a finite-dimensional Lie algebra L acts nilpotently on a finite-dimensional L-module M, then so does every ad-nilpotent element of L. The Lie subalgebra S is any Levi complement, that is, any complement of the solvable radical; the conclusion does not depend on it.

LieSubalgebra.isNilpotent_toEnd_of_isNilpotent_ad_of_isCompl_radical.{u_1, u_2, u_3} {K : Type u_1}
  {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M]
  [_root_.Module K M] [FiniteDimensional K M] [LieRingModule L M] [LieModule K L M]
  [FiniteDimensional K L] (S : LieSubalgebra K L)
  (hS : IsCompl (↑(LieAlgebra.radical K L)) S.toSubmodule)
  (hM : ∀ n ∈ TauCeti.LieAlgebra.nilradical K L, IsNilpotent ((LieModule.toEnd K L M) n)) {x : L}
  (hx : IsNilpotent ((LieAlgebra.ad K L) x)) : IsNilpotent ((LieModule.toEnd K L M) x)

Lean

Formalized in Tau Ceti as LieSubalgebra.isNilpotent_toEnd_of_isNilpotent_ad_of_isCompl_radical.

Sources

• Tau Ceti documentation: LieSubalgebra.isNilpotent_toEnd_of_isNilpotent_ad_of_isCompl_radical
• Source of LieSubalgebra.isNilpotent_toEnd_of_isNilpotent_ad_of_isCompl_radical in TauCeti/RepresentationTheory/Lie/AdNilpotent.lean

LeanLieSubalgebra.isNilpotent_toEnd_of_isNilpotent_ad_of_isCompl_radical

Used by 1

Used byHochschild's strengthening of Ado's theorem in characteristic zero

TheoremHochschild's strengthening of Ado's theorem in characteristic zero#

A finite-dimensional Lie algebra over a field of characteristic zero has a faithful finite-dimensional representation that preserves nilpotence of the adjoint action: every ad-nilpotent element acts nilpotently.

For semisimple L the nilradical is zero, so the nilpotence clause of TauCeti.exists_faithful_nilrepresentation_charZero is empty there, while this one still constrains every ad-nilpotent element.

TauCeti.exists_faithful_preserving_ad_nilpotence_charZero.{u, v} (K : Type u) (L : Type v) [Field K]
  [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [CharZero K] :
  ∃ V x x_1,
    ∃ (_ : FiniteDimensional K V),
      ∃ ρ,
        Function.Injective ⇑ρ ∧
          ∀ (x_3 : L), IsNilpotent ((LieAlgebra.ad K L) x_3) → IsNilpotent (ρ x_3)

Lean

Formalized in Tau Ceti as TauCeti.exists_faithful_preserving_ad_nilpotence_charZero.

Sources

• Tau Ceti documentation: TauCeti.exists_faithful_preserving_ad_nilpotence_charZero
• Source of TauCeti.exists_faithful_preserving_ad_nilpotence_charZero in TauCeti/RepresentationTheory/Lie/Ado/CharacteristicZero.lean

LeanTauCeti.exists_faithful_preserving_ad_nilpotence_charZero

Uses 3 · Used by 1

Proof usesAdo's theorem in characteristic zero · Hochschild's nilpotence theorem in characteristic zero · Levi's theorem

Used byHochschild's strengthening of the Ado–Iwasawa theorem

TheoremHochschild's strengthening of the Ado–Iwasawa theorem#

A finite-dimensional Lie algebra over an arbitrary field has a faithful finite-dimensional representation that preserves nilpotence of the adjoint action: every ad-nilpotent element acts nilpotently.

TauCeti.exists_faithful_preserving_ad_nilpotence.{u, v} (K : Type u) (L : Type v) [Field K]
  [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] :
  ∃ V x x_1,
    ∃ (_ : FiniteDimensional K V),
      ∃ ρ,
        Function.Injective ⇑ρ ∧
          ∀ (x_3 : L), IsNilpotent ((LieAlgebra.ad K L) x_3) → IsNilpotent (ρ x_3)

Lean

Formalized in Tau Ceti as TauCeti.exists_faithful_preserving_ad_nilpotence.

Sources

• Tau Ceti documentation: TauCeti.exists_faithful_preserving_ad_nilpotence
• Source of TauCeti.exists_faithful_preserving_ad_nilpotence in TauCeti/RepresentationTheory/Lie/Ado/ArbitraryField.lean

LeanTauCeti.exists_faithful_preserving_ad_nilpotence

Uses 5 · Used by 1

Proof usesThe Frobenius commutator identity · Hochschild's strengthening of Ado's theorem in characteristic zero · The Krull intersection theorem for an extended ideal · The linear-independence half of the Poincaré--Birkhoff--Witt theorem · The Poincaré--Birkhoff--Witt theorem

Used byThe Ado–Iwasawa theorem

TheoremThe matrix form of the Ado–Iwasawa theorem#

Every finite-dimensional Lie algebra over a field embeds in 𝔤𝔩_n = Matrix (Fin n) (Fin n) K for some n. Over ℝ this is the embedding consumed by the integration of a real Lie algebra to a Lie group.

TauCeti.exists_injective_lieHom_matrix.{u, v} (K : Type u) (L : Type v) [Field K] [LieRing L]
  [LieAlgebra K L] [FiniteDimensional K L] : ∃ n f, Function.Injective ⇑f

Lean

Formalized in Tau Ceti as TauCeti.exists_injective_lieHom_matrix.

Sources

• Tau Ceti documentation: TauCeti.exists_injective_lieHom_matrix
• Source of TauCeti.exists_injective_lieHom_matrix in TauCeti/RepresentationTheory/Lie/Ado/ArbitraryField.lean

LeanTauCeti.exists_injective_lieHom_matrix

Uses 1

Proof usesThe Ado–Iwasawa theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.