# Zulip Chat Archive

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

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

I'm not asking for irony, I'm asking whether it's already somewhere

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

#### Mario Carneiro (Mar 05 2019 at 00:22):

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