chap 22 exercise 1

c22-e1

namespace hidden

variables {A B C : Type}
open function

-- From chapter 16, but has no implementation in the lean function namespace.
theorem surjective_of_right_inverse {g : B  → A} {f : A → B} :
  right_inverse g f → surjective f :=
assume h, assume y,
let  x : A := g y in
  have f x = y,
  from calc f x  = (f (g y))    : rfl
              ... = y            : by rw [h y],
  show ∃ x, f x = y, from exists.intro x this

-- A more constructive version of inverse than was in chapter 16
def inverse (g : B → A) (f : A → B) :=
left_inverse g f ∧ right_inverse g f

def inverse_rev {g : B → A} {f : A → B} (fg_inv : inverse g f)
: inverse f g
:= ⟨fg_inv.right,fg_inv.left⟩

-- The next two aren't used below, but maybe think they help clarify some things.
def inverse_comp (f : A → B) (g : B → A) (fg_inv : inverse g f)
: (∀ (a : A), (g ∘ f) a = a) ∧ (∀ (b : B), (f ∘ g) b = b) :=
  ⟨fg_inv.left, fg_inv.right⟩

def inverse_comp_id (f : A → B) (g : B → A) (fg_inv  : inverse g f)
: (g ∘ f = id) ∧ (f ∘ g = id)
:= have gof : ∀ a, (g ∘ f) a = id a, 
     from (λ (a : A),
       have it : ∀x, g(f x) = x, from (inverse_comp f g fg_inv).left,
       show (g ∘ f) a = id a,
         from calc (g ∘ f) a = g(f a) : by refl
                         ... = a      : by rw it
                         ... = id a   : by rw id),
   -- The first and second are basically the same exchanging the left/right.
  ⟨funext gof, funext (λ _, by rw [(inverse_comp f g fg_inv).right, id])⟩

def inverse_bijective {f : A → B} {g : B → A} (gf_inv  : inverse g f)
: bijective f ∧ bijective g :=
   have injective f, from injective_of_left_inverse gf_inv.left,
   have surjective f, from surjective_of_right_inverse (gf_inv.right),
   have injective g, from injective_of_left_inverse (inverse_rev gf_inv).left,
   have surjective g, from surjective_of_right_inverse (inverse_rev gf_inv).right,      
   ⟨⟨‹injective f›, ‹surjective f›⟩, ⟨‹injective g›, ‹surjective g ›⟩⟩

/- Classical stuff from chapter 16 -/
open classical

local attribute [instance] prop_decidable

noncomputable def classical_inverse (f : A → B ) (default : A)
: B  → A
:= λ y, if h : ∃ x, f x = y then some h else default

theorem inverse_of_exists (f : A → B ) (default : A) (y : B )
  (h : ∃ x, f x = y) :
f (classical_inverse f default y) = y :=
have h1 : classical_inverse f default y = some h, from dif_pos h,
have h2 : f (some h) = y, from some_spec h,
eq.subst (eq.symm h1) h2

theorem is_left_inverse_of_injective (f : A → B ) (default : A)
  (injf : injective f) :
left_inverse (classical_inverse f default) f :=
let finv := (classical_inverse f default) in
assume x,
have h1 : ∃ x', f x' = f x, from exists.intro x rfl,
have h2 : f (finv (f x)) = f x, from inverse_of_exists f default (f x) h1,
show finv (f x) = x, from injf h2


/- Done with setup now the proofs... -/
theorem reflexivity {f : A → B } : ∃ (g : A → A), bijective g
:= have id_bij : bijective id, from @bijective_id A,
   exists.intro id (id_bij)

theorem symmetry {f : A → B } (f_bij : bijective f) (xs : nonempty A)
: ∃ (g : B  → A), bijective g :=
  have x : A, from choice xs,
  let g : B → A := (classical_inverse (f) x) in
    have l_inv : left_inverse g f,
      from is_left_inverse_of_injective (f) x (f_bij.left),
    have r_inv : right_inverse g f,
      from (λ y', inverse_of_exists (f) (x) (y') (f_bij.right y')),
    have fg_inv : inverse g f,
      from ⟨l_inv, r_inv⟩,
    show ∃ (g : B  → A), bijective g,
      from exists.intro g ((inverse_bijective fg_inv).right)

theorem transitivity {f : A → B} (f_bij : bijective f)
                     {g : B → C} (g_bij : bijective g)
: ∃ (gof : A → C), bijective gof 
:= exists.intro (g ∘ f) (bijective_comp (g_bij) (f_bij))

end hidden