Stream: math-comp users

Topic: Surjectivity


view this post on Zulip Pierre Jouvelot (Apr 11 2023 at 20:36):

It seems to me that the following proposition should be a case for iinv or other codomain-, image-, or injective-related library lemmas, but I'm not able to find one that seems to work:

Lemma f_surj
      n (lt0n : 0 < n)
      (T : finType) (cardT : #|T| = n.+1) (t : n.-tuple T)
      (f : 'I_n -> T) (injf : injective f) (fint : forall i : 'I_n, f i \in t) g :
  g \in t -> exists i : 'I_n, f i = g.

Any suggestion .... or proof that it is wrong? ;)

view this post on Zulip Paolo Giarrusso (Apr 11 2023 at 22:35):

Seems you can drop that T is finite, it only needs decidable equality to implement a search over I_n?

view this post on Zulip Paolo Giarrusso (Apr 11 2023 at 22:35):

If the search failed, that'd imply having n + 1 distinct elements of t, so you'll need a pigeonhole lemma

view this post on Zulip Paolo Giarrusso (Apr 11 2023 at 22:40):

I'm sorry I can't help further; but I hope that's a helpful proof sketch at least

view this post on Zulip Laurent Théry (Apr 12 2023 at 01:39):

The statement of surjectivity looks a bit weird to me but here is one way to prove it :

Lemma f_surj n (T : eqType) (t : n.-tuple T)
  (f : 'I_n -> T) (injf : injective f) (fint : forall i : 'I_n, f i \in t) g :
  g \in t -> exists i : 'I_n, f i = g.
Proof.
suff <- : codom f =i t by case/codomP => i ->;  exists i.
have [|y /codomP[i ->]//||//] :=
    uniq_min_size _ (_ : {subset (codom f) <= t})  _.
  by rewrite map_inj_uniq // enum_uniq.
by rewrite size_map size_enum_ord size_tuple.
Qed.

view this post on Zulip Pierre Jouvelot (Apr 12 2023 at 08:58):

Thanks a lot @Laurent Théry and @Paolo Giarrusso. The lemma is indeed a bit weird (thanks for the simplification of the hypothesis, also), since it's a somewhat generalized version of a property I need within a proof related to matching problems.


Last updated: Jul 15 2024 at 21:02 UTC