Zulip Chat Archive

Stream: Is there code for X?

Topic: Filtered algebras

Joseph Chaumont (Dec 02 2023 at 07:23):

I know we have RingTheory.GradedAlgebra for grading the ring structure of algebras, but I can't find an equivalent for filtered algebras. For context, I'm working towards the Poincare-Birkhoff-Witt theorem.

Eric Wieser (Dec 02 2023 at 08:37):

I think lean-liquid might have this (in lean 3), but mathlib certainly doesn't

Eric Wieser (Dec 02 2023 at 08:39):

I also wrote a version of this myself at https://github.com/pygae/lean-ga/blob/0947a6d21cf5a724732c29dabbc7f543edb66d4e/src/for_mathlib/algebra/filtration.lean#L12-L17, but I think bundling the submodules may have been a mistake

Eric Wieser (Dec 02 2023 at 08:40):

(this predates GradedAlgebra, so does not have a particularly compatible design)

Last updated: Dec 20 2023 at 11:08 UTC