Commit 2026-02-03 19:46 effc0dc0

View on Github →

feat(Algebra/Lie): basics of loop algebras (#33606) This PR introduces the Lie algebra of polynomial loops in a base Lie algebra, together with the 2-cocycle induced by a symmetric invariant bilinear form on the base Lie algebra.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/EvenFunction.lean

added theorem Function.Odd.finset_sum_eq_zero

modified theorem Function.Odd.sum_eq_zero

Modified Mathlib/Algebra/Lie/BaseChange.lean

Modified Mathlib/Algebra/Lie/Extension.lean

Created Mathlib/Algebra/Lie/Loop.lean

added def LieAlgebra.LoopAlgebra.residuePairing

added def LieAlgebra.LoopAlgebra.toFinsupp

added theorem LieAlgebra.LoopAlgebra.toFinsupp_single_tmul

added theorem LieAlgebra.LoopAlgebra.toFinsupp_symm_single

added def LieAlgebra.LoopAlgebra.twoCochainOfBilinear

added theorem LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply

added def LieAlgebra.LoopAlgebra.twoCocycleOfBilinear

added def LieAlgebra.loopAlgebraEquivLaurent

Modified Mathlib/Algebra/MonoidAlgebra/Module.lean

added def MonoidAlgebra.basis

added theorem MonoidAlgebra.basis_apply

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

added theorem Module.Basis.card_fintype

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

deleted theorem Module.card_fintype