Zulip Chat Archive

Stream: maths

Topic: Removing duplicates from an open cover


view this post on Zulip Justus Springer (Apr 26 2021 at 06:23):

Hi everyone,

so I'm working on a PR in algebraic geometry and I'm almost done! If you want to check out my progess, my branch is called structure_sheaf_basic_opens_iso. There is just one sorry left, which I can't seem to get rid of (in the proof of to_basic_open_surjective, you can safely ignore everything else if you want). The situation is: I have a finite open cover of basic_open f by finitely many basic_open (h i), for h : ι → R. Later, I need to rewrite withfinset.sum_image, which requires all the h i to be distinct. If I could prove that all opens of the cover are distinct, I would be done. I feel like this is so annoyingly trivial, because surely you can just "leave out any duplicates, which is fine because it would still be a finite cover", but I can't seem to formalize this argument. Here's a #mwe:

import topology.opens

open topological_space

variables (X : Type*) [topological_space X] {ι : Type*}

lemma foo (U : ι  opens X) (t : finset ι) (hU : X =  i  t, (U i).1) :
   (s : finset ι) (hs : s  t), (X =  i  s, (U i).1)  ( i j  s, U i = U j  i = j) :=
begin
  sorry
end

If anyone wants to help me out, so that I can make that PR sooner rather than later, I'd be very thankful!

view this post on Zulip Johan Commelin (Apr 26 2021 at 06:47):

Sounds like we're not putting strong enough conditions on the covers that we're producing...

view this post on Zulip Yaël Dillies (Apr 26 2021 at 06:53):

Surely we can prove another version of the same lemma with the extra result that the opens are all distinct, or write a lemma that given a cover we can can get a cover without duplicates (maybe there's even a more general pattern behind it?). What's the lemma you're getting your opens out of?

view this post on Zulip Justus Springer (Apr 26 2021 at 06:59):

I start with an infinte cover, with one neighborhood for each point, and then pass to a finite cover using is_compact.elim_finite_subcover

view this post on Zulip Sebastien Gouezel (Apr 26 2021 at 07:01):

This looks like an #xy problem to me. Normally, the fact that your covers have distinct elements should never matter. Can you tell us more on where you would need this condition?

view this post on Zulip Justus Springer (Apr 26 2021 at 07:01):

The most general pattern I could make out is this: Given any function f:XYf : X\to Y, we can always find a set AXA\subset X on which ff is injective: Just choose a right-inverse g:f(X)Xg:f(X)\to X, then g(f(X))Yg(f(X))\subset Y is our subset. Basically just choose one preimage in every fiber of ff

view this post on Zulip Johan Commelin (Apr 26 2021 at 07:03):

@Justus Springer what is the algebraic geometry lemma where you need the finset.sum_image?

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:03):

Do you absolutely need to keep the index set the same? If not then you can just replace iota with opens X and t with the image

view this post on Zulip Justus Springer (Apr 26 2021 at 07:17):

Sebastien Gouezel said:

This looks like an #xy problem to me. Normally, the fact that your covers have distinct elements should never matter. Can you tell us more on where you would need this condition?

Possible, I am formalizing surjectivity of the map RfOX(D(f))R_f\to\mathcal O_X(D(f)), following Hartshorne, Prop. 2.2 (b).
The proof is somewhat bulky, but I will try to describe the situation. We have a section sOX(D(f))s\in\mathcal{O}_X(D(f)) and want to find a representation of ss as a fraction a/fna/f^n. We already know that we can cover D(f)D(f) with finitely many D(hi)D(h_i), where on each D(hi)D(h_i), we have ss represented as some ai/hia_i/h_i. From D(f)iD(hi)D(f)\subset\bigcup_iD(h_i) we can conclude that fh1,...,hrf\in\sqrt{\langle h_1,...,h_r\rangle}, therefore fn=bihif^n=\sum b_ih_i. We need this to define a:=biaia:=\sum b_ia_i.

The problem is: Hartshorne just enumerates the hih_i as h1,...,hrh_1,...,h_r. In Lean, I'm working with some index set ι\iota and h:ιRh:\iota\to R and a finset tιt \subset\iota. I the conclude fh(t)f\in\sqrt{h(t)}, which gives me a linear combination that runs over h(t). I need finset.sum_image to change that into a sum running over tt, which I need because I can only define aa this way

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:19):

What does h(t)\sqrt{h(t)} mean?

view this post on Zulip Justus Springer (Apr 26 2021 at 07:20):

Kevin Buzzard said:

What does h(t)\sqrt{h(t)} mean?

Radical of the ideal generated by the set h(t)h(t)

view this post on Zulip Justus Springer (Apr 26 2021 at 07:20):

Justus Springer said:

Sebastien Gouezel said:

This looks like an #xy problem to me. Normally, the fact that your covers have distinct elements should never matter. Can you tell us more on where you would need this condition?

Possible, I am formalizing surjectivity of the map RfOX(D(f))R_f\to\mathcal O_X(D(f)), following Hartshorne, Prop. 2.2 (b).
The proof is somewhat bulky, but I will try to describe the situation. We have a section sOX(D(f))s\in\mathcal{O}_X(D(f)) and want to find a representation of ss as a fraction a/fna/f^n. We already know that we can cover D(f)D(f) with finitely many D(hi)D(h_i), where on each D(hi)D(h_i), we have ss represented as some ai/hia_i/h_i. From D(f)iD(hi)D(f)\subset\bigcup_iD(h_i) we can conclude that fh1,...,hrf\in\sqrt{\langle h_1,...,h_r\rangle}, therefore fn=bihif^n=\sum b_ih_i. We need this to define a:=biaia:=\sum b_ia_i.

The problem is: Hartshorne just enumerates the hih_i as h1,...,hrh_1,...,h_r. In Lean, I'm working with some index set ι\iota and h:ιRh:\iota\to R and a finset tιt \subset\iota. I the conclude fh(t)f\in\sqrt{\langle h(t)\rangle}, which gives me a linear combination that runs over h(t). I need finset.sum_image to change that into a sum running over tt, which I need because I can only define aa this way

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:20):

What is the problem with defining aa?

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:22):

I see, you have an ideal generated by a set and not a sequence?

view this post on Zulip Justus Springer (Apr 26 2021 at 07:23):

I only have fn=xh(t)b(x)xf^n=\sum_{x\in h(t)}b(x)\cdot x, for a function b ⁣:RRb\colon R\rightarrow R. On the other hand a ⁣:ιRa\colon\iota\rightarrow R, so I can't define the sum iaibi\sum_i a_i\cdot b_i because bib_i doesn't make sense

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:24):

Then why not replace the D(hi)D(h_i) right at the beginning with a collection of subsets of D(f)D(f) rather than indexing over iota?

view this post on Zulip Justus Springer (Apr 26 2021 at 07:25):

Well, a sequence would be nice, it just turns out that I'm working with an indexing set ι\iota and a finset tιt\subset\iota. I don't know how I would convert that into a sequence h1,...,hrh_1,...,h_r...

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:25):

Sometimes it's convenient to work with an indexing set, sometimes it's more convenient to work with a subset. It looks like here it might be easier to work with a subset.

view this post on Zulip Justus Springer (Apr 26 2021 at 07:26):

Kevin Buzzard said:

Then why not replace the D(hi)D(h_i) right at the beginning with a collection of subsets of D(f)D(f) rather than indexing over iota?

How would I express "collection of subsets of D(f)D(f)" without an indexing set?

view this post on Zulip Justus Springer (Apr 26 2021 at 07:26):

Justus Springer said:

Kevin Buzzard said:

Then why not replace the D(hi)D(h_i) right at the beginning with a collection of subsets of D(f)D(f) rather than indexing over iota?

How would I express "collection of subsets of D(f)D(f)" without an indexing type?

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:26):

A set of subsets of D(f)D(f).

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:26):

set (set D f)

view this post on Zulip Justus Springer (Apr 26 2021 at 07:27):

Okay I need to think about that... I guess it needs to be finset (set D f) then?

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:28):

For example in the definition of topological space we have (is_open_sUnion : ∀s, (∀t∈s, is_open t) → is_open (⋃₀ s)) and here s is a term of type set (set alpha)

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:28):

and then we deduce that the union of an indexed family of open sets is open from that

view this post on Zulip Justus Springer (Apr 26 2021 at 07:30):

I see. But what would my sum ibihi\sum_i b_ih_i run over if not a finset of an indexing type iota?

view this post on Zulip Justus Springer (Apr 26 2021 at 07:32):

My open subsets have the form basic_open (h i), so I guess the topological data is intertwined doing algebra over RR in some sense...

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:32):

Your iota can just be the finset

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:32):

or the set of all basic opens

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:33):

and for each basic open you can use classical.some to extract an hih_i

view this post on Zulip Justus Springer (Apr 26 2021 at 07:34):

Right, so I need to choose something after all!

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:34):

I would imagine.

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:35):

You say "we already know we can cover D(f)D(f) with finitely many D(hi)D(h_i) where on each D(hi)D(h_i) we have ss represented as ai/hia_i/h_i" but I guess I am not sure of the Lean formalisation of the statement of that claim

view this post on Zulip Justus Springer (Apr 26 2021 at 07:36):

That statement is actually formalized, I outsourced it in a lemma locally_const_basic_open on my branch

view this post on Zulip Justus Springer (Apr 26 2021 at 07:37):

Together with the fact that basic opens are compact

view this post on Zulip Justus Springer (Apr 26 2021 at 07:37):

Anyway, thanks so much for your input so far!

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:37):

sure, but I'm asking about the precise formalisation. By "finitely many D(hi)D(h_i)" do you mean "finitely many subsets D(hi)D(h_i)" or "finitely many elements hih_i"?

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:38):

because different hih_i can give the same subsets D(hi)D(h_i)

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:40):

My impression is that your cover of D(f)D(f) should be indexed by the subset of RR consisting of hh such that D(h)D(f)D(h)\subset D(f), and then all your problems are solved.

view this post on Zulip Justus Springer (Apr 26 2021 at 07:40):

I mean "finitely many elements hih_i". I guess it boils down to the fact that is_compact.elim_finite_subcover takes in an indexed family U:\iota -> opens X rather than a set of subsets

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:40):

Right, but you'll find that there will be about 10 variants of this

view this post on Zulip Justus Springer (Apr 26 2021 at 07:41):

Then I've not yet found the one suitable for my situation :)

view this post on Zulip Justus Springer (Apr 26 2021 at 07:42):

Kevin Buzzard said:

My impression is that your cover of D(f)D(f) should be indexed by the subset of RR consisting of hh such that D(h)D(f)D(h)\subset D(f), and then all your problems are solved.

Hm, I'm not sure I understand that...

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:43):

For the proof to be natural, I'm guessing you want iota : finset R and for i : iota elements a i and h i.

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:44):

No, I've still not got it right

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:44):

you want iota : finset R to be the hh's

view this post on Zulip Justus Springer (Apr 26 2021 at 07:47):

I guess so. The problem is initially, I start out with indexing type ι = basic_open f because I prove that for each point xD(f)x\in D(f), there exists an ax,hxRa_x, h_x\in R such that s=ax/hxs=a_x/h_x on D(hx)D(h_x).

view this post on Zulip Justus Springer (Apr 26 2021 at 07:47):

(and xD(hx)x\in D(h_x))

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:48):

Don't you want to consider X : set R := {h | D h \subseteq D f} and then find iota : finset R with iota \subseteq X and D h covering D f as h ranges through iota and s=a(h)/hs=a(h)/h on D h for h \in iota?

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:50):

This would solve your problems, right?

view this post on Zulip Justus Springer (Apr 26 2021 at 07:50):

Aha I think I see what you mean now

view this post on Zulip Justus Springer (Apr 26 2021 at 07:51):

That would indeed solve my problem, because then I could define a=hιa(h)ha=\sum_{h\in\iota}a(h)\cdot h

view this post on Zulip Justus Springer (Apr 26 2021 at 07:52):

Not sure how I best go about in changing my proof now. I will give it a try

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:53):

:-/ Formalisation is hard sometimes :-(

view this post on Zulip Justus Springer (Apr 26 2021 at 07:53):

Yeah, I thought "thinning out" my open cover to eliminate duplicates would be an easy operation, so I fixated on doing it this way

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 07:54):

My guess is that my suggestion is ultimately less work

view this post on Zulip Patrick Massot (Apr 26 2021 at 09:37):

I agree with what Sébastien and Kevin wrote, but Justus' question is still legitimate. Having difficulties to formalize his strategy is really annoying.

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 09:38):

Having sUnion, Union and bUnion is annoying, but it seems necessary.

view this post on Zulip Patrick Massot (Apr 26 2021 at 09:38):

In his original lemma, there is something really wrong. He writes X = ⋃ i ∈ t, (U i).1 instead of univ = ⋃ i ∈ t, (U i).1.

view this post on Zulip Patrick Massot (Apr 26 2021 at 09:38):

But otherwise this is a legitimate question.

view this post on Zulip Patrick Massot (Apr 26 2021 at 09:39):

And it seems we are missing lots of stupid supporting lemmas. So I wrote them.

view this post on Zulip Patrick Massot (Apr 26 2021 at 09:39):

import topology.opens
import data.set.function

open set


lemma bar {ι α : Type*} (f : ι  α) :
   J : set ι, inj_on f J  f '' J = range f :=
begin
  have :  z : range f,  i, f i = z,
  { rintros z, i, rfl⟩⟩,
    exact i, rfl },
  choose g hg using this,
  refine range g,_, _⟩,
  { rintros - z, rfl - w, rfl H,
    rw [hg, hg] at H,
    rw subtype.ext H },
  ext a,
  split,
  { rintro -, ⟨⟨-, i, rfl⟩, rfl⟩, rfl⟩,
    simp [hg] },
  { rintro i, rfl⟩,
    refine g  f i, mem_range_self i⟩, mem_range_self _, _⟩,
    simp [hg] },
end

lemma bar' {ι α : Type*} (f : ι  α) (I : set ι) :
   J : set ι, J  I  inj_on f J  f '' J = f '' I :=
begin
  rcases bar (restrict f I) with J₀, h₀_inj, h⟩,
  refine ⟨(coe : I  ι) '' J₀, by simp, _, _⟩,
  { rintro - j, hj, rfl - j', hj', rfl H,
    rw h₀_inj hj hj' H },
  { have : (λ a : I, f a) '' J₀ = f '' I, by simpa using h,
    rw [ this,  image_comp] }
end

lemma set.finite_of_subset_finset {α : Type*} {I : set α} {J : finset α} (h : I  J) : finite I :=
(finset.finite_to_set J).subset h

lemma bar'' {ι α : Type*} (f : ι  α) (I : finset ι) :
   J : finset ι, J  I  inj_on f J  f '' J = f '' I :=
begin
  rcases bar' f I with J, h, h', h''⟩,
  rcases (set.finite_of_subset_finset h).exists_finset_coe with J, rfl⟩,
  exact J, h, h', h''
end

open topological_space

variables (X : Type*) [topological_space X] {ι : Type*}

lemma bUnion_eq_bUnion {ι α : Type*} {f : ι  set α} {s t : set ι} (h : f '' s = f '' t) :
  ( i  s, f i) =  i  t, f i :=
begin
  ext x,
  simp only [mem_Union],
  split,
  { rintros i, hi, hx⟩,
    have : f i  f '' t,
    { rw  h, exact mem_image_of_mem f hi },
    rcases this with j, hj, H⟩,
    exact j, hj, H.symm  hx },
  { rintros i, hi, hx⟩,
    have : f i  f '' s,
    { rw h, exact mem_image_of_mem f hi },
    rcases this with j, hj, H⟩,
    exact j, hj, H.symm  hx },
end

lemma bUnion_eq_bUnion' {ι α : Type*} {f : ι  set α} {s t : finset ι} (h : f '' s = f '' t) :
  ( i  s, f i) =  i  t, f i :=
bUnion_eq_bUnion h

lemma foo (U : ι  opens X) (t : finset ι) (hU : univ =  i  t, (U i).1) :
   (s : finset ι) (hs : s  t), (univ =  i  s, (U i).1)  ( i j  s, U i = U j  i = j) :=
begin
  rcases bar'' U t with s, hs, hs', hs''⟩,
  refine s, hs, _, _⟩,
  { rw hU,
    ext x,
    rw bUnion_eq_bUnion',
    change (subtype.val  U) '' t = (subtype.val  U) '' s,
    conv_rhs { rw [image_comp] },
    rw [image_comp, hs''] },
  { intros i j hi hj hij,
    exact hs' hi hj hij },
end

view this post on Zulip Patrick Massot (Apr 26 2021 at 09:40):

Let's first see whether someone find them in mathlib or golf them.

view this post on Zulip Justus Springer (Apr 26 2021 at 10:18):

That's great, thanks!

view this post on Zulip Justus Springer (Apr 26 2021 at 10:20):

Patrick Massot said:

Let's first see whether someone find them in mathlib or golf them.

I did have some look in the API for finsets, sets and functions on sets and couldn't find what I was looking for. But I might be missing something, after all, the finset API is pretty big...

view this post on Zulip Justus Springer (Apr 26 2021 at 10:22):

Patrick Massot said:

In his original lemma, there is something really wrong. He writes X = ⋃ i ∈ t, (U i).1 instead of univ = ⋃ i ∈ t, (U i).1.

Just to make sure I understand, could you elaborate what's wrong with writing X = ⋃ i ∈ t, (U i).1? Isn't Xcoerced to a univ : set X in this context?

view this post on Zulip Justus Springer (Apr 26 2021 at 10:23):

I agree writing univis better

view this post on Zulip Patrick Massot (Apr 26 2021 at 10:43):

No it isn't. The right hand side is coerced into a type.

view this post on Zulip Justus Springer (Apr 26 2021 at 10:46):

Oh that makes sense, I see

view this post on Zulip Patrick Massot (Apr 26 2021 at 10:53):

This distinction between X and (univ : set X) was among the things I found weird when I started using Lean. And now this flipped over. Each time I use X on paper or blackboard when I mean (univ : set X) it feels weird. I've lectured on topology earlier this year and I caught myself saying "X, seen as a subset of itself" when commenting the definition of topological spaces.

view this post on Zulip Eric Wieser (Apr 26 2021 at 15:07):

bar golfs very slightly to:

lemma bar {ι α : Type*} (f : ι  α) :
   J : set ι, inj_on f J  f '' J = range f :=
begin
  choose g hg using (subtype.prop :  z : range f,  i, f i = z),
  refine range g, _, _⟩,
  { rintros - z, rfl - w, rfl H,
    rw [hg, hg] at H,
    rw subtype.ext H },
  { rw range_comp,
    ext a,
    split,
    { rintro ⟨⟨-, i, rfl⟩, rfl⟩,
      exact _, rfl⟩},
    { rintros i, rfl⟩,
      exact ⟨⟨_, i, rfl⟩, hg _⟩} }
end

where the first have is just subtype.prop and range_comp tidies up some angle brackets

view this post on Zulip Justus Springer (Apr 29 2021 at 11:10):

To give an update on this: I finally got a working version and PR'd it: #7405
Thanks again @Kevin Buzzard and @Patrick Massot for your help! I tried implementing a solution based on Kevin's comments, unfortunately that did not quite go as expected, as the proof got quirky in other ways that are hard to describe briefly. I then found out that I could use docs#finsupp.mem_span_iff_total to directly conclude from fnh(t) f^n\in \sqrt{\langle h(t) \rangle} that there is finitely supported function b:ιR b:\iota\to R such that fn=itb(i)h(i)f^n=\sum_{i\in t} b(i)h(i). Now this sum runs over t instead of h(t), so I could easily define a:=itb(i)a(i)a:=\sum_{i\in t}b(i)a(i) just like I would on paper, no injectivity assumptions needed!
Basically I wasted a whole bunch of time on solving a problem which doesn't occur, had I just found the right lemma to use from the start. I guess knowing how to navigate big libraries efficiently and knowing what to search for really is key for formalization projects like this

view this post on Zulip Kevin Buzzard (Apr 29 2021 at 12:02):

You are experiencing exactly what I experienced when I embarked on the "trivial" process of defining a scheme in 2017. There's a great slide about this in Mario's UMD talk -- I'm on mobile right now but it was something like "after you've done a bunch of formalisation it starts to become as easy as you thought it would be before you started"

view this post on Zulip Kevin Buzzard (Apr 29 2021 at 12:05):

You're exactly right that it takes time to get on top of these subtleties. There are two or three ways to do various things (eg Union, bUnion, sUnion, or finset.sum, finsum or...) and it's a bit of a knack working out which one to use sometimes. These things are math-indistinguishable.


Last updated: Jun 17 2021 at 16:20 UTC