# Zulip Chat Archive

## 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 := 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 (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.

#### Simon Hudon (Apr 06 2018 at 21:01):

Glad to hear it :)

Last updated: May 11 2021 at 00:31 UTC