Zulip Chat Archive

Stream: maths

Topic: is_integral_of_finite_extension


Jack J Garzella (Jun 23 2020 at 20:03):

I am attempting to prove the following lemma:

lemma is_integral_of_finite_extension {F : Type u} {L : Type v}
[field F] [field L] [algebra F L] [finite_dimensional F L]
(x : L) : is_integral F x :=
sorry

I thought the best approach would be to use the is_integral_of_mem_of_fg lemma, combined with iff_fg in finite_dimensional.lean. However, I have been unable to get lean to translate between these three objects:

  • ⊤ : submodule F L
  • ⊤ : subalgebra F L
  • L itself

Put succinctly, iff_fg is written in terms of ⊤ : submodule F L, and is_integral_of_mem_of_fg requires a subalgebra type, while my mental model wants to use L.
I see three possible approaches:

  1. write everything in terms of ⊤ : subalgebra F L.
    But doing this would require a term of type (⊤ : subalgebra F L).to_submodule = (⊤ : submodule F L), which I don't know how to do.

  2. write everthing in terms of ⊤ : submodule F L.
    In this case, I just don't know how to convert a submodule into a subalgebra in the presence of multiplication.

  3. write everthing in terms of L.
    This seems to require coercing L to be a submodule and proving that it is equal to ⊤ : submodule F L.

Any advice on which direction I should go?

Kevin Buzzard (Jun 23 2020 at 20:17):

@Kenny Lau did you already prove this?

Kenny Lau (Jun 23 2020 at 20:17):

I don't think so

Kevin Buzzard (Jun 23 2020 at 20:18):

It's some noetherian thing

Chris Hughes (Jun 23 2020 at 20:30):

I recall seeing this recently in a PR.

Chris Hughes (Jun 23 2020 at 20:35):

#3096

Jack J Garzella (Jun 23 2020 at 23:39):

#3096 works great--thanks!


Last updated: Dec 20 2023 at 11:08 UTC