How to express a linear map has finite rank?

Stream: mathlib4

[Niels Voss]

What is the best way to express that a LinearMap (or in my case, a ContinuousLinearMap) has finite rank? Options include:

• Module.rank R ↥(LinearMap.range T) < Cardinal.aleph0
• FiniteDimensional ↥(LinearMap.range T)
• LinearMap.rank T < Cardinal.aleph0

As a second question, what's the best way to actually get that rank as a natural number, if it exists? Options include:

• T.rank.toNat
• Module.finrank R ↥(LinearMap.range T)

[Kevin Buzzard]

What I would do: FiniteDimensional and Module.finrank (and I'd avoid cardinals in general)

[Niels Voss]

The main disadvantage of that is it depends on a CoeSort

[Niels Voss]

I did implicitly use cardinals here #Is there code for X? > Singular Value Decomposition @ 💬 . Would you recommend replacing S.rank ≤ ↑n with the conjunction of FiniteDimensional R (LinearMap.range S) and Module.finrank R (LinearMap.range S) ≤ n?

[Niels Voss]

I guess what's unclear to me is that if we aren't supposed to use Cardinal for non set-theory-heavy things, then what's the use of LinearMap.rank at all?

[Yaël Dillies]

Niels Voss said:

The main disadvantage of that is it depends on a CoeSort

I've been wanting to add Submodule.finrank to dodge this precise issue. Feel free to do so!

[Kevin Buzzard]

I have no idea what the point of LinearMap.rank is and to be quite honest I'm not that clear about what the point of cardinals are at least in the area of maths I work in. There's the naturals, countably infinite (typically used for counting, not dimension), and "other" as far as I'm concerned.

[Jireh Loreaux]

Now that we have more API for ENat it could make sense to have Module.erank too.

[Kevin Buzzard]

This is always my instinct, but with cyclotomic fields people were saying "oh we have API for PNat now, let's use that" and two years later it all got refactored back to Nat.

[Jireh Loreaux]

I think having a spurious value is less of an issue than missing a value and overusing an existing one in its place.

[Niels Voss]

As far as I understand, so far, we have:

• Module.rank Module -> Cardinal
• Module.finrank Module -> Nat
• FiniteDimensional (aka Module.Finite) Module -> Prop
• LinearMap.rank LinearMap -> Cardinal
• Submodule.FG Submodule -> Prop

And in this thread the following have been proposed:

• Submodule.finrank Submodule -> Nat
• Module.erank Module -> ENat

It seems to me that there's 12 possible combinations: [Module|Submodule|LinearMap].[rank|nrank|enrank|FiniteDimensional]. How do we decide which ones we want? Plus, I think Module.finrank is inconsistent with the Set.card/Set.ncard/Set.encard naming convention.

[Niels Voss]

Is it fine if I do developments with Module.rank for now until there's a good enough alternative to express things like "Linear map T is finite dimensional and has rank <= n" without a conjunction?

[Niels Voss]

One option would be to make rank generic by adding something like

class Rank (T : Type*) where
  rank : T -> Cardinal

def nrank {T : Type*} [Rank T] (t : T) : Nat := Cardinal.toNat (Rank.rank t)
def enrank {T : Type*} [Rank T] (t : T) : ENat := Cardinal.toENat (Rank.rank t)
def FiniteRank {T : Type*} [Rank T] (t : T) : Prop := Rank.rank t < Cardinal.aleph0

or

class Rank (T : Type*) (R : Type*) where
  rank : T -> Cardinal

def nrank {T : Type*} (R : Type*) [Rank T R] (t : T) : Nat := Cardinal.toNat (Rank.rank t)
def enrank {T : Type*} (R : Type*) [Rank T R] (t : T) : ENat := Cardinal.toENat (Rank.rank t)
def FiniteRank {T : Type*} (R : Type*) [Rank T R] (t : T) : Prop := Rank.rank t < Cardinal.aleph0

(maybe only for Submodule and LinearMap, because I don't know if this can be set up for Module)

[Niels Voss]

I'm worried this might make things more complicated, or not interact properly with Modules that aren't vector spaces or for which the field needs to be specified explicitly. I'm also not sure the benefit is really that great.

[Artie Khovanov]

I find that using the Nat-valued quantities is easier in practice, even though it makes the generic theory a bit messier to state

[Kevin Buzzard]

I think that attempting to make Cardinal usable will inevitably run into the same issues as making PNat and ENat usable -- you might make 100 lemmas for them but Nat has thousands of lemmas and omega so you will never compete.