Zulip Chat Archive

Stream: new members

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


Sebastian Monnet (Jan 08 2022 at 17:28):

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 (Jan 08 2022 at 17:46):

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 (Jan 08 2022 at 18:13):

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 (Jan 09 2022 at 08:26):

Something like docs#submonoid.equiv_map_of_injective?

Eric Wieser (Jan 09 2022 at 08:32):

Ideally it would be stated as equiv_of_left_inverse

Eric Wieser (Jan 09 2022 at 08:33):

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

Sebastian Monnet (Jan 09 2022 at 12:56):

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

Kevin Buzzard (Jan 09 2022 at 13:15):

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 (Jan 09 2022 at 13:41):

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


Last updated: Dec 20 2023 at 11:08 UTC