## Stream: maths

### Topic: easy proof of surjective_iff_injective

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

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

#### Kevin Buzzard (Apr 06 2018 at 16:42):

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

#### Kevin Buzzard (Apr 06 2018 at 16:42):

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

#### Chris Hughes (Apr 06 2018 at 16:52):

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

#### 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 :=
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 (Apr 06 2018 at 19:12):

Some of the monoid stuff is there already actually.

#### 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?

#### 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

#### 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

#### Kevin Buzzard (Apr 06 2018 at 20:31):

Aah, endomorphisms of an arbitrary set are a monoid.

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

#### Kevin Buzzard (Apr 06 2018 at 20:33):

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

#### Kevin Buzzard (Apr 06 2018 at 20:33):

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

#### Kevin Buzzard (Apr 06 2018 at 20:36):

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

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

#### Kevin Buzzard (Apr 06 2018 at 20:56):

Oh, +1 for use of wlog ;-)

#### Simon Hudon (Apr 06 2018 at 20:57):

Was wlog hard to use?

#### 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 :-)

#### Kevin Buzzard (Apr 06 2018 at 20:58):

So just the opposite really.