Behaviour of finrank under morphisms

Stream: Is there code for X?

[Heather Macbeth]

Does mathlib have: the finrank of the map of a submodule by a linear map is less than or equal to the finrank of the original submodule? Better, that for a linear equiv, it's an equality (as follows by pairing the inequalities in the two directions)?

import linear_algebra.finite_dimensional

open finite_dimensional

variables {R : Type*} [field R]
variables {V : Type*} [add_comm_group V] [module R V]
variables {W : Type*} [add_comm_group W] [module R W]

example (f : V →ₗ[R] W) (p : submodule R V) : finrank R (p.map f) ≤ finrank R p :=
sorry

example (f : V ≃ₗ[R] W) (p : submodule R V) :
  finrank R (p.map (f : V →ₗ[R] W)) = finrank R p :=
sorry

[Scott Morrison]

We have this for plain ranks (i.e. without the finiteness assumption).

[Scott Morrison]

src#dim_map_le

[Heather Macbeth]

Ah -- and I suppose I need finite_dimensional R p or it's not true.

[Heather Macbeth]

Trying to translate the dim_map_le lemma using finite_dimensional.finrank_eq_dim but it apparently requires V and W to be in the same universe ... any idea how to get around that?

[Heather Macbeth]

Something lift?

[Floris van Doorn]

V and W don't have to be in the same universe:

import linear_algebra.finite_dimensional

open finite_dimensional

universe variable u
variables {R : Type*} [field R]
variables {V : Type u} [add_comm_group V] [module R V]
variables {W : Type u} [add_comm_group W] [module R W]

example (f : V →ₗ[R] W) (p : submodule R V) [finite_dimensional R p]
  [finite_dimensional R (p.map f)] : finrank R (p.map f) ≤ finrank R p :=
begin
  rw [← cardinal.nat_cast_le, finrank_eq_dim R p, finrank_eq_dim R (p.map f)],
  exact dim_map_le f p
end

EDIT: I'm stupid, I assumed them to be in the same universe, and then forgot that I did.

[Floris van Doorn]

If the second example is already proven for rank, then this will translate it to finrank

example (f : V ≃ₗ[R] W) (p : submodule R V) [finite_dimensional R p]
  [finite_dimensional R (p.map (f : V →ₗ[R] W))] :
    finrank R (p.map (f : V →ₗ[R] W)) = finrank R p :=
begin
  erw [← cardinal.nat_cast_inj, finrank_eq_dim R p,
    finrank_eq_dim R (p.map (f : V →ₗ[R] W))],
  -- to prove: the result for rank
end

[Floris van Doorn]

But yes, a lift will help...

[Heather Macbeth]

I was hoping to deduce finite_dimensional R (p.map f) from finite_dimensional R p, rather than assuming it explicitly -- any idea how to do that?

[Heather Macbeth]

Because from dim_map_le we get that its dim is less than or equal to a natural number.

[Floris van Doorn]

Heather Macbeth said:

I was hoping to deduce finite_dimensional R (p.map f) from finite_dimensional R p, rather than assuming it explicitly -- any idea how to do that?

I didn't look, but I hoped that would be a lemma somewhere. Otherwise, it should probably follow from dim_map_le.

[Floris van Doorn]

If V and W are in the same universe:

instance (f : V →ₗ[R] W) (p : submodule R V) [finite_dimensional R p] :
  finite_dimensional R (p.map f) :=
begin
  unfreezingI { rw [finite_dimensional, is_noetherian.iff_dim_lt_omega] at * },
  refine (dim_map_le f p).trans_lt ‹_›
end

[Scott Morrison]

Okay, I am working on the universe variable version of dim_map_le

[Heather Macbeth]

@Floris van Doorn nice!

[Floris van Doorn]

Is this your statement @Scott Morrison ?

universe variables u v
variables {R : Type*} [field R]
variables {V : Type u} [add_comm_group V] [module R V]
variables {W : Type v} [add_comm_group W] [module R W]
variables (f : V →ₗ[R] W) (p : submodule R V)

lemma lift_dim_map_le :
  cardinal.lift.{_ u} (module.rank R (p.map f)) ≤ cardinal.lift.{_ v} (module.rank R p) :=
sorry

[Scott Morrison]

yes, that's what I was aiming at

[Scott Morrison]

it will need a few other lemmas generalised first

[Scott Morrison]

We have cardinal.lift_sup_le_lift_sup', newly added exactly for this sort of problem.

[Floris van Doorn]

Once @Scott Morrison has the lemma above:

import linear_algebra.finite_dimensional

open finite_dimensional module

universe variables u v
variables {R : Type*} [field R]
variables {V : Type u} [add_comm_group V] [module R V]
variables {W : Type v} [add_comm_group W] [module R W]
variables (f : V →ₗ[R] W) (p : submodule R V)

lemma lift_dim_map_le :
  cardinal.lift.{v u} (module.rank R (p.map f)) ≤ cardinal.lift.{u v} (module.rank R p) :=
sorry

instance (f : V →ₗ[R] W) (p : submodule R V) [h : finite_dimensional R p] :
  finite_dimensional R (p.map f) :=
begin
  unfreezingI { rw [finite_dimensional, is_noetherian.iff_dim_lt_omega ] at h ⊢ },
  rw [← cardinal.lift_lt.{v u}],
  rw [← cardinal.lift_lt.{u v}] at h,
  rw [cardinal.lift_omega] at h ⊢,
  exact (lift_dim_map_le f p).trans_lt h
end

example (f : V →ₗ[R] W) (p : submodule R V) [finite_dimensional R p] :
  finrank R (p.map f) ≤ finrank R p :=
begin
  rw [← cardinal.nat_cast_le.{max u v}, ← cardinal.lift_nat_cast.{v u},
    ← cardinal.lift_nat_cast.{u v}, finrank_eq_dim R p, finrank_eq_dim R (p.map f)],
  exact lift_dim_map_le f p
end

[Floris van Doorn]

And here is the reduction of the second example into the corresponding lemma for rank:

lemma lift_dim_map_eq (f : V ≃ₗ[R] W) (p : submodule R V) :
  cardinal.lift.{v u} (module.rank R (p.map (f : V →ₗ[R] W))) =
    cardinal.lift.{u v} (module.rank R p) :=
sorry

example (f : V ≃ₗ[R] W) (p : submodule R V) [finite_dimensional R p]
  [finite_dimensional R (p.map (f : V →ₗ[R] W))] :
    finrank R (p.map (f : V →ₗ[R] W)) = finrank R p :=
begin
  rw [← cardinal.nat_cast_inj.{max u v}, ← cardinal.lift_nat_cast.{v u},
    ← cardinal.lift_nat_cast.{u v}, finrank_eq_dim R p, finrank_eq_dim R (p.map f)],
  exact lift_dim_map_eq f p
end

[Floris van Doorn]

I'm going to bed now. Good luck with generalizing dim_map_le!

[Scott Morrison]

@Heather Macbeth, lift_dim_map_le is done. Do you want it as a separate PR, or should I just push it to whatever branch you're working on?

[Scott Morrison]

It's on branch#lift_dim_map_le

[Heather Macbeth]

A separate PR from you would be great, thank you! (the branch I was working on when I noticed this gap is very preliminary)

[Heather Macbeth]

Thank you both very much for wrangling these universes for me.

[Scott Morrison]

#8800

[Scott Morrison]

Universes are such a pain. :-) Happily I'd just recently fought them in this file, so remembered how to do it!

[Heather Macbeth]

Yes, they really are!!

[Heather Macbeth]

I hope @Floris van Doorn will also PR the proof of the main lemma in the morning -- or Floris I can do it, whatever's easiest for you.

[Floris van Doorn]

#8815

[Heather Macbeth]

Thanks!