Zulip Chat Archive

Stream: Is there code for X?

Topic: Preimage of finite sets


view this post on Zulip Adam Topaz (Jun 06 2020 at 18:40):

Hi everyone. I'm looking for the statement that the preimage under an injective map of a finite subset is finite, using finset. So, approximately something like this:

import data.finset
open function

example {S : Type*} {T : Type*} {f : S  T} {h : injective f} {F : finset T} :
   G : finset S, f ⁻¹' F = G := sorry

Does mathlib have anything close to this?

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:21):

There is indeed no mention of comap in finset.lean.

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:24):

finset.lean has map and image but no comap. This would be a neat little PR unless I have completely missed something.

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:25):

finset.lean must have been written by a bunch of amateurs

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:29):

Oh golly there is not even multiset.comap

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:33):

Yeah this is all a bit crazy. finset.map is defined only for embeddings, when it could be defined in general; finset.comap, which does need embeddings, is missing. multiset.map is correctly defined for all maps. @Mario Carneiro if it was decided that finset.map was worth writing over 20 lemmas for in the special case where the map was an embedding, would the same apply for multiset.comap and finset.comap?

view this post on Zulip Adam Topaz (Jun 06 2020 at 19:33):

Does something like this exist?

import data.finset
open function

open_locale classical

example {S : Type*} {T : Type*} {f : S  T} {F : finset T} :
   G : finset S, finset.image f G = F := sorry -- WRONG

Presumably this would be enough...

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:34):

That's not true unless f is surjective

view this post on Zulip Patrick Massot (Jun 06 2020 at 19:34):

Kevin, are you missing https://github.com/leanprover-community/mathlib/blob/e48c2af4f2f92c2331a912c588610db73085939d/src/data/finset.lean#L1225?

view this post on Zulip Adam Topaz (Jun 06 2020 at 19:34):

Oh ovbiously... I should take an intersection with the image (and I don't know how to do that...)

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:34):

We're going the other way Patrick (I think)

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:35):

Aah but I see what you're saying. That's a map with no injectivity assumption

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:36):

Just to be clear Adam, the issue is not how to define the function, the issue is whether it is already in mathlib

view this post on Zulip Adam Topaz (Jun 06 2020 at 19:37):

Yeah I know... I've just haven't used finsets before so it is an issue for me :)

view this post on Zulip Johan Commelin (Jun 06 2020 at 19:37):

docs#finset.preimage

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:39):

So it is there, but in set.finite, and it's called preimage not comap.

view this post on Zulip Adam Topaz (Jun 06 2020 at 19:46):

While we're here, is there something like this? (which should have been what I wrote above):

import data.finset
open function

open_locale classical

example {S : Type*} {T : Type*} {f : S  T} {F : finset T} :
  F  set.range f   G : finset S, finset.image f G = F := sorry

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:50):

This you'll need the axiom of choice for.

view this post on Zulip Adam Topaz (Jun 06 2020 at 19:50):

I'm happy with that...

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:51):

Oh -- you can do better than f '' set.univ -- we have image f.

view this post on Zulip Adam Topaz (Jun 06 2020 at 19:52):

Which namespace is that in?

view this post on Zulip Adam Topaz (Jun 06 2020 at 19:52):

Or am I missing some import?

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:54):

oh sorry! It's called range f

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:54):

docs#set.range

view this post on Zulip Adam Topaz (Jun 06 2020 at 19:55):

Thanks! I updated the code.

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:55):

It's easier to use because you don't have to prove that x \in univ.

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 19:56):

It wouldn't surprise me if this is not in the library, and my idea for how to do it is kind of a horrible mess.

view this post on Zulip Adam Topaz (Jun 06 2020 at 20:08):

It's not slick, and I don't know enough of the library to quickly fill in the sorry's, but here is a sketch -- is this what you had in mind?

import data.finset
open function

open_locale classical

example {S : Type*} {T : Type*} {f : S  T} {F : finset T} :
  F  set.range f  G : finset S, finset.image f G = F :=
begin
  refine finset.induction_on F _ _,
  {
    intro h,
    use ,
    trivial,
  },
  {
    intros a U ha ind sur,
    have h1 : U  set.range f, by sorry, -- from sur
    have h2 :  s : S, f s = a, by sorry, -- from sur
    cases ind h1 with G hG,
    cases h2 with s hs,
    use insert s G,
    rw [finset.image_insert, hs],
    refine congr_arg (insert a) hG,
  }
end

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 20:16):

    have h1 : U  set.range f,
    { intros x hx, apply sur, simp [hx]},

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 20:18):

    have h2 :  s : S, f s = a,
    { show a  set.range f,
      apply sur,
      simp},

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 20:19):

I don't know whether this apply sur is mathlib-approved, but X \sub Y is sugar for forall a, a \in X -> a \in Y so you can just apply sur like a function

view this post on Zulip Adam Topaz (Jun 06 2020 at 20:19):

You beat me to it :)
I got this:

import data.finset
open function

open_locale classical

example {S : Type*} {T : Type*} {f : S  T} {F : finset T} :
  F  set.range f  G : finset S, finset.image f G = F :=
begin
  refine finset.induction_on F _ _,
  {
    intro h,
    use ,
    trivial,
  },
  {
    intros a U ha ind sur,
    have h1 : U  set.range f,
    { intros x hx, apply sur, simp [hx]},
    have h2 :  s : S, f s = a,
    {
      suffices : a   (insert a U), by exact @sur a this,
      simp,
    },
    cases ind h1 with G hG,
    cases h2 with s hs,
    use insert s G,
    rw [finset.image_insert, hs],
    refine congr_arg (insert a) hG,
  }
end

Last updated: May 17 2021 at 16:26 UTC