Filter golf

Stream: Is there code for X?

[Heather Macbeth]

Is there a slick way of proving this fact about filters?

example {α β γ δ} [topological_space γ] [topological_space δ] {f : α → γ} {g : β → δ}
  (hf : tendsto f cofinite (cocompact _)) (hg : tendsto g cofinite (cocompact _)) :
  tendsto (λ x : α × β, (f x.1, g x.2)) cofinite (cocompact _) :=

At the moment I have a long proof, but perhaps I am unpacking things that don't need to be unpacked.

import topology.subset_properties

open filter

lemma filter.tendsto.finite_preimage_compact {α : Type*} {β : Type*} [topological_space β]
  {f : α → β} (hf : tendsto f cofinite (cocompact _)) {s : set β} (hs : is_compact s) :
  set.finite (f ⁻¹' s) :=
begin
  rw [tendsto_def] at hf,
  have := hf sᶜ,
  rw mem_cofinite at this,
  convert this _,
  { simp },
  rw mem_cocompact,
  refine ⟨s, hs, rfl.subset⟩
end

example {α β γ δ} [topological_space γ] [topological_space δ] {f : α → γ} {g : β → δ}
  (hf : tendsto f cofinite (cocompact _)) (hg : tendsto g cofinite (cocompact _)) :
  tendsto (λ x : α × β, (f x.1, g x.2)) cofinite (cocompact _) :=
begin
  simp only [tendsto_def, mem_cofinite, mem_cocompact'],
  rintros s ⟨t, ht, hts⟩,
  let t₁ : set γ := prod.fst '' t,
  let t₂ : set δ := prod.snd '' t,
  have ht₁ : is_compact t₁ := ht.image continuous_fst,
  have ht₂ : is_compact t₂ := ht.image continuous_snd,
  have hft : (f ⁻¹' t₁).finite := hf.finite_preimage_compact ht₁,
  have hgt : (g ⁻¹' t₂).finite := hg.finite_preimage_compact ht₂,
  refine (hft.prod hgt).subset _,
  have : (λ x : α × β, (f x.1, g x.2)) ⁻¹' (t₁.prod t₂) = (f ⁻¹' t₁).prod (g ⁻¹' t₂),
  { ext,
    simp },
  rw ← this,
  rw ← set.preimage_compl,
  have ht' : t ⊆ t₁.prod t₂,
  { intros x hx,
    exact ⟨⟨x, hx, rfl⟩, ⟨x, hx, rfl⟩⟩ },
  refine set.preimage_mono (set.subset.trans hts ht'),
end

[Kevin Buzzard]

Nice question! I was wondering whether some filter.prod trick could help, but it seems to me that the product of the cofinite filters on alpha and beta is not the cofinite filter on alpha x beta.

One thing I noticed when thinking about filters over the last week or so is that there's this dual concept of an ideal. Just like in topological spaces where it's equivalent to carry around the open sets or the closed sets, in a parallel universe the fundamental concept turned out not to be a filter but the ideal of sets whose complements were in the filter. So you get the finite ideal, the subset-of-compact ideal etc, and the axioms are just the duals of the filter axioms -- empty set is in the ideal, shrinking an element of the ideal gives you something in the ideal, and union of two things in the ideal is in the ideal. I would imagine that there's a product of ideals, and the product of two finite ideals is the finite ideal on the product, but somehow the fact that (a + b) * (c + d) isn't ac+bd means that this doesn't translate into the product of two cofinite filters being the cofinite filter.

[Kevin Buzzard]

I guess the reason filters caught on rather than ideals is that the neighbourhood filter translates into the ideal of subsets whose closure does not contain x, which has a "not" in so it's somehow an indication that you're doing something the wrong way around.

[Adam Topaz]

They're not the same filter, but they're comparable.

[Kevin Buzzard]

The reason I mention all this is that your proof is somehow ideal-theoretic. You're trying to prove the preimage of a cocompact set is cofinite, and this is the same as proving that the preimage of a subset-of-a-compact-set is finite. But any subset-of-a-compact-set is a subset of a product of subsets-of-a-compact-set (consider projections), and a product of finite sets is finite, so done. I know you know all this, I'm just noting that because we have all this machinery for filters and perhaps less machinery for ideals you're having to turn everything around manually.

[Johan Commelin]

Note that there recently was a PR about such ideals: #5937

[Heather Macbeth]

Adam Topaz said:

They're not the same filter, but they're comparable.

@Adam Topaz This comment refers to the relationship between (cofinite : filter (α × β)) and (cofinite : filter α).prod (cofinite : filter β)?

[Kevin Buzzard]

Presumably comparable means one is < the other?

[Adam Topaz]

Yeah exactly.

[Heather Macbeth]

I see. But then presumably the same inequality holds for the relationship between cocompact (α × β) and (cocompact α).prod (cocompact β), so it doesn't help us (one inequality goes the helpful direction, one the unhelpful direction)?

[Adam Topaz]

Hmm.... yeah you're probably right

[Kevin Buzzard]

Right, that's my gut instinct too

[Kevin Buzzard]

But with the ideals it might work perfectly

[Kevin Buzzard]

I think the filter prod is something like the meet of two pulled back ideals and we want the join,

[Kevin Buzzard]

Or possibly vice versa

[Heather Macbeth]

Kevin Buzzard said:

I would imagine that there's a product of ideals, and the product of two finite ideals is the finite ideal on the product, but somehow the fact that (a + b) * (c + d) isn't ac+bd means that this doesn't translate into the product of two cofinite filters being the cofinite filter.

It'd be nice to have a name and API for this operation on filters, whatever it is!

[Kevin Buzzard]

protected def coprod (f : filter α) (g : filter β) : filter (α × β) :=
f.comap prod.fst ⊔ g.comap prod.snd

? I've got no idea if filter.coprod is a silly name for it.

[Heather Macbeth]

Ah, this is great! I can now prove

example : (cofinite : filter α).coprod (cofinite : filter β) = cofinite :=

[Kevin Buzzard]

Me too! So at least the construction isn't completely degenerate :-) Here's my effort:

import order.filter.cofinite

namespace filter

variables {α β : Type*}

protected def coprod (f : filter α) (g : filter β) : filter (α × β) :=
f.comap prod.fst ⊔ g.comap prod.snd

example (f : α → β) (S : set β) : f ⁻¹' Sᶜ = (f ⁻¹' S)ᶜ := set.preimage_compl

open set

example : filter.coprod (cofinite : filter α) (cofinite : filter β) = cofinite :=
begin
  ext S,
  unfold filter.coprod,
  simp only [exists_prop, mem_comap_sets, mem_sup_sets, mem_cofinite] at *,
  split,
  { rintro ⟨⟨A, hAf, hAS⟩, B, hBf, hBS⟩,
    rw [← compl_subset_compl, ← preimage_compl] at hAS hBS,
    let ABc := set.prod Aᶜ Bᶜ,
    have hS : Sᶜ ⊆ ABc := subset_inter hAS hBS,
    exact (finite.prod hAf hBf).subset hS,
  },
  { intro hS,
    split,
    { use (prod.fst '' Sᶜ)ᶜ,
      rw compl_compl,
      use hS.image prod.fst,
      rw [preimage_compl, compl_subset_comm],
      exact subset_preimage_image prod.fst Sᶜ },
    { use (prod.snd '' Sᶜ)ᶜ,
      rw compl_compl,
      use hS.image prod.snd,
      rw [preimage_compl, compl_subset_comm],
      exact subset_preimage_image prod.snd Sᶜ } },
end

end filter

[Heather Macbeth]

Presumably one also wants a lemma

example {α β γ δ} (a : filter α) (b : filter β) (c : filter γ) (d : filter δ) {f : α → γ} {g : β → δ}
  (hf : tendsto f a c) (hg : tendsto g b d) :
  tendsto (λ x : α × β, (f x.1, g x.2)) (a.coprod b) (c.coprod d) :=

[Kevin Buzzard]

I was rather hoping that finish could take over at some point but I never managed to get it to :-(

[Heather Macbeth]

And then some category theorist should tell us whether we're allowed to call it a coproduct :)

[Kevin Buzzard]

So of course now the question is whether there is some kind of useful tendsto.coprod

[Heather Macbeth]

Heather Macbeth said:

Presumably one also wants a lemma

example {α β γ δ} (a : filter α) (b : filter β) (c : filter γ) (d : filter δ) {f : α → γ} {g : β → δ}
  (hf : tendsto f a c) (hg : tendsto g b d) :
  tendsto (λ x : α × β, (f x.1, g x.2)) (a.coprod b) (c.coprod d) :=

Yes, this, right?

[Kevin Buzzard]

So coproduct of cofinite will be cofinite, for basically the same reasons?

[Heather Macbeth]

You mean cocompact, right? I suspect so ....

[Kevin Buzzard]

Yes, sorry to add the confusion! cocompact.

[Adam Topaz]

Heather Macbeth said:

And then some category theorist should tell us whether we're allowed to call it a coproduct :)

If this is the coproduct in the category given by the lattice stucture, then sure! (looks like it is!)

[Kevin Buzzard]

The thing is that this "product of filters" isn't some internal product, it's a map filter X x filter Y -> filter (X x Y)

[Heather Macbeth]

(I need to go teach, see you in a bit)

[Kevin Buzzard]

For all I know, filter.coprod should go to filter X \coprod Y or whatever

[Adam Topaz]

oh maybe it's not a good name then...

[Kevin Buzzard]

Heather Macbeth said:

Presumably one also wants a lemma

example {α β γ δ} (a : filter α) (b : filter β) (c : filter γ) (d : filter δ) {f : α → γ} {g : β → δ}
  (hf : tendsto f a c) (hg : tendsto g b d) :
  tendsto (λ x : α × β, (f x.1, g x.2)) (a.coprod b) (c.coprod d) :=

It's true :D

[Kevin Buzzard]

import order.filter.cofinite

namespace filter

variables {α β : Type*}

-- this corresponds to `ideal.prod`, where an ideal on a type X is
-- a set of subsets of X such that the complements of these sets
-- are a filter.
protected def coprod (f : filter α) (g : filter β) : filter (α × β) :=
f.comap prod.fst ⊔ g.comap prod.snd

open set

example : filter.coprod (cofinite : filter α) (cofinite : filter β) = cofinite :=
begin
  ext S,
  unfold filter.coprod,
  simp only [exists_prop, mem_comap_sets, mem_sup_sets, mem_cofinite] at *,
  split,
  { rintro ⟨⟨A, hAf, hAS⟩, B, hBf, hBS⟩,
    rw [← compl_subset_compl, ← preimage_compl] at hAS hBS,
    let ABc := set.prod Aᶜ Bᶜ,
    have hS : Sᶜ ⊆ ABc := subset_inter hAS hBS,
    exact (finite.prod hAf hBf).subset hS,
  },
  { intro hS,
    split,
    { use (prod.fst '' Sᶜ)ᶜ,
      rw compl_compl,
      use hS.image prod.fst,
      rw [preimage_compl, compl_subset_comm],
      exact subset_preimage_image prod.fst Sᶜ },
    { use (prod.snd '' Sᶜ)ᶜ,
      rw compl_compl,
      use hS.image prod.snd,
      rw [preimage_compl, compl_subset_comm],
      exact subset_preimage_image prod.snd Sᶜ } },
end

example {α β γ δ} (a : filter α) (b : filter β) (c : filter γ) (d : filter δ) {f : α → γ} {g : β → δ}
  (hf : tendsto f a c) (hg : tendsto g b d) :
  tendsto (λ x : α × β, (f x.1, g x.2)) (a.coprod b) (c.coprod d) :=
begin
  rw tendsto_def,
  intros s hs,
  unfold filter.coprod at hs,
  simp only [exists_prop, mem_comap_sets, mem_sup_sets] at hs,
  rcases hs with ⟨⟨C, hCc, hCs⟩, ⟨D, hDd, hDs⟩⟩,
  unfold filter.coprod,
  simp only [exists_prop, mem_comap_sets, mem_sup_sets],
  split,
  { rw tendsto_def at hf,
    specialize hf C hCc,
    use [f ⁻¹' C, hf],
    rintro ⟨aa,bb⟩ haaC,
    apply hCs,
    exact haaC },
  { rw tendsto_def at hg,
    specialize hg D hDd,
    use [g ⁻¹' D, hg],
    rintro ⟨aa,bb⟩ hbbD,
    apply hDs,
    exact hbbD },
end

end filter

[Kevin Buzzard]

About two weeks ago I would have ignored this question because I didn't know what a filter was. It was preparing last week's workshop and my current work on this week's workshop which meant that I was no longer scared of them. The way I'm thinking about filters now is that they are some kind of weird generalisation of subsets. Filters are a lattice containing the lattice of subsets (thought of as principal filters) as a sublattice, and given a filter F you can ask which subsets S have the property that F <= S. The fundamental fact about filters is that this set S of subsets determines the filter, and indeed F.sets is precisely these subsets. What about the subsets contained in F? For some reason these give far less information. This asymmetry is fixed if you model a filter by ideals; then you get some other model of a "fuzzy set" which is determined by the subsets it contains but not by the ones it's contained in. Given a subset you get a filter, the principal filter, and conversely given a filter you can just take the intersection of the subsets it is contained in and get some kind of "best approximation subset" of a filter. I am surprised that this isn't some fundamental construction, it seems to be some kind of standard adjoint functor / galois insertion thing but I couldn't find it in order.filter.basic .

That was what I learnt last week. This week I've been thinking about tendsto, and it's equally simple. If f : X -> Y and S is a subset of X and T is a subset of Y, then the concept "f restricts to a function from S to T" can be said in the following two equivalent ways: f(S) subset T, or S subset f^{-1}(T). This is the tendsto predicate on principal filters, it just says the image of set 1 is contained in set 2. image and preimage are adjoint functors between set X and set Y and because we're in this situation where all hom sets have size <= 1 (partially ordered sets like these complete lattices are categories with all hom sets having size <= 1) if you have two adjoint functors (or a Galois connection or however you want to think of it) then you get a predicate: either Hom(a,Phi b)=Hom(Psi a,b) has size 0 or size 1, and if it has size 1 then you say the predicate is satisfied. For filters this predicate is precisely tendsto, and informally tendsto f F G is the statement that the function f : X -> Y restricts to a function from the fuzzy set (F : filter X) to the fuzzy set (G : filter Y).

None of this point of view helps at all with your question! It's just that it helps me be a whole lot less scared by filters. In particular, when I was focussed on the underlying F.sets I would find the fact that <= was "backwards" really confusing -- thinking of filters as fuzzy subsets has completely eliminated this confusion.

[Kevin Buzzard]

A great example of a fuzzy set is the neighbourhood filter of a point in a topological space; the corresponding fuzzy set is an infinitesimal neighbourhood of the point in the sense of Isaac Newton. A function is continuous if the preimage of an infinitesimal nhd of f(a) contains an infinitesimal nhd of a and this is precisely tendsto (N a) (N (f a)), or in other words f doesn't just map a to f(a), it maps the infinitesimal nhd of a to the infinitesimal nhd of f(a).

Sorry, I should go back to writing all this down in a blog post rather than here! In the mean time someone needs to come along and tell us how we're re-inventing the wheel with filter.coprod.

[Heather Macbeth]

@Kevin Buzzard, mind if I add a proof of the cocompact version and then open a PR? (Or feel free to do it yourself.)

[Heather Macbeth]

Obviously, we can close the PR if someone figures out how this is a wheel-reinvention :)

[Bryan Gin-ge Chen]

If you and Kevin have been reinventing the wheel all this time, then we surely need to better document the wheel!

[Kevin Buzzard]

Please feel free to open a PR! I have three open right now which is more than my usual max and so I'd rather not open another one. My proof is a typical Kevin meandering, probably it can be cleared up. @Patrick Massot is this already a thing?

[Patrick Massot]

I haven't followed. Is the question about golfing you last big code message?

[Heather Macbeth]

TL;DR Kevin defined a notion of coproduct of filters,

protected def coprod (f : filter α) (g : filter β) : filter (α × β) :=
f.comap prod.fst ⊔ g.comap prod.snd

which is useful for the original problem. Is this a known concept?

[Kevin Buzzard]

It differs from filter.prod because we use the join not the meet

[Heather Macbeth]

Its properties:

example : filter.coprod (cofinite : filter α) (cofinite : filter β) = cofinite := sorry

example : filter.coprod (cocompact α) (cocompact β) = cocompact (α × β) := sorry

example {α β γ δ} (a : filter α) (b : filter β) (c : filter γ) (d : filter δ) {f : α → γ} {g : β → δ}
  (hf : tendsto f a c) (hg : tendsto g b d) :
  tendsto (λ x : α × β, (f x.1, g x.2)) (a.coprod b) (c.coprod d) :=
sorry

[Kevin Buzzard]

The name might be wrong, we made it up

[Patrick Massot]

I've never seen this (and the same does feel wrong)

[Patrick Massot]

The name cocompact is also weird because it makes me think of groups acting with compact quotients. Is this new?

[Heather Macbeth]

docs#filter.cocompact

[Heather Macbeth]

#4666

[Patrick Massot]

Oh, I merged that...

[Patrick Massot]

:older_man:

[Heather Macbeth]

Yury introduced it, but I found it useful today in order to work with proper maps (which are tendsto _ cocompact cocompact)

[Patrick Massot]

I'm sure Kevin has another definition for proper maps...

[Kevin Buzzard]

But actually for complex varieties I think they coincide

[Kevin Buzzard]

For this coprod name, if S is a subset of X and T is a subset of Y then the coproduct is S x Y union X x T. Does this have a name in set land? Is it some kind of box construction or something?

[Kevin Buzzard]

(thinking of sets as principal filters)

[Kevin Buzzard]

It's complement of the product of the complements for sets, but unlike sets filters don't have this canonical complement antiautomorphism

[Heather Macbeth]

#6472, anyone should feel free to suggest a better name for the construction (or we can also just rewrite to refer to it as

f.comap prod.fst ⊔ g.comap prod.snd

throughout, without naming it).

[Kevin Buzzard]

Seems to me that coprod has a natural meaning as a filter on alpha \coprod beta (push forward and then \lub). @Reid Barton do you know a good name for this construction?

[Patrick Massot]

The issue is that $\alpha \times \beta$ is not the coproduct in Type. The coproduct in Type is the sum type.

[Patrick Massot]

Also I think we can include in the PR

lemma principal_coprod_principal (s  : set α) (t : set β) :
(𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ.prod tᶜ)ᶜ :=
begin
  rw [filter.coprod, comap_principal, comap_principal, sup_principal],
  congr,
  ext x,
  simp ; tauto,
end

[Patrick Massot]

And maybe it's a good time to start including counter-examples. Here we want an example with map (prod.map f g) (a.coprod b) < filter.prod (map f a) (map g b). Using the above lemma you can make an example where all types are fin 2.

[Patrick Massot]

Also the proof of the tendsto lemma can be reduced to map_prod_map_coprod_le.trans (coprod_mono hf hg)

[Patrick Massot]

And I still don't have a good name. Maybe cross_prod since the case of principal filters is drawing a cross in the product space.

[Kevin Buzzard]

I had it in my head that there was a word for this in topology, like smash product or something, it's probably not that but in the set case this is surely construction which is useful to somebody

[Heather Macbeth]

Is this analogous? Given vector bundles $E_1$, $E_2$ over manifolds $M_1$, $M_2$ respectively, one has the projections $\pi_i:M_1\times M_2\to M_i$, and can pull back to vector bundles $\pi_i{}^*E_i$ over $M_1\times M_2$. One can then, in two ways, get a "combined" vector bundle over $M_1\times M_2$:

• $\pi_1{}^*E_1\otimes \pi_2{}^*E_2$ (which I have seen denoted $E_1\boxtimes E_2$)
• $\pi_1{}^*E_1\oplus \pi_2{}^*E_2$

Presumably there's a similar story for sheaves.

[Adam Topaz]

Maybe you should denote the second one with $\boxplus$?

[Adam Topaz]

I think this is the one which is analogous to the construction you were discussing, right?

[Patrick Massot]

@Heather Macbeth you requested my review but haven't integrated the above lemma and remove the equality question.

[Kevin Buzzard]

I really like how the proofs got even more golfed in the PR process :-)

[Heather Macbeth]

@Patrick Massot When you say "remove the equality question", this is by giving an example of

map (prod.map f g) (a.coprod b) < (map f a).coprod (map g b)

? In the discussion above you referred to an example with

map (prod.map f g) (a.coprod b) < (map f a).prod (map g b)

[Patrick Massot]

Oh sorry, this was a typo.

[Patrick Massot]

I meant map (prod.map f g) (a.coprod b) < (map f a).coprod (map g b)

[Patrick Massot]

I fear I lost the piece of paper where I wrote that counter-example. It was something like alpha = beta = gamma = delta = fin 2, f = id, g = lambda x, 1, a = b = principal {0].

[Heather Macbeth]

@Patrick Massot Thanks, indeed it works:

example {α β ι : Type*} (a : α) (b : β) (i : ι) :
  (map (λ _ : α, b) (𝓟 {a})).coprod (map id (𝓟 {i}))
  = 𝓟 (({b} : set β).prod (univ : set ι) ∪ (univ : set β).prod {i}) :=
begin
  rw [map_principal, map_principal, principal_coprod_principal],
  congr,
  ext ⟨b', i'⟩,
  simp,
  tauto,
end

example {α β ι : Type*} (a : α) (b : β) (i : ι) :
  map (prod.map (λ _ : α, b) id) ((𝓟 {a}).coprod (𝓟 {i}))
  = 𝓟 (({b} : set β).prod (univ : set ι)) :=
begin
  rw [principal_coprod_principal, map_principal],
  congr,
  ext ⟨b', i'⟩,
  split,
  { rintros ⟨⟨a'', i''⟩, h₁, ⟨h₂, h₃⟩⟩,
    simp },
  { rintros ⟨h₁, h₂⟩,
    use (a, i'),
    simpa using h₁.symm }
end

[Heather Macbeth]

Do we actually want this (a not-intrinsically-interesting counterexample) in mathlib? Maybe in archive or test?

[Heather Macbeth]

For now I just pushed the principal filter lemma and a description of the counterexample in words.

[Patrick Massot]

I would keep those as examples right after the inequality lemma. What would be really great would be to figure out how to use slim_check for this kind of things. I'm sure most wrong results about filters have this kind of counter-examples.

[Damiano Testa]

Heather, I created a counterexamples branch of mathlib, with a folder counterexamples in src: I am putting there the formalized counterexamples that I come across. There are two at the moment.

I'd be very happy if you wanted to contribute something there!

[Heather Macbeth]

@Damiano Testa For sure, I'll add it to the branch, is the plan to incorporate the branch into master at some point?

[Damiano Testa]

I think that it would be good if it appeared in mathlib, but I am happy to go with what everyone else also thinks is appropriate.

Personally, I find examples and counterexamples to be fundamental aspects of mathematics, so I would really like them to be in mathlib!

I remember many years ago reading books called `counterexamples in [topology/analysis/geometry]" and being fascinated by them!

[Heather Macbeth]

@Patrick Massot I pushed the counterexamples. @Damiano Testa I'll add them to the counterexamples branch once my PR is merged -- they rely on a new definition in the PR, filter.coprod (or maybe it will be renamed).

[Damiano Testa]

Great! Of course there is no rush! I am very happy to see the counterexamples branch grow!