inverse

Stream: maths

[Patrick Massot]

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]

or maybe even in core?

[Kenny Lau]

interesting lemma, I've never known that

[Patrick Massot]

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

[Kenny Lau]

no I really never thought of it

[Kenny Lau]

it's really an interesting lemma

[Kenny Lau]

I wasn't being sarcastic

[Kevin Buzzard]

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

[Kenny Lau]

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]

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

[Patrick Massot]

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]

lgtm

[matt rice]

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]

added some more proofs to the above...