Zulip Chat Archive

Stream: maths

Topic: finite-dimensionality of field over subfield


view this post on Zulip Kevin Buzzard (Feb 16 2020 at 12:33):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 13:19):

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

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 13:19):

But I don't even know how to say it

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 13:19):

and I might well need more

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 13:20):

I thought formalising the Nullstellensatz would be easy :-/

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 13:26):

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

view this post on Zulip Chris Hughes (Feb 16 2020 at 13:45):

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

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 13:45):

Is what's going on that when we say ABA\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 AA-algebra or they want B to be the leader and (A : set B) [is_subring A] to be the subalgebra?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 13:48):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 13:49):

Am I missing something?

view this post on Zulip Chris Hughes (Feb 16 2020 at 13:51):

That sounds possible.

view this post on Zulip Chris Hughes (Feb 16 2020 at 13:51):

But maybe subfields should be bundled.

view this post on Zulip 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),

view this post on Zulip Chris Hughes (Feb 16 2020 at 13:53):

Use finset.induction

view this post on Zulip Chris Hughes (Feb 16 2020 at 13:55):

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

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 13:56):

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

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 13:57):

You think I should be using algebra k K?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 13:59):

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

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 14:00):

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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Feb 16 2020 at 14:05):

apply finset.induction S?

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 14:06):

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

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 14:07):

which has size one less.

view this post on Zulip Chris Hughes (Feb 16 2020 at 14:07):

Okay, so it is a strong induction really.

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 14:08):

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

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 14:08):

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

view this post on Zulip Chris Hughes (Feb 16 2020 at 14:09):

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

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 14:10):

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

view this post on Zulip Chris Hughes (Feb 16 2020 at 14:12):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 14:19):

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

view this post on Zulip Chris Hughes (Feb 16 2020 at 14:25):

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

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 14:26):

Not even with some exact trick?

view this post on Zulip Chris Hughes (Feb 16 2020 at 14:27):

no

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Feb 16 2020 at 14:29):

There's finset.strong_induction_on as well.

view this post on Zulip 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 :-/

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 14:33):

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

view this post on Zulip 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 kk is a subfield of KK and SsS\ni s is a finite subset of KK such that K=k(S)K=k(S), then K=L(S)K=L(S') where L=K(s)L=K(s) and S=S{s}S'=S-\{s\}

view this post on Zulip 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}) = 

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 16:31):

This feels like it would be easy with subsets.

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 16:40):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 21:08):

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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Feb 16 2020 at 21:18):

That's probably even the definition of the set.

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip Chris Hughes (Feb 16 2020 at 22:53):

Is range_subtype_val a theorem.

view this post on Zulip Chris Hughes (Feb 16 2020 at 22:53):

That's not it actually.

view this post on Zulip Chris Hughes (Feb 16 2020 at 22:54):

Yes it is

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 23:02):

Oh nice. This is surprisingly messy!

view this post on Zulip 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