michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

restore quotient_group.hlean

Browse source
This commit is contained in:
Jeremy Avigad 2017-09-07 15:22:04 -04:00
parent dc327487f6
commit af30b19099
1 changed files with 737 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

737
algebra/quotient_group.hlean Normal file
View file

@ -0,0 +1,737 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Egbert Rijke, Jeremy Avigad
Constructions with groups
-/
import hit.set_quotient .subgroup ..move_to_lib types.equiv
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod trunc function equiv is_equiv
open property
namespace group
variables {G G' : Group}
(H : property G) [is_subgroup G H]
(N : property G) [is_normal_subgroup G N]
{g g' h h' k : G}
(N' : property G') [is_normal_subgroup G' N']
variables {A B : AbGroup}
/- Quotient Group -/
definition homotopy_of_homomorphism_eq {f g : G →g G'}(p : f = g) : f ~ g :=
λx : G , ap010 group_fun p x
definition quotient_rel [constructor] (g h : G) : Prop := g * h⁻¹ ∈ N
variable {N}
-- We prove that quotient_rel is an equivalence relation
theorem quotient_rel_refl (g : G) : quotient_rel N g g :=
transport (λx, N x) !mul.right_inv⁻¹ (subgroup_one_mem N)
theorem quotient_rel_symm (r : quotient_rel N g h) : quotient_rel N h g :=
transport (λx, N x) (!mul_inv ⬝ ap (λx, x * _) !inv_inv)
begin apply subgroup_inv_mem r end
theorem quotient_rel_trans (r : quotient_rel N g h) (s : quotient_rel N h k)
: quotient_rel N g k :=
have H1 : N ((g * h⁻¹) * (h * k⁻¹)), from subgroup_mul_mem r s,
have H2 : (g * h⁻¹) * (h * k⁻¹) = g * k⁻¹, from calc
(g * h⁻¹) * (h * k⁻¹) = ((g * h⁻¹) * h) * k⁻¹ : by rewrite [mul.assoc (g * h⁻¹)]
... = g * k⁻¹ : by rewrite inv_mul_cancel_right,
show N (g * k⁻¹), by rewrite [-H2]; exact H1
theorem is_equivalence_quotient_rel : is_equivalence (quotient_rel N) :=
is_equivalence.mk quotient_rel_refl
(λg h, quotient_rel_symm)
(λg h k, quotient_rel_trans)
-- We prove that quotient_rel respects inverses and multiplication, so
-- it is a congruence relation
theorem quotient_rel_resp_inv (r : quotient_rel N g h) : quotient_rel N g⁻¹ h⁻¹ :=
have H1 : g⁻¹ * (h * g⁻¹) * g ∈ N, from
is_normal_subgroup' g (quotient_rel_symm r),
have H2 : g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h⁻¹⁻¹, from calc
g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h * g⁻¹ * g : by rewrite -mul.assoc
... = g⁻¹ * h : inv_mul_cancel_right
... = g⁻¹ * h⁻¹⁻¹ : by rewrite algebra.inv_inv,
show g⁻¹ * h⁻¹⁻¹ ∈ N, by rewrite [-H2]; exact H1
theorem quotient_rel_resp_mul (r : quotient_rel N g h) (r' : quotient_rel N g' h')
: quotient_rel N (g * g') (h * h') :=
have H1 : g * ((g' * h'⁻¹) * h⁻¹) ∈ N, from
normal_subgroup_insert r' r,
have H2 : g * ((g' * h'⁻¹) * h⁻¹) = (g * g') * (h * h')⁻¹, from calc
g * ((g' * h'⁻¹) * h⁻¹) = g * (g' * (h'⁻¹ * h⁻¹)) : by rewrite [mul.assoc]
... = (g * g') * (h'⁻¹ * h⁻¹) : mul.assoc
... = (g * g') * (h * h')⁻¹ : by rewrite [mul_inv],
show N ((g * g') * (h * h')⁻¹), from transport (λx, N x) H2 H1
local attribute is_equivalence_quotient_rel [instance]
variable (N)
definition qg : Type := set_quotient (quotient_rel N)
variable {N}
local attribute qg [reducible]
definition quotient_one [constructor] : qg N := class_of one
definition quotient_inv [unfold 3] : qg N → qg N :=
quotient_unary_map has_inv.inv (λg g' r, quotient_rel_resp_inv r)
definition quotient_mul [unfold 3 4] : qg N → qg N → qg N :=
quotient_binary_map has_mul.mul (λg g' r h h' r', quotient_rel_resp_mul r r')
section
local notation 1 := quotient_one
local postfix ⁻¹ := quotient_inv
local infix * := quotient_mul
theorem quotient_mul_assoc (g₁ g₂ g₃ : qg N) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
begin
refine set_quotient.rec_prop _ g₁,
refine set_quotient.rec_prop _ g₂,
refine set_quotient.rec_prop _ g₃,
clear g₁ g₂ g₃, intro g₁ g₂ g₃,
exact ap class_of !mul.assoc
end
theorem quotient_one_mul (g : qg N) : 1 * g = g :=
begin
refine set_quotient.rec_prop _ g, clear g, intro g,
exact ap class_of !one_mul
end
theorem quotient_mul_one (g : qg N) : g * 1 = g :=
begin
refine set_quotient.rec_prop _ g, clear g, intro g,
exact ap class_of !mul_one
end
theorem quotient_mul_left_inv (g : qg N) : g⁻¹ * g = 1 :=
begin
refine set_quotient.rec_prop _ g, clear g, intro g,
exact ap class_of !mul.left_inv
end
theorem quotient_mul_comm {G : AbGroup} {N : property G} [is_normal_subgroup G N] (g h : qg N)
: g * h = h * g :=
begin
refine set_quotient.rec_prop _ g, clear g, intro g,
refine set_quotient.rec_prop _ h, clear h, intro h,
apply ap class_of, esimp, apply mul.comm
end
end
variable (N)
definition group_qg [constructor] : group (qg N) :=
group.mk _ quotient_mul quotient_mul_assoc quotient_one quotient_one_mul quotient_mul_one
quotient_inv quotient_mul_left_inv
definition quotient_group [constructor] : Group :=
Group.mk _ (group_qg N)
definition ab_group_qg [constructor] {G : AbGroup} (N : property G) [is_normal_subgroup G N]
: ab_group (qg N) :=
⦃ab_group, group_qg N, mul_comm := quotient_mul_comm⦄
definition quotient_ab_group [constructor] {G : AbGroup} (N : property G) [is_subgroup G N]
: AbGroup :=
AbGroup.mk _ (@ab_group_qg G N (is_normal_subgroup_ab _))
definition qg_map [constructor] : G →g quotient_group N :=
homomorphism.mk class_of (λ g h, idp)
definition ab_qg_map {G : AbGroup} (N : property G) [is_subgroup G N] : G →g quotient_ab_group N :=
@qg_map _ N (is_normal_subgroup_ab _)
definition is_surjective_ab_qg_map {A : AbGroup} (N : property A) [is_subgroup A N] : is_surjective (ab_qg_map N) :=
begin
intro x, induction x,
fapply image.mk,
exact a, reflexivity,
apply is_prop.elimo
end
namespace quotient
notation `⟦`:max a `⟧`:0 := qg_map _ a
end quotient
open quotient
variables {N N'}
definition qg_map_eq_one (g : G) (H : N g) : qg_map N g = 1 :=
begin
apply eq_of_rel,
have e : (g * 1⁻¹ = g),
from calc
g * 1⁻¹ = g * 1 : one_inv
... = g : mul_one,
unfold quotient_rel, rewrite e, exact H
end
definition ab_qg_map_eq_one {K : property A} [is_subgroup A K] (g :A) (H : K g) : ab_qg_map K g = 1 :=
begin
apply eq_of_rel,
have e : (g * 1⁻¹ = g),
from calc
g * 1⁻¹ = g * 1 : one_inv
... = g : mul_one,
unfold quotient_rel, xrewrite e, exact H
end
--- there should be a smarter way to do this!! Please have a look, Floris.
definition rel_of_qg_map_eq_one (g : G) (H : qg_map N g = 1) : g ∈ N :=
begin
have e : (g * 1⁻¹ = g),
from calc
g * 1⁻¹ = g * 1 : one_inv
... = g : mul_one,
rewrite (inverse e),
apply rel_of_eq _ H
end
definition rel_of_ab_qg_map_eq_one {K : property A} [is_subgroup A K] (a :A) (H : ab_qg_map K a = 1) : a ∈ K :=
begin
have e : (a * 1⁻¹ = a),
from calc
a * 1⁻¹ = a * 1 : one_inv
... = a : mul_one,
rewrite (inverse e),
have is_normal_subgroup A K, from is_normal_subgroup_ab _,
apply rel_of_eq (quotient_rel K) H
end
definition quotient_group_elim_fun [unfold 6] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1)
(g : quotient_group N) : G' :=
begin
refine set_quotient.elim f _ g,
intro g h K,
apply eq_of_mul_inv_eq_one,
have e : f (g * h⁻¹) = f g * (f h)⁻¹,
from calc
f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul
... = f g * (f h)⁻¹ : to_respect_inv,
rewrite (inverse e),
apply H, exact K
end
definition quotient_group_elim [constructor] (f : G →g G') (H : Π⦃g⦄, g ∈ N → f g = 1) : quotient_group N →g G' :=
begin
fapply homomorphism.mk,
-- define function
{ exact quotient_group_elim_fun f H },
{ intro g h, induction g using set_quotient.rec_prop with g,
induction h using set_quotient.rec_prop with h,
krewrite (inverse (to_respect_mul (qg_map N) g h)),
unfold qg_map, esimp, exact to_respect_mul f g h }
end
example {K : property A} [is_subgroup A K] :
quotient_ab_group K = @quotient_group A K (is_normal_subgroup_ab _) := rfl
definition quotient_ab_group_elim [constructor] {K : property A} [is_subgroup A K] (f : A →g B)
(H : Π⦃g⦄, g ∈ K → f g = 1) : quotient_ab_group K →g B :=
@quotient_group_elim A B K (is_normal_subgroup_ab _) f H
definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (g : G) :
quotient_group_elim f H (qg_map N g) = f g :=
begin
reflexivity
end
definition gelim_unique (f : G →g G') (H : Π⦃g⦄, g ∈ N → f g = 1) (k : quotient_group N →g G')
: ( k ∘g qg_map N ~ f ) → k ~ quotient_group_elim f H :=
begin
intro K cg, induction cg using set_quotient.rec_prop with g,
exact K g
end
definition ab_gelim_unique {K : property A} [is_subgroup A K] (f : A →g B) (H : Π (a :A), a ∈ K → f a = 1) (k : quotient_ab_group K →g B)
: ( k ∘g ab_qg_map K ~ f) → k ~ quotient_ab_group_elim f H :=
--@quotient_group_elim A B K (is_normal_subgroup_ab _) f H :=
@gelim_unique _ _ K (is_normal_subgroup_ab _) f H _
definition qg_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) :
is_contr (Σ(g : quotient_group N →g G'), g ∘ qg_map N ~ f) :=
begin
fapply is_contr.mk,
-- give center of contraction
{ fapply sigma.mk, exact quotient_group_elim f H, exact quotient_group_compute f H },
-- give contraction
{ intro pair, induction pair with g p, fapply sigma_eq,
{esimp, apply homomorphism_eq, symmetry, exact gelim_unique f H g p},
{fapply is_prop.elimo} }
end
definition ab_qg_universal_property {K : property A} [is_subgroup A K] (f : A →g B) (H : Π (a :A), K a → f a = 1) :
is_contr ((Σ(g : quotient_ab_group K →g B), g ∘g ab_qg_map K ~ f) ) :=
begin
fapply @qg_universal_property _ _ K (is_normal_subgroup_ab _),
exact H
end
definition quotient_group_functor_contr {K L : property A} [is_subgroup A K] [is_subgroup A L]
(H : Π (a : A), K a → L a) :
is_contr ((Σ(g : quotient_ab_group K →g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L) ) :=
begin
fapply ab_qg_universal_property,
intro a p,
fapply ab_qg_map_eq_one,
exact H a p
end
definition quotient_group_functor_id {K : property A} [is_subgroup A K] (H : Π (a : A), K a → K a) :
center' (@quotient_group_functor_contr _ K K _ _ H) = ⟨gid (quotient_ab_group K), λ x, rfl⟩ :=
begin
note p := @quotient_group_functor_contr _ K K _ _ H,
fapply eq_of_is_contr,
end
section quotient_group_iso_ua
set_option pp.universes true
definition subgroup_rel_eq' {K L : property A} [HK : is_subgroup A K] [HL : is_subgroup A L] (htpy : Π (a : A), K a ≃ L a) : K = L :=
begin
induction HK with Rone Rmul Rinv, induction HL with Rone' Rmul' Rinv', esimp at *,
assert q : K = L,
begin
fapply eq_of_homotopy,
intro a,
fapply tua,
exact htpy a,
end,
induction q,
assert q : Rone = Rone',
begin
fapply is_prop.elim,
end,
induction q,
assert q2 : @Rmul = @Rmul',
begin
fapply is_prop.elim,
end,
induction q2,
assert q : @Rinv = @Rinv',
begin
fapply is_prop.elim,
end,
induction q,
reflexivity
end
definition subgroup_rel_eq {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), a ∈ K → a ∈ L) (L_in_K : Π (a : A), a ∈ L → a ∈ K) : K = L :=
begin
have htpy : Π (a : A), K a ≃ L a,
begin
intro a,
apply @equiv_of_is_prop (a ∈ K) (a ∈ L) _ _ (K_in_L a) (L_in_K a),
end,
exact subgroup_rel_eq' htpy,
end
definition eq_of_ab_qg_group' {K L : property A} [HK : is_subgroup A K] [HL : is_subgroup A L] (p : K = L) : quotient_ab_group K = quotient_ab_group L :=
begin
revert HK, revert HL, induction p, intros,
have HK = HL, begin apply @is_prop.elim _ _ HK HL end,
rewrite this
end
definition iso_of_eq {B : AbGroup} (p : A = B) : A ≃g B :=
begin
induction p, fapply isomorphism.mk, exact gid A, fapply adjointify, exact id, intro a, reflexivity, intro a, reflexivity
end
definition iso_of_ab_qg_group' {K L : property A} [is_subgroup A K] [is_subgroup A L] (p : K = L) : quotient_ab_group K ≃g quotient_ab_group L :=
iso_of_eq (eq_of_ab_qg_group' p)
/-
definition htpy_of_ab_qg_group' {K L : property A} [HK : is_subgroup A K] [HL : is_subgroup A L] (p : K = L) : (iso_of_ab_qg_group' p) ∘g ab_qg_map K ~ ab_qg_map L :=
begin
revert HK, revert HL, induction p, intros HK HL, unfold iso_of_ab_qg_group', unfold ab_qg_map
-- have HK = HL, begin apply @is_prop.elim _ _ HK HL end,
-- rewrite this
-- induction p, reflexivity
end
-/
definition eq_of_ab_qg_group {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : quotient_ab_group K = quotient_ab_group L :=
eq_of_ab_qg_group' (subgroup_rel_eq K_in_L L_in_K)
definition iso_of_ab_qg_group {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : quotient_ab_group K ≃g quotient_ab_group L :=
iso_of_eq (eq_of_ab_qg_group K_in_L L_in_K)
/-
definition htpy_of_ab_qg_group {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : iso_of_ab_qg_group K_in_L L_in_K ∘g ab_qg_map K ~ ab_qg_map L :=
begin
fapply htpy_of_ab_qg_group'
end
-/
end quotient_group_iso_ua
section quotient_group_iso
variables {K L : property A} [is_subgroup A K] [is_subgroup A L] (H1 : Π (a : A), K a → L a) (H2 : Π (a : A), L a → K a)
include H1
include H2
definition quotient_group_iso_contr_KL_map :
quotient_ab_group K →g quotient_ab_group L :=
pr1 (center' (quotient_group_functor_contr H1))
definition quotient_group_iso_contr_KL_triangle :
quotient_group_iso_contr_KL_map H1 H2 ∘g ab_qg_map K ~ ab_qg_map L :=
pr2 (center' (quotient_group_functor_contr H1))
definition quotient_group_iso_contr_KK :
is_contr (Σ (g : quotient_ab_group K →g quotient_ab_group K), g ∘g ab_qg_map K ~ ab_qg_map K) :=
@quotient_group_functor_contr A K K _ _ (λ a, H2 a ∘ H1 a)
definition quotient_group_iso_contr_LK :
quotient_ab_group L →g quotient_ab_group K :=
pr1 (center' (@quotient_group_functor_contr A L K _ _ H2))
definition quotient_group_iso_contr_LL :
quotient_ab_group L →g quotient_ab_group L :=
pr1 (center' (@quotient_group_functor_contr A L L _ _ (λ a, H1 a ∘ H2 a)))
/-
definition quotient_group_iso : quotient_ab_group K ≃g quotient_ab_group L :=
begin
fapply isomorphism.mk,
exact pr1 (center' (quotient_group_iso_contr_KL H1 H2)),
fapply adjointify,
exact quotient_group_iso_contr_LK H1 H2,
intro x,
induction x, reflexivity,
end
-/
definition quotient_group_iso_contr_aux :
is_contr (Σ(gh : Σ (g : quotient_ab_group K →g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L), is_equiv (group_fun (pr1 gh))) :=
begin
fapply is_trunc_sigma,
exact quotient_group_functor_contr H1,
intro a, induction a with g h,
fapply is_contr_of_inhabited_prop,
fapply adjointify,
rexact group_fun (pr1 (center' (@quotient_group_functor_contr A L K _ _ H2))),
note htpy := homotopy_of_eq (ap group_fun (ap sigma.pr1 (@quotient_group_functor_id _ L _ (λ a, (H1 a) ∘ (H2 a))))),
have KK : is_contr ((Σ(g' : quotient_ab_group K →g quotient_ab_group K), g' ∘g ab_qg_map K ~ ab_qg_map K) ), from
quotient_group_functor_contr (λ a, (H2 a) ∘ (H1 a)),
-- have KK_path : ⟨g, h⟩ = ⟨id, λ a, refl (ab_qg_map K a)⟩, from eq_of_is_contr ⟨g, h⟩ ⟨id, λ a, refl (ab_qg_map K a)⟩,
repeat exact sorry
end
/-
definition quotient_group_iso_contr {K L : property A} [is_subgroup A K] [is_subgroup A L] (H1 : Π (a : A), K a → L a) (H2 : Π (a : A), L a → K a) :
is_contr (Σ (g : quotient_ab_group K ≃g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L) :=
begin
refine @is_trunc_equiv_closed (Σ(gh : Σ (g : quotient_ab_group K →g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L), is_equiv (group_fun (pr1 gh))) (Σ (g : quotient_ab_group K ≃g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L) -2 _ (quotient_group_iso_contr_aux H1 H2),
exact calc
(Σ gh, is_equiv (group_fun gh.1)) ≃ Σ (g : quotient_ab_group K →g quotient_ab_group L) (h : g ∘g ab_qg_map K ~ ab_qg_map L), is_equiv (group_fun g) : by exact (sigma_assoc_equiv (λ gh, is_equiv (group_fun gh.1)))⁻¹
... ≃ (Σ (g : quotient_ab_group K ≃g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L) : _
end
-/
end quotient_group_iso
definition quotient_group_functor [constructor] (φ : G →g G') (h : Πg, g ∈ N → φ g ∈ N') :
quotient_group N →g quotient_group N' :=
begin
apply quotient_group_elim (qg_map N' ∘g φ),
intro g Ng, esimp,
refine qg_map_eq_one (φ g) (h g Ng)
end
------------------------------------------------
-- FIRST ISOMORPHISM THEOREM
------------------------------------------------
definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_ab_group (kernel f) →g B :=
begin
unfold quotient_ab_group,
fapply @quotient_group_elim A B _ (@is_normal_subgroup_ab _ (kernel f) _) f,
intro a, intro p, exact p
end
definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) :
kernel_quotient_extension f ∘ ab_qg_map (kernel f) ~ f :=
begin
intro a,
apply @quotient_group_compute _ _ _ (@is_normal_subgroup_ab _ (kernel f) _)
end
definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B) :
is_embedding (kernel_quotient_extension f) :=
begin
fapply is_embedding_of_is_mul_hom,
intro x,
note H := is_surjective_ab_qg_map (kernel f) x,
induction H, induction p,
intro q,
apply @qg_map_eq_one _ _ (@is_normal_subgroup_ab _ (kernel f) _),
refine _ ⬝ q,
symmetry,
rexact kernel_quotient_extension_triangle f a
end
definition ab_group_quotient_homomorphism (A B : AbGroup)(K : property A)(L : property B) [is_subgroup A K] [is_subgroup B L] (f : A →g B)
(p : Π(a:A), a ∈ K → f a ∈ L) : quotient_ab_group K →g quotient_ab_group L :=
begin
fapply @quotient_group_elim,
exact (ab_qg_map L) ∘g f,
intro a,
intro k,
exact @ab_qg_map_eq_one B L _ (f a) (p a k),
end
definition ab_group_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g )
: kernel g ⊆ kernel f :=
begin
intro a,
intro p,
exact calc
f a = i (g a) : homotopy_of_eq (ap group_fun H) a
... = i 1 : ap i p
... = 1 : respect_one i
end
definition ab_group_triv_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g ) :
kernel f ⊆ '{1} → kernel g ⊆ '{1} :=
λ p, subproperty.trans (ab_group_kernel_factor f g H) p
definition is_embedding_of_kernel_subproperty_one {A B : AbGroup} (f : A →g B) :
kernel f ⊆ '{1} → is_embedding f :=
λ p, is_embedding_of_is_mul_hom _
(take x, assume h : f x = 1,
show x = 1, from eq_of_mem_singleton (p _ h))
definition kernel_subproperty_one {A B : AbGroup} (f : A →g B) :
is_embedding f → kernel f ⊆ '{1} :=
λ h x hx,
have x = 1, from eq_one_of_is_mul_hom hx,
show x ∈ '{1}, from mem_singleton_of_eq this
definition ab_group_kernel_equivalent {A B : AbGroup} (C : AbGroup) (f : A →g B)(g : A →g C)(i : C →g B)(H : f = i ∘g g )(K : is_embedding i)
: Π a:A, a ∈ kernel g ↔ a ∈ kernel f :=
exteq_of_subproperty_of_subproperty
(show kernel g ⊆ kernel f, from ab_group_kernel_factor f g H)
(show kernel f ⊆ kernel g, from
take a,
suppose f a = 1,
have i (g a) = i 1, from calc
i (g a) = f a : (homotopy_of_eq (ap group_fun H) a)⁻¹
... = 1 : this
... = i 1 : (respect_one i)⁻¹,
is_injective_of_is_embedding this)
definition ab_group_kernel_image_lift (A B : AbGroup) (f : A →g B)
: Π a : A, a ∈ kernel (image_lift f) ↔ a ∈ kernel f :=
begin
fapply ab_group_kernel_equivalent (ab_Image f) (f) (image_lift(f)) (image_incl(f)),
exact image_factor f,
exact is_embedding_of_is_injective (image_incl_injective(f)),
end
definition ab_group_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
: quotient_ab_group (kernel f) →g ab_Image (f) :=
begin
fapply quotient_ab_group_elim (image_lift f), intro a, intro p,
apply iff.mpr (ab_group_kernel_image_lift _ _ f a) p
end
definition ab_group_kernel_quotient_to_image_domain_triangle {A B : AbGroup} (f : A →g B)
: ab_group_kernel_quotient_to_image (f) ∘g ab_qg_map (kernel f) ~ image_lift(f) :=
begin
intros a,
esimp,
end
definition ab_group_kernel_quotient_to_image_codomain_triangle {A B : AbGroup} (f : A →g B)
: image_incl f ∘g ab_group_kernel_quotient_to_image f ~ kernel_quotient_extension f :=
begin
intro x,
induction x,
reflexivity,
fapply is_prop.elimo
end
definition is_surjective_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
: is_surjective (ab_group_kernel_quotient_to_image f) :=
begin
fapply is_surjective_factor (group_fun (ab_qg_map (kernel f))),
exact image_lift f,
apply @quotient_group_compute _ _ _ (@is_normal_subgroup_ab _ (kernel f) _),
exact is_surjective_image_lift f
end
definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
: is_embedding (ab_group_kernel_quotient_to_image f) :=
begin
fapply is_embedding_factor (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f),
exact ab_group_kernel_quotient_to_image_codomain_triangle f,
exact is_embedding_kernel_quotient_extension f
end
definition ab_group_first_iso_thm {A B : AbGroup} (f : A →g B)
: quotient_ab_group (kernel f) ≃g ab_Image f :=
begin
fapply isomorphism.mk,
exact ab_group_kernel_quotient_to_image f,
fapply is_equiv_of_is_surjective_of_is_embedding,
exact is_embedding_kernel_quotient_to_image f,
exact is_surjective_kernel_quotient_to_image f
end
definition codomain_surjection_is_quotient {A B : AbGroup} (f : A →g B)( H : is_surjective f)
: quotient_ab_group (kernel f) ≃g B :=
begin
exact (ab_group_first_iso_thm f) ⬝g (iso_surjection_ab_image_incl f H)
end
definition codomain_surjection_is_quotient_triangle {A B : AbGroup} (f : A →g B)( H : is_surjective f)
: codomain_surjection_is_quotient (f)(H) ∘g ab_qg_map (kernel f) ~ f :=
begin
intro a,
esimp
end
-- print iff.mpr
/- set generating normal subgroup -/
section
parameters {A₁ : AbGroup} (S : A₁ → Prop)
variable {A₂ : AbGroup}
inductive generating_relation' : A₁ → Type :=
| rincl : Π{g}, S g → generating_relation' g
| rmul : Π{g h}, generating_relation' g → generating_relation' h → generating_relation' (g * h)
| rinv : Π{g}, generating_relation' g → generating_relation' g⁻¹
| rone : generating_relation' 1
open generating_relation'
definition generating_relation (g : A₁) : Prop := ∥ generating_relation' g ∥
local abbreviation R := generating_relation
definition gr_one : R 1 := tr (rone S)
definition gr_inv (g : A₁) : R g → R g⁻¹ :=
trunc_functor -1 rinv
definition gr_mul (g h : A₁) : R g → R h → R (g * h) :=
trunc_functor2 rmul
definition normal_generating_relation [instance] : is_subgroup A₁ generating_relation :=
⦃ is_subgroup,
one_mem := gr_one,
inv_mem := gr_inv,
mul_mem := gr_mul⦄
parameter (A₁)
definition quotient_ab_group_gen : AbGroup := quotient_ab_group generating_relation
definition gqg_map [constructor] : A₁ →g quotient_ab_group_gen :=
ab_qg_map _
parameter {A₁}
definition gqg_eq_of_rel {g h : A₁} (H : S (g * h⁻¹)) : gqg_map g = gqg_map h :=
eq_of_rel (tr (rincl H))
-- this one might work if the previous one doesn't (maybe make this the default one?)
definition gqg_eq_of_rel' {g h : A₁} (H : S (g * h⁻¹)) : class_of g = class_of h :> quotient_ab_group_gen :=
gqg_eq_of_rel H
definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
: quotient_ab_group_gen →g A₂ :=
begin
apply quotient_ab_group_elim f,
intro g r, induction r with r,
induction r with g s g h r r' IH1 IH2 g r IH,
{ exact H s },
{ exact !respect_mul ⬝ ap011 mul IH1 IH2 ⬝ !one_mul },
{ exact !respect_inv ⬝ ap inv IH ⬝ !one_inv },
{ apply respect_one }
end
definition gqg_elim_compute (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
: gqg_elim f H ∘ gqg_map ~ f :=
begin
intro g, reflexivity
end
definition gqg_elim_unique (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
(k : quotient_ab_group_gen →g A₂) : ( k ∘g gqg_map ~ f ) → k ~ gqg_elim f H :=
!ab_gelim_unique
end
end group
namespace group
variables {G H K : Group} {R : property G} [is_normal_subgroup G R]
{S : property H} [is_normal_subgroup H S]
{T : property K} [is_normal_subgroup K T]
theorem quotient_group_functor_compose (ψ : H →g K) (φ : G →g H)
(hψ : Πg, g ∈ S → ψ g ∈ T) (hφ : Πg, g ∈ R → φ g ∈ S) :
quotient_group_functor ψ hψ ∘g quotient_group_functor φ hφ ~
quotient_group_functor (ψ ∘g φ) (λg, proof hψ (φ g) qed ∘ hφ g) :=
begin
intro g, induction g using set_quotient.rec_prop with g hg, reflexivity
end
definition quotient_group_functor_gid :
quotient_group_functor (gid G) (λg, id) ~ gid (quotient_group R) :=
begin
intro g, induction g using set_quotient.rec_prop with g hg, reflexivity
end
definition quotient_group_functor_homotopy {ψ φ : G →g H} (hψ : Πg, R g → S (ψ g))
(hφ : Πg, g ∈ R → φ g ∈ S) (p : φ ~ ψ) :
quotient_group_functor φ hφ ~ quotient_group_functor ψ hψ :=
begin
intro g, induction g using set_quotient.rec_prop with g hg,
exact ap set_quotient.class_of (p g)
end
end group
namespace group
variables {G H K : AbGroup} {R : property G} [is_subgroup G R]
{S : property H} [is_subgroup H S]
{T : property K} [is_subgroup K T]
definition quotient_ab_group_functor [constructor] (φ : G →g H)
(h : Πg, g ∈ R → φ g ∈ S) : quotient_ab_group R →g quotient_ab_group S :=
@quotient_group_functor G H R (is_normal_subgroup_ab _) S (is_normal_subgroup_ab _) φ h
definition quotient_ab_group_functor_mul
(ψ φ : G →g H) (hψ : Πg, g ∈ R → ψ g ∈ S) (hφ : Πg, g ∈ R → φ g ∈ S) :
homomorphism_mul (quotient_ab_group_functor ψ hψ) (quotient_ab_group_functor φ hφ) ~
quotient_ab_group_functor (homomorphism_mul ψ φ)
(λg hg, is_subgroup.mul_mem (hψ g hg) (hφ g hg)) :=
begin
intro g, induction g using set_quotient.rec_prop with g hg, reflexivity
end
theorem quotient_ab_group_functor_compose (ψ : H →g K) (φ : G →g H)
(hψ : Πg, g ∈ S → ψ g ∈ T) (hφ : Πg, g ∈ R → φ g ∈ S) :
quotient_ab_group_functor ψ hψ ∘g quotient_ab_group_functor φ hφ ~
quotient_ab_group_functor (ψ ∘g φ) (λg, proof hψ (φ g) qed ∘ hφ g) :=
@quotient_group_functor_compose G H K R _ S _ T _ ψ φ hψ hφ
definition quotient_ab_group_functor_gid :
quotient_ab_group_functor (gid G) (λg, id) ~ gid (quotient_ab_group R) :=
@quotient_group_functor_gid G R _
definition quotient_ab_group_functor_homotopy {ψ φ : G →g H} (hψ : Πg, R g → S (ψ g))
(hφ : Πg, g ∈ R → φ g ∈ S) (p : φ ~ ψ) :
quotient_ab_group_functor φ hφ ~ quotient_ab_group_functor ψ hψ :=
@quotient_group_functor_homotopy G H R _ S _ ψ φ hψ hφ p
end group