Zulip Chat Archive

Stream: maths

Topic: inverse


view this post on Zulip 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)⟩⟩

view this post on Zulip Patrick Massot (Mar 04 2019 at 21:19):

or maybe even in core?

view this post on Zulip Kenny Lau (Mar 04 2019 at 21:20):

interesting lemma, I've never known that

view this post on Zulip Patrick Massot (Mar 04 2019 at 21:23):

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

view this post on Zulip Kenny Lau (Mar 04 2019 at 21:25):

no I really never thought of it

view this post on Zulip Kenny Lau (Mar 04 2019 at 21:25):

it's really an interesting lemma

view this post on Zulip Kenny Lau (Mar 04 2019 at 21:25):

I wasn't being sarcastic

view this post on Zulip Kevin Buzzard (Mar 04 2019 at 21:26):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 05 2019 at 00:22):

lgtm

view this post on Zulip 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 ›⟩⟩

view this post on Zulip matt rice (Mar 10 2019 at 19:11):

added some more proofs to the above...


Last updated: May 19 2021 at 02:10 UTC