Associated graded objects (modules/rings)

Stream: new members

[Coleton Kotch]

Do we have anything on associated graded objects in the library already? In particular I am looking to construct the associated graded algebra of a universal enveloping algebra.

If not then I suppose that the correct way of formalizing the associated graded algebra would be to consider the context of an algebra with a filtration indexed by a well-ordered monoid?

[Kevin Buzzard]

You might only need a SuccOrder, but do you know any examples coming up in the wild where the index set isn't the naturals?

[Coleton Kotch]

SuccOrder should indeed work better, though I do not know of any examples where we don't use the naturals. Do you think it would be better to just formalize for the case of the naturals then?

[Kevin Buzzard]

I can imagine that the construction is also useful for the integers but in my area I don't think we go much beyond that...

[Ravi Vakil]

Non-lean-expert speaking (so don't take my opinion too seriously), but it seems to me that doing the naturals would be very helpful, and then useful in the near-term in other settings (such as in algebraic geometry).

[Coleton Kotch]

Interestingly I've found the case of the integers to be more natural to implement given that if we have a filtration $A_n$ and define the nth graded object $G_n = A_n / A_{n - 1}$, we don't have to worry about specially treating the $n = 0$ case.

So far I've been working in the context of a OrderedCommutativeMonoid, which is also a PredOrder, allowing us to reference "$i - 1$", and using an auxiliary function to deal with the "zero case".

import Mathlib.Algebra.Algebra.Basic
import Mathlib.Order.SuccPred.Basic
import Mathlib.LinearAlgebra.Quotient
import Mathlib.Algebra.DirectSum.Basic
import Mathlib.Algebra.Algebra.Operations

universe u v w

open scoped DirectSum


variable {R : Type u} {A : Type v} {ι : Type w}
[CommRing R] [Ring A] [Algebra R A] [OrderedAddCommMonoid ι] [PredOrder ι] [DecidableEq ι]


class FilteredAlgebra (𝓐 : ι → Submodule R A) where
  whole : iSup 𝓐 = ⊤
  mono : Monotone 𝓐
  mul_compat : ∀ i j, 𝓐 i * 𝓐 j ≤ 𝓐 (i + j)
  one : 1 ∈ 𝓐 0

namespace FilteredAlgebra

def aux (𝓐 : ι → Submodule R A) (i : ι) [FilteredAlgebra 𝓐] : Submodule R A :=
  match decEq i (Order.pred i) with
  | isTrue _ => ⊥
  | isFalse _ => 𝓐 (Order.pred i)

def gradedObject (𝓐 : ι → Submodule R A) (i : ι) [FilteredAlgebra 𝓐] :=
  Submodule.map (aux 𝓐 i).mkQ <| 𝓐 i

[Johan Commelin]

I guess that with filtered objects we might want to support both increasing and decreasing filtrations. Just like we support both chain complexes and cochain complexes. The abstraction is given using a docs#ComplexShape which basically abstracts away the "direction" of the arrows.

The issues with n - 1 also came up in the theory of complexes, as well as how to work with homology of indexed objects. Of course for graded objects the quotient is a trivial example of homology, so it is maybe not necessary to use the homology API. But it could still be good to consider the interactions.

[Joël Riou]

A filtered object is essentially a functor F from a preorder to an abelian category (in such a way that all maps are sent to monomorphisms). In this context, we may define (F.obj j)/(F.obj i) as the cokernel of F.map _ : F.obj i ⟶ F.obj j whenever i ≤ j.

This gets more complicated when we want to consider such quotients only when i and j are consecutive in some way. In my formalization of spectral sequences (not in mathlib yet), I expressed the convergence by using a filtration on an object X defined as a functor WithBot α ⥤ MonoOver X with some additional structure on α, essentially a map pred : WithBot α → α.
https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/Algebra/Homology/SpectralSequence/Convergence.lean#L330-L346

[Coleton Kotch]

I had considered the approach as a colimit of a functor sending maps to monomorphisms, but it is worth noting that case of a filtered algebra is not as nicely encapsulated as such as we are taking a colimit of modules with a special structure such that we get an algebra.

It still may be worth defining filtration's and filtered objects in a general setting, and then building off the case of modules for filtered algebras. The ComplexShape structure should work nicely for this.

Edit: Upon thinking a bit more, it seems that the ComplexShape structure will not be as nice as I at first thought as we would want to consider say the embedding $M_0 \xhookrightarrow{} M_2$. It seems as though using a preorder with some successor or predecessor for the descending/ascending cases would work better.

[Adam Topaz]

Here is another approach (which does come up in valuation theory, for example): take the n-th term of the associated graded to be the quotient of M_n by M_m for all m < n. In other words, this is the universal object such that maps out of it correspond to maps out of M_n which kill M_m for all m < n. This way there is no need for predecessors or successors. It also a reasonable definition for filtrations whose indexing type is not discrete (although in such cases this can give a trivial answer in many natural examples).

[Adam Topaz]

It should be easy to write this down if you consider your filtration as a functor as suggested above

[Coleton Kotch]

@Adam Topaz This approach seems elegant, though it seems it places more requirements on the category than other approaches.

One thing I did notice, though I am not sure if it is something worth worrying about, is that CategoryTheory.Limits.cokernel is noncomputable and thus this more general definition of graded objects is noncomputable. A less general approach, say only defining for modules (or filtered algebras) is computable however. I am not sure how big a deal this is or if it warrants giving both specific and general constructions.

On the case of filtered algebras it seems we could generalize them as something along the lines of a filtration on a monoidal category C with indexing category a partially ordered monoid $M$ in the form of a monoidal category, having product given $M \times M \rightarrow M$. Then, writing $\alpha : M \rightarrow C$ the base filtration, we would have two functors $M \times M \rightarrow C$ given by $\otimes \circ (\alpha \times \alpha)$ and $\alpha \circ m$ and a natural transformation from the former to the later would give us our product.