Zulip Chat Archive

Stream: maths

Topic: easy proof of surjective_iff_injective


view this post on Zulip Chris Hughes (Apr 06 2018 at 16:38):

Is there an easy proof of

lemma  injective_iff_surjective [fintype α] {f : α  β} (e : α  β) : injective f   surjective f

It took me 40 lines, but with stuff like this, there's often some one or two line proof.

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 16:42):

I have no idea whether this maths idea is easily leanified, but using e you can build a map alpha -> alpha (f then e to get you back to alpha), and if the collection of all such maps alpha -> alpha is known to be a fintype then you know there must exist nats a<b with f^a = f^b (f^n = f composed with itself n times).

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 16:42):

Now under either the injectivity or the surjectivity assumption you can deduce f^{b-a} = id

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 16:42):

and then f^{b-a-1} is the inverse

view this post on Zulip Chris Hughes (Apr 06 2018 at 16:52):

Sounds very doable. I'm not sure there's a power function on functions yet though.

view this post on Zulip Chris Hughes (Apr 06 2018 at 19:07):

Longer, but cooler

instance fun.monoid {α : Type*} : monoid (α  α) :=
{ mul := (),
  mul_assoc := λ _ _ _, rfl,
  one := id,
  one_mul := λ _, rfl,
  mul_one := λ _, rfl }

lemma eq_of_left_inv_of_right_inv [monoid α] {a b c : α}
    (h₁ : a * b = 1) (h₂ : c * a = 1) : b = c :=
have h₃ : c  * a * b = c * 1 := by rw [ h₁, mul_assoc],
by rwa [h₂, one_mul, mul_one] at h₃

lemma pow_mul_pow_eq_one [monoid α] {a b : α} :  n, a * b = 1  a^n * b^n = 1
| 0     := λ h, one_mul _
| (n+1) := λ h,
  by rw [pow_succ', _root_.pow_succ, mul_assoc,  mul_assoc a, h, one_mul];
  exact pow_mul_pow_eq_one n h

lemma mul_eq_one_of_mul_eq_one [fintype α] [monoid α]
    (a b : α) (h : a * b = 1) : b * a = 1 :=
have hmn :  m n, m  n  a^n = a^m :=
by_contradiction $ λ h, set.not_injective_nat_fintype
(show injective (monoid.pow a), from
λ m n h₁, by_contradiction $ λ h₂, h m, n, h₂, h₁.symm),
let m, n, hmn₁, hmn₂ := hmn in
begin
  clear _let_match,
  wlog hn : n  m using n m,
  have : 0 < m - n := nat.sub_pos_of_lt (lt_of_le_of_ne hn hmn₁.symm),
  have h₁ : a^n * b^n = a^(m - n) * a^n * b^n :=
    by rw [ _root_.pow_add, nat.sub_add_cancel hn, hmn₂],
  rw [mul_assoc, pow_mul_pow_eq_one _ h, mul_one,  succ_pred_eq_of_pos
      this, pow_succ'] at h₁,
  rw [eq_of_left_inv_of_right_inv h h₁.symm, h₁],
end

lemma surjective_iff_injective [fintype α] {f : α  α} : injective f  surjective f :=
or.cases_on (classical.em (nonempty α))
  (λ a, ⟨λ hinj, surjective_of_has_right_inverse $
    let g, hg := @injective.has_left_inverse _ a _ _ hinj in
    g, λ x, show (f * g) x = x, by rw mul_eq_one_of_mul_eq_one
        g f (id_of_left_inverse hg); refl,
  λ hsurj, injective_of_has_left_inverse $
    let g, hg := surjective.has_right_inverse hsurj in
    g, λ x, show (g * f) x = x, by rw mul_eq_one_of_mul_eq_one
        f g (id_of_right_inverse hg); refl⟩⟩)
(λ h, ⟨λ _ a, false.elim (h a), λ _ a, false.elim (h a))

view this post on Zulip Chris Hughes (Apr 06 2018 at 19:12):

Some of the monoid stuff is there already actually.

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:25):

I agree it's cooler, in the sense that you seem here to be proving what look like fundamental facts about monoids. Dumb question: is there some infinite monoid for which an element can have a left inverse which is not a right inverse?

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 19:26):

That's the sort of question asked by someone who does not have a good enough collection of monoids in their brain

view this post on Zulip Mario Carneiro (Apr 06 2018 at 19:33):

Yes. pred and succ are a perfect example of this: pred (succ n) = n but succ (pred n) != n

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 20:31):

Aah, endomorphisms of an arbitrary set are a monoid.

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 20:33):

I see. In fact a category with one object is the same thing as a monoid, and an example of a category with one object is take your favourite algebraic structure and consider structure-preserving endomorphisms of an object with that structure.

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 20:33):

Here we have the simple case of a set, i.e. no algebraic structure at all.

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 20:33):

well, maybe "the empty algebraic structure" is a better way of saying it

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 20:36):

so this (succ and pred) is a proof that the naturals are not a fintype.

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 20:55):

actually, that's circular, because Chris (and me!) uses the fact that they're infinite in the proof.

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 20:56):

Oh, +1 for use of wlog ;-)

view this post on Zulip Simon Hudon (Apr 06 2018 at 20:57):

Was wlog hard to use?

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 20:58):

No, it's just such a natural maths thing to use and it wasn't there a few weeks ago :-)

view this post on Zulip Kevin Buzzard (Apr 06 2018 at 20:58):

So just the opposite really.

view this post on Zulip Simon Hudon (Apr 06 2018 at 21:01):

Glad to hear it :)


Last updated: May 11 2021 at 00:31 UTC