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:

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. 
write everthing in terms of
⊤ : submodule F L
.
In this case, I just don't know how to convert asubmodule
into asubalgebra
in the presence of multiplication. 
write everthing in terms of
L
.
This seems to require coercingL
to be asubmodule
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):
Jack J Garzella (Jun 23 2020 at 23:39):
#3096 works greatthanks!
Last updated: May 14 2021 at 18:28 UTC