finite_dimensional_of_injective

Stream: Is there code for X?

[Scott Morrison]

Surely we have

import linear_algebra.finite_dimensional

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

def finite_dimensional_of_injective (f : V →ₗ[k] W) (w : f.ker = ⊥)
  [finite_dimensional k W] : finite_dimensional k V :=
sorry

[Scott Morrison]

(Or with w : function.injective f.)

[Scott Morrison]

I guess

def finite_dimensional_of_injective (f : V →ₗ[k] W) (w : function.injective f)
  [finite_dimensional k W] : finite_dimensional k V :=
begin
  haveI : is_noetherian k W := is_noetherian.iff_fg.mpr ‹_›,
  exact module.finite.of_injective f w,
end

works, and it's just a matter of API not being built for finite_dimensional.

[Eric Wieser]

That matches what we do in src#continuous_linear_map.finite_dimensional

[Scott Morrison]

Okay. I'll just roll this into the PR that needs it.

[Riccardo Brasca]

docs#module.finite.of_injective should do the job

[Riccardo Brasca]

finite_dimensional is defined as finite (I promise sooner or later I will finish the refactor)

[Riccardo Brasca]

ah sorry, you already found this