Working with inverse functions

Stream: new members

[Philipp SL Schäfer]

I am currently working through MIL, and I find the definition of inverse functions rather difficult. So as an exercise I wanted to proof (g ∘ f)⁻¹ = f⁻¹ ∘ g⁻¹, and while the proof works, the definition of all inverses (following the example from MIL) is quite lengthy and I would like to know if there is a better way to approach this?

import Mathlib.Tactic

open Function
open Set
open Classical

noncomputable section

variable {X Y Z: Type*} [Inhabited X] [Inhabited Y]

variable (f: X → Y)
def inverse_f (f : X → Y) : Y → X := fun y : Y ↦
  if h : ∃ x, f x = y then Classical.choose h else default
theorem inverse_spec_f {f : X → Y} (y : Y) (h : ∃ x, f x = y) : f (inverse_f f y) = y := by
  rewrite [inverse_f]
  rewrite [dif_pos h]
  exact Classical.choose_spec h

variable (g: Y → Z)
def inverse_g (g : Y → Z) : Z → Y := fun z : Z ↦
  if h : ∃ y, g y = z then Classical.choose h else default
theorem inverse_spec_g {g : Y → Z} (z : Z) (h : ∃ y, g y = z) : g (inverse_g g z) = z := by
  rewrite [inverse_g]
  rewrite [dif_pos h]
  exact Classical.choose_spec h

def inverse_gf (g : Y → Z) (f : X → Y) : Z → X := fun z : Z ↦
  if h : ∃ x, g (f x) = z then Classical.choose h else default
theorem inverse_spec_gf {g : Y → Z} {f : X → Y} (z : Z) (h : ∃ x, g (f x) = z) : g (f (inverse_gf g f z)) = z := by
  rewrite [inverse_gf]
  rewrite [dif_pos h]
  exact Classical.choose_spec h

example (hf: Bijective f) (hg: Bijective g) (hgf : Bijective (g ∘ f)): inverse_gf g f = (inverse_f f) ∘ (inverse_g g) := by
  ext z
  simp only [Bijective] at *
  apply hgf.1
  rewrite [comp]; dsimp
  have hsurj_gf: ∃ x, (g ∘ f) x = z := hgf.2 z; dsimp at hsurj_gf
  rewrite [inverse_spec_gf z hsurj_gf]
  have hsurj_g: ∃ y, g y = z := hg.2 z
  have hsurj_f: ∃ x, f x = (inverse_g g z) := hf.2 (inverse_g g z)
  rewrite [inverse_spec_f (inverse_g g z) hsurj_f]
  rewrite [inverse_spec_g z hsurj_g]
  rfl

[Kevin Buzzard]

Use Equiv and not Bijective and everything's going to be much easier.

[Philipp SL Schäfer]

How exactly can I use Equiv? Is there small example to see how it is used in Lean?

[Moritz Doll]

To expand on Kevin's comment: what you are looking for is docs#Equiv.symm_trans_apply, docs#Equiv.symm is the inverse of an Equiv (again as an Equiv) and docs#Equiv.trans is the composition. The page Mathlib.Logic.Equiv.Defs should also give ample examples on how Equivs are used, but if you have more specific questions, please ask.

[Philipp SL Schäfer]

Thanks a lot! One more question what exactly is the difference between f.invFun and f.symm? E.g here I had to rewrite f.invFun to f.symm using Equiv.invFun_as_coe.

section

variable {α β: Type*} {A : Set α} {B : Set β} (f : A ≃ B)

def l_BB : B → B := fun b ↦ b

#check f.invFun
#check f.symm

example : f ∘ (f.invFun) = l_BB := by
  ext x
  simp only [comp]
  rewrite [l_BB]
  rewrite [Equiv.invFun_as_coe]
  rewrite [Equiv.apply_symm_apply]
  rfl

end

[Moritz Doll]

f.symm is an Equiv and f.invFun is just the bare inverse. You almost always want to use the object with more structure, so using f.invFun is probably not the right way of doing things. fyi your lemma is a combination of docs#Equiv.self_comp_symm and docs#Equiv.invFun_as_coe (and there you see that simp wants to change f.invFun to f.symm)

[Antoine Chambert-Loir]

F.invFun is the inverse function, without any property.
F.symm is the inverse equivalence, that contains the inverse function as the main object, its inverse F.toFun, and the fact that they're left/right inverses.

[Eric Wieser]

Perhaps a more useful description is "e.toFun and e.invFun are implementation details that you should never use"

[Philipp SL Schäfer]

Thanks everyone, that was super helpful! (I would resolve this thread, but I cannot do it anymore since there are "messages older than 7 days in this organisation. Contact a moderator to resolve this topic.")

[Matt Diamond]

we prefer that you don't resolve threads, actually... it changes the name of the thread which can screw up links