is_integral_of_finite_extension

Stream: maths

[Jack J Garzella]

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]

@Kenny Lau did you already prove this?

[Kenny Lau]

I don't think so

[Kevin Buzzard]

It's some noetherian thing

[Chris Hughes]

I recall seeing this recently in a PR.

[Chris Hughes]

#3096

[Jack J Garzella]

#3096 works great--thanks!