Zulip Chat Archive

Stream: new members

Topic: Bottom subalgebra over fields is finite-dimensional

Sebastian Monnet (Dec 19 2021 at 10:48):

Let L/KL/K be a field extension. I'm trying to show that is finite-dimensional over $K$. Here's my attempt:

import field_theory.galois

lemma fin_dim_bot (K L : Type*) [field K] [field L] [algebra K L] : finite_dimensional K ( : intermediate_field K L) :=
  exact finite_dimensional_of_dim_eq_one (subalgebra.dim_bot),

The problem is that the subalgebra.dim_bot has type module.rank ?m_1 ↥⊥ = 1, and I need it to have type module.rank K ↥⊥ = 1. I've seen this ?m_1 notation before, and I think it means that the result is true for any type, but I don't know how to insert the type I want (namely K). I've tried things like subalgebra.dim_bot K and subalgebra.dim_bot K L, but none of it has worked.

I'd appreciate any guidance or explanation of what I need to do.

Eric Wieser (Dec 19 2021 at 10:54):

set_option pp.implicit true will give a clearer message

Eric Wieser (Dec 19 2021 at 10:56):

  refine finite_dimensional_of_dim_eq_one _,
  convert subalgebra.dim_bot,

Might help you understand what's going wrong

Eric Wieser (Dec 19 2021 at 10:56):


Sebastian Monnet (Dec 19 2021 at 11:14):

Hmm, well I solved the problem by using your refine tactic and then just whacking it with simp. I still have no idea what the original problem was, or what simp actually did in this instance.

Using convert subalgebra.dim_bot creates six goals, some of which are really weird. The first one is module.rank K ↥⊥ = module.rank ?m_1 ↥⊥, which seems to be exactly the same as the original problem, since I don't know what this ?m_1 is or how to interact with it.

Eric Wieser (Dec 19 2021 at 11:28):

?m_1 means " I can't work out what to put here"

Eric Wieser (Dec 19 2021 at 11:29):

Probably because the bits you can't see without pp.implicit true don't match at all

Eric Wieser (Dec 19 2021 at 11:29):

simp? will tell you what simp did

Stuart Presnell (Dec 19 2021 at 11:58):

This might be a way to see more clearly what's going on:

Last updated: Dec 20 2023 at 11:08 UTC