## Stream: maths

### Topic: Removing duplicates from an open cover

#### 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!

#### Johan Commelin (Apr 26 2021 at 06:47):

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

#### 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?

#### 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

#### 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?

#### Justus Springer (Apr 26 2021 at 07:01):

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

#### Johan Commelin (Apr 26 2021 at 07:03):

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

#### 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

#### 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 $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 $s\in\mathcal{O}_X(D(f))$ and want to find a representation of $s$ as a fraction $a/f^n$. We already know that we can cover $D(f)$ with finitely many $D(h_i)$, where on each $D(h_i)$, we have $s$ represented as some $a_i/h_i$. From $D(f)\subset\bigcup_iD(h_i)$ we can conclude that $f\in\sqrt{\langle h_1,...,h_r\rangle}$, therefore $f^n=\sum b_ih_i$. We need this to define $a:=\sum b_ia_i$.

The problem is: Hartshorne just enumerates the $h_i$ as $h_1,...,h_r$. In Lean, I'm working with some index set $\iota$ and $h:\iota\to R$ and a finset $t \subset\iota$. I the conclude $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 $t$, which I need because I can only define $a$ this way

#### Kevin Buzzard (Apr 26 2021 at 07:19):

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

#### Justus Springer (Apr 26 2021 at 07:20):

Kevin Buzzard said:

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

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

#### 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 $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 $s\in\mathcal{O}_X(D(f))$ and want to find a representation of $s$ as a fraction $a/f^n$. We already know that we can cover $D(f)$ with finitely many $D(h_i)$, where on each $D(h_i)$, we have $s$ represented as some $a_i/h_i$. From $D(f)\subset\bigcup_iD(h_i)$ we can conclude that $f\in\sqrt{\langle h_1,...,h_r\rangle}$, therefore $f^n=\sum b_ih_i$. We need this to define $a:=\sum b_ia_i$.

The problem is: Hartshorne just enumerates the $h_i$ as $h_1,...,h_r$. In Lean, I'm working with some index set $\iota$ and $h:\iota\to R$ and a finset $t \subset\iota$. I the conclude $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 $t$, which I need because I can only define $a$ this way

#### Kevin Buzzard (Apr 26 2021 at 07:20):

What is the problem with defining $a$?

#### Kevin Buzzard (Apr 26 2021 at 07:22):

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

#### Justus Springer (Apr 26 2021 at 07:23):

I only have $f^n=\sum_{x\in h(t)}b(x)\cdot x$, for a function $b\colon R\rightarrow R$. On the other hand $a\colon\iota\rightarrow R$, so I can't define the sum $\sum_i a_i\cdot b_i$ because $b_i$ doesn't make sense

#### Kevin Buzzard (Apr 26 2021 at 07:24):

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

#### 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\subset\iota$. I don't know how I would convert that into a sequence $h_1,...,h_r$...

#### 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.

#### Justus Springer (Apr 26 2021 at 07:26):

Kevin Buzzard said:

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

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

#### Justus Springer (Apr 26 2021 at 07:26):

Justus Springer said:

Kevin Buzzard said:

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

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

#### Kevin Buzzard (Apr 26 2021 at 07:26):

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

#### Kevin Buzzard (Apr 26 2021 at 07:26):

set (set D f)

#### 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?

#### 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)

#### 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

#### Justus Springer (Apr 26 2021 at 07:30):

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

#### 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 $R$ in some sense...

#### Kevin Buzzard (Apr 26 2021 at 07:32):

Your iota can just be the finset

#### Kevin Buzzard (Apr 26 2021 at 07:32):

or the set of all basic opens

#### Kevin Buzzard (Apr 26 2021 at 07:33):

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

#### Justus Springer (Apr 26 2021 at 07:34):

Right, so I need to choose something after all!

I would imagine.

#### Kevin Buzzard (Apr 26 2021 at 07:35):

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

#### 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

#### Justus Springer (Apr 26 2021 at 07:37):

Together with the fact that basic opens are compact

#### Justus Springer (Apr 26 2021 at 07:37):

Anyway, thanks so much for your input so far!

#### Kevin Buzzard (Apr 26 2021 at 07:37):

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

#### Kevin Buzzard (Apr 26 2021 at 07:38):

because different $h_i$ can give the same subsets $D(h_i)$

#### Kevin Buzzard (Apr 26 2021 at 07:40):

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

#### Justus Springer (Apr 26 2021 at 07:40):

I mean "finitely many elements $h_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

#### Kevin Buzzard (Apr 26 2021 at 07:40):

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

#### Justus Springer (Apr 26 2021 at 07:41):

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

#### Justus Springer (Apr 26 2021 at 07:42):

Kevin Buzzard said:

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

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

#### 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.

#### Kevin Buzzard (Apr 26 2021 at 07:44):

No, I've still not got it right

#### Kevin Buzzard (Apr 26 2021 at 07:44):

you want iota : finset R to be the $h$'s

#### 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 $x\in D(f)$, there exists an $a_x, h_x\in R$ such that $s=a_x/h_x$ on $D(h_x)$.

#### Justus Springer (Apr 26 2021 at 07:47):

(and $x\in D(h_x)$)

#### 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)/h$ on D h for h \in iota?

#### Kevin Buzzard (Apr 26 2021 at 07:50):

This would solve your problems, right?

#### Justus Springer (Apr 26 2021 at 07:50):

Aha I think I see what you mean now

#### Justus Springer (Apr 26 2021 at 07:51):

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

#### 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

#### Kevin Buzzard (Apr 26 2021 at 07:53):

:-/ Formalisation is hard sometimes :-(

#### 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

#### Kevin Buzzard (Apr 26 2021 at 07:54):

My guess is that my suggestion is ultimately less work

#### 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.

#### Kevin Buzzard (Apr 26 2021 at 09:38):

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

#### 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.

#### Patrick Massot (Apr 26 2021 at 09:38):

But otherwise this is a legitimate question.

#### Patrick Massot (Apr 26 2021 at 09:39):

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

#### 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


#### Patrick Massot (Apr 26 2021 at 09:40):

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

#### Justus Springer (Apr 26 2021 at 10:18):

That's great, thanks!

#### 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...

#### 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?

#### Justus Springer (Apr 26 2021 at 10:23):

I agree writing univis better

#### Patrick Massot (Apr 26 2021 at 10:43):

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

#### Justus Springer (Apr 26 2021 at 10:46):

Oh that makes sense, I see

#### 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.

#### 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

#### 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 $f^n\in \sqrt{\langle h(t) \rangle}$ that there is finitely supported function $b:\iota\to R$ such that $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:=\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

#### 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"

#### 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