Quantum groups: compact reconstruction and generic rank-one representations

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremComplete reducibility#

At a generic parameter, every finite-dimensional UqSl2 q-module is semisimple.

TauCeti.UqSl2.isSemisimpleModule_of_finiteDimensional.{u_1} {q : ℂ} {V : Type u_1} [AddCommGroup V]
  [_root_.Module ℂ V] [_root_.Module (TauCeti.UqSl2 q) V] [IsScalarTower ℂ (TauCeti.UqSl2 q) V]
  [FiniteDimensional ℂ V] (hq : TauCeti.IsGenericQuantumParameter q) :
  IsSemisimpleModule (TauCeti.UqSl2 q) V

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.isSemisimpleModule_of_finiteDimensional.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.isSemisimpleModule_of_finiteDimensional
• Source of TauCeti.UqSl2.isSemisimpleModule_of_finiteDimensional in TauCeti/QuantumGroups/UqSl2/CompleteReducibility.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.UqSl2.isSemisimpleModule_of_finiteDimensional

Uses 1 · Used by 3

Proof usesTauCeti.UqSl2.LadderModule

Used byTauCeti.UqSl2.isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule · The evaluation isomorphism · Type-1 locally finite modules

TheoremTauCeti.UqSl2.isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule#

At a generic parameter, a UqSl2 q-module is locally finite exactly when it is isomorphic to a direct sum of signed ladder modules L_m^ε.

TauCeti.UqSl2.isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule.{u} {q : ℂ}
  {V : Type u} [AddCommGroup V] [_root_.Module ℂ V] [_root_.Module (TauCeti.UqSl2 q) V]
  [IsScalarTower ℂ (TauCeti.UqSl2 q) V] [Fact (q ≠ 0)] (hq : TauCeti.IsGenericQuantumParameter q) :
  TauCeti.IsLocallyFiniteModule ℂ (TauCeti.UqSl2 q) V ↔
    ∃ ι m ε, Nonempty (V ≃ₗ[TauCeti.UqSl2 q] Π₀ (i : ι), TauCeti.UqSl2.LadderModule q (m i) (ε i))

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule
• Source of TauCeti.UqSl2.isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule in TauCeti/QuantumGroups/UqSl2/LocallyFinite.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.UqSl2.isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule

Uses 2

Statement usesTauCeti.UqSl2.LadderModule

Proof usesComplete reducibility

TheoremType-1 locally finite modules#

At a generic parameter, a module is of type 1 and locally finite exactly when it is isomorphic to a direct sum of positive signed ladder modules L_m^+.

TauCeti.UqSl2.isTypeOne_and_isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule.{u}
  {q : ℂ} [Fact (q ≠ 0)] {V : Type u} [AddCommGroup V] [_root_.Module ℂ V]
  [_root_.Module (TauCeti.UqSl2 q) V] [IsScalarTower ℂ (TauCeti.UqSl2 q) V]
  (hq : TauCeti.IsGenericQuantumParameter q) :
  TauCeti.UqSl2.IsTypeOne q V ∧ TauCeti.IsLocallyFiniteModule ℂ (TauCeti.UqSl2 q) V ↔
    ∃ ι m, Nonempty (V ≃ₗ[TauCeti.UqSl2 q] Π₀ (i : ι), TauCeti.UqSl2.LadderModule q (m i) 1)

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.isTypeOne_and_isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.isTypeOne_and_isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule
• Source of TauCeti.UqSl2.isTypeOne_and_isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule in TauCeti/QuantumGroups/UqSl2/TypeOne.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.UqSl2.isTypeOne_and_isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule

Uses 2

Statement usesTauCeti.UqSl2.LadderModule

Proof usesComplete reducibility

TheoremClassification of finite-dimensional simple U_q(sl₂)-modules#

At a generic parameter, every finite-dimensional simple UqSl2 q-module is isomorphic to L_m^ε for exactly one natural number m and sign ε.

TauCeti.UqSl2.existsUnique_linearEquiv_ladderModule.{u_1} {q : ℂ} {V : Type u_1} [AddCommGroup V]
  [_root_.Module ℂ V] [_root_.Module (TauCeti.UqSl2 q) V] [IsScalarTower ℂ (TauCeti.UqSl2 q) V]
  [Fact (q ≠ 0)] [FiniteDimensional ℂ V] [IsSimpleModule (TauCeti.UqSl2 q) V]
  (hq : TauCeti.IsGenericQuantumParameter q) :
  ∃! p, Nonempty (TauCeti.UqSl2.LadderModule q p.1 p.2 ≃ₗ[TauCeti.UqSl2 q] V)

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.existsUnique_linearEquiv_ladderModule.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.existsUnique_linearEquiv_ladderModule
• Source of TauCeti.UqSl2.existsUnique_linearEquiv_ladderModule in TauCeti/QuantumGroups/UqSl2/SimpleClassification.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.UqSl2.existsUnique_linearEquiv_ladderModule

Uses 1

Statement usesTauCeti.UqSl2.LadderModule

DefinitionTauCeti.UqSl2.polynomialAlgEquivCenter#

At a generic parameter, the center of U_q(sl₂) is a polynomial algebra in one variable: evaluation at the Casimir element is an isomorphism ℂ[X] ≃ₐ[ℂ] Z(U_q(sl₂)).

TauCeti.UqSl2.polynomialAlgEquivCenter {q : ℂ} (hq : TauCeti.IsGenericQuantumParameter q) :
  Polynomial ℂ ≃ₐ[ℂ] ↥(Subalgebra.center ℂ (TauCeti.UqSl2 q))

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.polynomialAlgEquivCenter.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.polynomialAlgEquivCenter
• Source of TauCeti.UqSl2.polynomialAlgEquivCenter in TauCeti/QuantumGroups/UqSl2/Center.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.UqSl2.polynomialAlgEquivCenter

Uses 2

Proof usesTauCeti.OreExtension · TauCeti.UqSl2.pbwBasis

DefinitionTauCeti.UqSl2.pbwBasis#

The Poincaré--Birkhoff--Witt basis of UqSl2 q, indexed by the exponents (a, b, c) of the ordered monomial F ^ a * K ^ b * E ^ c.

TauCeti.UqSl2.pbwBasis (q : ℂ) [Fact (q ≠ 0)] : Module.Basis (ℕ × ℤ × ℕ) ℂ (TauCeti.UqSl2 q)

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.pbwBasis.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.pbwBasis
• Source of TauCeti.UqSl2.pbwBasis in TauCeti/QuantumGroups/UqSl2/PBW.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.UqSl2.pbwBasis

Uses 1 · Used by 2

Statement usesTauCeti.OreExtension

Used byTauCeti.UqSl2.polynomialAlgEquivCenter · Triangular decomposition of U_q(sl₂)

DefinitionTriangular decomposition of U_q(sl₂)#

Multiplication p ⊗ r ⊗ s ↦ p(F) * r(K) * s(E) is a linear isomorphism ℂ[X] ⊗ ℂ[T, T⁻¹] ⊗ ℂ[X] ≃ UqSl2 q, that is, U⁻ ⊗ U⁰ ⊗ U⁺ ≃ U_q(sl₂). It sends the tensor product of monomial bases to the PBW basis.

TauCeti.UqSl2.triangularEquiv (q : ℂ) [Fact (q ≠ 0)] :
  TensorProduct ℂ (Polynomial ℂ) (TensorProduct ℂ (LaurentPolynomial ℂ) (Polynomial ℂ)) ≃ₗ[ℂ]
    TauCeti.UqSl2 q

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.triangularEquiv.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.triangularEquiv
• Source of TauCeti.UqSl2.triangularEquiv in TauCeti/QuantumGroups/UqSl2/Triangular.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.UqSl2.triangularEquiv

Uses 2

Proof usesTauCeti.OreExtension · TauCeti.UqSl2.pbwBasis

TheoremTauCeti.UqSl2.instIsDomain#

For a nonzero parameter, UqSl2 q is a domain: both twists of its Ore tower are injective, and an Ore extension of a domain by an injective twist is a domain. In particular the presentation is nontrivial.

TauCeti.UqSl2.instIsDomain (q : ℂ) [Fact (q ≠ 0)] : IsDomain (TauCeti.UqSl2 q)

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.instIsDomain.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.instIsDomain
• Source of TauCeti.UqSl2.instIsDomain in TauCeti/QuantumGroups/UqSl2/OreTower.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.UqSl2.instIsDomain

Uses 1

Proof usesTauCeti.OreExtension

StructureTauCeti.OreExtension#

The Ore extension R[X; σ, δ], represented by its finitely supported left coefficients.

TauCeti.OreExtension.{u, v} {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R]
  (σ : R →ₐ[k] R) (δ : TauCeti.SigmaDerivation σ) : Type v

Lean

Formalized in Tau Ceti as TauCeti.OreExtension.

Sources

• Tau Ceti documentation: TauCeti.OreExtension
• Source of TauCeti.OreExtension in TauCeti/Algebra/OreExtension/Basic.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.OreExtension

Used by 4

Used byTauCeti.UqSl2.instIsDomain · TauCeti.UqSl2.pbwBasis · TauCeti.UqSl2.polynomialAlgEquivCenter · Triangular decomposition of U_q(sl₂)

DefinitionTauCeti.UqSl2.LadderModule#

The underlying complex vector space ℂ^(m + 1) of the signed ladder module L_m^ε of UqSl2 q. Its UqSl2 q-module structure, defined for nonzero q, is LadderModule.instModule.

TauCeti.UqSl2.LadderModule (_q : ℂ) (m : ℕ) (_ε : ℤˣ) : Type

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.LadderModule.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.LadderModule
• Source of TauCeti.UqSl2.LadderModule in TauCeti/QuantumGroups/UqSl2/LadderModule/Basic.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.UqSl2.LadderModule

Used by 7

Used byThe Biedenharn–Elliott pentagon identity · Classification of finite-dimensional simple U_q(sl₂)-modules · Complete reducibility · TauCeti.UqSl2.isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule · The evaluation isomorphism · The simple quotient of M(ε q^m) · Type-1 locally finite modules

DefinitionThe simple quotient of M(ε q^m)#

At a generic parameter, the quotient of M(ε q^m) by the submodule generated by v_(m + 1) is isomorphic to the signed ladder module L_m^ε, by the module map sending v₀ to the class of v₀.

TauCeti.UqSl2.VermaModule.ladderModuleEquivQuotient {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)]
  (hq : TauCeti.IsGenericQuantumParameter q) :
  TauCeti.UqSl2.LadderModule q m ε ≃ₗ[TauCeti.UqSl2 q]
    TauCeti.UqSl2.VermaModule q (↑↑ε * q ^ m) ⧸
      TauCeti.UqSl2 q ∙ TauCeti.UqSl2.VermaModule.vec q (↑↑ε * q ^ m) (m + 1)

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.VermaModule.ladderModuleEquivQuotient.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.VermaModule.ladderModuleEquivQuotient
• Source of TauCeti.UqSl2.VermaModule.ladderModuleEquivQuotient in TauCeti/QuantumGroups/UqSl2/Verma/Submodule.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.UqSl2.VermaModule.ladderModuleEquivQuotient

Uses 1

Statement usesTauCeti.UqSl2.LadderModule

DefinitionThe evaluation isomorphism#

At a generic parameter, a locally finite UqSl2 q-module V is the direct sum over (m, ε) of L_m^ε ⊗ Hom_U(L_m^ε, V), by v ⊗ φ ↦ φ v. Here UqSl2 q acts on the left tensor factors, and the multiplicity spaces Hom_U(L_m^ε, V) may be infinite-dimensional.

TauCeti.UqSl2.ladderModuleTensorHomEquiv.{u} {q : ℂ} {V : Type u} [AddCommGroup V]
  [_root_.Module ℂ V] [_root_.Module (TauCeti.UqSl2 q) V] [IsScalarTower ℂ (TauCeti.UqSl2 q) V]
  [Fact (q ≠ 0)] (hq : TauCeti.IsGenericQuantumParameter q)
  [TauCeti.IsLocallyFiniteModule ℂ (TauCeti.UqSl2 q) V] :
  (Π₀ (p : ℕ × ℤˣ),
      TensorProduct ℂ (TauCeti.UqSl2.LadderModule q p.1 p.2)
        (TauCeti.UqSl2.LadderModule q p.1 p.2 →ₗ[TauCeti.UqSl2 q] V)) ≃ₗ[TauCeti.UqSl2 q]
    V

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.ladderModuleTensorHomEquiv.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.ladderModuleTensorHomEquiv
• Source of TauCeti.UqSl2.ladderModuleTensorHomEquiv in TauCeti/QuantumGroups/UqSl2/LocallyFinite.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.UqSl2.ladderModuleTensorHomEquiv

Uses 3

Statement usesThe isotypic decomposition of a semisimple module · TauCeti.UqSl2.LadderModule

Proof usesComplete reducibility

DefinitionThe isotypic decomposition of a semisimple module#

Let S j be pairwise non-isomorphic simple modules, finite-dimensional over the algebraically closed field k, such that every simple submodule of the semisimple module M is isomorphic to one of them. Then evaluation s ⊗ f ↦ f s is an isomorphism ⨁ⱼ S j ⊗[k] (S j →ₗ[A] M) ≃ M of A-modules.

TauCeti.directSumIsotypicTensorEquiv.{u_1, u_2, u_3, u_4, u_5} (k : Type u_1) {A : Type u_2}
  [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] {κ : Type u_3} [DecidableEq κ] (S : κ → Type u_4)
  [(j : κ) → AddCommGroup (S j)] [(j : κ) → _root_.Module k (S j)] [(j : κ) → _root_.Module A (S j)]
  [∀ (j : κ), IsScalarTower k A (S j)] [∀ (j : κ), IsSimpleModule A (S j)]
  [∀ (j : κ), FiniteDimensional k (S j)] {M : Type u_5} [AddCommGroup M] [_root_.Module k M]
  [_root_.Module A M] [IsScalarTower k A M] [IsSemisimpleModule A M]
  (hS : ∀ (i j : κ), Nonempty (S i ≃ₗ[A] S j) → i = j)
  (hcover : ∀ (m : Submodule A M), IsSimpleModule A ↥m → ∃ j, Nonempty (S j ≃ₗ[A] ↥m)) :
  (Π₀ (j : κ), TensorProduct k (S j) (S j →ₗ[A] M)) ≃ₗ[A] M

Lean

Formalized in Tau Ceti as TauCeti.directSumIsotypicTensorEquiv.

Sources

• Tau Ceti documentation: TauCeti.directSumIsotypicTensorEquiv
• Source of TauCeti.directSumIsotypicTensorEquiv in TauCeti/RingTheory/Semisimple/IsotypicTensor.lean
• Tau Ceti roadmap status: Quantum groups: compact reconstruction and generic rank-one representations

LeanTauCeti.directSumIsotypicTensorEquiv

Uses 1 · Used by 1

Proof usesThe multiplicity theorem

Used byThe evaluation isomorphism

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.