((max)?gen)?{eigen,weight}space

Stream: maths

[Johan Commelin]

With eigenspaces, there are various different notions:

• docs#eigenspace: the kernel of f - algebraMap R (End R M) μ
• docs#genEigenspace: for k : ℕ the kernel of (f - algebraMap R (End R M) μ) ^ k (Nb: this decl is implemented as order hom from nats to submodules)
• docs#maxGenEigenspace: which is ⨆ k, f.genEigenspace μ k

And then in Lie theory, there can be similar versions for weight spaces. At the moment we only have the 3rd variant. I recently renamed weightSpace to docs#genWeightSpace. But it should have been maxGenWeightSpace. :see_no_evil:

I am wondering whether we can unify the 3 notions. Certainly eigenspace could be a thin wrapper around genEigenspace 1. But we could also try to unify with maxGenEigenspace. One way to do that is to take a filter as argument, so that genEigenspace k could be filterEigenspace (principal k) and maxGenEigenspace would be filterEigenspace atTop.
(Note that this would drop the order hom from the type, but of course it is still maths-true.)

The benefit of this unification would be that it is a lot easier to also have a unified approach to the three versions for weight spaces, instead of developing 3 separate APIs.

Question: what is the best design here?

The only relevant filters are principal k and atTop. Exactly because of the monotonicity of genEigenspace. So it seems like filters are not exactly the right tool for the job. An alternative would be to take an ENat as argument... but it doesn't feel exactly natural to me to do that, even though I don't know why... :thinking: :oops:

[Johan Commelin]

Here is a concrete definition using ENat:

def unifEigenspace (f : End R M) (μ : R) (k : ENat) : Submodule R M where
  carrier := {m | ∃ l : ℕ, l ≤ k ∧ m ∈ LinearMap.ker ((f - algebraMap R (End R M) μ) ^ l)}
  add_mem' :=  by
    rintro a b ⟨l, hl, ha⟩ ⟨m, hm, hb⟩
    use max l m
    refine ⟨?_, ?_⟩
    · rintro k rfl
      use max l m, rfl
      simp_all
    · apply Submodule.add_mem
      · exact ker_le_ker_of_le _ _ _ (le_max_left _ _) ha
      · exact ker_le_ker_of_le _ _ _ (le_max_right _ _) hb
  zero_mem' := ⟨0, zero_le _, zero_mem _⟩
  smul_mem' := by
    rintro c x ⟨l, hl, hx⟩
    use l, hl
    apply Submodule.smul_mem _ _ hx

[Ruben Van de Velde]

More like extendedly natural (sorry)

[Scott Carnahan]

An ENat argument seems like an excellent choice to me informally, but I have zero experience with eigenspaces in mathlib.

[Oliver Nash]

I like the ENat idea.

[Johan Commelin]

Ok, will try to build an mvp

[Johan Commelin]

#16025 sets up a bunch of basic api, and rewrites the existing api (only for Basic.lean) in terms of the new one.

[Johan Commelin]

existing definitions became abbrevs, but otherwise no existing decls should've been changed

[Johan Commelin]

#16738 prepares the library for the refactor by relying less on defeqs

[Antoine Chambert-Loir]

I wonder whether the ultimate generalization isn't working with some completion of the multiplicative monoid $K[T]$ (let's pretend we work over a field $K$), obtained by adding a possible infinite element at each irreducible polynomial.
In fact, this would work for any principal ideal ring $R$, and corresponds more or less to the classification of submodules of $K/R$, where $$K$ is the fraction field of $R$.

[Johan Commelin]

Hmmz, not sure what an API for that would look like...

[Johan Commelin]

refactor(LinearAlgebra/Eigenspace): unified definition of (max(gen)?)?Eigenspace #16025

now compiles. I would be happy to get some feedback on whether this is desirable, and how to get this into mathlib as smoothly as possible.

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/compare/jmc-eigenspace-filter...jmc-eigenspace-post shows further changes that can be made after the initial refactor.

[Antoine Chambert-Loir]

Johan Commelin said:

Hmmz, not sure what an API for that would look like...

It's not clear how to write an API, but this is just duality. If $D(M)=\operatorname{Hom}(M,K/R)$ (I assume $R$ is principal), there is a duality map $M \times D(M) \to K/R$, hence a map $M \to \operatorname{Hom}(D(M),K/R)$ and for a submodule $P$ of $K/R$, the corresponding submodule $M[P]$ of $M$ is nothing but the kernel of the composition to $\operatorname{Hom}(D(M), K/R/P)$.

[Bhavik Mehta]

I don't know this part of the library well, but I need to use it sometimes and the unification of the eigenspaces looks super useful. Is the plan to eventually remove maxGenEigenspace and only talk about unifEigenspace ⊤? Otherwise I worry slightly that we go from having three different notions to four different notions...

[Johan Commelin]

Yes. We might still have eigenspace for convenience. At least I want to remove genEigenspace and later rename unifEigenspace to genEigenspace.
But I would prefer to do all of that in a follow-up PR.

[Johan Commelin]

Btw, CI is now happy with the PR. So all feedback is welcome.

[Bhavik Mehta]

Okay perfect, I'm fully on board with this generalisation if that's the plan, and fully on board with making those changes in a later PR.