Skip to content

Instantly share code, notes, and snippets.

@nyuichi
Last active September 10, 2017 18:07
Show Gist options
  • Save nyuichi/8224e41d79943897796f0b0e025a2f93 to your computer and use it in GitHub Desktop.
Save nyuichi/8224e41d79943897796f0b0e025a2f93 to your computer and use it in GitHub Desktop.
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 α :=
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⟩
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment