Zulip Chat Archive

Stream: Is there code for X?

Topic: Preimage of finite sets

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?

Kevin Buzzard (Jun 06 2020 at 19:21):

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

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.

Kevin Buzzard (Jun 06 2020 at 19:25):

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

Kevin Buzzard (Jun 06 2020 at 19:29):

Oh golly there is not even multiset.comap

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?

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

Kevin Buzzard (Jun 06 2020 at 19:34):

That's not true unless f is surjective

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?

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

Kevin Buzzard (Jun 06 2020 at 19:34):

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

Kevin Buzzard (Jun 06 2020 at 19:35):

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

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

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

Johan Commelin (Jun 06 2020 at 19:37):

docs#finset.preimage

Kevin Buzzard (Jun 06 2020 at 19:39):

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

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

Kevin Buzzard (Jun 06 2020 at 19:50):

This you'll need the axiom of choice for.

Adam Topaz (Jun 06 2020 at 19:50):

I'm happy with that...

Kevin Buzzard (Jun 06 2020 at 19:51):

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

Adam Topaz (Jun 06 2020 at 19:52):

Which namespace is that in?

Adam Topaz (Jun 06 2020 at 19:52):

Or am I missing some import?

Kevin Buzzard (Jun 06 2020 at 19:54):

oh sorry! It's called range f

Kevin Buzzard (Jun 06 2020 at 19:54):

docs#set.range

Adam Topaz (Jun 06 2020 at 19:55):

Thanks! I updated the code.

Kevin Buzzard (Jun 06 2020 at 19:55):

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

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.

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

Kevin Buzzard (Jun 06 2020 at 20:16):

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

Kevin Buzzard (Jun 06 2020 at 20:18):

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

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

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: Dec 20 2023 at 11:08 UTC