Zulip Chat Archive

Stream: Is there code for X?

Topic: Filter golf


view this post on Zulip Heather Macbeth (Feb 22 2021 at 17:52):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 18:20):

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.

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 18:21):

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.

view this post on Zulip Adam Topaz (Feb 22 2021 at 18:22):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 18:25):

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.

view this post on Zulip Johan Commelin (Feb 22 2021 at 18:27):

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

view this post on Zulip Heather Macbeth (Feb 22 2021 at 18:36):

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 β)?

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 18:37):

Presumably comparable means one is < the other?

view this post on Zulip Adam Topaz (Feb 22 2021 at 18:39):

Yeah exactly.

view this post on Zulip Heather Macbeth (Feb 22 2021 at 18:39):

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

view this post on Zulip Adam Topaz (Feb 22 2021 at 18:39):

Hmm.... yeah you're probably right

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 18:39):

Right, that's my gut instinct too

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 18:40):

But with the ideals it might work perfectly

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 18:40):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 18:41):

Or possibly vice versa

view this post on Zulip Heather Macbeth (Feb 22 2021 at 18:41):

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!

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 18:49):

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.

view this post on Zulip Heather Macbeth (Feb 22 2021 at 19:06):

Ah, this is great! I can now prove

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 19:07):

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

view this post on Zulip Heather Macbeth (Feb 22 2021 at 19:08):

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) :=

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 19:08):

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

view this post on Zulip Heather Macbeth (Feb 22 2021 at 19:08):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 19:09):

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

view this post on Zulip Heather Macbeth (Feb 22 2021 at 19:09):

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?

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 19:10):

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

view this post on Zulip Heather Macbeth (Feb 22 2021 at 19:10):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 19:11):

Yes, sorry to add the confusion! cocompact.

view this post on Zulip Adam Topaz (Feb 22 2021 at 19:11):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 19:11):

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)

view this post on Zulip Heather Macbeth (Feb 22 2021 at 19:12):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 19:12):

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

view this post on Zulip Adam Topaz (Feb 22 2021 at 19:12):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 19:26):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 19:29):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 19:41):

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.

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 19:45):

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.

view this post on Zulip Heather Macbeth (Feb 22 2021 at 20:33):

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

view this post on Zulip Heather Macbeth (Feb 22 2021 at 20:35):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 22 2021 at 20:37):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 21:25):

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?

view this post on Zulip Patrick Massot (Feb 22 2021 at 21:26):

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

view this post on Zulip Heather Macbeth (Feb 22 2021 at 21:28):

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?

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 21:29):

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

view this post on Zulip Heather Macbeth (Feb 22 2021 at 21:29):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 21:29):

The name might be wrong, we made it up

view this post on Zulip Patrick Massot (Feb 22 2021 at 21:30):

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

view this post on Zulip Patrick Massot (Feb 22 2021 at 21:31):

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

view this post on Zulip Heather Macbeth (Feb 22 2021 at 21:31):

docs#filter.cocompact

view this post on Zulip Heather Macbeth (Feb 22 2021 at 21:32):

#4666

view this post on Zulip Patrick Massot (Feb 22 2021 at 21:33):

Oh, I merged that...

view this post on Zulip Patrick Massot (Feb 22 2021 at 21:33):

:older_man:

view this post on Zulip Heather Macbeth (Feb 22 2021 at 21:33):

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

view this post on Zulip Patrick Massot (Feb 22 2021 at 21:34):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 21:35):

But actually for complex varieties I think they coincide

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 21:37):

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?

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 21:37):

(thinking of sets as principal filters)

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 21:39):

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

view this post on Zulip Heather Macbeth (Feb 23 2021 at 00:15):

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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 00:41):

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?

view this post on Zulip Patrick Massot (Feb 23 2021 at 09:53):

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

view this post on Zulip Patrick Massot (Feb 23 2021 at 09:54):

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

view this post on Zulip Patrick Massot (Feb 23 2021 at 09:57):

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.

view this post on Zulip Patrick Massot (Feb 23 2021 at 09:57):

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

view this post on Zulip Patrick Massot (Feb 23 2021 at 09:59):

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.

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 13:29):

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

view this post on Zulip Heather Macbeth (Feb 23 2021 at 16:06):

Is this analogous? Given vector bundles E1E_1, E2E_2 over manifolds M1M_1, M2M_2 respectively, one has the projections πi:M1×M2Mi\pi_i:M_1\times M_2\to M_i, and can pull back to vector bundles πiEi\pi_i{}^*E_i over M1×M2M_1\times M_2. One can then, in two ways, get a "combined" vector bundle over M1×M2M_1\times M_2:

  • π1E1π2E2\pi_1{}^*E_1\otimes \pi_2{}^*E_2 (which I have seen denoted E1E2E_1\boxtimes E_2)
  • π1E1π2E2\pi_1{}^*E_1\oplus \pi_2{}^*E_2

Presumably there's a similar story for sheaves.

view this post on Zulip Adam Topaz (Feb 23 2021 at 16:36):

Maybe you should denote the second one with \boxplus?

view this post on Zulip Adam Topaz (Feb 23 2021 at 16:37):

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

view this post on Zulip Patrick Massot (Feb 26 2021 at 11:24):

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

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 11:41):

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

view this post on Zulip Heather Macbeth (Feb 26 2021 at 15:17):

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

view this post on Zulip Patrick Massot (Feb 26 2021 at 20:01):

Oh sorry, this was a typo.

view this post on Zulip Patrick Massot (Feb 26 2021 at 20:01):

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

view this post on Zulip Patrick Massot (Feb 26 2021 at 20:07):

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

view this post on Zulip Heather Macbeth (Feb 27 2021 at 03:43):

@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

view this post on Zulip Heather Macbeth (Feb 27 2021 at 03:44):

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

view this post on Zulip Heather Macbeth (Feb 27 2021 at 03:50):

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

view this post on Zulip Patrick Massot (Feb 27 2021 at 08:30):

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.

view this post on Zulip Damiano Testa (Feb 27 2021 at 08:42):

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!

view this post on Zulip Heather Macbeth (Feb 27 2021 at 16:13):

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

view this post on Zulip Damiano Testa (Feb 27 2021 at 16:15):

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!

view this post on Zulip Heather Macbeth (Feb 27 2021 at 16:42):

@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).

view this post on Zulip Damiano Testa (Feb 27 2021 at 16:44):

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


Last updated: May 17 2021 at 16:26 UTC