cardinal.lean

import data.set
open function

universes u
variables {α β γ : Type u} 

noncomputable def bijective_inv (f : α → β) (h : bijective f) (b : β) : α :=
classical.some (h.right b)

lemma bijective_inv_spec (f : α → β) (h : bijective f) (b : β) : f (bijective_inv f h b) = b :=
classical.some_spec (h.right b)

lemma bijective_inv_bijective (f : α → β) (h : bijective f) : bijective (bijective_inv f h) :=
begin
  unfold bijective,
  split,
  unfold injective,
  intros,
  have : f (bijective_inv f h a₁) = f (bijective_inv f h a₂) := by rw a,
  rw bijective_inv_spec f h a₁ at this,
  rw bijective_inv_spec f h a₂ at this,
  assumption,
  unfold surjective,
  intro a,
  existsi f a,
  have : f (bijective_inv f h (f a)) = f a := bijective_inv_spec _ _ _,
  exact h.left this
end

lemma bij_comp_inj_bij (f : β → γ) (hf : bijective f) (i : α → β) (hi : injective i) : injective (f ∘ i) :=
begin
  unfold bijective at hf,
  unfold injective at *,
  intros,
  unfold comp at a,
  apply hi,
  apply hf.left,
  assumption
end

lemma inj_comp_bij_bij (i : β → γ) (hi : injective i) (f : α → β) (hf : bijective f) : injective (i ∘ f) :=
begin
  unfold bijective at hf,
  unfold injective at *,
  intros,
  unfold comp at a,
  apply hf.left,
  apply hi,
  assumption
end

def equinumerous (α : Type u) (β : Type u) := ∃ f : α → β, bijective f

lemma equinumerous_iseqv : equivalence equinumerous :=
begin
  apply mk_equivalence,
  unfold reflexive,
  intro,
  existsi id,
  exact bijective_id,
  unfold symmetric,
  intros,
  cases a,
  existsi bijective_inv a a_1,
  exact bijective_inv_bijective _ _,
  unfold transitive,
  intros,
  cases a,
  cases a_1,
  existsi a_1 ∘ a,
  apply bijective_comp,
  repeat { assumption }
end

instance equinumerous_setoid : setoid (Type u) :=
{ r := equinumerous,
  iseqv := equinumerous_iseqv }

def card : Type (u+1) := quotient equinumerous_setoid

instance card_has_le : has_le (quotient equinumerous_setoid) :=
{ le := @quotient.lift₂ (Type u) (Type u) _ _ _ (λ α β, ∃ f : α → β, injective f)
(assume a₁ a₂ b₁ b₂ (h₁ : ∃ f : a₁ → b₁, bijective f) (h₂ : ∃ f : a₂ → b₂, bijective f),
begin
  cases h₁ with f hf,
  cases h₂ with g hg,
  apply propext,
  split,
  { intro h,
    cases h with i hi,
    existsi g ∘ i ∘ bijective_inv f hf,
    apply bij_comp_inj_bij,
    assumption,
    apply inj_comp_bij_bij,
    assumption,
    apply bijective_inv_bijective, },
  intro h,
  cases h with i hi,
  existsi bijective_inv g hg ∘ i ∘ f,
  apply bij_comp_inj_bij,
  apply bijective_inv_bijective,
  apply inj_comp_bij_bij,
  assumption,
  assumption,
end) }

lemma card_le_def : ⟦α⟧ ≤ ⟦β⟧ = (∃ f : α → β, injective f) := rfl

lemma card_le_refl' (α : Type u) : ⟦α⟧ ≤ ⟦α⟧ :=
begin
  rw card_le_def,
  existsi id,
  exact injective_id
end

lemma card_le_refl (a : quotient equinumerous_setoid) : a ≤ a :=
@quotient.induction_on _ _ (λa, a ≤ a) a card_le_refl'

lemma card_le_trans (a b c : quotient equinumerous_setoid) : a ≤ b → b ≤ c → a ≤ c :=
@quotient.induction_on₃ _ _ _ _ _ _ (λ a b c, a ≤ b → b ≤ c → a ≤ c) a b c
begin
  intros α β γ,
  intros h1 h2,
  rw card_le_def at h1 h2,
  rw card_le_def,
  cases h1 with f hf,
  cases h2 with g hg,
  existsi g ∘ f,
  apply injective_comp,
  assumption,
  assumption,
end

instance card_preorder : preorder (quotient equinumerous_setoid) :=
{ card_has_le with
  le_refl := card_le_refl,
  le_trans := card_le_trans,
  lt := λ a b, a ≤ b ∧ ¬ b ≤ a,
  lt_iff_le_not_le := by order_laws_tac }

-- class well_order (α : Type u) extends linear_order α :=
-- (le_wf : well_founded le)

-- def g {α : Type u} [well_order α] (a : α) : set α :=

fundamental_theorem.lean

import data.set.basic
open set function

universes u v w
variables {α : Type u} {β : Type v} {γ : Type w}

lemma surjective_of_right_inverse {g : β → α} {f : α → β} : right_inverse g f → surjective f :=
assume h, surjective_of_has_right_inverse ⟨g, by assumption⟩

lemma surj_image_univ_eq_univ {f : α → β} : surjective f → f '' univ = univ :=
assume h, set.ext (assume x, iff.intro (assume _, by trivial) (assume _,
by cases h x with a ha; exact ⟨a, ⟨by trivial, by assumption⟩⟩))

variables [group α] [group β] [group γ]

class homomorphism (f : α → β) : Prop :=
(homomorphic : ∀x y, f (x * y) = f x * f y)

def homomorphic (f : α → β) [h : homomorphism f] := h.homomorphic

lemma one_to_one (f : α → β) [homomorphism f] : f 1 = 1 :=
calc f 1 = f 1 * 1             : by simp
 ...     = f 1 * f 1 * (f 1)⁻¹ : by simp
 ...     = f (1 * 1) * (f 1)⁻¹ : by rw homomorphic f
 ...     = f 1 * (f 1)⁻¹       : by simp
 ...     = 1                   : by simp

lemma inv_to_inv (f : α → β) [homomorphism f] (x : α) : f x⁻¹ = (f x)⁻¹ :=
calc f x⁻¹ = f x⁻¹ * 1               : by simp
 ...       = f x⁻¹ * (f x * (f x)⁻¹) : by simp
 ...       = f x⁻¹ * f x * (f x)⁻¹   : by simp
 ...       = f (x⁻¹ * x) * (f x)⁻¹   : by rw homomorphic f
 ...       = f 1 * (f x)⁻¹           : by simp
 ...       = 1 * (f x)⁻¹             : by rw one_to_one f
 ...       = (f x)⁻¹                 : by simp

instance hom_comp {g : β → γ} [homomorphism g] {f : α → β} [homomorphism f] : homomorphism (g ∘ f) :=
{ homomorphic := assume x y,
calc (g ∘ f) (x * y) = g (f (x * y))         : by simp
 ...                 = g (f x * f y)         : by rw homomorphic f
 ...                 = g (f x) * g (f y)     : by rw homomorphic g
 ...                 = (g ∘ f) x * (g ∘ f) y : by simp }

class isomorphism (f : α → β) extends homomorphism f : Prop :=
(isomorphic : bijective f)

def isomorphic (f : α → β) [h : isomorphism f] := h.isomorphic

def iso (α : Type u) [group α] (β : Type v) [group β] := ∃f : α → β, isomorphism f

precedence `≅` : 50
infix `≅` := iso

instance iso_comp {g : β → γ} [isomorphism g] {f : α → β} [isomorphism f] : isomorphism (g ∘ f) :=
{ hom_comp with isomorphic := bijective_comp (isomorphic g) (isomorphic f)}

class subgroup (s : set α) :=
(mul : ∀a b ∈ s, a * b ∈ s)
(one : (1 : α) ∈ s)
(inv : ∀a ∈ s, a⁻¹ ∈ s)

instance subgroup_group {s : set α} [subgroup s] : group (subtype s) :=
{ mul          := assume a b, by existsi a.val * b.val; exact subgroup.mul _ a b a.property b.property,
  mul_assoc    := assume a b c, subtype.eq $ group.mul_assoc a b c,
  one          := by existsi (1 : α); exact subgroup.one _ _,
  one_mul      := assume a, subtype.eq $ group.one_mul a,
  mul_one      := assume a, subtype.eq $ group.mul_one a,
  inv          := assume a, by existsi a.val⁻¹; exact subgroup.inv _ a a.property,
  mul_left_inv := assume a, subtype.eq $ group.mul_left_inv a}

lemma subgroup_mul_def (s : set α) [subgroup s] (a b : subtype s) : (a * b).val = a.val * b.val := rfl
lemma subgroup_one_def (s : set α) [subgroup s] : (1 : subtype s).val = 1 := rfl
lemma subgroup_inv_def (s : set α) [subgroup s] (a : subtype s) : a⁻¹.val = a.val⁻¹ := rfl

instance preimage_subgroup {f : α → β} [homomorphism f] {t : set β} [subgroup t] : subgroup (f ⁻¹' t) :=
{ mul := assume a b (ha : f a ∈ t) (hb : f b ∈ t), show f (a * b) ∈ t, by rw homomorphic f; exact subgroup.mul _ _ _ ha hb,
  one := show f 1 ∈ t, by rw one_to_one f; exact subgroup.one _ _,
  inv := assume a (ha : f a ∈ t), show f a⁻¹ ∈ t, by rw inv_to_inv f; exact subgroup.inv _ _ ha}

instance image_subgroup {f : α → β} [homomorphism f] {s : set α} [subgroup s] : subgroup (f '' s) :=
{ mul := assume a b (ha : ∃x, x ∈ s ∧ f x = a) (hb : ∃x, x ∈ s ∧ f x = b),
  show ∃x, x ∈ s ∧ f x = a * b, begin
    cases ha with u hu, cases hu with su hu,
    cases hb with v hv, cases hv with sv hv,
    existsi u * v,
    constructor,
    exact subgroup.mul _ _ _ su sv,
    rw homomorphic f; subst a; subst b
  end,
  one := show ∃x, x ∈ s ∧ f x = 1, begin
    existsi (1 : α),
    constructor,
    exact subgroup.one _ _,
    exact one_to_one f,
  end,
  inv := assume a (ha : ∃x, x ∈ s ∧ f x = a),
  show ∃x, x ∈ s ∧ f x = a⁻¹, begin
    cases ha with u hu, cases hu with su hu,
    existsi u⁻¹,
    constructor,
    exact subgroup.inv _ _ su,
    rw inv_to_inv f, subst a
  end}

def univ (α : Type u) [group α] : set α := @set.univ α

instance univ_subgroup : subgroup (univ α) :=
{ mul := by intros; trivial,
  one := trivial,
  inv := by intros; trivial }

def null (α : Type u) [group α] : set α := { x | x = 1 }  -- { 1 }

instance null_subgroup : subgroup (null α) :=
{ mul := assume a b (ha : a = 1) (hb : b = 1), show a * b = 1, by simp *,
  one := rfl,
  inv := assume a (ha : a = 1), show a⁻¹ = 1, by simp *}

def ker (f : α → β) [homomorphism f] := f ⁻¹' (null β)

instance ker_subgroup {f : α → β} [homomorphism f] : subgroup (ker f) := preimage_subgroup

def im (f : α → β) [homomorphism f] := f '' (univ α)

instance im_subgroup {f : α → β} [homomorphism f] : subgroup (im f) := image_subgroup

lemma eq_iff_mem_ker (f : α → β) [homomorphism f] : ∀a b, f a = f b ↔ a⁻¹ * b ∈ ker f :=
assume a b, iff.intro
(assume h : f a = f b,
calc f (a⁻¹ * b) = f a⁻¹ * f b   : by rw homomorphic f
 ...             = (f a)⁻¹ * f b : by rw inv_to_inv f
 ...             = (f a)⁻¹ * f a : by rw h
 ...             = 1             : by simp)
(assume h : f (a⁻¹ * b) = 1,
calc f a = f a * 1             : by simp
 ...     = f a * f (a⁻¹ * b)   : by rw h
 ...     = f a * f a⁻¹ * f b   : by rw [homomorphic f, mul_assoc]
 ...     = f a * (f a)⁻¹ * f b : by rw inv_to_inv f
 ...     = f b                 : by simp)

def surj_restr (f : α → β) [homomorphism f] : α → subtype (im f) :=
assume a, subtype.mk (f a) ⟨a, ⟨trivial, rfl⟩⟩

lemma surj_restr_def (f : α → β) [homomorphism f] (a : α) : (surj_restr f a).val = f a := rfl

instance surj_restr_hom {f : α → β} [homomorphism f] : homomorphism (surj_restr f) :=
{ homomorphic := assume a b,
show surj_restr f (a * b) = surj_restr f a * surj_restr f b,
from subtype.eq $ show f (a * b) = f a * f b, by rw homomorphic f}

lemma surj_restr_surj (f : α → β) [homomorphism f] : surjective (surj_restr f) :=
assume ⟨b, ⟨a, h⟩⟩, exists.intro a (subtype.eq (show f a = b, from h.right))

lemma inj_imp_surj_restr_inj (f : α → β) [homomorphism f] : injective f → injective (surj_restr f) :=
assume h a b H, h (by injection H)

def inj_imp_surj_restr_iso {f : α → β} [homomorphism f] (h : injective f) : isomorphism (surj_restr f) :=
{ surj_restr_hom with isomorphic := ⟨inj_imp_surj_restr_inj _ h, surj_restr_surj f⟩}

def lcoset (a : α) (s : set α) : set α := (λx, a * x) '' s
def rcoset (s : set α) (a : α) : set α := (λx, x * a) '' s

infix * := lcoset
infix * := rcoset

lemma lcoset_def (a : α) (s : set α) (x : α) : x ∈ a * s = ∃u ∈ s, a * u = x :=
by rw [lcoset, image, mem_set_of_eq]; simp

lemma rcoset_def (s : set α) (a : α) (x : α) : x ∈ s * a = ∃u ∈ s, u * a = x :=
by rw [rcoset, image, mem_set_of_eq]; simp

private lemma lmul_lmul : ∀x y : α, (λa : α, x * y * a) = (λa : α, x * a) ∘ (λa : α, y * a) :=
assume x y, funext (assume a, by simp)

private lemma lmul_rmul : ∀x y : α, (λa : α, x * a) ∘ (λa : α, a * y) = (λa : α, a * y) ∘ (λa : α, x * a) :=
assume x y, funext (assume a, show x * (a * y) = x * a * y, by simp)

private lemma rmul_rmul : ∀x y : α, (λa : α, a * (x * y)) = (λa : α, a * y) ∘ (λa : α, a * x) :=
assume x y, funext (assume a, show a * (x * y) = a * x * y, by simp)

private lemma one_lmul : (λa : α, 1 * a) = id :=
funext (assume a, by simp)

private lemma rmul_one : (λa : α, a * 1) = id :=
funext (assume a, by simp)

variables (s t : set α)

lemma lcoset_lcoset : ∀x y : α, x * y * s = x * (y * s) :=
assume x y,
calc x * y * s = (λa : α, x * y * a) '' s                 : by refl
 ...           = ((λa : α, x * a) ∘ (λa : α, y * a)) '' s : by rw lmul_lmul
 ...           = x * (y * s)                              : by rw image_comp; refl

lemma lcoset_rcoset : ∀x y : α, x * (s * y) = x * s * y :=
assume x y,
calc x * (s * y) = ((λa : α, x * a) ∘ (λa : α, a * y)) '' s : by rw image_comp; refl
 ...             = ((λa : α, a * y) ∘ (λa : α, x * a)) '' s : by rw lmul_rmul
 ...             = (x * s) * y                              : by rw image_comp; refl

lemma rcoset_rcoset : ∀x y : α, s * (x * y) = s * x * y :=
assume x y,
calc s * (x * y) = (λa : α, a * (x * y)) '' s               : by refl
 ...             = ((λa : α, a * y) ∘ (λa : α, a * x)) '' s : by rw rmul_rmul
 ...             = (s * x) * y                              : by rw image_comp; refl

@[simp] lemma one_lcoset : 1 * s = s :=
calc 1 * s = (λa : α, 1 * a) '' s : by refl
 ...       = id '' s              : by rw one_lmul
 ...       = s                    : by rw image_id

@[simp] lemma rcoset_one : s * 1 = s :=
calc s * 1 = (λa : α, a * 1) '' s : by refl
 ...       = id '' s              : by rw rmul_one
 ...       = s                    : by rw image_id

lemma mono_lcoset : ∀a, s ⊆ t → a * s ⊆ a * t :=
assume a, mono_image

lemma mono_rcoset : ∀a, s ⊆ t → s * a ⊆ t * a :=
assume a, mono_image

lemma mul_mem_lcoset : ∀a x : α, x ∈ s → a * x ∈ a * s :=
assume a x, mem_image_of_mem (λb : α, a * b)

lemma mul_mem_rcoset : ∀a x : α, x ∈ s → x * a ∈ s * a :=
assume a x, mem_image_of_mem (λb : α, b * a)

def normal₁ := ∀a : α, a * s * a⁻¹ = s

def normal₂ := ∀a : α, a * s * a⁻¹ ⊆ s

def normal₃ := ∀a : α, a * s = s * a

private lemma normal₁_imp_normal₃ : normal₁ s → normal₃ s :=
assume h a,
calc a * s = a * s * 1         : by simp
 ...       = a * s * (a⁻¹ * a) : by simp
 ...       = a * s * a⁻¹ * a   : by rw rcoset_rcoset
 ...       = s * a             : by rw h

private lemma normal₃_imp_normal₁ : normal₃ s → normal₁ s := 
assume h a,
calc a * s * a⁻¹ = s * a * a⁻¹   : by rw h
 ...             = s * (a * a⁻¹) : by rw rcoset_rcoset
 ...             = s             : by simp

lemma normal₁_iff_normal₃ : normal₁ s ↔ normal₃ s :=
iff.intro (normal₁_imp_normal₃ s) (normal₃_imp_normal₁ s)

private lemma normal₁_imp_normal₂ : normal₁ s → normal₂ s :=
assume h a, show ∀ ⦃x : α⦄, x ∈ a * s * a⁻¹ → x ∈ s, by rw h; intros; assumption

private lemma normal₂_imp_conv_normal₂ : normal₂ s → ∀a : α, s ⊆ a * s * a⁻¹ :=
assume h a,
calc s = 1 * s * 1                   : by simp
 ...   = (a * a⁻¹) * s * (a * a⁻¹)   : by simp
 ...   = a * (a⁻¹ * s * a) * a⁻¹     : by rw [rcoset_rcoset, lcoset_lcoset, lcoset_rcoset]
 ...   = a * (a⁻¹ * s * a⁻¹⁻¹) * a⁻¹ : by simp
 ...   ⊆ a * s * a⁻¹                 : mono_rcoset _ _ _ (mono_lcoset _ _ _ (h a⁻¹))

private lemma normal₂_imp_normal₁ : normal₂ s → normal₁ s :=
assume h a, set.subset.antisymm (h a) (normal₂_imp_conv_normal₂ s h a)

lemma normal₁_iff_normal₂ : normal₁ s ↔ normal₂ s :=
iff.intro (normal₁_imp_normal₂ s) (normal₂_imp_normal₁ s)

lemma normal₂_iff_normal₃ : normal₂ s ↔ normal₃ s :=
by rw [←normal₁_iff_normal₂, normal₁_iff_normal₃]

class normal_subgroup (s : set α) extends subgroup s :=
(normal : normal₃ s)

def normal (s : set α) [n : normal_subgroup s] := n.normal

private lemma ker_normal (f : α → β) [homomorphism f] : normal₂ (ker f) :=
assume a x ⟨w, ⟨⟨v, ⟨(u : f v = 1), h⟩⟩, hv⟩⟩, begin
  subst h,
  calc f x = f (a * v * a⁻¹)   : by rw ←hv
   ...     = f a * f v * f a⁻¹ : by rw [homomorphic f, homomorphic f]
   ...     = f a * 1 * f a⁻¹   : by rw u
   ...     = f a * 1 * (f a)⁻¹ : by rw inv_to_inv f
   ...     = 1                 : by simp
end

instance ker_normal_subgroup {f : α → β} [homomorphism f] : normal_subgroup (ker f) :=
{ ker_subgroup with normal := (normal₂_iff_normal₃ (ker f)).mp $ ker_normal f}

instance normal_subgroup_setoid [normal_subgroup s] : setoid α :=
{ r := λa b, a * s = b * s,
  iseqv := mk_equivalence _ (λa, rfl) (λa b, eq.symm) (λa b c, eq.trans) }

lemma normal_mul_prsv_eqv [normal_subgroup s] (a₁ b₁ a₂ b₂ : α) : a₁ ≈ a₂ → b₁ ≈ b₂ → a₁ * b₁ ≈ a₂ * b₂ :=
assume (ha : a₁ * s = a₂ * s) (hb : b₁ * s = b₂ * s),
calc a₁ * b₁ * s = a₁ * (b₁ * s) : by rw lcoset_lcoset
 ...             = a₁ * (b₂ * s) : by rw hb
 ...             = a₁ * (s * b₂) : by rw normal s
 ...             = (a₁ * s) * b₂ : by rw lcoset_rcoset
 ...             = (a₂ * s) * b₂ : by rw ha
 ...             = a₂ * (s * b₂) : by rw lcoset_rcoset
 ...             = a₂ * (b₂ * s) : by rw normal s
 ...             = a₂ * b₂ * s   : by rw lcoset_lcoset

lemma normal_inv_prsv_eqv [normal_subgroup s] (a₁ a₂ : α) : a₁ ≈ a₂ → a₁⁻¹ ≈ a₂⁻¹ :=
assume (ha : a₁ * s = a₂ * s),
calc a₁⁻¹ * s = a₁⁻¹ * (s * 1)           : by simp
 ...          = a₁⁻¹ * (s * (a₂ * a₂⁻¹)) : by simp
 ...          = a₁⁻¹ * ((s * a₂) * a₂⁻¹) : by rw rcoset_rcoset
 ...          = a₁⁻¹ * ((a₂ * s) * a₂⁻¹) : by rw normal s
 ...          = a₁⁻¹ * ((a₁ * s) * a₂⁻¹) : by rw ha
 ...          = a₁⁻¹ * (a₁ * s) * a₂⁻¹   : by rw lcoset_rcoset
 ...          = (a₁⁻¹ * a₁) * s * a₂⁻¹   : by rw lcoset_lcoset
 ...          = 1 * s * a₂⁻¹             : by simp
 ...          = s * a₂⁻¹                 : by simp
 ...          = a₂⁻¹ * s                 : by rw normal s

def quotient_group (α : Type u) [group α] (s : set α) [normal_subgroup s] := quotient (normal_subgroup_setoid s)

infix `/` := quotient_group

instance quotient_group_group {s : set α} [normal_subgroup s] : group (α / s) :=
{ mul          := quotient.lift₂ (λa b : α, ⟦a * b⟧) (assume a₁ b₁ a₂ b₂ ha hb, quotient.sound (normal_mul_prsv_eqv s a₁ b₁ a₂ b₂ ha hb)),
  mul_assoc    := assume a b c, quotient.induction_on₃ a b c (λa b c, show ⟦a * b * c⟧ = ⟦a * (b * c)⟧, by rw [mul_assoc]),
  one          := ⟦1⟧,
  one_mul      := assume a, quotient.induction_on a (λa, show ⟦1 * a⟧ = ⟦a⟧, by rw [one_mul]),
  mul_one      := assume a, quotient.induction_on a (λa, show ⟦a * 1⟧ = ⟦a⟧, by rw [mul_one]),
  inv          := quotient.lift (λa, ⟦a⁻¹⟧) (assume a₁ a₂ ha, quotient.sound (normal_inv_prsv_eqv s a₁ a₂ ha)),
  mul_left_inv := assume a, quotient.induction_on a (λa, show ⟦a⁻¹ * a⟧ = ⟦1⟧, by rw [mul_left_inv])}

lemma quot_mul_def {s : set α} [normal_subgroup s] {a b : α} : (⟦a⟧ * ⟦b⟧ : α / s) = ⟦a * b⟧ := rfl
lemma quot_one_def {s : set α} [normal_subgroup s] : (1 : α / s) = ⟦1⟧ := rfl
lemma quot_inv_def {s : set α} [normal_subgroup s] {a : α} : (⟦a⟧⁻¹ : α / s) = ⟦a⁻¹⟧ := rfl

def coker [normal_subgroup s] : α → α / s := λa, ⟦a⟧

instance coker_homomorphism [normal_subgroup s] : homomorphism (coker s) :=
{ homomorphic := assume x y, quot_mul_def }

lemma coker_surj [normal_subgroup s] : surjective (coker s) :=
assume a, quotient.induction_on a (assume a, ⟨a, rfl⟩)

lemma lcoset_normal_mem [normal_subgroup s] : ∀a, a * s = s ↔ a ∈ s :=
assume a, iff.intro
(assume h,
  have x : a * 1 ∈ a * s := mul_mem_lcoset _ _ _ (subgroup.one _ _),
  have y : a * 1 ∈ s := h ▸ x,
  mul_one a ▸ y)
(assume h, set.ext (assume x, iff.intro
(assume ⟨w, ⟨h1, h2⟩⟩, h2 ▸ subgroup.mul _ a w h h1)
(assume H, ⟨a⁻¹ * x, ⟨subgroup.mul _ _ _ (subgroup.inv _ _ h) H,
  show a * (a⁻¹ * x) = x, by rw [←mul_assoc, mul_right_inv, one_mul]⟩⟩)))

lemma canon_well_defined (f : α → β) [homomorphism f] : ∀a b : α, a ≈ b → f a = f b :=
assume a b (h : a * ker f = b * ker f), (eq_iff_mem_ker f a b).mpr $ (lcoset_normal_mem _ _).mp $
  calc a⁻¹ * b * ker f = a⁻¹ * (b * ker f) : by rw lcoset_lcoset
   ...                 = a⁻¹ * (a * ker f) : by rw h
   ...                 = (a⁻¹ * a) * ker f : by rw lcoset_lcoset
   ...                 = ker f             : by simp

def canon (f : α → β) [homomorphism f] : α / ker f → β := quotient.lift f (canon_well_defined f)

precedence `̂` : std.prec.max_plus
local postfix `̂` := canon

lemma canon_def (f : α → β) [homomorphism f] (a : α) : f̂ ⟦a⟧ = f a := rfl

instance canon_hom {f : α → β} [homomorphism f] : homomorphism f̂ :=
{ homomorphic := assume a b, quotient.induction_on₂ a b (assume a b, show f (a * b) = f a * f b, by rw homomorphic f)}

private lemma canon_prop (f : α → β) [homomorphism f] : f̂ ∘ coker (ker f) = f := rfl

private lemma canon_unique (f : α → β) [homomorphism f] (g : α / ker f → β) : homomorphism g ∧ g ∘ coker (ker f) = f → g = f̂ :=
assume h, funext (assume x, quotient.induction_on x (assume x, show g ⟦x⟧ = f x, from congr_fun h.right x))

theorem fundamental_theorem (f : α → β) [homomorphism f] : ∃!g : α / ker f → β, homomorphism g ∧ g ∘ coker (ker f) = f :=
exists_unique.intro f̂ (and.intro canon_hom (canon_prop f)) (canon_unique f)

lemma canon_inj (f : α → β) [homomorphism f] : injective f̂ :=
assume a b, quotient.induction_on₂ a b (assume a b (h : f a = f b), quotient.sound
(calc a * ker f = a * (a⁻¹ * b * ker f) : by rw [(lcoset_normal_mem _ _).mpr $ (eq_iff_mem_ker _ _ _).mp $ h]
  ...           = (a * a⁻¹) * b * ker f : by rw [←lcoset_lcoset, mul_assoc]
  ...           = b * ker f             : by simp))

lemma canon_im_eq_im (f : α → β) [homomorphism f] : im f = im f̂ :=
calc im f = @im _ _ _ _ (f̂ ∘ coker (ker f)) hom_comp : by refl
 ...      = (f̂ ∘ coker (ker f)) '' univ              : by refl
 ...      = f̂ '' ((coker (ker f)) '' univ)           : by rw image_comp
 ...      = f̂ '' univ                                : by rw surj_image_univ_eq_univ (coker_surj _)
 ...      = im f̂                                     : by refl

def subtype_lift {s t : set α} (h : s = t) : subtype s → subtype t :=
assume x, subtype.mk x (h ▸ x.property)

lemma subtype_lift_bij {s t : set α} (h : s = t) : bijective (subtype_lift h) :=
and.intro
(assume a₁ a₂ H, subtype.eq $ show (subtype_lift h a₁).val = (subtype_lift h a₂).val, by rw H)
(assume H, ⟨⟨H, eq.symm h ▸ H.property⟩, subtype.eq rfl⟩)

instance subtype_lift_iso {s : set α} [subgroup s] {t : set α} [subgroup t] {h : s = t} : isomorphism (subtype_lift h) :=
{ homomorphic := assume x y, subtype.eq rfl,
  isomorphic := subtype_lift_bij h}

def canonical_isomorphism (f : α → β) [homomorphism f] : α / ker f → subtype (im f) :=
subtype_lift (eq.symm $ canon_im_eq_im f) ∘ surj_restr f̂

instance canonical_isomorphism_iso {f : α → β} [homomorphism f] : isomorphism (canonical_isomorphism f) :=
@iso_comp _ _ _ _ _ _ _ _ _ (inj_imp_surj_restr_iso (canon_inj f))

theorem isomorphism_theorem (f : α → β) [homomorphism f] : α / ker f ≅ subtype (im f) :=
⟨canonical_isomorphism f, canonical_isomorphism_iso⟩