finrank K (E.map f) = finrank K E

Stream: new members

[Sebastian Monnet]

I'm trying to get rid of the sorry in this proof:

import field_theory.galois

lemma eq_of_map_le {K L : Type*} [field K] [field L] [algebra K L] {E : intermediate_field K L}
{f : L →ₐ[K] L} (h_findim : finite_dimensional K E) (h_map_le : E.map f ≤ E) :
E.map f = E :=
begin
  have h_finrank_eq : finite_dimensional.finrank K (E.map f) =
  finite_dimensional.finrank K E,
  {
    sorry,
  },
  have h_submod_le : (E.map f).to_subalgebra.to_submodule ≤ E.to_subalgebra.to_submodule,
  {
    exact h_map_le,
  },
  haveI hE_submod_fin : finite_dimensional K E.to_subalgebra.to_submodule,
  {
    exact h_findim,
  },
  exact intermediate_field.to_subalgebra_eq_iff.mp (subalgebra.to_submodule_injective
  (finite_dimensional.eq_of_le_of_finrank_eq h_map_le h_finrank_eq)),
end

The maths argument is that f is bijective and K-linear, so it's a K-isomorphism. Can anyone see a good way to do this? It feels like it must be straightforward, but I haven't been able to find anything useful in mathlib.

[Kevin Buzzard]

You're not assuming f is bijective and in this generality it need not be. Why not prove that E.map f and E are isomorphic? This only needs injectivity.

[Sebastian Monnet]

Sorry, I mean that f is injective as a map E \to E.map f. Yeah I guess I'm wondering if the isomorphism between E and E.map f is in mathlib

[Eric Wieser]

Something like docs#submonoid.equiv_map_of_injective?

[Eric Wieser]

Ideally it would be stated as equiv_of_left_inverse

[Eric Wieser]

As then we could implement docs#mul_equiv.map_submonoid in terms of it

[Sebastian Monnet]

Do you think I can use submonoid.equiv_map_of_injective directly, or should I prove an analogue for subalgebras/vector spaces?

[Kevin Buzzard]

I think you need an analogue. Just because some map is an isomorphism of add_monoids underlying vector spaces doesn't mean that the dimensions are equal.

[Eric Wieser]

Most likely we have something analogous for submodule already (docs#submodule.equiv_map_of_injective?)