Affine Lie algebras, smooth modules and completed centers

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

DefinitionInvariant forms classify the continuous second cohomology of formal loops #

For a finite-dimensional Lie algebra with nondegenerate Killing form over a field of characteristic zero, for instance a semisimple Lie algebra, Φ ↦ [c_Φ] is a linear equivalence from the invariant symmetric forms on L onto the continuous second cohomology of formal currents with trivial coefficients.

TauCeti.CurrentAlgebra.invariantFormsResidueClassEquiv.{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] :
  ↥(TauCeti.LieModule.invariantForms K L L) ≃ₗ[K]
    TauCeti.LieModule.Cohomology.continuousSecondCohomology K (TauCeti.currentAlgebra K L)
      (TrivialLieModule K (TauCeti.currentAlgebra K L) K)

Lean

Formalized in Tau Ceti as TauCeti.CurrentAlgebra.invariantFormsResidueClassEquiv.

Sources

LeanTauCeti.CurrentAlgebra.invariantFormsResidueClassEquiv

Uses 2

Statement usesTauCeti.LieModule.Cohomology.continuousSecondCohomology

Proof usesWhitehead's first lemma

TheoremThe continuous second cohomology of the formal loop algebra of a simple Lie algebra is one-dimensional #

Here L is a finite-dimensional Lie algebra over an algebraically closed field of characteristic zero whose adjoint module is irreducible and whose Killing form is nondegenerate, for instance a simple Lie algebra; the residue class of the Killing form spans.

TauCeti.CurrentAlgebra.finrank_continuousSecondCohomology_eq_one.{u_4, u_5} (K : Type u_4)
  (L : Type u_5) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L]
  [LieAlgebra.IsKilling K L] [IsAlgClosed K] [LieModule.IsIrreducible K L L] :
  Module.finrank K
      (TauCeti.LieModule.Cohomology.continuousSecondCohomology K (TauCeti.currentAlgebra K L)
        (TrivialLieModule K (TauCeti.currentAlgebra K L) K)) =
    1

Lean

Formalized in Tau Ceti as TauCeti.CurrentAlgebra.finrank_continuousSecondCohomology_eq_one.

Sources

LeanTauCeti.CurrentAlgebra.finrank_continuousSecondCohomology_eq_one

Uses 3

Statement usesTauCeti.LieModule.Cohomology.continuousSecondCohomology

Proof usesTauCeti.LieAlgebra.exists_eq_smul_killingForm · Whitehead's first lemma

TheoremThe second cohomology of the loop algebra of a simple Lie algebra is spanned by the residue class of the Killing form #

Here L is a finite-dimensional Lie algebra over an algebraically closed field of characteristic zero whose adjoint module is irreducible and whose Killing form is nondegenerate, for instance a simple Lie algebra. Together with smul_twoCochainOfBilinear_mem_range_d₁₂_iff, this says that the second cohomology of loopAlgebra K ℤ L with trivial coefficients is one-dimensional.

TauCeti.LieAlgebra.LoopAlgebra.twoCocycle_eq_span_killingForm_sup_range_d₁₂.{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] [IsAlgClosed K]
  [LieModule.IsIrreducible K L L] :
  LieModule.Cohomology.twoCocycle K (LieAlgebra.loopAlgebra K ℤ L)
      (TrivialLieModule K (LieAlgebra.loopAlgebra K ℤ L) K) =
    K ∙ LieAlgebra.LoopAlgebra.twoCochainOfBilinear K ℤ L (killingForm K L) ⋯ ⊔
      (LieModule.Cohomology.d₁₂ K (LieAlgebra.loopAlgebra K ℤ L)
          (TrivialLieModule K (LieAlgebra.loopAlgebra K ℤ L) K)).range

Lean

Formalized in Tau Ceti as TauCeti.LieAlgebra.LoopAlgebra.twoCocycle_eq_span_killingForm_sup_range_d₁₂.

Sources

LeanTauCeti.LieAlgebra.LoopAlgebra.twoCocycle_eq_span_killingForm_sup_range_d₁₂

Uses 2

Proof usesTauCeti.LieAlgebra.exists_eq_smul_killingForm · Whitehead's first lemma

TheoremWhitehead's second lemma, as an equality of submodules #

the 2-cocycles of a Lie algebra with nondegenerate Killing form in characteristic zero, with values in a finite-dimensional module, are exactly the coboundaries.

LieModule.Cohomology.twoCocycle_eq_range_d₁₂.{u, v, w} {K : Type u} {L : Type v} {M : Type w}
  [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [AddCommGroup M]
  [_root_.Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] :
  LieModule.Cohomology.twoCocycle K L M = (LieModule.Cohomology.d₁₂ K L M).range

Lean

Formalized in Tau Ceti as LieModule.Cohomology.twoCocycle_eq_range_d₁₂.

Other forms

Whitehead's second lemma. Formalized in Tau Ceti as LieModule.Cohomology.exists_d₁₂_eq.

LieModule.Cohomology.exists_d₁₂_eq.{u, v, w} {K : Type u} {L : Type v} {M : Type w} [Field K]
  [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [AddCommGroup M]
  [_root_.Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M]
  (c : ↥(LieModule.Cohomology.twoCocycle K L M)) : ∃ f, (LieModule.Cohomology.d₁₂ K L M) f = ↑c

Sources

LeanLieModule.Cohomology.twoCocycle_eq_range_d₁₂ · LieModule.Cohomology.exists_d₁₂_eq

Uses 2

Proof usesThe first isomorphism theorem for a surjective homomorphism of Lie algebras · Weyl's theorem as a decomposition

TheoremWhitehead's first lemma #

Over a field of characteristic zero, every Lie derivation from a Lie algebra with nondegenerate Killing form (necessarily finite-dimensional) into a finite-dimensional module is inner: it is x ↦ ⁅x, m⁆ for some m.

LieDerivation.IsKilling.exists_eq_inner.{u, v, w} {K : Type u} {L : Type v} {M : Type w} [Field K]
  [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [AddCommGroup M]
  [_root_.Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M]
  (D : LieDerivation K L M) : ∃ m, (LieDerivation.inner K L M) m = D

Lean

Formalized in Tau Ceti as LieDerivation.IsKilling.exists_eq_inner.

Other forms

Whitehead's first lemma for cochains. Formalized in Tau Ceti as LieModule.Cohomology.exists_eq_lie_of_d₁₂_eq_zero.

LieModule.Cohomology.exists_eq_lie_of_d₁₂_eq_zero.{u, v, w} {K : Type u} {L : Type v} {M : Type w}
  [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [AddCommGroup M]
  [_root_.Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M]
  {f : LieModule.Cohomology.oneCochain K L M} (hf : (LieModule.Cohomology.d₁₂ K L M) f = 0) :
  ∃ m, ∀ (x : L), f x = ⁅x, m⁆

Sources

LeanLieDerivation.IsKilling.exists_eq_inner · LieModule.Cohomology.exists_eq_lie_of_d₁₂_eq_zero

Used by 3

Used byInvariant forms classify the continuous second cohomology of formal loops · The continuous second cohomology of the formal loop algebra of a simple Lie algebra is one-dimensional · The second cohomology of the loop algebra of a simple Lie algebra is spanned by the residue class of the Killing form

TheoremTauCeti.CurrentAlgebra.derivedSeries_ofTwoCocycle_eq_top_iff #

The residue central extension of a perfect Lie algebra over a field is perfect if and only if its form is nonzero. No finite-dimensionality or characteristic assumption is needed.

TauCeti.CurrentAlgebra.derivedSeries_ofTwoCocycle_eq_top_iff.{u_2, u_3} (L : Type u_2) [LieRing L]
  {K : Type u_3} [Field K] [LieAlgebra K L] (Ψ : LinearMap.BilinForm K L)
  (hΨ : LinearMap.BilinForm.lieInvariant L Ψ) (hΨs : Ψ.IsSymm)
  (hperfect : LieAlgebra.derivedSeries K L 1 = ⊤) :
  LieAlgebra.derivedSeries K
        (LieAlgebra.ofTwoCocycle (TauCeti.CurrentAlgebra.twoCocycleOfBilinear K L Ψ hΨ hΨs)) 1 =
      ⊤ ↔
    Ψ ≠ 0

Lean

Formalized in Tau Ceti as TauCeti.CurrentAlgebra.derivedSeries_ofTwoCocycle_eq_top_iff.

Sources

LeanTauCeti.CurrentAlgebra.derivedSeries_ofTwoCocycle_eq_top_iff

TheoremTauCeti.LieAlgebra.exists_eq_smul_killingForm #

Every invariant bilinear form on a Lie algebra is a multiple of the Killing form, for a finite-dimensional Lie algebra over an algebraically closed field whose adjoint module is irreducible and whose Killing form is nondegenerate, such as a simple Lie algebra in characteristic zero.

TauCeti.LieAlgebra.exists_eq_smul_killingForm.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K]
  [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L]
  [LieModule.IsIrreducible K L L] [LieAlgebra.IsKilling K L] {Φ : LinearMap.BilinForm K L}
  (hΦ : LinearMap.BilinForm.lieInvariant L Φ) : ∃ c, Φ = c • killingForm K L

Lean

Formalized in Tau Ceti as TauCeti.LieAlgebra.exists_eq_smul_killingForm.

Sources

LeanTauCeti.LieAlgebra.exists_eq_smul_killingForm

Uses 1 · Used by 2

Proof usesSchur's lemma for Lie modules

Used byThe continuous second cohomology of the formal loop algebra of a simple Lie algebra is one-dimensional · The second cohomology of the loop algebra of a simple Lie algebra is spanned by the residue class of the Killing form

TheoremTauCeti.CurrentAlgebra.instCompleteSpace #

The order topology is complete over a finite free coefficient module.

TauCeti.CurrentAlgebra.instCompleteSpace.{u_1, u_2} (R : Type u_1) (L : Type u_2) [CommRing R]
  [AddCommGroup L] [_root_.Module R L] [Module.Free R L] [Module.Finite R L] :
  CompleteSpace (TauCeti.currentAlgebra R L)

Lean

Formalized in Tau Ceti as TauCeti.CurrentAlgebra.instCompleteSpace.

Sources

LeanTauCeti.CurrentAlgebra.instCompleteSpace

AbbreviationTauCeti.LieModule.Cohomology.continuousSecondCohomology #

Continuous second Lie algebra cohomology with discrete coefficients: continuous two-cocycles modulo the continuous coboundaries of continuous one-cochains.

TauCeti.LieModule.Cohomology.continuousSecondCohomology.{u_1, u_2, u_3} (R : Type u_1)
  (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [TopologicalSpace L]
  [AddCommGroup M] [_root_.Module R M] [LieRingModule L M] [LieModule R L M] : Type (max u_2 u_3)

Lean

Formalized in Tau Ceti as TauCeti.LieModule.Cohomology.continuousSecondCohomology.

Sources

LeanTauCeti.LieModule.Cohomology.continuousSecondCohomology

Used by 2

Used byInvariant forms classify the continuous second cohomology of formal loops · The continuous second cohomology of the formal loop algebra of a simple Lie algebra is one-dimensional

DefinitionTauCeti.coinduction #

The coinduction of R-modules to smooth A-modules along f : R →+* A: the smooth part of the coextension of scalars Hom_R(A, V), which is the module of continuous R-linear maps A → V when the J i form a basis of neighborhoods of 0 (TauCeti.mem_smoothPart_coextendScalars_iff_continuous).

TauCeti.coinduction.{w, u₁, u, u_1} {R : Type u₁} {A : Type u} [Ring R] [Ring A] (f : R →+* A)
  {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun x1 x2 => x1 ≥ x2) J) :
  CategoryTheory.Functor (ModuleCat R) (TauCeti.smoothModules J).FullSubcategory

Lean

Formalized in Tau Ceti as TauCeti.coinduction.

Sources

LeanTauCeti.coinduction

Used by 1

Used byTauCeti.enoughInjectives_smoothModules

TheoremTauCeti.enoughInjectives_smoothModules #

For a directed family J of left ideals of A : Type u, the smooth A-modules in universe max u w have enough injectives: every smooth module embeds, through the unit of the coinduction adjunction along ℤ →+* A, into the coinduction of an injective abelian group.

TauCeti.enoughInjectives_smoothModules.{w, u, u_1} {A : Type u} [Ring A] {ι : Type u_1}
  {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun x1 x2 => x1 ≥ x2) J) :
  CategoryTheory.EnoughInjectives (TauCeti.smoothModules J).FullSubcategory

Lean

Formalized in Tau Ceti as TauCeti.enoughInjectives_smoothModules.

Sources

LeanTauCeti.enoughInjectives_smoothModules

Uses 1

Proof usesTauCeti.coinduction

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Affine Lie algebras, smooth modules and completed centers

DefinitionInvariant forms classify the continuous second cohomology of formal loops#

Lean

Sources

TheoremThe continuous second cohomology of the formal loop algebra of a simple Lie algebra is one-dimensional#

Lean

Sources

TheoremThe second cohomology of the loop algebra of a simple Lie algebra is spanned by the residue class of the Killing form#

Lean

Sources

TheoremWhitehead's second lemma, as an equality of submodules#

Lean

Other forms

Sources

TheoremWhitehead's first lemma#

Lean

Other forms

Sources

TheoremTauCeti.CurrentAlgebra.derivedSeries_ofTwoCocycle_eq_top_iff#

Lean

Sources

TheoremTauCeti.LieAlgebra.exists_eq_smul_killingForm#

Lean

Sources

TheoremTauCeti.CurrentAlgebra.instCompleteSpace#

Lean

Sources

AbbreviationTauCeti.LieModule.Cohomology.continuousSecondCohomology#

Lean

Sources

DefinitionTauCeti.coinduction#

Lean

Sources

TheoremTauCeti.enoughInjectives_smoothModules#

Lean

Sources

DefinitionInvariant forms classify the continuous second cohomology of formal loops #

TheoremThe continuous second cohomology of the formal loop algebra of a simple Lie algebra is one-dimensional #

TheoremThe second cohomology of the loop algebra of a simple Lie algebra is spanned by the residue class of the Killing form #

TheoremWhitehead's second lemma, as an equality of submodules #

TheoremWhitehead's first lemma #

TheoremTauCeti.CurrentAlgebra.derivedSeries_ofTwoCocycle_eq_top_iff #

TheoremTauCeti.LieAlgebra.exists_eq_smul_killingForm #

TheoremTauCeti.CurrentAlgebra.instCompleteSpace #

AbbreviationTauCeti.LieModule.Cohomology.continuousSecondCohomology #

DefinitionTauCeti.coinduction #

TheoremTauCeti.enoughInjectives_smoothModules #