Basis for span of iterated linear map

Stream: Is there code for X?

[Lucas Whitfield]

I have V a finite dimensional vector space over some field F, a vector v and an endomorphism f. I want to show that I can find a basis of Span($\{f^{[k]}(v) | k \in \mathbb{N}\}$) given by looking at the first k vectors: $(v, f(v), ..., f^{[k]}(v))$.

Are there any good tricks/results that exist to solve this?

import Mathlib.LinearAlgebra.FiniteDimensional

theorem exists_basis_iterate (F V : Type*) [Field F] [AddCommGroup V] [Module F V] [FiniteDimensional F V]
    (v : V) (f : V →ₗ[F] V) : ∃ (k : ℕ) (B : Basis (Fin k) F (Submodule.span F (Set.range (fun n ↦ f^[n] v)))),
    ∀ i : Fin k, B i = f^[i] v := sorry

[Junyan Xu]

I'm not aware of any shortcut and I'd just define k to be the smallest such that f^[k] v isn't in the span of f^[i] v with i < k, and then inductively show f^[i] v with i < k are linearly independent using docs#linearIndependent_fin_snoc and docs#Nat.le_induction, and separately inductively show f^[i] v with i >= k lie in their span (where docs#Submodule.span_image could be useful).

[Anatole Dedecker]

There’s also an abstract argument through F[X] modules right ? Do we have the necessary glue for this ?

[Jireh Loreaux]

I don't think we do, but it would probably be nice to have it because I bet it would make all these sorts of generalized eigenvector / Jordan canonical form / rational canonical form arguments smoother in the long run.

[Adam Topaz]

I thought we had the structure theorem for modules over PIDs?

[Adam Topaz]

And I would hope that mathlib knows about the basis of $K[X]/(f)$ in terms of monomials.

[Riccardo Brasca]

We have! It's in Mathlib.LinearAlgebra.FreeModule.PID.

[Riccardo Brasca]

It can probably be stated in several way and we may need some glue, but I think all the mathematics is there.

[Anatole Dedecker]

Ah, and the glue would be docs#Module.AEval' right?

[Johan Commelin]

It's maybe not exactly the result you are looking for, but often LinearMap.eventually_codisjoint_ker_pow_range_pow is quite useful.

[Jireh Loreaux]

Ah, I had no idea about Module.AEval'!

[Junyan Xu]

Following @Anatole Dedecker's idea:

import Mathlib.RingTheory.AdjoinRoot
import Mathlib.RingTheory.MvPolynomial.Basic

variable {F V : Type*} [Field F] [AddCommGroup V] [Module F V] [FiniteDimensional F V] (v : V) (f : V →ₗ[F] V)

open scoped Polynomial

noncomputable section

def toAEval' : F[X] →ₗ[F[X]] Module.AEval' f := LinearMap.toSpanSingleton F[X] _ (.of f v)

def gen : F[X] := Submodule.IsPrincipal.generator (LinearMap.ker (toAEval' v f))

def toAEval'' : F[X] →ₗ[F] V := (Module.AEval'.of f).symm ∘ₗ (toAEval' v f).restrictScalars F

lemma gen_ne_zero : gen v f ≠ 0 := fun h ↦
  Polynomial.not_finite <| FiniteDimensional.of_injective (toAEval'' v f) <| by
    apply_fun (Ideal.span {·}) at h
    rwa [gen, Ideal.span_singleton_generator,
      Ideal.span_singleton_eq_bot.mpr rfl, LinearMap.ker_eq_bot] at h

theorem toAEval''_monomial_one (n : ℕ) : toAEval'' v f (Polynomial.monomial n 1) = f^[n] v := by
  simp [toAEval'', toAEval', LinearMap.coe_pow]

theorem range_toAEVal' : LinearMap.range (toAEval'' v f) = Submodule.span F (Set.range (f^[·] v)) := by
  rw [LinearMap.range_eq_map, ← (Polynomial.basisMonomials F).span_eq, Submodule.map_span, ← Set.range_comp]
  simp_rw [Function.comp, Polynomial.coe_basisMonomials, toAEval''_monomial_one]

def genEquiv : AdjoinRoot (gen v f) ≃ₗ[F] Submodule.span F (Set.range (f^[·] v)) :=
  (Submodule.quotEquivOfEq _ _ <| Submodule.IsPrincipal.span_singleton_generator _).restrictScalars F
    ≪≫ₗ (toAEval'' v f).quotKerEquivRange ≪≫ₗ .ofEq _ _ (range_toAEVal' v f)

theorem exists_basis_iterate : ∃ (k : ℕ) (B : Basis (Fin k) F <| Submodule.span F <| Set.range (f^[·] v)),
    ∀ i : Fin k, B i = f^[i] v :=
  ⟨_, (AdjoinRoot.powerBasis <| gen_ne_zero v f).basis.map (genEquiv v f), fun i ↦ by
    rw [Basis.map_apply, PowerBasis.coe_basis]
    change toAEval'' v f (Polynomial.X ^ ↑i) = _
    rw [← Polynomial.monomial_one_right_eq_X_pow, toAEval''_monomial_one]⟩

[Anatole Dedecker]

Nice, I’ve learnt a dozen of "algebra in Lean" tricks by reading this :tada:

[Patrick Massot]

What is ≪≫ₗ??

[Anatole Dedecker]

Is it annoying to define the generator in terms of docs#Submodule.annihilator instead ? I think it would be more natural

[Anatole Dedecker]

Patrick Massot said:

What is ≪≫ₗ??

docs#LinearEquiv.trans

[Junyan Xu]

Anatole Dedecker said:

Is it annoying to define the generator in terms of docs#Submodule.annihilator instead ? I think it would be more natural

You'd need to obtain a F[X]-module structure on Submodule.span F (Set.range (f^[·] v)) (or rather its copy in Module.AEval' f) using docs#Module.AEval.mapSubmodule, which may or may not be simpler ...

[Anatole Dedecker]

Could you move only v to Module.AEval' f and take the F[X]-span there ?

[Junyan Xu]

Not sure what you mean, but we could restrict f : V →ₗ[F] V (i.e. f : Module.End F V) to f' : Module.End F (Submodule.span F (Set.range (f^[·] v))) using docs#LinearMap.domRestrict and docs#LinearMap.codRestrict, and then we can just take minpoly F f'. But another concern is that iterated f is not defeq to iterated f', and I don't know whether a relevant lemma exists ...

[Anatole Dedecker]

I mean define gen as a generator of the annihilator of Submodule.span F[X] (AEval'.of f v) (hope that makes sense, I’m on mobile…)

[Junyan Xu]

I think my definition of gen makes things easier because it's the generator of a kernel, so you can immediately apply the first isomorphism theorem and get an isomorphism between the quotient (defeq to AdjoinRoot) and the range (a submodule in Module.AEval' f). With your suggestion

  def gen : F[X] := Submodule.IsPrincipal.generator (Submodule.span F[X] {Module.AEval'.of f v}).annihilator

although the annihilator is also defined as a kernel

    Submodule.annihilator N = LinearMap.ker (LinearMap.lsmul R ↥N)

the image is a submodule in Module.End R N where N := span F[X] {Module.AEval'.of f v}, and it's not straightforward to connect this to a submodule of Module.AEval' f and then to V. I hope I'm not missing something!

[Anatole Dedecker]

I haven’t thought about it carefully, I was genuinely asking wether it got harder and I was half-expecting the answer to be yes ! I’ll have to think more about it tomorrow

[Anatole Dedecker]

Last idea if you want to try it : what about doing everything in an F[X] module for the multiplication by X map, and then only going back to f at the end, which should be easy since the statement is about F vector spaces with an endomorphism ?

[Junyan Xu]

If W is a f.d. F[X]-module and w : W, you should be able to prove

example : ∃ (k : ℕ) (B : Basis (Fin k) F <| Submodule.span F <| Set.range (X ^ · • w)),
    ∀ i : Fin k, B i = X ^ i • w :=

or maybe

example : ∃ (k : ℕ) (B : Basis (Fin k) F <| Submodule.span F[X] w),

the same way.
Then you can apply this to W := Module.AEval' f and use the F-LinearEquiv (or abuse defeq) between W and V and get the result in terms of f^[n]. This definitely seems a reasonable refactoring to do.

[Adam Topaz]

Anatole Dedecker said:

Patrick Massot said:

What is ≪≫ₗ??

docs#LinearEquiv.trans

This is motivated by the notation for docs#CategoryTheory.Iso.trans