Representation theory

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.

DefinitionThe linear Harish-Chandra isomorphism Z(U(L)) ≃ₐ[K] S(H)^W#

the linear Harish-Chandra projection TauCeti.hcProjectionLinear b, with its values in the Weyl invariants.

TauCeti.harishChandraLinearIso.{v} {K : Type} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K]
  [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L]
  {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L]
  (b : (LieAlgebra.IsKilling.rootSystem H).Base) :
  ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L)) ≃ₐ[K] ↥(TauCeti.linearInvariants H)
Lean

Formalized in Tau Ceti as TauCeti.harishChandraLinearIso.

Sources
LeanTauCeti.harishChandraLinearIso
Uses 4
Proof usesChevalley's restriction theorem, image form · Harish-Chandra surjectivity with a degree bound · The linear-independence half of the Poincaré--Birkhoff--Witt theorem · The Poincaré--Birkhoff--Witt theorem

TheoremHarish-Chandra's theorem on central characters#

two weights lam and mu have the same central character, χ_lam = χ_mu, exactly when mu lies in the dot orbit of lam, that is mu = w · lam = w (lam + ρ) - ρ for an element w of the Weyl group.

TauCeti.vermaCentralCharacter_eq_iff.{v} {K : Type} {L : Type v} [Field K] [CharZero K]
  [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L]
  {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L]
  (b : (LieAlgebra.IsKilling.rootSystem H).Base) {lam mu : Module.Dual K ↥H} :
  TauCeti.vermaCentralCharacter b lam = TauCeti.vermaCentralCharacter b mu ↔
    ∃ w, TauCeti.dotAction (LieAlgebra.IsKilling.rootSystem H) b w lam = mu
Lean

Formalized in Tau Ceti as TauCeti.vermaCentralCharacter_eq_iff.

Sources
LeanTauCeti.vermaCentralCharacter_eq_iff
Uses 3
Proof usesHarish-Chandra surjectivity with a degree bound · The linear-independence half of the Poincaré--Birkhoff--Witt theorem · The Poincaré--Birkhoff--Witt theorem

DefinitionChevalley's restriction theorem#

Restriction of polynomial functions from L to H, TauCeti.lieCartanRestriction H, is an isomorphism from the invariants S(L)^L onto the Weyl invariants S(H)^W.

LieSubalgebra.lieChevalleyRestrictionIso.{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] [IsAlgClosed K] :
  ↥(TauCeti.SymmetricAlgebra.lieInvariants K L L) ≃ₐ[K] ↥(TauCeti.linearInvariants H)
Lean

Formalized in Tau Ceti as LieSubalgebra.lieChevalleyRestrictionIso.

Sources
LeanLieSubalgebra.lieChevalleyRestrictionIso
Uses 1
Proof usesChevalley's restriction theorem, image form

TheoremModuleCat.exists_isAlmostSplit_X₃_eq_iff#

Over a finite-dimensional algebra, a finitely generated module ends an almost-split sequence of A-modules exactly when it is indecomposable and non-projective.

ModuleCat.exists_isAlmostSplit_X₃_eq_iff.{u, v, w} (k : Type u) {A : Type v} [Field k] [Ring A]
  [Algebra k A] [FiniteDimensional k A] (M : ModuleCat A) [Module.Finite A ↑M] :
  (∃ S, S.X₃ = M ∧ S.IsAlmostSplit) ↔ CategoryTheory.Indecomposable M ∧ ¬CategoryTheory.Projective M
Lean

Formalized in Tau Ceti as ModuleCat.exists_isAlmostSplit_X₃_eq_iff.

Sources
LeanModuleCat.exists_isAlmostSplit_X₃_eq_iff
Uses 2
Proof usesThe Auslander–Reiten theorem, existence · Nakayama's lemma for a nilpotent ideal

DefinitionThe Peter-Weyl theorem, unconditionally#

The normalized matrix coefficients of the models chosen in the unitary equivalence classes are a Hilbert basis of L²(G), indexed by Σ i, Fin (IrrepClass.model i).dim × Fin (IrrepClass.model i).dim. No skeleton is assumed: isIrrepSkeleton_model supplies one.

TauCeti.coe_stdPeterWeylBasis identifies the elements of this basis with TauCeti.peterWeylFamily IrrepClass.model.

TauCeti.stdPeterWeylBasis.{u_1, u_2} (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [IsAlgClosed 𝕜]
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G]
  [BorelSpace G] :
  HilbertBasis ((i : TauCeti.IrrepClass 𝕜 G) × Fin i.model.dim × Fin i.model.dim) 𝕜
    ↥(MeasureTheory.Lp 𝕜 2 (TauCeti.haarProb G))
Lean

Formalized in Tau Ceti as TauCeti.stdPeterWeylBasis.

Sources
LeanTauCeti.stdPeterWeylBasis
Uses 2
Statement usesThe Peter-Weyl theorem
Proof usesSchur's lemma, scalar half

TheoremGabriel's theorem, Tits form version#

A finite connected quiver has finite representation type exactly when its Tits form is positive definite.

TauCeti.isFiniteRepType_iff_titsForm_posDef.{u, v, w} {Q : Type v} [Quiver Q] [Fintype Q]
  [(a b : Q) → Fintype (a ⟶ b)] {k : Type u} [Field k]
  (hconn : (TauCeti.Quiver.underlyingGraph Q).Connected) :
  TauCeti.IsFiniteRepType k Q ↔ (TauCeti.titsForm Q).PosDef
Lean

Formalized in Tau Ceti as TauCeti.isFiniteRepType_iff_titsForm_posDef.

Other forms

Gabriel's theorem. Formalized in Tau Ceti as TauCeti.isFiniteRepType_iff_card_hom_add_card_hom_le_one_and_exists_dynkinType_iso.

TauCeti.isFiniteRepType_iff_card_hom_add_card_hom_le_one_and_exists_dynkinType_iso.{u, v, w}
  {Q : Type v} [Quiver Q] [(a b : Q) → Fintype (a ⟶ b)] {k : Type u} [Field k] [Finite Q]
  (hconn : (TauCeti.Quiver.underlyingGraph Q).Connected) :
  TauCeti.IsFiniteRepType k Q ↔
    (∀ (a b : Q), Fintype.card (a ⟶ b) + Fintype.card (b ⟶ a) ≤ 1) ∧
      ∃ t,
        t.Valid ∧
          t.IsSimplyLaced ∧
            Nonempty (TauCeti.Quiver.underlyingGraph Q ≃g TauCeti.diagramGraph t.cartanMatrix)

Gabriel's theorem for path algebras. Formalized in Tau Ceti as TauCeti.isRepresentationFinite_pathAlgebra_iff_titsForm_posDef.

TauCeti.isRepresentationFinite_pathAlgebra_iff_titsForm_posDef.{u, v, w} (k : Type u) (Q : Type v)
  [Field k] [Quiver Q] [Finite (TauCeti.Quiver.TotalPath Q)] [Fintype Q]
  [(a b : Q) → Fintype (a ⟶ b)] (hconn : (TauCeti.Quiver.underlyingGraph Q).Connected) :
  TauCeti.IsRepresentationFinite (TauCeti.pathAlgebra k Q) ↔ (TauCeti.titsForm Q).PosDef
Sources
LeanTauCeti.isFiniteRepType_iff_titsForm_posDef · TauCeti.isFiniteRepType_iff_card_hom_add_card_hom_le_one_and_exists_dynkinType_iso · TauCeti.isRepresentationFinite_pathAlgebra_iff_titsForm_posDef

AbbreviationTauCeti.UniversalEnvelopingAlgebra.reesAlgebra#

The PBW Rees algebra: the coefficient of tⁿ belongs to PBW filtration degree n.

TauCeti.UniversalEnvelopingAlgebra.reesAlgebra.{u, v} (R : Type u) (L : Type v) [CommRing R]
  [LieRing L] [LieAlgebra R L] : Subalgebra R (Polynomial (UniversalEnvelopingAlgebra R L))
Lean

Formalized in Tau Ceti as TauCeti.UniversalEnvelopingAlgebra.reesAlgebra.

Sources
LeanTauCeti.UniversalEnvelopingAlgebra.reesAlgebra
Used by 2
Used byTauCeti.UniversalEnvelopingAlgebra.reesOneFiberEquiv · TauCeti.UniversalEnvelopingAlgebra.reesZeroFiberEquiv

DefinitionTauCeti.UniversalEnvelopingAlgebra.reesZeroFiberEquiv#

The PBW zero fibre is canonically the symmetric algebra, without a choice of basis.

TauCeti.UniversalEnvelopingAlgebra.reesZeroFiberEquiv.{u, v} (R : Type u) (L : Type v) [CommRing R]
  [LieRing L] [LieAlgebra R L] [Module.Free R L] :
  (↥(TauCeti.UniversalEnvelopingAlgebra.reesAlgebra R L) ⧸
      Ideal.span {TauCeti.UniversalEnvelopingAlgebra.reesParameter R L}) ≃ₐ[R]
    SymmetricAlgebra R L
Lean

Formalized in Tau Ceti as TauCeti.UniversalEnvelopingAlgebra.reesZeroFiberEquiv.

Sources
LeanTauCeti.UniversalEnvelopingAlgebra.reesZeroFiberEquiv
Uses 2
Statement usesThe Poincaré--Birkhoff--Witt theorem · TauCeti.UniversalEnvelopingAlgebra.reesAlgebra

DefinitionTauCeti.UniversalEnvelopingAlgebra.reesOneFiberEquiv#

Tensor base change of the PBW Rees algebra at one is the enveloping algebra. The polynomial parameter acts on the left tensor factor by evaluation at one.

TauCeti.UniversalEnvelopingAlgebra.reesOneFiberEquiv.{u, v} (R : Type u) (L : Type v) [CommRing R]
  [LieRing L] [LieAlgebra R L] :
  TensorProduct (Polynomial R) R ↥(TauCeti.UniversalEnvelopingAlgebra.reesAlgebra R L) ≃ₐ[R]
    UniversalEnvelopingAlgebra R L
Lean

Formalized in Tau Ceti as TauCeti.UniversalEnvelopingAlgebra.reesOneFiberEquiv.

Sources
LeanTauCeti.UniversalEnvelopingAlgebra.reesOneFiberEquiv
Uses 1
Statement usesTauCeti.UniversalEnvelopingAlgebra.reesAlgebra

DefinitionTauCeti.gelfandTsetlinGenerator#

The Gelfand-Tsetlin generator of degree r at level k ≤ n: the image in U(gl (Fin n)) of the Gelfand invariant Cᵣ of the upper-left corner gl (Fin k).

TauCeti.gelfandTsetlinGenerator.{u_1} (K : Type u_1) [CommRing K] {n k : ℕ} (hk : k ≤ n) (r : ℕ) :
  UniversalEnvelopingAlgebra K (Matrix (Fin n) (Fin n) K)
Lean

Formalized in Tau Ceti as TauCeti.gelfandTsetlinGenerator.

Sources
LeanTauCeti.gelfandTsetlinGenerator

TheoremThe Auslander–Reiten theorem, existence#

Over a finite-dimensional algebra, a finitely generated indecomposable non-projective module M ends an almost-split sequence 0 → τ M → E → M → 0 of A-modules whose left-hand end is the translate τ M and whose middle term is finitely generated.

ModuleCat.exists_isAlmostSplit_arTranslate.{u, v, w} (k : Type u) {A : Type v} [Field k] [Ring A]
  [Algebra k A] [FiniteDimensional k A] (M : ModuleCat A) [Module.Finite A ↑M]
  (hiM : CategoryTheory.Indecomposable M) (hpM : ¬CategoryTheory.Projective M) :
  ∃ E i p,
    ∃ (h : CategoryTheory.CategoryStruct.comp i p = 0),
      Module.Finite A ↑E ∧
        { X₁ := ModuleCat.arTranslate k M, X₂ := E, X₃ := M, f := i, g := p,
            zero := h }.IsAlmostSplit
Lean

Formalized in Tau Ceti as ModuleCat.exists_isAlmostSplit_arTranslate.

Other forms

The Auslander–Reiten theorem, existence on the left. Formalized in Tau Ceti as ModuleCat.exists_isAlmostSplit_of_not_injective.

ModuleCat.exists_isAlmostSplit_of_not_injective.{u, v, w} (k : Type u) {A : Type v} [Field k]
  [Ring A] [Algebra k A] [FiniteDimensional k A] (N : ModuleCat A) [Module.Finite A ↑N]
  (hiN : CategoryTheory.Indecomposable N) (hinj : ¬CategoryTheory.Injective N) :
  ∃ E M i p,
    ∃ (h : CategoryTheory.CategoryStruct.comp i p = 0),
      Module.Finite A ↑E ∧
        Module.Finite A ↑M ∧ { X₁ := N, X₂ := E, X₃ := M, f := i, g := p, zero := h }.IsAlmostSplit
Sources
LeanModuleCat.exists_isAlmostSplit_arTranslate · ModuleCat.exists_isAlmostSplit_of_not_injective
Uses 4 · Used by 1
Proof usesFitting's lemma, categorically · Jacobson's lemma · Nakayama's lemma for a nilpotent ideal · TauCeti.isLocalRing_end_of_indecomposable
Used byModuleCat.exists_isAlmostSplit_X₃_eq_iff

TheoremChevalley's restriction theorem, image form#

Restriction to H maps the invariants S(L)^L onto the Weyl invariants S(H)^W.

LieSubalgebra.map_lieInvariants_lieCartanRestriction.{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] [IsAlgClosed K] :
  Subalgebra.map (TauCeti.lieCartanRestriction H) (TauCeti.SymmetricAlgebra.lieInvariants K L L) =
    TauCeti.linearInvariants H
Lean

Formalized in Tau Ceti as LieSubalgebra.map_lieInvariants_lieCartanRestriction.

Other forms

Chevalley's restriction theorem, injectivity. Formalized in Tau Ceti as LieSubalgebra.lieCartanRestriction_injOn_lieInvariants.

LieSubalgebra.lieCartanRestriction_injOn_lieInvariants.{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] :
  Set.InjOn ⇑(TauCeti.lieCartanRestriction H) ↑(TauCeti.SymmetricAlgebra.lieInvariants K L L)
Sources
LeanLieSubalgebra.map_lieInvariants_lieCartanRestriction · LieSubalgebra.lieCartanRestriction_injOn_lieInvariants
Uses 2 · Used by 2
Proof usesRepresentation.symmetricAlgebraInvariants · Representation.symmetricAlgebraReynolds
Used byChevalley's restriction theorem · The linear Harish-Chandra isomorphism Z(U(L)) ≃ₐ[K] S(H)^W

TheoremHarish-Chandra surjectivity with a degree bound#

A Weyl invariant q ∈ S(H)^W of degree at most n is the linear Harish-Chandra projection of a central element of U(L) of PBW degree at most n.

TauCeti.exists_mem_pbwFiltration_hcProjectionLinear_eq.{v} {K : Type} {L : Type v} [Field K]
  [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L]
  [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra]
  (b : (LieAlgebra.IsKilling.rootSystem H).Base) {n : ℕ} {q : SymmetricAlgebra K ↥H}
  (hq : q ∈ TauCeti.linearInvariants H)
  (hqn : q ∈ TauCeti.Algebra.wordFiltration (SymmetricAlgebra.ι K ↥H) n) :
  ∃ z,
    ↑z ∈ TauCeti.UniversalEnvelopingAlgebra.pbwFiltration K L n ∧
      (TauCeti.hcProjectionLinear b) z = q
Lean

Formalized in Tau Ceti as TauCeti.exists_mem_pbwFiltration_hcProjectionLinear_eq.

Other forms

Harish-Chandra surjectivity with a degree bound, dot form. Formalized in Tau Ceti as TauCeti.exists_mem_pbwFiltration_hcProjection_eq.

TauCeti.exists_mem_pbwFiltration_hcProjection_eq.{v} {K : Type} {L : Type v} [Field K] [CharZero K]
  [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L]
  {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (b : (LieAlgebra.IsKilling.rootSystem H).Base)
  {n : ℕ} {q : SymmetricAlgebra K ↥H} (hq : q ∈ TauCeti.dotInvariants b)
  (hqn : q ∈ TauCeti.Algebra.wordFiltration (SymmetricAlgebra.ι K ↥H) n) :
  ∃ z, ↑z ∈ TauCeti.UniversalEnvelopingAlgebra.pbwFiltration K L n ∧ (TauCeti.hcProjection b) z = q
Sources
LeanTauCeti.exists_mem_pbwFiltration_hcProjectionLinear_eq · TauCeti.exists_mem_pbwFiltration_hcProjection_eq
Uses 4 · Used by 2
Proof usesThe linear-independence half of the Poincaré--Birkhoff--Witt theorem · The Poincaré--Birkhoff--Witt theorem · Representation.symmetricAlgebraInvariants · Representation.symmetricAlgebraReynolds
Used byHarish-Chandra's theorem on central characters · The linear Harish-Chandra isomorphism Z(U(L)) ≃ₐ[K] S(H)^W

DefinitionThe Peter-Weyl theorem#

For a skeleton of the unitary dual of a compact group, the normalized matrix coefficients √(dim V_i) · (models i)_{ab} are a Hilbert basis of L²(G), indexed by Σ i, Fin (models i).dim × Fin (models i).dim.

Algebraic closedness of the scalars is Schur's lemma, and enters through the orthonormality half.

TauCeti.peterWeylBasis.{u_1, u_2, u_3} {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜]
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsAlgClosed 𝕜] {models : ι → TauCeti.IrrepModel 𝕜 G}
  (h : TauCeti.IsIrrepSkeleton models) :
  HilbertBasis ((i : ι) × Fin (models i).dim × Fin (models i).dim) 𝕜
    ↥(MeasureTheory.Lp 𝕜 2 (TauCeti.haarProb G))
Lean

Formalized in Tau Ceti as TauCeti.peterWeylBasis.

Other forms

The Peter-Weyl density theorem. Formalized in Tau Ceti as TauCeti.dense_representativeSubmodule.

TauCeti.dense_representativeSubmodule.{u_1, u_2} (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] :
  Dense ↑(TauCeti.representativeSubmodule 𝕜 G)
Sources
LeanTauCeti.peterWeylBasis · TauCeti.dense_representativeSubmodule
Uses 2 · Used by 1
Proof usesSchur's lemma, scalar half · The spectral theorem for a symmetric convolution operator
Used byThe Peter-Weyl theorem, unconditionally

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.