## Stream: maths

### Topic: Span of finite set is sequentially closed

#### Lambert A'Campo (Dec 03 2019 at 15:47):

I am trying to prove the following lemma

open metric set

variables
{V : Type*} [normed_group V] [normed_space ℝ V]

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
sorry,
end


Is this somewhere in mathlib? If not, how can you induct on the cardinality of A?

#### Kevin Buzzard (Dec 03 2019 at 15:59):

It might be in there -- @Sebastien Gouezel ? Oh, I just remembered he's giving a talk in Orsay right now ;-)

If it's not then maybe this is a useful induction procedure for you:

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
intro h,
apply finite.induction_on h,
sorry, sorry
end


#### Lambert A'Campo (Dec 03 2019 at 16:57):

So it turns out it is actually in mathlib!

variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
{E : Type u} [normed_group E] [normed_space 𝕜 E]
[complete_space 𝕜]

lemma submodule.closed_of_finite_dimensional (s : submodule 𝕜 E) [finite_dimensional 𝕜 s] :
is_closed (s : set E)


but I'm not quite sure how to make lean transform this into what I need.

#### Kevin Buzzard (Dec 03 2019 at 16:59):

I guess you want to find the following facts:
(1) Closed implies sequentially closed [this will be proved near the definition of sequentially closed]
(2) the reals are a nondiscrete normed field [type class inference will handle this]
(3) the vector space spanned by a finite set is finite-dimensional [that will surely be there somewhere]

#### Kevin Buzzard (Dec 03 2019 at 17:00):

(2) is indeed there:

noncomputable example : nondiscrete_normed_field ℝ := by apply_instance


so you don't have to do anything -- type class inference will do it for you.

#### Lambert A'Campo (Dec 03 2019 at 17:00):

So we are this far

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
intro h_fin,
let S := (submodule.span ℝ A).carrier,
apply is_seq_closed_of_is_closed S,

apply submodule.closed_of_finite_dimensional,
end


but we get an error:
invalid apply tactic, failed to unify
is_closed S
with
is_closed ↑?m_6

#### Lambert A'Campo (Dec 03 2019 at 17:01):

I thought that this should reduce it to showing that submodule.span \R A is finite dimensional

#### Kevin Buzzard (Dec 03 2019 at 17:01):

Is there any possibility that you can post some fully working code?

#### Kevin Buzzard (Dec 03 2019 at 17:02):

I'm getting a bit sick of having to guess all the imports ;-)

#### Lambert A'Campo (Dec 03 2019 at 17:03):

Yes of course, sorry.

import analysis.normed_space.banach
import analysis.normed_space.basic
import linear_algebra.basic
import linear_algebra.basis
import linear_algebra.dimension
import linear_algebra.finite_dimensional
import topology.subset_properties
import set_theory.cardinal
import data.real.basic
import topology.sequences
import order.bounded_lattice
import analysis.specific_limits
import analysis.normed_space.finite_dimension

noncomputable theory
open_locale classical

open metric set

variables
{V : Type*} [normed_group V] [normed_space ℝ V]

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
intro h_fin,
let S := (submodule.span ℝ A).carrier,
apply is_seq_closed_of_is_closed S,

apply submodule.closed_of_finite_dimensional,
end


#### Kevin Buzzard (Dec 03 2019 at 17:09):

Yeah. There might be a universe issue and also a typeclass issue.

#### Kevin Buzzard (Dec 03 2019 at 17:11):

#check @submodule.closed_of_finite_dimensional
/-
submodule.closed_of_finite_dimensional :
∀ {𝕜 : Type u_2} [_inst_1 : nondiscrete_normed_field 𝕜] {E : Type u_2} [_inst_2 : normed_group E]
[_inst_3 : normed_space 𝕜 E] [_inst_6 : complete_space 𝕜] (s : submodule 𝕜 E)
[_inst_7 : finite_dimensional 𝕜 ↥s], is_closed ↑s
-/


For some reason 𝕜 and E are supposed to be in the same universe in this lemma. This might be some subtlety that I don't know about, or it might be an error in mathlib.

#### Kevin Buzzard (Dec 03 2019 at 17:12):

-- we use linear equivs, which require all the types to live in the same universe
variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
{E : Type u} [normed_group E] [normed_space 𝕜 E]
{F : Type v} [normed_group F] [normed_space 𝕜 F]


This is explicit design decision. I don't know what's going on here. This has consequences for you -- the reals have type Type so Lean expects your vector space also to have type Type.

#### Kevin Buzzard (Dec 03 2019 at 17:13):

But changing the variable to {V : Type} unmasks a new problem.

#### Kevin Buzzard (Dec 03 2019 at 17:15):

which is that type class inference cannot figure out why s is finite-dimensional.

#### Kevin Buzzard (Dec 03 2019 at 17:15):

variables
{V : Type} [normed_group V] [normed_space ℝ V]

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
intro h_fin,
let S : set V := ↑(submodule.span ℝ A),
apply is_seq_closed_of_is_closed S,
exact @submodule.closed_of_finite_dimensional ℝ _ V _ _ _ _ sorry,
end


works, but there's a sorry

#### Kevin Buzzard (Dec 03 2019 at 17:17):

So what is left is the proof that S is finite-dimensional. Oh -- by the way -- in Lean there is a "canonical" way of doing many things, and your definition of S as (...).carrier is non-canonical: I changed it to the canonical way of writing this, with the little up-arrow.

#### Kevin Buzzard (Dec 03 2019 at 17:23):

variables {V : Type} [normed_group V] [normed_space ℝ V]

instance moo {V : Type} [normed_group V] [normed_space ℝ V] (A : set V) (hA : finite A) :
finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
sorry
end

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
intro h_fin,
let S : set V := ↑(submodule.span ℝ A),
apply is_seq_closed_of_is_closed S,
exact @submodule.closed_of_finite_dimensional ℝ _ V _ _ _ _ (moo A h_fin),
end


There is this thing called type class inference, which mathematicians tend to push in all sorts of directions which it turns out that Lean 3 was not quite expecting, because computer scientists did not really know what mathematicians wanted to do with it. I can't actually get it to work in this situation (hence all the ridiculous _s and the moo in the lemma) but probably some fiddling around with priorities could fix this.

#### Patrick Massot (Dec 03 2019 at 17:25):

You should really change the statement to use the coercion.

#### Kevin Buzzard (Dec 03 2019 at 17:25):

Actually I see now that perhaps moo is a bad instance, because finite is not a typeclass which might mean that typeclass inference will not be able to find the hypothesis that A is finite. I am a bit out of my depth here.

However this is eventually resolved, the missing part of the argument is still the sorry above.

#### Patrick Massot (Dec 03 2019 at 17:26):

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (↑(submodule.span ℝ A) : set V)

#### Patrick Massot (Dec 03 2019 at 17:26):

Needing this up-arrow in the statement is really painful, but we don't know how to avoid this. We explain a tiny variation on this issue in our perfectoid paper.

#### Patrick Massot (Dec 03 2019 at 17:27):

Exactly in the paragraph where we complain about Lean elaboration being not yet good enough for maths.

#### Patrick Massot (Dec 03 2019 at 17:28):

Then you can write:

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (↑(submodule.span ℝ A) : set V) :=
begin
intro h_fin,
apply is_seq_closed_of_is_closed,
haveI : finite_dimensional ℝ (submodule.span ℝ A) := sorry,
exact submodule.closed_of_finite_dimensional _,
end


#### Patrick Massot (Dec 03 2019 at 17:28):

Where the sorry is still the same one, but there is no more Morse code @... _ _ _ _ _

#### Kevin Buzzard (Dec 03 2019 at 17:29):

Patrick do you understand why V has to have type Type?

#### Patrick Massot (Dec 03 2019 at 17:30):

It might be in there -- Sebastien Gouezel ? Oh, I just remembered he's giving a talk in Orsay right now ;-)

Yes, he was finishing his talk at that moment. It was very nice talk. He explained maths for 15 minutes, then propaganda for Sledgehammer for 30 minutes then 15 minutes about how simple type theory is unfortunately unbearable.

#### Kevin Buzzard (Dec 03 2019 at 17:31):

theorem finite_dimensional_of_finite_span {V : Type} [normed_group V] [normed_space ℝ V] {A : set V} (hA : finite A) :
finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
sorry
end

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (↑(submodule.span ℝ A) : set V) :=
begin
intro h_fin,
apply is_seq_closed_of_is_closed,
haveI : finite_dimensional ℝ (submodule.span ℝ A) := finite_dimensional_of_finite_span h_fin,
exact submodule.closed_of_finite_dimensional _,
end


I moved the sorry to a more respectable place.

#### Patrick Massot (Dec 03 2019 at 17:32):

He was a bit unfair to Lean though. He explained how Lean is harder to read than Isabelle by comparing tactic scripts on a white background with proof terms on a black background (using a video beamer making it impossible to read VScode's default dark theme).

#### Patrick Massot (Dec 03 2019 at 17:32):

I would rename that as finite_dimensional_span_of_finite.

#### Patrick Massot (Dec 03 2019 at 17:32):

And no, I don't know anything about universe issues.

#### Kevin Buzzard (Dec 03 2019 at 17:33):

but then did someone ask him the question about which system is more likely to be able to define the tangent space of a manifold, a trivial undergraduate thing?

#### Kevin Buzzard (Dec 03 2019 at 17:33):

theorem finite_dimensional_span_of_finite {V : Type} [normed_group V] [normed_space ℝ V] {A : set V} (hA : finite A) :
finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
sorry
end

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (↑(submodule.span ℝ A) : set V) :=
begin
intro h_fin,
apply is_seq_closed_of_is_closed,
haveI : finite_dimensional ℝ (submodule.span ℝ A) := finite_dimensional_span_of_finite h_fin,
exact submodule.closed_of_finite_dimensional _,
end


#### Patrick Massot (Dec 03 2019 at 17:35):

He was very clear Isabelle/HOL is unusable for maths. And also very clear that any system giving him dependant type (and the type Type -> X) + Sledgehammer would make him quit Lean without thinking twice (which looks like a very sensible thing to do).

#### Kevin Buzzard (Dec 03 2019 at 17:35):

theorem finite_dimensional_span_of_finite {V : Type} [normed_group V] [normed_space ℝ V] {A : set V} (hA : finite A) :
finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
apply finite_dimensional.of_fg,
sorry
end


Now we need a finset from a finite set

#### Kevin Buzzard (Dec 03 2019 at 17:37):

He was very clear Isabelle/HOL is unusable for maths. And also very clear that any system giving him dependant type (and the type Type -> X) + Sledgehammer would make him quit Lean without thinking twice (which looks like a very sensible thing to do).

So we need to make a sledgehammer? Then he'll quit Lean for Lean.

#### Patrick Massot (Dec 03 2019 at 17:41):

Look at the discussion we are having. How could we say this software is usable if two non-beginners cannot prove finite_dimensional_span_of_finite within 10 seconds?

#### Patrick Massot (Dec 03 2019 at 17:43):

Of course we don't know the linear algebra part of the library, but this was Sébastien main point: sledgehammer makes knowing the library much much less important.

#### Patrick Massot (Dec 03 2019 at 17:44):

Jasmin's project http://matryoshka.gforge.inria.fr/ was meant to solve this problem, but it doesn't seem to progress much :sad:

#### Kevin Buzzard (Dec 03 2019 at 17:44):

I see -- so this is the sort of thing which Sledgehammer does quickly?

#### Kevin Buzzard (Dec 03 2019 at 17:47):

Of course this result is easily provable, we just have to look through the library and learn the relevant parts (except that I need to leave the office in 10 minutes and I'm trying to finish a grant proposal before that ;-) )

#### Wojciech Nawrocki (Dec 03 2019 at 17:49):

sledgehammer makes knowing the library much much less important

I found this to be the nicest thing about sledgehammer in Isabelle, even more so than the fact that it gives you a proof. The generated snippet is a proof of the goal at hand, but more importantly it contains a list of lemmas which can be used to prove it. Effectively, it's like library_search on steroids, because it automatically finds relevant facts - you can look at the lemmas it found and use them to write a nicer proof.

#### Kevin Buzzard (Dec 03 2019 at 17:53):

Then what is our long-term plan for getting a sledgehammer for Lean?

#### Gabriel Ebner (Dec 03 2019 at 17:55):

Then what is our long-term plan for getting a sledgehammer for Lean?

Me moving to Amsterdam. :smile: I'll talk about the current status in January.

#### Sebastien Gouezel (Dec 03 2019 at 17:58):

Yes, he was finishing his talk at that moment. It was very nice talk. He explained maths for 15 minutes, then propaganda for Sledgehammer for 30 minutes then 15 minutes about how simple type theory is unfortunately unbearable.

I think that's a fair summary. I also said that Sledgehammer makes the learning curve much smoother in Isabelle/HOL than in Lean or COQ.

#### Sebastien Gouezel (Dec 03 2019 at 18:00):

He was a bit unfair to Lean though. He explained how Lean is harder to read than Isabelle by comparing tactic scripts on a white background with proof terms on a black background (using a video beamer making it impossible to read VScode's default dark theme).

The point is that, proof terms don't exist in Isabelle, and this proof in Isabelle would just have been done by automation without needing to think at all. While a tactic proof in Lean would not have been nicer than the term proof. So, I don't think I have been really unfair :)

#### Rob Lewis (Dec 03 2019 at 18:00):

Jasmin's project http://matryoshka.gforge.inria.fr/ was meant to solve this problem, but it doesn't seem to progress much :sad:

I don't think that's fair at all, the higher order proving work that they're doing is great progress.

#### Lambert A'Campo (Dec 03 2019 at 18:29):

Thanks for the extensive discussion. So do I understand correctly that I cannot use this lemma unless R and V have the same type? I find this very strange.

#### Lambert A'Campo (Dec 03 2019 at 18:39):

When I try to prove this theorem I need to transform A : set V to A set ↥(submodule.span ℝ A)... How does that work?

theorem finite_dimensional_span_of_finite {V : Type} [normed_group V] [normed_space ℝ V] {A : set V} (hA : finite A) :
finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
apply finite_dimensional.of_fg,
rw submodule.fg_def,
existsi (A : set ↥(submodule.span ℝ A)),
end


#### Kevin Buzzard (Dec 03 2019 at 19:36):

Things which mathematicians think of as equal are perhaps not equal in type theory. The submodule.span has type submodule ℝ V and probably A has type set V, but when you start talking about the span as an abstract vector space you want A to be a subset of the span, so the span needs to become a type (the ↥) rather than a term, and then A needs to be changed from set V to set <the finite-dimensional space>.

#### Kevin Buzzard (Dec 03 2019 at 19:39):

I don't think that's fair at all, the higher order proving work that they're doing is great progress

I don't know anything about what they're doing. I looked at the website and it didn't seem to mention Lean. So the plan is their work + Gabriel will result in a sledgehammer for Lean? This makes me happy, I am somehow convinced that Gabriel can do anything :D

#### Sebastien Gouezel (Dec 03 2019 at 19:57):

So do I understand correctly that I cannot use this lemma unless R and V have the same type? I find this very strange.

Not the same type, the same universe. This is an issue with the linear algebra library, that requires vector spaces to be in the same universe to define linear equivalences between them. But in practice one can do all mathematics in a single universe, so this is not a real issue.

#### Kevin Buzzard (Dec 03 2019 at 20:21):

But in practice one can do all mathematics in a single universe, so this is not a real issue.

That is not the message we get from the CS people. They assure us that it is important that we be maximally universe polymorphic. Is there an actual reason why this design decision was made or was it just for convenience?

Clark Barwick gave a talk at Imperial yesterday and when he was talking about pyknotic sets he had to fix a strongly inaccessible cardinal. This is a point where one really cannot do mathematics in a single universe. Scholze's condensed sets are a variant of this which does not need the inaccessible cardinal, however Scholze ends up with a slightly different class of objects (and he has to jump through a lot of set-theoretic hoops, choosing uncountable cardinals with properties whose existence can be proved in ZFC). We have to make a decision about whether to follow Scholze's point of view or Barwick's, and Barwick's would be much easier to do in Lean, although his pyknotic sets will end up having type Type 1, so pyknotic vector spaces are not going to work in Lean.

#### Mario Carneiro (Dec 03 2019 at 20:34):

But in practice one can do all mathematics in a single universe, so this is not a real issue.

I think that should read "in principle one can do all mathematics in a single universe". In practice you run into exactly the issues that Lambert is noting. Do we have a comprehensive set of instances on ulift? (Including a ulift_instance tactic for making more instances.) If so, it might be possible to work around this by using ulift R as the scalar ring, but it's not a particularly natural solution to work with.

#### Kevin Buzzard (Dec 03 2019 at 20:35):

And what about the solution of making mathlib properly polymorphic? Why is it not polymorphic here?

#### Sebastien Gouezel (Dec 03 2019 at 20:35):

What prevents you from adding a large cardinal axiom and doing exactly his construction in Type? (Note that I wouldn't mind using the additional flexibility of type theory to simplify things, but my point is that everything you do in usual mathematics with set theory should be doable in Type).

#### Kevin Buzzard (Dec 03 2019 at 20:36):

What prevents you from adding a large cardinal axiom and doing exactly his construction in Type? (Note that I wouldn't mind using the additional flexibility of type theory to simplify things, but my point is that everything you do in usual mathematics with set theory should be doable in Type).

Nothing, I believe. Except then you'll have an extra axiom which somehow looks silly in Lean because it basically says "assume Type -1 exists".

#### Kevin Buzzard (Dec 03 2019 at 20:36):

The obvious response is "why not renumber?"

#### Kevin Buzzard (Dec 03 2019 at 20:39):

And to be honest if we're going to start using cardinal bounds then we may as well do it the Scholze way anyway, because proving the existence of an uncountable strong limit cardinal (a fun exercise for you Mario? ;-) ) will be possible in Lean without any extra axioms.

#### Kevin Buzzard (Dec 03 2019 at 20:39):

(what we need is an uncountable $\kappa$ such that $\lambda<\kappa\implies 2^{\lambda}<\kappa$)

#### Kevin Buzzard (Dec 03 2019 at 20:42):

(proof: define a sequence of cardinals $\kappa_\alpha$ for $\alpha$ an ordinal by $\kappa_0=\aleph_0$, $\kappa_{\alpha+1}=2^{\kappa_\alpha}$, and unions at limits; then $\kappa_\alpha$ for any (positive) limit ordinal will do the trick)

#### Sebastien Gouezel (Dec 03 2019 at 20:45):

I don't know where the root of polymorphism loss is, but dimension.lean starts with the line

variables {K : Type u} {V V₂ V₃ V₄ : Type v}


And since this file was written by Mario and Johannes I am pretty sure there is a very good reason for this.

#### Sebastien Gouezel (Dec 03 2019 at 20:46):

Probably when you have maps between these modules you want to compare their dimensions, which are cardinals in some fixed universe.

#### Kevin Buzzard (Dec 03 2019 at 20:48):

Probably you sometimes want to compare their dimensions, but you often do not? That's like saying that equiv should only take two types from the same universe because sometimes you might want to compare their cardinalities. That is not what is done there. I am confused.

#### Sebastien Gouezel (Dec 03 2019 at 20:49):

For instance

theorem linear_equiv.dim_eq (f : V ≃ₗ[K] V₂) :
dim K V = dim K V₂


does not make sense if V and V_2 are not in the same universe, as their dimensions don't live in the same place.

#### Kevin Buzzard (Dec 03 2019 at 20:50):

So that one theorem could be formalised under the assumption that the universes are the same.

#### Sebastien Gouezel (Dec 03 2019 at 20:50):

That's the first statement that breaks in this file if I change the universe constraints, but there are many more below. But I agree with you that it would make sense to only assume the same universe when it is really necessary.

#### Kevin Buzzard (Dec 03 2019 at 20:51):

or some ulift nonsense could be added. There are ways around this and all I am saying is that I am surprised that this design decision was taken by people who take universe polymorphism so seriously.

#### Kevin Buzzard (Dec 03 2019 at 20:53):

Of course the Barwick example is very much an extreme case. I absolutely agree with you that 99% of modern maths can be done within one universe. I'm sure Lambert doesn't want to assume the existence of an inaccessible cardinal in his proof so he could change V to have type Type and not lose too much sleep about it.

Can the finite-dimensionality proof be made into an instance?

#### Sebastien Gouezel (Dec 03 2019 at 20:53):

Sorry, which proof?

#### Kevin Buzzard (Dec 03 2019 at 20:58):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Span.20of.20finite.20set.20is.20sequentially.20closed/near/182481084

finite_dimensional is a class but finite is not.

#### Kevin Buzzard (Dec 03 2019 at 20:59):

Oh -- this does not even compile for me! I thought Lambert had done it!

#### Kevin Buzzard (Dec 03 2019 at 20:59):

sorry the proof for now :D

#### Sebastien Gouezel (Dec 03 2019 at 21:00):

It doesn't look like an instance. It could be one if you replaced your finite set by a finset, I guess.

#### Mario Carneiro (Dec 03 2019 at 21:01):

There are a few statements in there that require the universe restriction to typecheck, but I'm wary about having that be in the variables list because this is likely to carry the restriction through to other theorems that don't have the restriction

#### Kevin Buzzard (Dec 03 2019 at 21:01):

I'm pretty sure that Lambert's result doesn't need V to be in Type.

#### Sebastien Gouezel (Dec 03 2019 at 21:03):

In the dimension file, most of the statements require it, as they talk about dimensions as cardinals. However, when one uses these results to prove things on findim, this imposes the universe restriction in situations where it shouldn't be needed any more.

#### Lambert A'Campo (Dec 03 2019 at 21:07):

Oh -- this does not even compile for me! I thought Lambert had done it!

I have not haha. I just changed V : Type* to V:Type (I don't understand what this means anyways.) and I now I am just left with this nonsensical theorem that the span of a finite set is finite dimensional but I don't know how to prove it because I don't understand the coercion stuff.

#### Lambert A'Campo (Dec 03 2019 at 21:10):

I tried this but now I don't know how to prove things about B...

theorem finite_dimensional_span_of_finite {V : Type} {A : set V} [normed_group V] [normed_space ℝ V] (hA : finite A) :
finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
apply finite_dimensional.of_fg,
rw submodule.fg_def,
let B : set ↥(submodule.span ℝ A) := {b | ∃ a : V, a ∈ A ∧ a = b},
existsi B,
sorry
end


#### Patrick Massot (Dec 03 2019 at 21:11):

Jasmin's project http://matryoshka.gforge.inria.fr/ was meant to solve this problem, but it doesn't seem to progress much :sad:

I don't think that's fair at all, the higher order proving work that they're doing is great progress.

I'm very sorry I wrote that too quickly. I was trying to help Lambert, report on Sébastien's talk and cook dinner for my kids in a 10 minutes time slot (on top of the frustration boost I get each time I see sledgehammer). I should have written that end users don't see any progress so far. But I understand there is foundational work to be done, and I'm very excited to read it's progressing (and Gabriel is helping).

#### Sebastien Gouezel (Dec 03 2019 at 21:23):

Something along the lines of

theorem finite_dimensional_of_finite_span {A : set V} (hA : set.finite A):
finite_dimensional K (submodule.span K A) :=
begin
apply is_noetherian_of_fg_of_noetherian,
exact submodule.fg_def.2 ⟨A, hA, rfl⟩,
end


#### Kevin Buzzard (Dec 03 2019 at 21:23):

Do we have to wait until January to hear the progress about Lean's sledgehammer?

#### Kevin Buzzard (Dec 03 2019 at 21:24):

Lambert -- you should come along to Xena and get educated by Imperial's undergraduates ;-)

#### Lambert A'Campo (Dec 03 2019 at 21:27):

Something along the lines of

theorem finite_dimensional_of_finite_span {A : set V} (hA : set.finite A):
finite_dimensional K (submodule.span K A) :=
begin
apply is_noetherian_of_fg_of_noetherian,
exact submodule.fg_def.2 ⟨A, hA, rfl⟩,
end


Thank you! That did it.

#### Lambert A'Campo (Dec 03 2019 at 21:28):

Lambert -- you should come along to Xena and get educated by Imperial's undergraduates ;-)

Yeah I want to come, I just didn't have time on Thursdays so far. But the unit ball compact -> finite dimensional proof is now complete !

#### Floris van Doorn (Dec 03 2019 at 21:32):

And to be honest if we're going to start using cardinal bounds then we may as well do it the Scholze way anyway, because proving the existence of an uncountable strong limit cardinal (a fun exercise for you Mario? ;-) ) will be possible in Lean without any extra axioms.

Mario already did this fun exercise:
https://github.com/leanprover-community/mathlib/blob/master/src/set_theory/cofinality.lean#L488

#### Floris van Doorn (Dec 03 2019 at 21:33):

Unless I misunderstand, and you want a strong limit ordinal in Type 0.

#### Patrick Massot (Dec 03 2019 at 21:38):

This certainly looks like a hole in mathlib (whose finite dimensional stuff is very sketchy). Shoud it be PRed? Probably something like:

variables (R : Type*) [comm_ring R] [is_noetherian_ring R]

theorem is_noetherian_span_of_finite {V : Type*} {A : set V} [add_comm_group V] [module R V] (hA : finite A) :
is_noetherian R (submodule.span R A) :=
is_noetherian_of_fg_of_noetherian _ (submodule.fg_def.mpr ⟨A, hA, rfl⟩)

variables (K : Type*) [discrete_field K]

theorem finite_dimensional_span_of_finite {V : Type*} {A : set V} [add_comm_group V] [vector_space K V] (hA : finite A) :
finite_dimensional K (submodule.span K A) :=
is_noetherian_span_of_finite K hA


PRed in noetherian.lean and finite_dimensional.lean

#### Kevin Buzzard (Dec 03 2019 at 21:46):

Oh that's totally the correct way to do it :-) Finitely-generated modules over a Noetherian ring are Noetherian, and hence finitely-generated vector spaces are finite-dimensional :D That's absolutely great :D My mind was muddied by the fact that they teach finite-dimensional vector spaces several years before Noetherian modules!

#### Patrick Massot (Dec 03 2019 at 21:48):

Seriously, that linear algebra library is really really hard to use. What Lambert was trying to do was completely natural, but ended up with had_coe_to_sort hell.

#### Kevin Buzzard (Dec 03 2019 at 21:51):

I think that if a part of the library is new to someone then they often find it hard to use.

#### Patrick Massot (Dec 03 2019 at 21:53):

In the topology part there is nothing that would get you stuck like Lambert was.

#### Johan Commelin (Dec 04 2019 at 08:11):

@Sebastien Gouezel Is there a recording of your talk? (With subtitles :grimacing:)

#### Patrick Massot (Dec 04 2019 at 08:49):

I think there will be video available soon (without subtitles).

#### Patrick Massot (Dec 04 2019 at 08:53):

I asked and immediately got a temporary url: https://webdiff.math.u-psud.fr/5de68f39862d2a0419e311ed

#### Patrick Massot (Dec 04 2019 at 08:56):

I have no idea why they kept the streams from cameras looking at the audience, especially since they were zooming on mostly empty areas of the lecture room.

#### Johan Commelin (Dec 04 2019 at 08:59):

Thanks for the link. I'll see if I can get anything out of it (-;

Last updated: May 09 2021 at 09:11 UTC