Nilpotent orbits, Springer resolution and subregular geometry

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe Jacobson–Morozov theorem#

In a finite-dimensional Lie algebra with nondegenerate Killing form over a field of characteristic zero, every nonzero ad-nilpotent element e is the nilpositive element of an sl₂ triple (h, e, f).

TauCeti.exists_isSl2Triple_of_isNilpotent_ad.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K]
  [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L]
  {e : L} (he : IsNilpotent ((LieAlgebra.ad K L) e)) (he0 : e ≠ 0) : ∃ h f, IsSl2Triple h e f
Lean

Formalized in Tau Ceti as TauCeti.exists_isSl2Triple_of_isNilpotent_ad.

Sources
LeanTauCeti.exists_isSl2Triple_of_isNilpotent_ad
Uses 2 · Used by 1
Proof usesJacobson's lemma on commutators · Morozov's lemma
Used byThe Jacobson–Morozov theorem for embeddings

TheoremThe Jacobson–Morozov theorem for embeddings#

In a finite-dimensional Lie algebra with nondegenerate Killing form over a field of characteristic zero, e is the image of the raising element E₀₁ under an injective Lie algebra homomorphism sl (Fin 2) K →ₗ⁅K⁆ L if and only if e ≠ 0 and ad e is nilpotent.

TauCeti.exists_injective_lieHom_slFinTwo_iff.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K]
  [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L]
  {e : L} :
  (∃ φ, Function.Injective ⇑φ ∧ φ ((LieAlgebra.SpecialLinear.single 0 1 ⋯) 1) = e) ↔
    IsNilpotent ((LieAlgebra.ad K L) e) ∧ e ≠ 0
Lean

Formalized in Tau Ceti as TauCeti.exists_injective_lieHom_slFinTwo_iff.

Sources
LeanTauCeti.exists_injective_lieHom_slFinTwo_iff
Uses 1
Proof usesThe Jacobson–Morozov theorem

TheoremKostant's conjugacy theorem#

Two sl₂ triples (h, e, f) and (h', e, f') with the same nilpositive element in a finite-dimensional Lie algebra over a field of characteristic zero are conjugate by an automorphism of L that fixes e and lies in the subgroup TauCeti.expAdSubgroup K e generated by the automorphisms exp (ad y) with y ∈ ker (ad e) ⊓ [e, L].

IsSl2Triple.exists_lieEquiv_apply_eq.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K] [CharZero K]
  [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f : L} [LieAlgebra ℚ L]
  (t : IsSl2Triple h e f) {h' f' : L} (t' : IsSl2Triple h' e f') :
  ∃ φ, φ.toLinearEquiv ∈ TauCeti.expAdSubgroup K e ∧ φ e = e ∧ φ h = h' ∧ φ f = f'
Lean

Formalized in Tau Ceti as IsSl2Triple.exists_lieEquiv_apply_eq.

Other forms

Kostant's conjugacy theorem for embeddings. Formalized in Tau Ceti as TauCeti.exists_lieEquiv_comp_eq_of_apply_eq.

TauCeti.exists_lieEquiv_comp_eq_of_apply_eq.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K]
  [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra ℚ L]
  {φ φ' : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) →ₗ⁅K⁆ L} (hφ : Function.Injective ⇑φ)
  (he :
    φ ((LieAlgebra.SpecialLinear.single 0 1 ⋯) 1) =
      φ' ((LieAlgebra.SpecialLinear.single 0 1 ⋯) 1)) :
  ∃ ψ,
    ψ.toLinearEquiv ∈ TauCeti.expAdSubgroup K (φ ((LieAlgebra.SpecialLinear.single 0 1 ⋯) 1)) ∧
      ψ.comp φ = φ'
Sources
LeanIsSl2Triple.exists_lieEquiv_apply_eq · TauCeti.exists_lieEquiv_comp_eq_of_apply_eq
Uses 2
Proof usesJacobson's lemma for the adjoint representation · Morozov's lemma

TheoremThe transverse decomposition L = [L, e] ⊕ ker (ad f)#

For an sl₂ triple (h, e, f) in a finite-dimensional Lie algebra over a field of characteristic zero, the range of ad e and the kernel of ad f are complementary.

IsSl2Triple.isCompl_range_ad_e_ker_ad_f.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K]
  [CharZero K] [LieRing L] [LieAlgebra K L] {h e f : L} [FiniteDimensional K L]
  (t : IsSl2Triple h e f) :
  IsCompl (LinearMap.range ((LieAlgebra.ad K L) e)) (LinearMap.ker ((LieAlgebra.ad K L) f))
Lean

Formalized in Tau Ceti as IsSl2Triple.isCompl_range_ad_e_ker_ad_f.

Sources
LeanIsSl2Triple.isCompl_range_ad_e_ker_ad_f

TheoremThe simple root values of a dominant neutral element lie in {0, 1, 2}#

If the neutral element h of an sl₂ triple lies in the Cartan subalgebra H and every simple root takes a natural value at h, then each simple root takes the value 0, 1 or 2 at h. These values label the weighted Dynkin diagram of the triple.

IsSl2Triple.root_apply_eq_zero_or_eq_one_or_eq_two.{u_1, u_2} {K : Type u_1} {L : Type u_2}
  [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L]
  [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {h : ↥H}
  {e f : L} (t : IsSl2Triple (↑h) e f) (hh : ∀ j ∈ b.support, ∃ n, ↑j h = ↑n)
  {i : ↥LieSubalgebra.root} (hi : i ∈ b.support) : ↑i h = 0 ∨ ↑i h = 1 ∨ ↑i h = 2
Lean

Formalized in Tau Ceti as IsSl2Triple.root_apply_eq_zero_or_eq_one_or_eq_two.

Sources
LeanIsSl2Triple.root_apply_eq_zero_or_eq_one_or_eq_two

TheoremThe dimension of a centralizer and of [𝔤, x]#

Over a field of characteristic zero, the dimension of a finite-type affine group G is the dimension of the centralizer C_G(x) of an element x of its Lie algebra 𝔤 plus the rank of ad x, the dimension of [𝔤, x].

TauCeti.ringKrullDim_quotient_centralizerHopfIdeal_add_finrank_range_ad.{u} {k : Type u} [Field k]
  [CharZero k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H]
  (x : Module.Dual k (TauCeti.Bialgebra.CotangentSpace k H)) :
  ringKrullDim (H ⧸ (TauCeti.centralizerHopfIdeal H x).toIdeal) +
      ↑(Module.finrank k
          ↥(LinearMap.range
              ((LieAlgebra.ad k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k H))) x))) =
    ringKrullDim H
Lean

Formalized in Tau Ceti as TauCeti.ringKrullDim_quotient_centralizerHopfIdeal_add_finrank_range_ad.

Sources
LeanTauCeti.ringKrullDim_quotient_centralizerHopfIdeal_add_finrank_range_ad
Uses 3
Statement usesTauCeti.centralizerHopfIdeal
Proof usesCartier's theorem · The Jacobian criterion for étaleness

DefinitionTauCeti.centralizerHopfIdeal#

The Hopf ideal of the centralizer of an element x of the Lie algebra, the stabilizer of x under the adjoint representation. Contravariantly, it cuts out the closed subgroup of Spec H fixing x under Ad.

TauCeti.centralizerHopfIdeal.{u} {k : Type u} [Field k] (H : Type u) [CommRing H] [HopfAlgebra k H]
  [Module.Finite k (TauCeti.Bialgebra.CotangentSpace k H)]
  (x : Module.Dual k (TauCeti.Bialgebra.CotangentSpace k H)) : TauCeti.HopfIdeal k H
Lean

Formalized in Tau Ceti as TauCeti.centralizerHopfIdeal.

Sources
LeanTauCeti.centralizerHopfIdeal
Used by 1
Used byThe dimension of a centralizer and of [𝔤, x]

DefinitionLieAlgebra.IsCentralizerRegular#

An element x of a Lie algebra is regular when its centralizer ker (ad x) has minimal dimension among the centralizers of all elements. The dimension is the cardinal Module.rank, so that an infinite-dimensional centralizer is never smaller than a finite-dimensional one. Over a field of characteristic zero this is the dimension of the group centralizer C_G(x) when the Lie algebra is that of an affine algebraic group G. This differs from Mathlib's LieAlgebra.IsRegular, which asks that the coefficient of index LieAlgebra.rank of the characteristic polynomial of ad x be nonzero, and from minimality of the dimension of the Engel subalgebra, the generalized 0-eigenspace of ad x.

LieAlgebra.IsCentralizerRegular.{u, u_1} (K : Type u_1) {L : Type u} [Field K] [LieRing L]
  [LieAlgebra K L] (x : L) : Prop
Lean

Formalized in Tau Ceti as LieAlgebra.IsCentralizerRegular.

Sources
LeanLieAlgebra.IsCentralizerRegular

DefinitionThe Slodowy slice e + ker (ad f), as an affine subspace of L#

When (h, e, f) is an sl₂ triple in a finite-dimensional Lie algebra over a field of characteristic zero, its direction ker (ad f) is complementary to [L, e] (IsSl2Triple.isCompl_range_ad_e_ker_ad_f). For f = 0, in particular in the degenerate case e = f = 0, it is all of L (TauCeti.slodowySlice_zero_right).

TauCeti.slodowySlice.{u_1, u_2} (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L]
  [LieAlgebra R L] (e f : L) : AffineSubspace R L
Lean

Formalized in Tau Ceti as TauCeti.slodowySlice.

Sources
LeanTauCeti.slodowySlice

DefinitionThe contracting action of Kˣ on L attached to an sl₂ triple (h, e, f)#

c acts by c ^ 2 • gradingAut c⁻¹, that is, by c ^ (2 - j) on the j-eigenspace of ad h (IsSl2Triple.contractingAction_apply_of_mem). For an algebraic group with Lie algebra L and a cocharacter λ with differential h this is c ↦ c ^ 2 • Ad (λ c⁻¹). It fixes e and preserves the Slodowy slice e + ker (ad f), on which it extends to c = 0 (IsSl2Triple.exists_contractingAction_eq).

IsSl2Triple.contractingAction.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K] [CharZero K]
  [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f : L} (t : IsSl2Triple h e f) :
  Kˣ →* Module.End K L
Lean

Formalized in Tau Ceti as IsSl2Triple.contractingAction.

Sources
LeanIsSl2Triple.contractingAction

TheoremMorozov's lemma#

Let ad e be nilpotent, ⁅h, e⁆ = 2 • e and h ∈ [e, L], over a field of characteristic zero. Then there is a unique f with ⁅e, f⁆ = h and ⁅h, f⁆ = -(2 • f). The case h = 0 is allowed.

TauCeti.existsUnique_lie_eq_and_lie_eq_neg_two_nsmul.{u_1, u_2} {K : Type u_1} {L : Type u_2}
  [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] {h e : L}
  (he : IsNilpotent ((LieAlgebra.ad K L) e)) (hhe : ⁅h, e⁆ = 2 • e)
  (hh : h ∈ LinearMap.range ((LieAlgebra.ad K L) e)) : ∃! f, ⁅e, f⁆ = h ∧ ⁅h, f⁆ = -(2 • f)
Lean

Formalized in Tau Ceti as TauCeti.existsUnique_lie_eq_and_lie_eq_neg_two_nsmul.

Other forms

Morozov's lemma for sl₂ triples. Formalized in Tau Ceti as TauCeti.existsUnique_isSl2Triple_of_isNilpotent_ad.

TauCeti.existsUnique_isSl2Triple_of_isNilpotent_ad.{u_1, u_2} {K : Type u_1} {L : Type u_2}
  [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] {h e : L}
  (he : IsNilpotent ((LieAlgebra.ad K L) e)) (hhe : ⁅h, e⁆ = 2 • e)
  (hh : h ∈ LinearMap.range ((LieAlgebra.ad K L) e)) (h0 : h ≠ 0) : ∃! f, IsSl2Triple h e f
Sources
LeanTauCeti.existsUnique_lie_eq_and_lie_eq_neg_two_nsmul · TauCeti.existsUnique_isSl2Triple_of_isNilpotent_ad
Used by 2
Used byKostant's conjugacy theorem · The Jacobson–Morozov theorem

TheoremThe rank-one Kostant straightening formula#

If H, E, and F satisfy the sl₂ commutator relations in an associative ℚ-algebra, then the product of a raising divided power and a lowering divided power is an integral sum in PBW order F, H, E.

The argument of the Cartan binomial is written as H - (m + n) + 2 * k; the natural numbers are coerced to the algebra, so this is the standard coefficient (H - m - n + 2k choose k).

TauCeti.Sl2.dividedPower_e_mul_dividedPower_f.{u} {A : Type u} [Ring A] [Algebra ℚ A] {H E F : A}
  (hef : E * F - F * E = H) (hhe : H * E - E * H = 2 • E) (hhf : H * F - F * H = -(2 • F))
  (m n : ℕ) :
  TauCeti.Associative.dividedPower m E * TauCeti.Associative.dividedPower n F =
    ∑ k ∈ Finset.range (min m n + 1),
      TauCeti.Associative.dividedPower (n - k) F * Ring.choose (H - ↑(m + n) + ↑(2 * k)) k *
        TauCeti.Associative.dividedPower (m - k) E
Lean

Formalized in Tau Ceti as TauCeti.Sl2.dividedPower_e_mul_dividedPower_f.

Sources
LeanTauCeti.Sl2.dividedPower_e_mul_dividedPower_f

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.