Removing duplicates from an open cover

Stream: maths

[Justus Springer]

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]

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

[Yaël Dillies]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Justus Springer]

Kevin Buzzard said:

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

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

[Justus Springer]

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]

What is the problem with defining $a$?

[Kevin Buzzard]

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

[Justus Springer]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

set (set D f)

[Justus Springer]

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

[Kevin Buzzard]

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]

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

[Justus Springer]

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]

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]

Your iota can just be the finset

[Kevin Buzzard]

or the set of all basic opens

[Kevin Buzzard]

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

[Justus Springer]

Right, so I need to choose something after all!

[Kevin Buzzard]

I would imagine.

[Kevin Buzzard]

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]

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

[Justus Springer]

Together with the fact that basic opens are compact

[Justus Springer]

Anyway, thanks so much for your input so far!

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Justus Springer]

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

[Justus Springer]

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]

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]

No, I've still not got it right

[Kevin Buzzard]

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

[Justus Springer]

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]

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

[Kevin Buzzard]

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]

This would solve your problems, right?

[Justus Springer]

Aha I think I see what you mean now

[Justus Springer]

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

[Justus Springer]

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

[Kevin Buzzard]

:-/ Formalisation is hard sometimes :-(

[Justus Springer]

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]

My guess is that my suggestion is ultimately less work

[Patrick Massot]

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]

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

[Patrick Massot]

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]

But otherwise this is a legitimate question.

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Justus Springer]

That's great, thanks!

[Justus Springer]

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]

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]

I agree writing univis better

[Patrick Massot]

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

[Justus Springer]

Oh that makes sense, I see

[Patrick Massot]

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]

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]

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]

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]

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.