## Stream: new members

### Topic: First Time Contributing

#### ccn (Jan 06 2022 at 20:40):

Hey there, I'd like to add the definition of rank of a set of vectors (https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets) to mathlib,

The definition of the rank of a set of vectors is the number of linearly independent vectors, so given the set { [1 0], [0 1], [a b], ... } it's rank is always going to be 2, whereas the rank of { [1 0 ] } is just 1. Another way to figure it out is to take the span of those vectors and then take the rank of it as a vector space/module.

so far I've followed this guide: https://leanprover-community.github.io/install/linux.html and I made my own branch with the changes

So far my definition looks like this :

You can see on online 1151 I replaced it with the new defn and it seems to work just fine. Should I replace all instances?

Let me know if it looks good to do a pull request, and then I can try and push it to mathlib (after I get access).

#### Kevin Buzzard (Jan 06 2022 at 21:10):

I guess you might want to look at the statements below where you are and see if there's any more finrank span stuff which you can rephrase in this new way. You t also make a little API for the definition, eg. prove that if s ⊆ t then hiv ≤ t.finrank (probably this is. called set.finrank

#### ccn (Jan 06 2022 at 21:20):

Kevin Buzzard said:

I guess you might want to look at the statements below where you are and see if there's any more finrank span stuff which you can rephrase in this new way. You should also make a little API for the definition, eg. prove that if s ⊆ t then s.finrank ≤ t.finrank (probably this is called set.finrank_mono)

Ok, I'll try to do it! What does mono stand for? And this would just be a lemma right?

#### Yaël Dillies (Jan 06 2022 at 21:21):

"monotone", aka "increasing"

#### Yaël Dillies (Jan 06 2022 at 21:21):

You can also spell it monotone finrank by using docs#monotone

#### ccn (Jan 06 2022 at 21:43):

So I'm starting to work on the proof that s.finrank K <= t.finrank K So far I
have this sketch

lemma set.finrank_mono (s t: set V) : s ⊆ t → s.finrank K ≤ t.finrank K :=
begin
intro h,
-- We can prove that span s is a subset of span t using span_mono
have x := span_mono h,
-- Now I need to somehow use that with finrank
have y := finrank_mono x,
exact y,
end


span_mono:

lemma span_mono (h : s ⊆ t) : span R s ≤ span R t :=
span_le.2 \$ subset.trans h subset_span


finrank_mono

lemma finrank_mono [finite_dimensional K V] :
monotone (λ (s : submodule K V), finrank K s) :=
λ s t hst,
calc finrank K s = finrank K (comap t.subtype s)
: linear_equiv.finrank_eq (comap_subtype_equiv_of_le hst).symm
... ≤ finrank K t : submodule.finrank_le _


Thing is, that proof doesn't work too well:

image.png

Any tips to fix it?

#### Yaël Dillies (Jan 06 2022 at 21:46):

Golf it down to one line. Then Lean will be able to figure all the types out.

#### Kevin Buzzard (Jan 06 2022 at 21:48):

Right now Lean can't guess that V is a vector space over K in have x := span_mono h because h can make it guess s and t and V, but not K. That's why you get all the extra goals. As Yael says, if you write the proof in term mode (\lam h, finrank_mono (span_mono h), like span_mono) then it should work.

#### Adam Topaz (Jan 06 2022 at 21:49):

Also, this lemma is false, because finrank gives zero for infinite dim vector spaces. Are you assuming V is f.d. ahead of time?

#### Yaël Dillies (Jan 06 2022 at 21:50):

If span_mono was

lemma span_mono : monotone (span R) :=


you could even use span_mono.comp finrank_mono

#### ccn (Jan 06 2022 at 21:51):

Also, this lemma is false, because finrank gives zero for infinite dim vector spaces. Are you assuming V is f.d. ahead of time?

The file I'm working in is called finite_dimensional so I think it's good

#### Adam Topaz (Jan 06 2022 at 21:52):

The instances listed in your goal window don't show me anything about finite dimensionality

#### ccn (Jan 06 2022 at 21:53):

Yaël Dillies said:

Golf it down to one line. Then Lean will be able to figure all the types out.

I made it into one line, it is still doesn't work out: image.png

#### Yaël Dillies (Jan 06 2022 at 21:54):

Yup, because as Adam said you're missing the finite dimensionality assumption on the statement of your lemma.

#### ccn (Jan 06 2022 at 21:54):

The instances listed in your goal window don't show me anything about finite dimensionality

I'm pretty new to this too, but I think it was defined at the top of the file like this: image.png

#### Yaël Dillies (Jan 06 2022 at 21:54):

This is a definition, not a variable declaration

#### Yaël Dillies (Jan 06 2022 at 21:55):

You need variables [finite_dimensional K V]

#### Adam Topaz (Jan 06 2022 at 21:55):

Or add [finite_dimensional V] to the lemma itself

#### Adam Topaz (Jan 06 2022 at 21:57):

How are you making these nice screenshots with rectangles by the way?

#### ccn (Jan 06 2022 at 21:57):

https://github.com/flameshot-org/flameshot

#### ccn (Jan 06 2022 at 21:59):

Thanks to both of you it works out now!

#### Adam Topaz (Jan 06 2022 at 22:00):

Be careful if you're using variable ... to obtain this instance, because the assumption might not be necessary in the rest of the file.

#### Adam Topaz (Jan 06 2022 at 22:01):

If you work in a section, and put the variable inside, that should be okay

#### Adam Topaz (Jan 06 2022 at 22:03):

E.g. finrank_span_le_card doesn't need this assumption

#### ccn (Jan 06 2022 at 22:05):

I utilized the solution which adds it to the lemma itself, so I think it'll stay in the scope of the lemma.

Also I am now trying to add a "link" to it via the undergrad.yaml file:

image.png

Since my definition looks like this:

noncomputable def set.finrank (s: set V) : ℕ := finrank K (span K s)


would I have to write finite_dimensional.set.finrank ?

#### ccn (Jan 06 2022 at 22:07):

Ok, so I think most things are in order

my github account is this: https://github.com/cuppajoeman

#### Kevin Buzzard (Jan 06 2022 at 22:23):

@maintainers (BTW please let me know if pinging you all whenever someone I'm "mentoring" asks for push access is not something you guys want me to be doing)

#### Bryan Gin-ge Chen (Jan 06 2022 at 22:26):

(Pings are appreciated, on my part, at least.)

#### Eric Wieser (Jan 06 2022 at 22:59):

I was hoping there would be some way to grant Kevin special "add permissions for new users" power without going through a ping, but github doesn't seem to support it

#### Henrik Böving (Jan 06 2022 at 23:01):

We could write a zulip bots that checks whether kevin pinged maintainers and mentioned push access and a github user in the message :p

#### ccn (Jan 06 2022 at 23:07):

Looks like my pull request failed: image.png

#### Kevin Buzzard (Jan 06 2022 at 23:09):

What has failed is that you broke mathlib. If you changed a definition which was used elsewhere then I guess this would not be surprising, but if you didn't do this then that's bad luck. You can see which proof you broke. Can you fix it?

#### ccn (Jan 06 2022 at 23:16):

I found the cause of the error:

geometry/euclidean/monge_point.lean @ line 391

/-- An altitude is one-dimensional (i.e., a line). -/
@[simp] lemma finrank_direction_altitude {n : ℕ} (s : simplex ℝ P (n + 1)) (i : fin (n + 2)) :
finrank ℝ ((s.altitude i).direction) = 1 :=
begin
rw direction_altitude,
(vector_span_mono ℝ (set.image_subset_range s.points ↑(univ.erase i))),
have hc : card (univ.erase i) = n + 1, { rw card_erase_of_mem (mem_univ _), simp },
rw [s.independent.finrank_vector_span (fintype.card_fin _),
← finset.coe_image, s.independent.finrank_vector_span_image_finset hc]
end


with error

rewrite tactic failed, did not find instance of the pattern in the target expression
set.finrank ?m_1 ?m_6
state:
V : Type u_1,
P : Type u_2,
_inst_1 : inner_product_space ℝ V,
_inst_2 : metric_space P,
n : ℕ,
s : simplex ℝ P (n + 1),
i : fin (n + 2),
p : P,
hne : p ≠ s.points i,
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ finrank ℝ ↥(submodule.span ℝ {p -ᵥ s.points i}) = 1


So what I think is happening is that instead of using the standard finrank that
operates on a module:

noncomputable def finrank (R V : Type*) [semiring R]
[add_comm_group V] [module R V] : ℕ :=
(module.rank R V).to_nat


it's somehow using my new definition:

noncomputable def set.finrank (s: set V) : ℕ := finrank K (span K s)


Even though in that proof they didn't use the set.finrank syntax

#### Kevin Buzzard (Jan 06 2022 at 23:17):

If the original finrank is in the root namespace then you can try _root_.finrank and see if it fixes the problem.

#### Floris van Doorn (Jan 06 2022 at 23:19):

You can also do protected noncomputable def (or is it noncomputable protected def?) for set.finrank. This means that finrank without anything else never means set.finrank, even if you open namespace set (you'd have to write set.finrank or s.finrank when s : set _).

#### ccn (Jan 06 2022 at 23:26):

Trying out Floris's solution, I just ran leanproject build how long does that usually take?

4 hours.

#### Kevin Buzzard (Jan 06 2022 at 23:38):

Better to push and go to bed :-)

o | o

#### ccn (Jan 06 2022 at 23:39):

Ok, I'll do the push

#### Kevin Buzzard (Jan 06 2022 at 23:47):

You can subscribe to #CI and see how long it took

#### Kevin Buzzard (Jan 06 2022 at 23:47):

We hit 4 hours for the first time a couple of weeks ago

#### ccn (Jan 07 2022 at 19:04):

So I've just been fixing up some of the other lemmas that depended on finrank K (span K s) and there's one that isn't working 100%

finite_dimensional @ 1177:

lemma finrank_span_set_eq_card (s : set V) [fin : fintype s]
(hs : linear_independent K (coe : s → V)) :
s.finrank K = s.to_finset.card :=
begin
haveI := span_of_finite K ⟨fin⟩,
have : module.rank K (span K s) = #s := dim_span_set hs,
rw [←finrank_eq_dim, cardinal.mk_fintype, ←set.to_finset_card] a t this,
exact_mod_cast this
end


It seems like since I changed line 1179 to use s.finrank K that what it's trying to prove becomes a little different and causes the proof that they had to not solve it anymore:

Peek-2022-01-07-14-02.gif

I think I would need to modify this line in some way:

  have : module.rank K (span K s) = #s := dim_span_set hs,


#### ccn (Jan 07 2022 at 19:06):

I tried this out to try to fix it, but it didn't work: image.png

#### Eric Wieser (Jan 07 2022 at 19:31):

You might find you want to define s.rank K to match s.finrank K

#### ccn (Jan 07 2022 at 20:03):

Ah I see what you're hinting at

#### ccn (Jan 07 2022 at 20:11):

Would section rank be a good place to store this? Peek-2022-01-07-15-11.gif

#### ccn (Jan 07 2022 at 20:13):

My definition of s.finrank K was in section span of finite_dimensional.lean maybe, I should make a similar section in dimension.lean (that's where rank is stored) but there is no section about span there. What do you think

#### Arthur Paulino (Jan 07 2022 at 20:22):

Just an idea, I think it's easier for people to provide more precise feedback once you actually open the PR :+1:

#### Eric Wieser (Jan 07 2022 at 20:24):

I'm starting to think though that the right thing to do might be to not change any other lemmas at all, and add set.finrank solely for the purpose of the undergrad yaml

#### Eric Wieser (Jan 07 2022 at 20:25):

Because otherwise you can't apply lemmas like submodule.span_image to (e '' s).finrank, which you could apply to finrank (span R (e '' s))

#### ccn (Jan 07 2022 at 20:26):

Eric Wieser said:

#### Eric Wieser (Jan 07 2022 at 20:26):

You can write #11290 in Zulip and it will link it for you :)

Oh neat

#### ccn (Jan 07 2022 at 20:32):

Eric Wieser said:

I'm starting to think though that the right thing to do might be to not change any other lemmas at all, and add set.finrank solely for the purpose of the undergrad yaml

Yeah, it looks like it might need some design work to make it fit in with all the other existing proofs, It should still be useful though right? For future proof writers?

#### ccn (Jan 07 2022 at 20:35):

For the rollback would you want me to remove it from all of the proofs or just the ones it isn't compatible with right now?

#### Eric Wieser (Jan 07 2022 at 21:12):

I'm suggesting remove it from everywhere, but I'd encourage getting more opinions first

#### ccn (Jan 08 2022 at 20:55):

I'm getting this issue: image.png

Here's the definition I have right now:

finite_dimensional.lean

/-- The rank of a set of vectors as a natural number. -/
protected noncomputable def set.finrank (s : set V) : ℕ := finrank K (span K s)


#### Alex J. Best (Jan 08 2022 at 21:02):

Is your declaration in the finite_dimensional namespace? If it isn't contained within the lines

namespace finite_dimensional
...
end finite_dimensional


it's name will just be set.finrank no matter which file it is in

#### ccn (Jan 08 2022 at 21:05):

Alex J. Best said:

Is your declaration in the finite_dimensional namespace? If it isn't contained within the lines

namespace finite_dimensional
...
end finite_dimensional


it's name will just be set.finrank no matter which file it is in

Ah you're correct it is outside of that scope, I've made the modifications so hopefully it will pass the CI tests now, thanks

Last updated: Dec 20 2023 at 11:08 UTC