easy proof of surjective_iff_injective

Stream: maths

[Chris Hughes]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Chris Hughes]

Some of the monoid stuff is there already actually.

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Aah, endomorphisms of an arbitrary set are a monoid.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Oh, +1 for use of wlog ;-)

[Simon Hudon]

Was wlog hard to use?

[Kevin Buzzard]

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

[Kevin Buzzard]

So just the opposite really.

[Simon Hudon]

Glad to hear it :)