Appearance of quot.sound in equiv_like.surjective

Stream: maths

[Roselyn Baxter]

So I really enjoy taking care to prove results using only precisely the axioms needed for the result to hold, and I've eliminated the need for any axioms in a certain theorem except quot.sound, which seems to come from equiv.surjective. That one in turn is defined as equiv_like.surjective, which is given as

 protected lemma surjective (e : E) : function.surjective e := (right_inv e).surjective

However, right_inverse.surjective and equiv_like.right_inv both list 'no axioms' when I call #print axioms, so why does equiv_like.surjective list quot.sound?

[Eric Wieser]

I would guess it comes from docs#equiv.equiv_like

[Roselyn Baxter]

Eric Wieser said:

I would guess it comes from docs#equiv.equiv_like

Calling #print axioms equiv.equiv_like also list 'no axioms', is that what you meant?

[Roselyn Baxter]

Also, quot.sound is present in equiv_like.surjective which should have nothing to do with equiv, right?

[Yaël Dillies]

It wouldn't be so surprising either, because quot.sound is used to prove function extensionality in Lean.

[Roselyn Baxter]

I'm not so much surprised that it's there, but I am curious why it's so hard to see when specifically it's invoked.

[Floris van Doorn]

the reason is stupid: in the statement of equiv_like.surjective there is a coercion to functions. This coercion uses the instance docs#equiv_like.to_embedding_like, which uses function extensionality, hence quot.sound.

[Roselyn Baxter]

Ah! Thank you very much :)

[Roselyn Baxter]

Guess I'm rewriting my own then haha

[Roselyn Baxter]

/- `equiv.surjective` relies on `quot.sound` because `equiv_like.surjective` coerces the equivalence to
a function, which calls `equiv_like.to_embedding_like`, which uses function extensionality to prove
injectivity. In other words, entirely unnecessary to prove this lemma. -/
private lemma equiv.surjective_nofunext {α β : Type*} (e : α ≃ β) : surjective e.to_fun :=
λ y, ⟨e.inv_fun y, e.right_inv y⟩

private lemma equiv_exists_surj {α β γ δ : Type*}
: α ≃ γ → β ≃ δ → ((∃ f : β → α, surjective f) ↔ (∃ f : δ → γ, surjective f)) :=
begin
  intros e₁ e₂,
  split; rintros ⟨f,surjf⟩,
    use (e₁.to_fun ∘ f ∘ e₂.inv_fun),
    apply surjective.comp,
      exact equiv.surjective_nofunext e₁,
    apply surjective.comp,
      exact surjf,
    exact equiv.surjective_nofunext e₂.symm,
  use (e₁.inv_fun ∘ f ∘ e₂.to_fun),
  apply surjective.comp,
    exact equiv.surjective_nofunext e₁.symm,
  apply surjective.comp,
    exact surjf,
  exact equiv.surjective_nofunext e₂,
end

#print axioms equiv_exists_surj -- no axioms

Beautiful.

[Eric Wieser]

Where's function extensionality being used? Is it in docs#function.left_inverse.eq_right_inverse?

[Eric Rodriguez]

yeah, comp_eq_id is literally funext