various forms of surjectivity

Stream: new members

[Daan van Gent]

I am looking for the 'canonical proof' of the following lemma

lemma eq_of_range_eq_top {A B : submodule R M} (hAB : A ≤ B) : A = B ↔ linear_map.range (of_le hAB) = ⊤

This should best be proven from a lemma like

lemma eq_of_im_inc_eq_top {α : Type*} {a b: set α} (hab : a ≤ b) : a = b ↔ image ( inclusion hab ) ⊤ = ⊤

where we might use

lemma range_eq_top_iff_surj {α β : Type*} (f: α → β) : f '' ⊤ = ⊤ ↔ function.surjective f

• First of all I have trouble finding any of these lemmas in mathlib, but I would not be surprised if the latter two exist.
• Secondly, I have a proof for all three lemmas which to me seem longer than they should be. Maybe you have some suggestions if the lemma does not exist in mathlib already. For example

lemma eq_of_im_inc_eq_top {α : Type*} {a b: set α} (hab : a ≤ b) :
  a = b ↔ image ( inclusion hab ) ⊤ = ⊤ :=
begin
  split; intro h, {
    apply le_antisymm le_top,
    intros x _,
    use x, {
      rw h,
      finish,
    }, {
      refine ⟨ a_1, _ ⟩,
      conv_rhs { rw ← inclusion_self x },
      refl,
    }
  }, {
    apply le_antisymm hab,
    rw range_eq_top_iff_surj at h,
    intros y hy,
    let y' : coe_sort b := ⟨y,hy⟩,
    cases h y' with x' hx',
    change y'.1 ∈ a,
    rw ← hx',
    simp,
  }
end

• Lastly, I wonder if there is an easy way to prove the first lemma from the second. It feels like this should be trivial, but I keep having to reduce to sets and coercion.

[Junyan Xu]

For the last one there is docs#set.image_univ and function.surjective.range_eq. Maybe you didn't find them because you were looking for ⊤ instead of the usual spelling ("simp normal form") set.univ.

[Junyan Xu]

For the second one, here is a pure rewrite proof:

import data.set.basic
open set
lemma eq_of_im_inc_eq_top {α : Type*} {a b: set α} (hab : a ≤ b) :
  a = b ↔ image (inclusion hab) ⊤ = ⊤ :=
begin
  rw le_iff_subset at hab,
  simp_rw [top_eq_univ, image_univ, range_inclusion, eq_univ_iff_forall, set_coe.forall,
    mem_set_of, subtype.coe_mk, ← subset_def, subset.antisymm_iff, and_iff_right hab],
end

The canonical spelling of le (≤) for sets is subset (⊆); you probably had trouble finding relevant lemmas because you didn't use the preferred spelling.

[Daan van Gent]

wow thanks! that proof is pretty neat. Using your suggestions of usual spelling, I found

theorem range_iff_surjective {α β : Type*} (f: α → β) : range f = univ ↔ function.surjective f

I did not expect this would make such a difference for library_search and suggest.

[Alex J. Best]

You can try library_search! which should use a weaker version of equality when searching for matches, this may see through these differences, but it is slower because of this.