## Stream: maths

### Topic: finite-dimensionality of field over subfield

#### Kevin Buzzard (Feb 16 2020 at 12:33):

What is the canonical way to say that a field $K$ is finite-dimensional over a subfield $k$, i.e. (k : set K) [is_subfield k]?

#### Kevin Buzzard (Feb 16 2020 at 13:01):

Kind-of related: how do I say that a subring of a ring {A : Type*} [ring A] (R : set A) [is_subring R] is commutative? So it's like algebra R A.

#### Kevin Buzzard (Feb 16 2020 at 13:19):

I think what I need for the subfields is that if $k_1\subseteq k_2$ are two subfields of $K$ and $K$ is finite-dimensional as a $k_1$-vector space then it's finite-dimensional as a $k_2$-vector space.

#### Kevin Buzzard (Feb 16 2020 at 13:19):

But I don't even know how to say it

#### Kevin Buzzard (Feb 16 2020 at 13:19):

and I might well need more

#### Kevin Buzzard (Feb 16 2020 at 13:20):

I thought formalising the Nullstellensatz would be easy :-/

#### Kevin Buzzard (Feb 16 2020 at 13:26):

Oh I don't even know the canonical way to say that a $k$-algebra is finite-dimensional as a vector space. is_noetherian?

#### Chris Hughes (Feb 16 2020 at 13:45):

There's a finite dimensional predicate for vector spaces. It's defined to be is_noetherian

#### Kevin Buzzard (Feb 16 2020 at 13:45):

Is what's going on that when we say $A\subseteq B$ an inclusion of rings, we're happy to let both rings play an equal role, whereas the CS people either want A to be the leader and (B : Type) [ring B] [algebra A B] to be the $A$-algebra or they want B to be the leader and (A : set B) [is_subring A] to be the subalgebra?

#### Kevin Buzzard (Feb 16 2020 at 13:47):

This is Zariski's Lemma.

1 goal
K : Type v,
_inst_1 : discrete_field K
⊢ ∀ (k : set K) (S : finset K) [_inst_2 : is_subfield k],
ring.closure (k ∪ finset.to_set S) = univ → is_noetherian ↥k K


#### Kevin Buzzard (Feb 16 2020 at 13:48):

(possibly -- I was super-surprised that typeclass inference succeeded with the ↥k-module structure on K.)

#### Chris Hughes (Feb 16 2020 at 13:49):

It's a problem that these two things are different I think. It's the same concept with two different ways of expressing it, and you can go between them on paper fluently, but in Lean, you have to be careful about proving things in the correct generality, and that makes statements look ugly.

#### Kevin Buzzard (Feb 16 2020 at 13:49):

The proof of Zariski's Lemma is by induction on the size of S and it quantifies over all k, so I have to use unfreeze_local_instances and then add them again with letI

#### Kevin Buzzard (Feb 16 2020 at 13:49):

Am I missing something?

#### Chris Hughes (Feb 16 2020 at 13:51):

That sounds possible.

#### Chris Hughes (Feb 16 2020 at 13:51):

But maybe subfields should be bundled.

#### Kevin Buzzard (Feb 16 2020 at 13:52):

  suffices :
∀ n : ℕ, ∀ (S : finset K), S.card = n → (∀ (k : set K) [hk : is_subfield k],

ring.closure (k ∪ finset.to_set S) = univ → by letI : is_subfield k := hk; exact is_noetherian ↥k K),


#### Chris Hughes (Feb 16 2020 at 13:53):

Use finset.induction

#### Chris Hughes (Feb 16 2020 at 13:55):

But using subfield for this seems wrong. You want a map.

#### Kevin Buzzard (Feb 16 2020 at 13:56):

For my inductive step I'll have a set $S$ and I will construct (nonconstructively) some element $s\in S$ with a certain property and I will then use that the lemma is true for $S-\{s\}$.

#### Kevin Buzzard (Feb 16 2020 at 13:57):

You think I should be using algebra k K?

#### Chris Hughes (Feb 16 2020 at 13:58):

It might be trick to use that during the proof actually, but you definitely want the final statement to be like that, even if you prove it for subfields first.

#### Kevin Buzzard (Feb 16 2020 at 13:59):

I see! Thanks for this. Should I be using finset.induction in my case?

#### Kevin Buzzard (Feb 16 2020 at 14:00):

I am happy to build what I need, but I want to do it right.

#### Kevin Buzzard (Feb 16 2020 at 14:04):

It seems like a bit of a kerfuffle to get from what I have to finset.induction

#### Chris Hughes (Feb 16 2020 at 14:05):

apply finset.induction S?

#### Chris Hughes (Feb 16 2020 at 14:05):

What is the induction, is it a one element at a time induction or a strong induction?

#### Kevin Buzzard (Feb 16 2020 at 14:06):

I prove P emptyset. I then show that if $S$ is non-empty then I can manufacture an element $s\in S$ which satisfies a certain property, and then I use the inductive hypothesis on $S-\{s\}$.

#### Kevin Buzzard (Feb 16 2020 at 14:07):

which has size one less.

#### Chris Hughes (Feb 16 2020 at 14:07):

Okay, so it is a strong induction really.

#### Kevin Buzzard (Feb 16 2020 at 14:08):

The manufacturing explicitly uses some nonconstructiveness because it's a case split: if no $s\in S$ has the property then I prove the result directly using other means.

#### Kevin Buzzard (Feb 16 2020 at 14:08):

It's what a mathematician would undoubtedly call "induction on the size of $S$".

#### Chris Hughes (Feb 16 2020 at 14:09):

I would use the equation compiler for this, but that's just my taste.

#### Kevin Buzzard (Feb 16 2020 at 14:10):

Are you suggesting I use a match S.card with?

#### Chris Hughes (Feb 16 2020 at 14:12):

No, because then you don't get an induction hypothesis.

#### Kevin Buzzard (Feb 16 2020 at 14:17):

This is my goal:

⊢ ∀ (S : finset K) (k : Type u) [_inst_1 : discrete_field k] [_inst_3 : algebra k K],
algebra.adjoin k (finset.to_set S) = ⊤ → submodule.fg ⊤


I'm in tactic mode. I want to prove it by induction on the size of S. What do I do? I'm not with you yet.

#### Kevin Buzzard (Feb 16 2020 at 14:19):

  obtain ⟨n, hn⟩ : {n : ℕ // S.card = n} :=
⟨_, rfl⟩,


#### Chris Hughes (Feb 16 2020 at 14:25):

You can't really do it in the middle of a proof.

#### Kevin Buzzard (Feb 16 2020 at 14:26):

Not even with some exact trick?

no

#### Kevin Buzzard (Feb 16 2020 at 14:28):

My obtain solution seems to be working fine. I just put induction n with d hd on the next step.

#### Chris Hughes (Feb 16 2020 at 14:29):

There's finset.strong_induction_on as well.

#### Kevin Buzzard (Feb 16 2020 at 14:31):

Oh that's exactly what I need! Thanks! I thought you were just philosophising, I didn't realise it was there; I checked finset.strong_induction and it wasn't :-/

#### Kevin Buzzard (Feb 16 2020 at 14:33):

 intro S, apply finset.strong_induction_on S, clear S,

#### Kevin Buzzard (Feb 16 2020 at 16:29):

Chris Hughes said:

It might be trick to use that during the proof actually, but you definitely want the final statement to be like that, even if you prove it for subfields first.

I tried to prove it directly and now I am faced with the issue that it is maths-trivial that if $k$ is a subfield of $K$ and $S\ni s$ is a finite subset of $K$ such that $K=k(S)$, then $K=L(S')$ where $L=K(s)$ and $S'=S-\{s\}$

#### Kevin Buzzard (Feb 16 2020 at 16:30):

K : Type u,
_inst_2 : discrete_field K,
S : finset K,
k : Type u,
hk : discrete_field k,
hka : algebra k K,
_inst : discrete_field k,
_inst_1 : algebra k K,
hSgen : algebra.adjoin k ↑S = ⊤,
s : K,
hs : s ∈ S,
L : set K := field.closure (set.range (algebra_map K) ∪ {s})
⊢ algebra.adjoin ↥L ↑(S \ {s}) = ⊤


#### Kevin Buzzard (Feb 16 2020 at 16:31):

This feels like it would be easy with subsets.

#### Kevin Buzzard (Feb 16 2020 at 16:40):

but if I use subsets it's hard to express finite-dimensionality of K over k

#### Kevin Buzzard (Feb 16 2020 at 16:43):

I think that at some point I need to use subsets and then talk about the sub-R-module of an R-algebra A generated by a subset of A in the subset language.

#### Kevin Buzzard (Feb 16 2020 at 20:59):

_inst_1 : algebra k K := hka,
s : K,
hs : s ∈ S,
L : set K := field.closure (set.range (algebra_map K) ∪ {s}),
x : K,
hSgen : x ∈ ↑(algebra.adjoin k ↑S)
⊢ x ∈ ↑(algebra.adjoin ↥L ↑(S \ {s}))


This is what I need to make the induction work. algebra.adjoin and ↑ is a Galois insertion between subsets and sub-R-algebras. My problem is that R changes from k to L.

#### Kevin Buzzard (Feb 16 2020 at 21:08):

and all the proper mathematicians are looking at me and laughing because $k(S)\subseteq L(S-\{s\})$ is trivial.

#### Chris Hughes (Feb 16 2020 at 21:18):

algebra.adjoin as a set is just ring.closure of k \cup S right? So it's easy if you write it like that.

#### Chris Hughes (Feb 16 2020 at 21:18):

That's probably even the definition of the set.

#### Kevin Buzzard (Feb 16 2020 at 21:29):

⊢ ring.closure (set.range (algebra_map K) ∪ finset.to_set S) ≤
ring.closure (set.range (algebra_map K) ∪ finset.to_set (finset.erase S s))


Looks wrong but there are two different algebra_maps involved; one from k and one from L.

#### Kevin Buzzard (Feb 16 2020 at 21:39):

I'm still not there. If (L : set K) [is_subfield L] then I need that L = range (algebra_map K) with the obvious instance of [algebra L K]

#### Chris Hughes (Feb 16 2020 at 22:53):

Is range_subtype_val a theorem.

#### Chris Hughes (Feb 16 2020 at 22:53):

That's not it actually.

Yes it is

#### Kevin Buzzard (Feb 16 2020 at 23:02):

Oh nice. This is surprisingly messy!

#### Kevin Buzzard (Feb 17 2020 at 18:02):

subtype.range_val : ∀ (s : set ?M_1), set.range subtype.val = s


Last updated: May 11 2021 at 16:22 UTC