finite-dimensionality of field over subfield

Stream: maths

[Kevin Buzzard]

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]

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]

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]

But I don't even know how to say it

[Kevin Buzzard]

and I might well need more

[Kevin Buzzard]

I thought formalising the Nullstellensatz would be easy :-/

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Chris Hughes]

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]

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]

Am I missing something?

[Chris Hughes]

That sounds possible.

[Chris Hughes]

But maybe subfields should be bundled.

[Kevin Buzzard]

  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]

Use finset.induction

[Chris Hughes]

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

[Kevin Buzzard]

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]

You think I should be using algebra k K?

[Chris Hughes]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

apply finset.induction S?

[Chris Hughes]

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

[Kevin Buzzard]

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]

which has size one less.

[Chris Hughes]

Okay, so it is a strong induction really.

[Kevin Buzzard]

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]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Chris Hughes]

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

[Kevin Buzzard]

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]

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

[Chris Hughes]

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

[Kevin Buzzard]

Not even with some exact trick?

[Chris Hughes]

no

[Kevin Buzzard]

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

[Chris Hughes]

There's finset.strong_induction_on as well.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

This feels like it would be easy with subsets.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

_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]

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

[Chris Hughes]

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]

That's probably even the definition of the set.

[Kevin Buzzard]

⊢ 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]

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]

Is range_subtype_val a theorem.

[Chris Hughes]

That's not it actually.

[Chris Hughes]

Yes it is

[Kevin Buzzard]

Oh nice. This is surprisingly messy!

[Kevin Buzzard]

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