Permutation group of a type.

perm.lean

import algebra.group
import tactic

-- Special thanks to Yakov Pechersky, Alex J. Best and the other folks on
-- Zulip.

-- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Holes.20in.20the.20goal!

section

parameters {α : Type*} [nonempty α]

def perm : Type* := {f : α → α // function.bijective f}

@[simp] def perm.mul : perm → perm → perm :=
λ ⟨f, hf⟩ ⟨g, hg⟩, ⟨f ∘ g, function.bijective.comp hf hg⟩

@[simp] lemma perm.mul_def (f g : perm) :
  perm.mul f g = ⟨f.val ∘ g.val, function.bijective.comp f.property g.property⟩ :=
begin
  cases f with f hf,
  cases g with g hg,
  simp
end

@[simp] def perm.id : perm := ⟨id, function.bijective_id⟩

open function (left_inverse) (right_inverse)

@[simp] lemma function.left_inverse_iff_right_inverse {β : Type*} {f : α → β} {g : β → α} :
  left_inverse f g ↔ right_inverse g f :=
⟨function.left_inverse.right_inverse, function.right_inverse.left_inverse⟩

lemma perm.inv' (f : perm) :
  ∃ g : perm, left_inverse g.val f.val ∧ right_inverse g.val f.val :=
begin
  cases f with f hf,
  rw function.bijective_iff_has_inverse at hf,
  cases hf with g hg,
  use g,
  { rw function.bijective_iff_has_inverse,
    use f,
    rwa and.comm },
  { simpa using hg }
end

noncomputable def perm.inv (f : perm) : perm := classical.some (perm.inv' f)

lemma perm.mul_left_inv (f : perm) :
  perm.mul (perm.inv f) f = perm.id :=
begin
  let g := perm.inv' f,
  rw perm.mul_def,
  congr,
  cases classical.some_spec g with h₁ h₂,
  ext x,
  exact h₁ x
end

noncomputable instance perm.group : group perm :=
{ mul := perm.mul,
  mul_assoc := λ ⟨_, _⟩ ⟨_, _⟩ ⟨_, _⟩, by simp,
  one := perm.id,
  one_mul := λ ⟨_, _⟩, by simp [has_mul.mul],
  mul_one := λ ⟨_, _⟩, by simp [has_mul.mul],
  inv := perm.inv,
  mul_left_inv := perm.mul_left_inv }

end