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

Removing troublesome composition of group homomorphism in quotient_group

Browse source
This commit is contained in:
Robert Rose 2017-06-07 12:02:09 -06:00
parent 21a0dcfcfe
commit 7ed3e47e09
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
algebra/quotient_group.hlean
View file

@ -227,10 +227,10 @@ namespace group
unfold qg_map, esimp, exact to_respect_mul f g h } unfold qg_map, esimp, exact to_respect_mul f g h }
end end
definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (g : G) :
quotient_group_elim f H ∘g qg_map N ~ f := quotient_group_elim f H (qg_map N g) = f g :=
begin begin
intro g, reflexivity reflexivity
end end
definition gelim_unique (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (k : quotient_group N →g G') definition gelim_unique (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (k : quotient_group N →g G')
@ -247,7 +247,7 @@ namespace group
end end
definition qg_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : definition qg_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) :
is_contr (Σ(g : quotient_group N →g G'), g ∘g qg_map N ~ f) := is_contr (Σ(g : quotient_group N →g G'), g ∘ qg_map N ~ f) :=
begin begin
fapply is_contr.mk, fapply is_contr.mk,
-- give center of contraction -- give center of contraction
@ -442,7 +442,7 @@ definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_a
end end
definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) : definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) :
kernel_quotient_extension f ∘g ab_qg_map (kernel_subgroup f) ~ f := kernel_quotient_extension f ∘ ab_qg_map (kernel_subgroup f) ~ f :=
begin begin
intro a, intro a,
apply quotient_group_compute apply quotient_group_compute