## Stream: maths

### Topic: inverse

#### Patrick Massot (Mar 04 2019 at 21:19):

I'm failing to find this in mathlib?

open function

def function.inverse {α : Type*} {β : Type*} (g : β → α) (f : α → β) :=
left_inverse g f ∧ right_inverse g f

lemma inverse_iff {α : Type*} {β : Type*} (f : α → β) (g : β → α) :
(∀ a b, f a = b ↔ a = g b) ↔ function.inverse g f :=
⟨assume h, ⟨λ a, eq.symm $(h a$ f a).1 rfl, λ b, (h (g b)  b).2 rfl⟩,
assume ⟨hl, hr⟩ a b, ⟨λ h, hl a ▸ congr_arg g h, λ h, eq.symm (congr_arg f h) ▸ (hr b)⟩⟩


#### Patrick Massot (Mar 04 2019 at 21:19):

or maybe even in core?

#### Kenny Lau (Mar 04 2019 at 21:20):

interesting lemma, I've never known that

#### Kenny Lau (Mar 04 2019 at 21:25):

no I really never thought of it

#### Kenny Lau (Mar 04 2019 at 21:25):

it's really an interesting lemma

#### Kenny Lau (Mar 04 2019 at 21:25):

I wasn't being sarcastic

#### Kevin Buzzard (Mar 04 2019 at 21:26):

Did you look in data.equiv.basic? It feels equiv-ish

#### Kenny Lau (Mar 04 2019 at 21:32):

this looks like a special case of the equivalence between the natural-bijection-formulation-of-adjunction and the unit-counit-formulation-of-adjunction

#### Johannes Hölzl (Mar 04 2019 at 21:41):

huh, I also didn't see this yet. We should add an equiv constructor for this.

#### Patrick Massot (Mar 04 2019 at 21:45):

Ok, I'll add the lemma to logic.function and a constructor in equiv.basic unless Mario tells us otherwise while I wait for the uniform split merge.

lgtm

#### matt rice (Mar 05 2019 at 15:54):

thought i would throw this up here, in case something like it was wanted as well, haven't much looked at mathlib/mathlib style yet though apologies

def inverse_rev {α : Type*} {β : Type*} {g : β → α} {f : α → β} (fg_inv : inverse g f)
: inverse f g
:= ⟨fg_inv.right,fg_inv.left⟩

def inverse_comp {α : Type*} {β : Type*} (f : α → β) (g : β → α) (fg_inv : inverse g f)
: (∀ a, (g ∘ f) a = a) ∧ (∀ b, (f ∘ g) b = b) :=
⟨fg_inv.left, fg_inv.right⟩

def inverse_comp_id {α : Type*} {β : Type*} (f : α → β) (g : β → α) (fg_inv  : inverse g f)
: (g ∘ f = id) ∧ (f ∘ g = id)
:= ⟨funext (λ a, by rw [(inverse_comp f g fg_inv).left, id]),
funext (λ b, by rw [(inverse_comp f g fg_inv).right, id])⟩

def inverse_bijective {α : Type*} {β : Type*} (f : α → β) (g : β → α) (gf_inv  : inverse g f)
: bijective f ∧ bijective g
:= have fg_inv : inverse f g, from inverse_rev gf_inv,
have injective f,
from (λ x₁ x₂, λ (h : f x₁ = f x₂),
show x₁ = x₂, by rw [<- gf_inv.left x₁, h, gf_inv.left]),
have surjective f, from (λ y, exists.intro (g y) (gf_inv.right y)),
have injective g,
from (λ y₁ y₂, λ (h : g y₁ = g y₂),
show y₁ = y₂, by rw [<- fg_inv.left y₁, h, fg_inv.left]),
have surjective g, from (λ x, exists.intro (f x) (fg_inv.right x)),
⟨⟨‹injective f›, ‹surjective f›⟩, ⟨‹injective g›, ‹surjective g ›⟩⟩


#### matt rice (Mar 10 2019 at 19:11):

added some more proofs to the above...

Last updated: May 19 2021 at 02:10 UTC